z3 - Z3 上的位向量算术

Question

我正在尝试使用 Z3 来解决使用位向量算术的算术方程。我想知道是否有办法处理实数。例如，如果我可以指定一个不同于 #x1 的常数并改用实数。

(set-option :pp.bv-literals false)
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
(assert (= (bvadd x y) #x1))
(check-sat)
(get-model)

Answer 1

是的，SMT-Lib（和 Z3）都完全支持实数：http ://smtlib.cs.uiowa.edu/theories-Reals.shtml

您可以简单地编写您的示例，如下所示：

(declare-const x Real)
(declare-const y Real)
(assert (= (+ x y) 1))
(check-sat)
(get-model)

您也可以混合/匹配// Int，只要所有内容都正确输入。下面是一个示例，展示了如何一起使用 Ints 和 Reals：RealBitvector

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> e (+ (to_real (+ a b)) 2.0)))
(assert (= d (+ (to_real c) 0.5)))
(assert (> a b))
(check-sat)
(get-model)

但是，请注意，从位向量到整数的转换通常是无法解释的。请参阅此处进行讨论：Z3 int2bv 操作