Support for activation literals

[rachitnigam]

Not sure if this is goal for this library but it might be useful to implement activation literals in the same way that the rsmt2 library does. In practice, they are a much more efficient alternative to push and pop since the latter force SMT solvers to reset a bunch of internal state and disable incremental solving which can be useful for subsequent queries.

[elliottt]

That's a neat idea! I'm not sure it's an explicit goal for the library -- originally it started as a rust implementation of the haskell simple-smt library, whose goal was to provide a uniform api for the smt-lib interface that many solvers provide. I think that supporting activation literals is the sort of thing that could be built on top of easy-smt, perhaps we could include a module that would help manage that state for those that would like to use them?

[rachitnigam]

Yup! That’s exactly how rsmt2 does it as well. I have a use case for it so might try implementing it. One nice thing in this library is since everything is interned, there might be a cleaner, simpler abstraction to support path dependent/activation literal-based asserts

[aur3l14no]

the latter force SMT solvers to reset a bunch of internal state and disable incremental solving which can be useful for subsequent queries.

@rachitnigam I thought push/pop can still preserve internal state. Can you provide some evidence/source for this? Thanks!

[rachitnigam]

Normally solvers need to reset lots of state and disable various tactics that are not compatible with "incremental solving" (which is what push and pop require).

[aur3l14no]

Yeah I know the latter half, but not the former. I think I'll rephrase my question to: what are the internal states that get reset in push/pop mode and not get reset in check-sat-assuming mode? For example, I thought the lemma learned before the corresponding push would be preserved. But maybe I was wrong? Or maybe this is more solver-specific and even solver-config-specific, which is gonna be very tricky. Could you share some info on these details?

Background: I have an application that requires incremental solving and have been using push/pops. I do find that under certain options, it is not quite "incremental" as I expect it to be. For example, vars irrelevant to new assertions whose constraints sit at the bottom of the assertion stack seem to be re-calculated every time I check. I think the actlit technique you propose here looks really promising and I will definitely try it out. So thanks for the info. :D