Z3 上的位向量算术答案

【问题标题】：Bitvector arithmetics on Z3Z3 上的位向量算术
【发布时间】：2016-03-26 00:10:36
【问题描述】：

我正在尝试使用 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)

【问题讨论】：

标签： z3 bitvector

【解决方案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/Real/Bitvector，只要输入正确即可。下面是一个示例，展示了如何同时使用 Ints 和 Reals：

(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 operation

【讨论】：

感谢您的回复。你说的是对的，无论如何使用“Real”我不能使用按位运算，但我必须使用位向量。
也允许混合/匹配类型；只要所有内容都输入正确。查看更新的答案。
stackoverflow.com/questions/16841212/… 可能是相关的。