Scala^Z3: Delete previous assertion

Question

I want to use Scala^Z3 for incremental solving. In each iteration I want to

a) add some part of the formula

b) add an assertion

The formula should be preserved for every following iteration, but I would need to delete the assertion, if I cant fulfill it, because the assertion in the next iteration will be different.

So is there a way to delete previous statements? Z3Context.pop() sounds a little like what I need, but I could not find a description of what it does..

Would be very thankful for some help there!

Best wishes, 1428162

score 3 · Answer 1 · edited May 23 '17 at 12:12

Yes, you're right, you want to pop (remove) the last assertion. To do this, you first need to save the current set of assertions with push. This is how Z3 supports scope.

By add some part of the formula, I'm going to assume you mean to define a variable containing an additional chunk of some original large formula you're doing the incremental checking on. I'll also assume the original formula is a large conjunction of sub-formulas. This new formula will remain defined between pushes and pops (assuming you keep a variable referencing it).

Here is a link to an example of roughly the following pseudo-code in z3py, except in the z3py script I also assume the formula and the constraint are actually the same thing, but maybe you want to create some different constraint based on that piece of the subformula: http://rise4fun.com/Z3Py/LIxW

I haven't used Scala^Z3, but roughly you want to do the following:

formula // list containing parts (sub-formulas) of original large formula
while (formulaPart = formula.removeFirst()) // remove first element of list
    Z3Context.push() // save current set of assertions

    assertion = makeConstraint( formulaPart ) // assertion based on sub-formula

    Z3Context.assertCnstr( assertion ) // add new assertion

    if !Z3Context.check() // check if assertions cannot be satisfied
        Z3Context.pop() // remove most recent assertion

Here is an example using pop/push from the .NET API: http://research.microsoft.com/en-us/um/redmond/projects/z3/test__managed_8cs_source.html#l00637

You'd also be interested in this: Soft/Hard constraints in Z3

Thx a lot, that answer really helped me out! I did a push() between adding the assertion and the pop(), but now you showed me how to do it, its working! :) — user1428162, Aug 24 '12 at 08:06

Philippe · Accepted Answer · 2012-08-23T22:06:43.887

Right, ctx.pop() is what you want. It can also take an argument, as in ctx.pop(2), but it defaults to 1 if you omit it. Intuitively, puts the state of the solver back to where it was "n pushes ago".

So if you do:

ctx.assertCnstr(formula1)
ctx.push()

ctx.assertCnstr(extraAssertion)
ctx.check() match {
  case Some(true)  => ... // SAT
  case Some(false) => ... // UNSAT
  case None        => ... // UNKNOWN
}

ctx.pop(1)

...the state of the solver is reverted to what it was before you called push().

Note that these behave exactly as their equivalent from the Z3 C API, so the documentation from there applies as well.

Note as well that calling push and pop on a context is deprecated as of Z3 4.0. The recommended way is now to have the context first create a solver, and then use push and pop on the solver directly (there was no notion of solver prior to Z3 4.0). Scala^Z3 hasn't caught up yet but you can expect that the change will eventually be propagated.

Thx for the answer + the additional infos! Guess I have to stick to push and pop for now.. But now that you told me how to use them, I would not want to change that anyway :) — user1428162, Aug 24 '12 at 08:19
Of course if you want to hack on Scala^Z3 and create a pull request on GitHub we'll be very grateful :) — Philippe, Aug 24 '12 at 12:54

Scala^Z3: Delete previous assertion

2 Answers2