与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 ...）