Mixing reagents and bit vectors

Question

I have two SMT2-Lib scripts using reals that are morally equivalent. The only difference is that bit vectors are also used, and the other is not.

Here's the version that uses both real and bit vectors:

; uses both reals and bit-vectors (set-option :produce-models true) (define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2)) (define-fun s3 () Real 0.0) (define-fun s6 () Real (/ 1.0 1.0)) (declare-fun s0 () (_ BitVec 1)) (declare-fun s1 () (_ BitVec 1)) (assert (let ((s4 (- s3 s2))) (let ((s5 (ite (= #b1 s1) s2 s4))) (let ((s7 (+ s5 s6))) (let ((s8 (- s5 s6))) (let ((s9 (ite (= #b1 s0) s7 s8))) (let ((s10 (ite (>= s9 s3) #b1 #b0))) (= s10 #b1)))))))) (check-sat) (get-model) 

Here's a morally equivalent script, using Bool instead of a bit vector of size 1, otherwise it is essentially the same:

 ; uses reals only (set-option :produce-models true) (define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2)) (define-fun s3 () Real 0.0) (define-fun s6 () Real (/ 1.0 1.0)) (declare-fun s0 () (Bool)) (declare-fun s1 () (Bool)) (assert (let ((s4 (- s3 s2))) (let ((s5 (ite s1 s2 s4))) (let ((s7 (+ s5 s6))) (let ((s8 (- s5 s6))) (let ((s9 (ite s0 s7 s8))) (let ((s10 (ite (>= s9 s3) #b1 #b0))) (= s10 #b1)))))))) (check-sat) (get-model) 

For the former, I get unknown from z3 (v4.1 on Mac), and the latter nicely produces sat and model.

While SMT-Lib2 does not allow mixing reals and bit vectors, I thought that Z3 handles these combinations just fine. Am I mistaken? Is there a workaround?

(Note that these are generated scripts, so just using Bool instead of (_ BitVec 1) is quite expensive, as it requires very few changes elsewhere.)

Answer 1

The new nonlinear solver is not yet integrated with other theories. It only supports real variables and booleans. In fact, it also allows integer variables, but there is very limited support for them. It actually solves nonlinear integer problems as real problems and simply checks to see if the whole variable is assigned to the integer value at the end. Moreover, this solver is the only complete procedure for non-linear (real) arithmetic available in Z3.

Since your first problem contains bit vectors, the non-linear solver is not used by Z3. Instead, Z3 uses a universal solver that combines many theories, but it is incomplete for nonlinear arithmetic.

Having said that, I understand that this is a limitation, and I am working on it. In the future (not so close), Z3 will have a new solver that combines nonlinear arithmetic, arrays, bit vectors, etc.

Finally, the theory of bit vectors is a very special case, since we easily reduce it to propositional logic in Z3. Z3 has a bit-blast tactic that applies this reduction. This tactic can reduce any non-linear + bit-vector problem into a problem containing only real and Boolean ones. Here is an example ( http://rise4fun.com/Z3/0xl ).

 ; uses both reals and bit-vectors (set-option :produce-models true) (define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2)) (define-fun s3 () Real 0.0) (define-fun s6 () Real (/ 1.0 1.0)) (declare-fun s0 () (_ BitVec 1)) (declare-fun s1 () (_ BitVec 1)) (declare-fun v2 () (_ BitVec 8)) (assert (let ((s4 (- s3 s2))) (let ((s5 (ite (= #b1 s1) s2 s4))) (let ((s7 (+ s5 s6))) (let ((s8 (- s5 s6))) (let ((s9 (ite (= #b1 s0) s7 s8))) (let ((s10 (ite (>= s9 s3) #b1 #b0))) (= s10 #b1)))))))) (assert (or (and (not (= v2 #x00)) (not (= v2 #x01))) (bvslt v2 #x00))) (assert (distinct (bvnot v2) #x00)) (check-sat-using (then simplify bit-blast qfnra)) (get-model)