與SSA

Question

瞭解Z3 bvsmod行爲我試圖用Z3學習。所以這個問題可能很愚蠢。

爲什麼我得到一個意外的值從Z3 x___0當我使用bvsmod相比在下面的代碼bvadd。我在這裏使用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)) 
) 

在公式，我用bvadd x___0得到一個值，這是有意義的情況。

爲什麼我會得到一個值在bvsmod的情況下，哪裏沒有接近預期值，即某個值以4結尾？

Answer 1

沒有什麼錯，你所得到的值。你的編碼很好。

請注意，您使用的是32位有符號整數（由bvsmod調用隱含暗示）。返回的模型爲您提供值爲32位的位向量值，其十進制等效值爲3720040335。當解釋爲簽署的價值，這其實是-574926961，你可以驗證(-574926961) % 5確實等於4按照您的要求。

注意，解算器是免費給你，滿足你的任何約束模型。如果你想要一個更具體的值，你需要添加額外的約束來編碼「簡單」應該正式表示的意思。

Answer 2

如果你想要寫這樣的公式，你需要的量詞。 我建議你改用SMT表達式;分享將免費發生。 寫例如： - (assert (= (bvmul (bvadd x___0 (_ bv1 32)) (_ bv2 32)) (_ bv8 32)))

如果您需要的中間值，以後可以隨時做一個（EVAL ...）