CODEWITHSUNDEEP
z3smtz3py
julian
julian

Reputation: 73

How to alter assertions in a solver without having to repeatedly create a new solver in z3 Python API

I am currently running into the problem that I create a large SMT formula (that I get from an external source) and I run Solver.check() with it. If the call fails I perform a rewrite on some assertions in the solver using the rewrite(s,f,t) presented here.

Now I am wondering how I can change the assertions in the solver that failed to the new ones obtained after the rewrite. That is assertions that still contain the same function defintions/declarations etc. as the previous solver except with the updated assertions that have been rewritten.

For example, this is how I would do it now. I wonder if there was a better/more efficient way:

solver = z3.Solver()
f = z3.Function(f, z3.Int(),z3.Int())
solver.add(f(3)== 5)
solver.check()
solver.model()
# I don't like the model let's rewrite
new_assertions = solver.assertions().rewrite(...)
new_solver = z3.Solver()
new_solver.add(new_assertions)
new_solver.check()
...

Upvotes: 0

Views: 184

Answers (1)

alias
alias

Reputation: 30418

This is what the push, and pop statements are for:

  • push: Creates a back-tracking point that you can jump back to
  • pop: Goes back to the last push'ed point

That is, you push before you add your assertions, and when you want to change them pop back to where you were. You can create as many backtracking points as you want.

This style of solver usage is called "incremental" and is described in Section 4.1.4 of the SMTLib document. To simplify programming with your rewrite function, you might want to keep the assertions in a list of your own, so they are easy to manipulate; but that's more or less tangential to the discussion at hand here.

Upvotes: 0

Related Questions