我有两个使用实数的 SMT2-Lib 脚本,它们在道德上是等效的。唯一的区别是一个也使用位向量而另一个不使用。
这是同时使用实数和位向量的版本:
; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(assert
(let ((s4 (- s3 s2)))
(let ((s5 (ite (= #b1 s1) s2 s4)))
(let ((s7 (+ s5 s6)))
(let ((s8 (- s5 s6)))
(let ((s9 (ite (= #b1 s0) s7 s8)))
(let ((s10 (ite (>= s9 s3) #b1 #b0)))
(= s10 #b1))))))))
(check-sat)
(get-model)
这是道德上等效的脚本,使用
Bool
而不是大小为 1 的位向量,否则基本相同:; uses reals only
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (Bool))
(declare-fun s1 () (Bool))
(assert
(let ((s4 (- s3 s2)))
(let ((s5 (ite s1 s2 s4)))
(let ((s7 (+ s5 s6)))
(let ((s8 (- s5 s6)))
(let ((s9 (ite s0 s7 s8)))
(let ((s10 (ite (>= s9 s3) #b1 #b0)))
(= s10 #b1))))))))
(check-sat)
(get-model)
对于前者,我得到
unknown
来自 z3(Mac 上的 v4.1),而后者很好地生成 sat
和一个模型。虽然 SMT-Lib2 不允许混合实数和位向量,但我认为 Z3 处理这些组合很好。我错了吗?有解决方法吗?
(请注意,这些是生成的脚本,因此仅使用
Bool
而不是 (_ BitVec 1)
成本相当高,因为它需要在其他地方进行大量更改。)
最佳答案
新款nonlinear solver尚未与其他理论结合。它只支持实数变量和 bool 值。实际上,它也允许整数变量,但对它们的支持非常有限。它实际上是将非线性整数问题作为真正的问题来解决,最后只是检查每个整数变量是否都分配了一个整数值。此外,该求解器是 Z3 中唯一可用的非线性(实数)算法的完整程序。
由于您的第一个问题包含位向量,因此 Z3 不使用非线性求解器。相反,Z3 使用了一个综合了许多理论的通用求解器,但它对于非线性算术来说是不完整的。
话虽如此,我明白这是一个限制,我正在努力解决这个问题。在不久的将来,Z3 将有一个新的求解器,它集成了非线性算术、数组、位向量等。
最后,位向量理论是一个非常特殊的情况,因为我们可以很容易地将其简化为 Z3 中的命题逻辑。
Z3有战术bit-blast
这适用于这种减少。这种策略可以将任何非线性+位向量问题简化为仅包含实数和 bool 值的问题。这是一个示例( http://rise4fun.com/Z3/0xl )。
; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(declare-fun v2 () (_ BitVec 8))
(assert
(let ((s4 (- s3 s2)))
(let ((s5 (ite (= #b1 s1) s2 s4)))
(let ((s7 (+ s5 s6)))
(let ((s8 (- s5 s6)))
(let ((s9 (ite (= #b1 s0) s7 s8)))
(let ((s10 (ite (>= s9 s3) #b1 #b0)))
(= s10 #b1))))))))
(assert (or (and (not (= v2 #x00)) (not (= v2 #x01))) (bvslt v2 #x00)))
(assert (distinct (bvnot v2) #x00))
(check-sat-using (then simplify bit-blast qfnra))
(get-model)
关于z3 - 混合实数和位向量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12929633/