0

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()
...
alias
  • 28,120
  • 2
  • 23
  • 40
julian
  • 73
  • 7

1 Answers1

0

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.

alias
  • 28,120
  • 2
  • 23
  • 40