Z3:可以总结一个BitVec和一个Real吗?

问题描述

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

I'm using Z3py to try to make some experiments on round-off error problem, it turns out that i have to sum up the a BitVec and a Real. However, when I try to do so, i get a 'sort mismatch' error. This is my code:

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

solve(y + x == 5)

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

Is there a way to sum a BitVec and a Real? or just to get the Int value of BitVec?

推荐答案

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

the Z3 C based API does contain conversion functions from bit-vectors to numerals (integers) and integers can be coerced to reals. However, the python API does not expose the relevant function directly, but you can wrap it:

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)

这篇关于Z3:可以总结一个BitVec和一个Real吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！