smt2 형식 예제에서 z3 해석기에 대한 여러 솔루션을 얻는 방법은 무엇입니까?

Question

sm3 형식의 z3 해석기를 사용하여 비트 벡터 수식에 대한 여러 모델을 생성하는 방법은 무엇입니까?

비트 벡터 용 IDEA 코드를 구현하는 동안 하나의 모델이 생성됩니다.

가능한 모든 모델을 생성하는 방법은 있습니까?

ex.smt2 파일

(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) 

Answer 1

일반적인 방법은 첫 번째 모델을 제외하는 새로운 제약 조건을 추가하는 것입니다. 이 예에서는 다음과 같이 표시됩니다.

(check-sat) 

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

모든 솔루션 또는 솔루션 수를 얻는 SMT2 명령은 없습니다. 어떤 속성이 모든 솔루션에 대해 보유한다는 사실에 따라 무언가가 달라지는 경우 수량을 사용하여 인코딩 할 수 있습니다 (예 :

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

그러나 이러한 유형의 문제는 물론 풀기가 어려우며 Z3에서는 다양한 결정 절차를 사용합니다.