3

I am just starting to use Z3 (v4.4.0), and I wanted to try one of the tutorial examples : 

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

As said, the second example fails with "unknown", and by increasing the verbose level (to 3) I think I understand why : some problem with the simplifying process, then the tactic fails. In order to have a better idea of the problem (and a shorter output), I decided to remove the first part of the code to test only the failed part : 

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

But magically, now I get "sat". I am not sure about how Z3 chooses its tactic when it is about non linear arithmetic, but can the problem be from Z3 choosing a tactic for the first formula that is useless for the second one ?

Thanks in advance

Stevendeo
  • 87
  • 6

1 Answers1

3

The second encoding is not equivalent to the first, hence the different behavior. The second encoding does not include the constraint (assert (> (* a a) 3)), so Z3 can find it is satisfiable that b^3 + b*c = 3 for some choice of reals b and c. However, when it has the constraint that a^2 > 3 for some integer a, it fails to find it's satisfiable, even though the two assertions are independent from one another.

For this problem, it's essentially that Z3 by default will not use the nonlinear real arithmetic solver (which is complete) when it encounters reals mixed with integers. Here's an example of how to force it using qfnra-nlsat (rise4fun link: http://rise4fun.com/Z3/KDRP ):

(declare-const a Int)
;(assert (> (* a a) 3))
;(check-sat)
;(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(push)
(assert (and (> (* a a) 3) (= (+ (* b b b) (* b c)) 3.0)))
(check-sat)
(check-sat-using qfnra-nlsat) ; force using nonlinear solver for nonlinear real arithimetic (coerce integers to reals)
(get-model)
(pop)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

Likewise, if you just change (declare-const a Int) to (declare-const a Real), it will by default pick the correct solver that can handle this. So yes, in essence this has to do with what solver is getting picked, which is determined in part by the sorts of the underlying terms.

Related Q/A: Combining nonlinear Real with linear Int

Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17
  • Thanks you Taylor for your clear and fast answer. I just still have one last question about the choice of solvers : when I add (set-option :produce-proofs true) to produce a proof of my formula, it gets back to unknown. Does this option forces to keep the same prover ? – Stevendeo Sep 09 '15 at 06:58
  • I may be wrong, but I think the qfnra-nlsat solver does not support proof production, which probably would preclude it from being used if that's enabled. In general, you can sometimes see toggling of behavior (sat/unknown or unsat/unknown) by toggling options like this. However, if you see a toggling between unsat/sat based on option changing, you should probably report it as a candidate bug. – Taylor T. Johnson Sep 09 '15 at 18:01