混合实数和位向量

Question

我有两个使用实数的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)相当昂贵,因为它需要在其他地方进行相当多的更改.)

Answer 1

新的非线性求解器尚未与其他理论相结合.它仅支持实变量和布尔值.实际上,它也允许整数变量,但对它们的支持非常有限.它实际上将非线性整数问题解决为实际问题,并且最后检查每个整数变量是否被赋值为整数值.此外,该求解器是Z3中唯一可用的非线性(实数)算法.

由于您的第一个问题包含位向量,因此Z3不使用非线性求解器.相反,Z3使用了一个结合了许多理论的通用求解器,但它对于非线性算法来说是不完整的.

话虽如此,我知道这是一个限制,我正在努力.在(不那么近)未来,Z3将有一个新的求解器,集成了非线性算法,数组,位向量等.

最后,位向量理论是一个非常特殊的情况,因为我们可以很容易地将它简化为Z3中的命题逻辑.Z3 bit-blast采用了减少战术的策略.这种策略可以将任何非线性+位向量问题简化为仅包含实数和布尔运算的问题.这是一个例子(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)