sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
187 stars 45 forks source link

Feature Request: Clone ProverEnvironment with Stack #322

Open lembergerth opened 1 year ago

lembergerth commented 1 year ago

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:

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 commented 1 year ago

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!).

baierd commented 1 year ago

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 commented 1 year ago

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

lembergerth commented 1 year ago

@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 commented 1 year ago

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 commented 1 year ago

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.