z3 - Z3：一个BitVec和一个Real是否可以概括？

Question

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

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

solve(y + x == 5)

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

Answer 1

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

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

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

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

Answer 2

基于 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)