我正在尝试学习使用 z3。所以这个问题可能很愚蠢。
当我在以下代码中使用 bvsmod 与 bvadd 相比时,为什么我会从 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))
)
如果我使用 bvadd x___0 的方程得到一个值 3,这是有道理的。
为什么在 bvsmod 的情况下我会得到一个值 3720040335,该值与预期值(即某个以 4 结尾的值)相差甚远?
最佳答案
您获得的值没有任何问题。你的编码很好。
请注意,您正在使用 32 位有符号整数(通过调用 bvsmod
隐式暗示)。返回的模型为您提供 32 位位向量值,其十进制等效值为 3720040335
。当解释为有符号值时,这实际上是 -574926961
,您可以验证 (-574926961) % 5
确实等于 4
已请求。
请注意,求解器可以免费为您提供满足您的约束条件的任何模型。如果您想要更具体的值,则需要添加额外的约束来编码“简单”的正式含义。
关于z3 - 了解 z3 bvsmod 与 SSA 的行为,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/42138499/