Incremental input and assertion sets in Z3

Question

I have a program that runs Z3 version 4.8.8 - 64 bit, with incremental input: the program starts Z3 once, executes many rounds of input-output to Z3, and then stops Z3. For performance reasons, running Z3 without incremental input is not an option.

Each round, the program inputs some (assert ...) statements to Z3, inputs (check-sat) to Z3, then gets the output of (check-sat) from Z3.

I have two rounds of input-output: the first round of inputs is as in z3.sat:

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)

which means: f is an even Int greater or equals to 2.

And the second round of inputs is as in z3.unsat:

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

which means: if f is an even Int greater or equals to 2, then there exists an alpha where alpha=f/2.

I assume that running Z3 with incremental input is similar to concatenating the two rounds of input, z3.sat and z3.unsat, into one input, as in z3.combined:

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)
(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

Running:

• z3 -smt2 z3.sat outputs sat
• z3 -smt2 z3.unsat outputs unsat
• z3 -smt2 z3.combined outputs errors, because the (assert ...) statements from the first round do not disappear:

  sat
  (error "line 8 column 21: invalid declaration, constant 'f' (with the given signature) already declared")
  (error "line 9 column 21: invalid declaration, constant 'n' (with the given signature) already declared")
  unknown
  

So it seems (push 1) and (pop 1) statements are needed for Z3 to forget previous assertion sets, so I added these statements at the start and end of z3.sat and z3.unsat, and re-concatenated z3.pushpop.sat and z3.pushpop.unsat to get z3.pushpop.combined.

• z3.pushpop.sat:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not false))
  (check-sat)
  (pop 1)
  

• z3.pushpop.unsat:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
  (check-sat)
  (pop 1)
  

• z3.pushpop.combined:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not false))
  (check-sat)
  (pop 1)
  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
  (check-sat)
  (pop 1)
  

However, now running:

• z3 -smt2 z3.pushpop.sat outputs sat
• z3 -smt2 z3.pushpop.unsat outputs unknown
• z3 -smt2 z3.pushpop.combined outputs:

  sat
  unknown
  

Why does z3 -smt2 z3.pushpop.unsat output unknown?

Answer 1

As Malte mentioned, the presence of pus/pop triggers "weaker" solvers in z3. (There are many technical reasons for this, but I agree from an end-user view-point, the change in behavior is unfortunate and can be rather confusing.)

But there are commands that let you do what you want without resorting to push and pop. Instead of it, simply insert:

(reset)

when you want to "start" a new session, and this will make sure it'll all work. That is, drop the push/pop and when you concatenate, insert a (reset) in between.

A slightly better approach

While the above will work, in general you only want to forget assertions, but not definitions. That is, you want to "remember" that you have an f and an n in the environment. If this is your use case, then put the following at the top of your script:

(set-option :global-declarations true)

and when you want to "switch" to a new problem, issue:

(reset-assertions)

This way, you won't have to "repeat" the declarations each time. That is, your entire interaction should look like:

(set-option :global-declarations true)

(declare-fun f () Int)
(declare-fun n () Int)

(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)

(reset-assertions)

(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

which produces:

sat
unsat

Reference

All of this is documented in the official SMTLib document. See Section 3.9, pg. 44, for the descripton of global-declarations, and Section 4.2.2, pg. 59, for the description of (reset-assertions).

Answer 2

Incremental mode forces Z3 to use different theory subsolvers, as explained by one of the developers in this SO answer. These "incremental mode" subsolvers are often less effective than the "regular" ones, or at least may behave differently. As far as I know, Z3 switches to incremental mode whenever an SMT program contains push-pop scopes or multiple check-sats.

You initially say that not using incremental mode is not an option, but at least your file z3.pushpop.combined looks easily splitable. Another option might be to reset Z3 (I think the SMT command (reset) exists for that purpose) in between, instead of having push-pop blocks. If what I claim above is correct, however, this wouldn't prevent Z3 from staying in non-incremental mode. You could consider asking the developers via a "question issue" on Z3's issue tracker.