Z3：一个BitVec和一个Real是否可以相加？答案

【问题标题】：Z3: Is it possible to sum up a BitVec and a Real?Z3：一个BitVec和一个Real是否可以相加？
【发布时间】：2013-05-10 06:46:43
【问题描述】：

我正在使用 Z3py 尝试对舍入误差问题进行一些实验，结果我必须总结一个 BitVec 和一个 Real。但是，当我尝试这样做时，出现“排序不匹配”错误。这是我的代码：

x = BitVecVal(8, 6)
y = Real('y')

solve(y + x == 5)

有没有办法将 BitVec 和 Real 相加？还是只是为了获取 BitVec 的 Int 值？

【问题讨论】：

标签： z3

【解决方案1】：

基于 Z3 C 的 API 确实包含从位向量到数字（整数）的转换函数，并且整数可以强制转换为实数。不过python API并没有直接暴露相关函数，但是可以封装一下：

x = BitVecVal(2,8)
y = Real('y')


def to_int(x):
    return ArithRef(Z3_mk_bv2int(x.ctx_ref(), x.as_ast(), 0), x.ctx)

print solve(to_int(x) + y == 5)

【讨论】：

很好的答案，谢谢你。我在文档中没有看到这一点。但是，这个 wrap 函数会影响 Solver 的性能吗？
在您的示例中，x 是一个值。所以对性能没有影响。 Z3 预处理器会将to_int(x) 转换为实数2。但是，如果x 不是一个值，则会对性能产生严重影响。 to_int 将被“爆破”成一个大的if-then-else 术语，该术语基于x 的位“构建”一个整数。我们得到每个位的if-then-else 术语。有一些“更聪明”的方式来处理to_int，但 Z3 目前使用这种简单/幼稚的方法。

【解决方案2】：

您可以将位向量值转换为有符号长整数：

x = BitVecVal(8, 6)
y = Real('y')

solve(y + x.as_signed_long() == 5)
# [y = -3]

顺便说一句，我通过检查y 找到了as_signed_long，就像在Python 中通常所做的那样，即通过print dir(y)。

【讨论】：

感谢您的回复，非常感谢。顺便说一句，as_signed_long 方法仅适用于 BitVecVal，不适用于 BitVec。如果我希望 x 成为 BitVec 而不是常量怎么办？有什么办法吗？
对不起，我也不知道BitVec怎么办。