1

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?

vutran
  • 2,145
  • 21
  • 34

2 Answers2

3

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).

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
  • Thank you for your response, i really appreciate this. By the way, as_signed_long method is available for BitVecVal only, not for BitVec. What if I want x to be a BitVec instead of a constant? Is there any way? – vutran May 10 '13 at 09:16
  • Sorry, I don't know what to do with `BitVec` either. – Malte Schwerhoff May 10 '13 at 09:28
3

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)
Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • Great answer, thank u man. I didn't see this in the documentation. However, does this wrap function affect Solver's performance? – vutran May 10 '13 at 14:40
  • In your example, `x` is a value. So there is no performance impact. The Z3 preprocessor will convert `to_int(x)` into the real number `2`. However, if `x` is not a value, then there is a serious performance impact. The `to_int` will be "blasted" into a big `if-then-else` term that "builds" an integer based on the bits of `x`. We get an `if-then-else` term for each bit. There are "smarter" ways to handle `to_int`, but Z3 currently uses this simple/naive approach. – Leonardo de Moura May 10 '13 at 16:24