混合实数和位向量 [英] mixing reals and bit-vectors

问题描述

我有两个使用实数的 SMT2-Lib 脚本，它们在道德上是等效的.唯一的区别是一个也使用位向量而另一个不使用.

I've two SMT2-Lib scripts using reals, which are morally equivalent. The only difference is that one also uses bit-vectors while the other does not.

这是同时使用实数和位向量的版本:

Here's the version that uses both reals and bit-vectors:

; 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 的位向量，否则本质上是相同的:

Here's the morally equivalent script, using Bool instead of a bit-vector of size 1, otherwise it's essentially the same:

; 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)

对于前者，我从 z3(Mac 上为 v4.1)获得 unknown，而后者很好地生成 sat 和一个模型.

For the former I get unknown from z3 (v4.1 on Mac), while the latter nicely produces sat and a model.

虽然 SMT-Lib2 不允许混合实数和位向量，但我认为 Z3 处理这些组合很好.我错了吗?有解决方法吗?

While SMT-Lib2 doesn't allow mixing reals and bit-vectors, I thought Z3 handled these combinations just fine. Am I mistaken? Is there a workaround?

(请注意，这些是生成的脚本，因此仅使用 Bool 而不是 (_ BitVec 1) 成本相当高，因为它需要在其他地方进行大量更改.)

(Note that these are generated scripts, so just using Bool instead of (_ BitVec 1) is rather costly, as it requires quite a bit of changes elsewhere.)

推荐答案

新的 非线性求解器尚未与其他理论集成.它只支持实数变量和布尔值.实际上，它也允许整数变量，但对它们的支持非常有限.它实际上是将非线性整数问题作为真正的问题来解决，最后只是检查每个整数变量是否都分配了一个整数值.此外，该求解器是 Z3 中唯一可用的非线性(实数)算法的完整程序.

The new nonlinear solver is not integrated with other theories yet. It supports only real variables and Booleans. Actually, it also allows integer variables, but it is very limited support for them. It actually solves nonlinear integer problems as real problems, and just checks in the end whether each integer variable is assigned to an integer value. Moreover, this solver is the only complete procedure for nonlinear (real) arithmetic available in Z3.

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

Since your first problem contains Bit-vectors, the nonlinear solver is not used by Z3. Instead, Z3 uses a general purpose solver that combines many theories, but it is incomplete for nonlinear arithmetic.

话虽如此，我明白这是一个限制，我正在努力解决这个问题.在不久的将来，Z3 将有一个新的求解器，它集成了非线性算术、数组、位向量等.

That being said, I understand this is a limitation, and I'm working on that. In the (not so near) future, Z3 will have a new solver that integrates nonlinear arithmetic, arrays, bit-vectors, etc.

最后，位向量理论是一个非常特殊的情况，因为我们可以轻松地将其简化为 Z3 中的命题逻辑.Z3 具有应用此减少的策略 bit-blast.这种策略可以将任何非线性+位向量问题简化为仅包含实数和布尔值的问题.这是一个示例(http://rise4fun.com/Z3/0xl).

Finally, the bit-vector theory is a very special case, since we can easily reduce it to propositional logic in Z3. Z3 has tactic bit-blast that applies this reduction. This tactic can reduce any nonlinear+bit-vector problem into a problem that contains only reals and Booleans. Here is an example (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)

这篇关于混合实数和位向量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！