1

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)
jwpfox
  • 5,124
  • 11
  • 45
  • 42
  • This question is flagged with `python` and `z3py`, so I presume [this](http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation) and [this](http://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models) answers might be relevant for you. – Patrick Trentin Nov 07 '16 at 08:50

1 Answers1

2

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.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • thanks for reply. I applied this logic to get multiple models.Now I want to check that diffusion requirement satisfied after every round.Are there any commands in smt2? – praveen gundaram Nov 16 '16 at 07:31
  • No, Z3 doesn't know about diffusion, you'll have to formalize that yourself. You'll likely need quantifiers over bit-vectors for that, since diffusion requires something to hold for all possible inputs. – Christoph Wintersteiger Nov 16 '16 at 13:32
  • I want to put a constrains k16>0x0010 and k16<0x1000. How will i add these constrains in smt2 format – praveen gundaram Jan 04 '17 at 06:38
  • E.g., (assert (bvult k16 #x0010)) bvult stands for bit-vector less-than, for other see http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV – Christoph Wintersteiger Jan 04 '17 at 11:15
  • I am running smt2 code in boolector. so model is giving binary format.I need to display in hexdecimal format.Could you please give me suggestion how to print hex decimal format in smt2 program – praveen gundaram Jan 05 '17 at 05:25
  • Boolector provides the -x and --hex options to force hex output. However, I conjecture that it (and other SMT solvers) may refuse to do that if the number of bits is not a multiple of 4. – Christoph Wintersteiger Jan 05 '17 at 14:38