Z3: Is it possible to sum up a BitVec and a 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)

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

回答1:

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)

回答2:

You could convert the bit vector value into a signed long:

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

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

By the way, I found as_signed_long by inspecting y as one usually does in Python, namely, by print dir(y).