Feature Request: Clone ProverEnvironment with Stack

[lembergerth]

It would be nice to clone a full ProverEnvironment with its current stack (it would also be ok if the full SolverContext is cloned).

Our use case: We incrementally build a conjunction of boolean formulas and want to check the satisfiability of the conjunction after each additional boolean formula.
To do this, the use of the prover stack yields a significant speedup (compared to always using a new prover environment).
Now we have the case that, for a given formula, we have two different options that we want to follow.

Example:

• Let's assume we have the formulas $a$ and $b$ on the current stack: $\langle a, b\rangle$.
• As a first option, we want to continue with formula $c$, so we push to get $\langle a, b, c\rangle$.
• As a second option, we want to continue with formula $\neg c$ instead. So we would like to clone the environment with $\langle a, b\rangle$ on the stack, and push $\neg c$ to get $\langle a, b, \neg c\rangle$.

Currently, we have to create a new prover environment for one of the two options because we can not clone the prover environment. This means that we have to do a first expensive SAT-check that (at least in my expectation) has to recompute everything it already knows about $\langle a, b \rangle$.

Question 1: Is it possible to clone a ProverEnvironment or SolverContext with current ProverEnvironment?

Question 2: Is this the correct way to go about it, or is there some other smart way to do this?

Thanks!

[kfriedberger]

Answer to question 1:
As far as I know, there is no SMT solver that supports cloning a complete stack with all solver-internal constraints. We would always have to create a new stack from scratch, and then perform the SAT check.

Answer to question 2:
There might be a better way to keep some base constraints (Warning: untested idea and without any benchmark!).

• Possibility 1:
  Instead of pushing <a, b,c>, you could push <a, b, x1==c> with x1 being a boolean symbol and then use isUnsatWithAssumptions(x1) and isUnsatWithAssumptions(-x1). This should keep the internal solver-state nearly unchanged and should not require an additional SAT check for the base-constraints.
• Possibility 2:
  You could push <a, b, c> and solve it. And afterwards pop c, push -c, and solve this. This should also keep most of the internal state.

[baierd]

I asked around for question 1:

I've asked the MathSAT5 devs (but he is currently not available till August, i guess vacation).

I also created a issue for Z3.

And we are currently in contact with the CVC5 and Bitwuzla team, where this question will also be asked.

Depending on the results of this, i will investigate this further.

[baierd]

Z3 might support the feature requests for Q1.
We @lembergerth should test this.

[lembergerth]

@kfriedberger thanks for the suggestions! We are currently investigating possibility 2, and it seems to work well for our use cases. On average, we can keep about 40% of formulas on the stack when "traversing" through a tree of boolean formulas with bfs, and significantly more with dfs. This also yields a performance boost.

@baierd thank you for asking around. Does java-smt already use Z3's Q1-version?

[kfriedberger]

JavaSMT does currently not provide this feature.
I will take a look this week how we can support this via a solver-independent API.

[baierd]

I've already added a possible implementation in a branch. I've added 2 methods to the context to copy a prover with and without interpolation enabled. The context was chosen by me as we create all provers from there and may need additional information besides the original prover from either the context or the user (options), hence why i didn't use the prover interface.

Please have a look at the PR and tell me what you think of it.