Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Feature Request: Clone ProverEnvironment with Stack #322

Open
lembergerth opened this issue Jul 20, 2023 · 6 comments · May be fixed by #324
Open

Feature Request: Clone ProverEnvironment with Stack #322

lembergerth opened this issue Jul 20, 2023 · 6 comments · May be fixed by #324
Assignees
@kfriedberger

Comments

@lembergerth
Copy link
Contributor

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
Copy link
Member

kfriedberger commented Jul 20, 2023 •
edited
Loading

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
Copy link
Collaborator

baierd commented Jul 21, 2023

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
Copy link
Collaborator

baierd commented Jul 21, 2023

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

@lembergerth
Copy link
Contributor Author

lembergerth commented Jul 24, 2023 •
edited
Loading

@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 kfriedberger self-assigned this Jul 31, 2023
@kfriedberger
Copy link
Member

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 baierd linked a pull request Jul 31, 2023 that will close this issue
322 feature request clone proverenvironment with stack #324
Open
@baierd
Copy link
Collaborator

baierd commented Jul 31, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kfriedberger kfriedberger

Labels
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

322 feature request clone proverenvironment with stack sosy-lab/java-smt
3 participants
@lembergerth @baierd @kfriedberger