SS3でz3 bvsmodの動作を理解する

Question

z3を使用して学習しようとしています。だからこの質問は愚かかもしれない。

次のコードでbvsmodと比較してbvsmodを使用すると、Z3からx___0の値が予期しない値になるのはなぜですか。ここでは実行フローを実装するためにSSAを使用しています。

Z3命令：

(set-option :pp.bv-literals false) 
; 
; The code 
; x %= 5 
; x * 2 == 8 
; Implement SSA 
; x1 = x0 % 5 
; x1 * 2 == 8 
; 
(push) 
(set-info :status unknown) 
(declare-const x___0 (_ BitVec 32)) 
(declare-const x___1 (_ BitVec 32)) 
(assert (= x___1 (bvsmod x___0 (_ bv5 32)))) 
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32))) 
(check-sat) 
(get-model) 
(pop) 
; 
; The code 
; x += 1 
; x * 2 == 8 
; Implement SSA 
; x1 = x0 + 1 
; x1 * 2 == 8 
; 
(push) 
(declare-const x___0 (_ BitVec 32)) 
(declare-const x___1 (_ BitVec 32)) 
(assert (= x___1 (bvadd x___0 (_ bv1 32)))) 
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32))) 
(check-sat) 
(get-model) 
(pop) 

結果：

sat 
(model 
    (define-fun x___1() (_ BitVec 32) 
     (_ bv4 32)) 
    (define-fun x___0() (_ BitVec 32) 
     (_ bv3720040335 32)) 
) 
sat 
(model 
    (define-fun x___1() (_ BitVec 32) 
     (_ bv4 32)) 
    (define-fun x___0() (_ BitVec 32) 
     (_ bv3 32)) 
) 

私は理にかなって値を取得x___0 bvadd使用方程式の場合。

bvsmodの場合、値がになるのはなぜですか？期待値に近くない値、つまり4で終わる値はありません。

Answer 1

あなたが取得している値には何の問題もありません。あなたのエンコーディングは問題ありません。

bvsmodの呼び出しによって暗黙的に暗黙指定された32ビット符号付き整数が使用されていることに注意してください。返されるモデルは、小数の同等物が3720040335の値の32ビットビットベクトル値を提供します。符号付き値として解釈される場合、これは実際には-574926961であり、が実際に4と等しいことを確認することができます。

ソルバーは、制約を満たすモデルを自由に与えることができます。より具体的な値が必要な場合は、制約を追加して、「シンプル」が正式に意味するものをエンコードする必要があります。

Answer 2

このような数式を書きたい場合は、数量子が必要です。 代わりにSMT式を使用することをお勧めします。共有は無料で行われます。 例えばを書く： (assert (= (bvmul (bvadd x___0 (_ bv1 32)) (_ bv2 32)) (_ bv8 32)))

あなたは中間の値が必要な場合は、後でいつでも行うことができます（evalのを...）