how to get multiple solutions for z3 solver in smt

问题:

How to generate multiple models for bit vector formula using z3 solver in smt2 format?

While implementing IDEA Code for Bit Vector it is generating one model.

How to generate all possible models for the same if exists?

ex.smt2 file

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-const A0  (_ BitVec 16))
(declare-const A1  (_ BitVec 16))
(declare-const A2  (_ BitVec 16))

(declare-const B0  (_ BitVec 16))
(declare-const B1  (_ BitVec 16))
(declare-const B2  (_ BitVec 16))

(declare-const C0  (_ BitVec 16))
(declare-const C1  (_ BitVec 16))
(declare-const C2  (_ BitVec 16))

(declare-const D0  (_ BitVec 16))
(declare-const D1  (_ BitVec 16))
(declare-const D2  (_ BitVec 16))

(declare-const k11  (_ BitVec 16))
(declare-const k12  (_ BitVec 16))
(declare-const k13  (_ BitVec 16))
(declare-const k14  (_ BitVec 16))
(declare-const k15  (_ BitVec 16))
(declare-const k16  (_ BitVec 16))
(declare-const k21  (_ BitVec 16))
(declare-const k22  (_ BitVec 16))
(declare-const k23  (_ BitVec 16))
(declare-const k24  (_ BitVec 16))
(declare-const k25  (_ BitVec 16))
(declare-const k26  (_ BitVec 16))

(declare-const E11  (_ BitVec 16))
(declare-const E12  (_ BitVec 16))
(declare-const E13  (_ BitVec 16))
(declare-const E21  (_ BitVec 16))
(declare-const E22  (_ BitVec 16))
(declare-const E23  (_ BitVec 16))

(declare-const F11  (_ BitVec 16))
(declare-const F12  (_ BitVec 16))
(declare-const F13  (_ BitVec 16))
(declare-const F21  (_ BitVec 16))
(declare-const F22  (_ BitVec 16))
(declare-const F23  (_ BitVec 16))

(declare-const t11  (_ BitVec 16))
(declare-const t12  (_ BitVec 16))
(declare-const t13  (_ BitVec 16))
(declare-const t14  (_ BitVec 16))
(declare-const t15  (_ BitVec 16))
(declare-const t16  (_ BitVec 16))
(declare-const t21  (_ BitVec 16))
(declare-const t22  (_ BitVec 16))
(declare-const t23  (_ BitVec 16))
(declare-const t24  (_ BitVec 16))
(declare-const t25  (_ BitVec 16))
(declare-const t26  (_ BitVec 16))

;round------ 1 -------
(assert (= t11 (bvmul A0 k11)))
(assert (= t12 (bvadd B0 k12)))
(assert (= t13 (bvadd C0 k13)))
(assert (= t14 (bvmul D0 k14)))
(assert (= E11 (bvxor t11 t13)))
(assert (= F11 (bvxor t12 t14)))
(assert (= E12 (bvmul E11 k15)))
(assert (= F12 (bvadd F11 E12)))
(assert (= E13 (bvadd E12 F13)))
(assert (= F13 (bvmul F12 k16)))
(assert (= A1 (bvxor t11 F13)))
(assert (= t15 (bvxor t12 E13)))
(assert (= B1 t16))
(assert (= t16 (bvxor t13 F13)))
(assert (= C1 t15))
(assert (= D1 (bvxor t14 E13)))

;round------ 2 -------
(assert (= t21 (bvmul A1 k21)))
(assert (= t22 (bvadd B1 k22)))
(assert (= t23 (bvadd C1 k23)))
(assert (= t24 (bvmul D1 k24)))
(assert (= E12 (bvxor t21 t23)))
(assert (= F12 (bvxor t22 t24)))
(assert (= E13 (bvmul E12 k25)))
(assert (= F13 (bvadd F12 E13)))
(assert (= E21 (bvadd E13 F21)))
(assert (= F21 (bvmul F13 k26)))
(assert (= A2 (bvxor t21 F21)))
(assert (= t25 (bvxor t22 E21)))
(assert (= B2 t26))
(assert (= t26 (bvxor t23 F21)))
(assert (= C2 t25))
(assert (= D2 (bvxor t24 E21)))

(assert (= A0 #xb621))
(assert (= B0 #xdf47))
(assert (= C0 #xa779))
(assert (= D0 #xac41))

(check-sat)

(get-value (k11))
(get-value (k12))
(get-value (k13))
(get-value (k14))
(get-value (k15))
(get-value (k16))

(get-value (k21))
(get-value (k22))
(get-value (k23))
(get-value (k24))
(get-value (k25))
(get-value (k26))

(exit)

回答1:

The usual approach is to add a new constraint that excludes the first model. In this example, this would look like so:

(check-sat)

(assert (and (not (= k16 #x2c7d))  (not (= ... ))
(check-sat)

There is no SMT2 command to get all solutions or the number of solutions. If something depends on the fact that some property holds for all solutions, we can encode that using quantifiers, e.g.

(assert (forall ((x (_ BitVec 16))) (... property depending on x ...))) 

However, those types of problems are of course harder to solve and Z3 will use different decision procedures under the hood.