Z3py: how to extend and trunc variables?

Question

I have two variables 'a' and 'b' of different size, see below. I have few questions:

(1) How can I copy value of 'a' to 'b'? (i.e extend operation)

(2) How can I copy value of 'b' to 'a'? (i.e trunc operation)

Thanks.

a = BitVec('a', 1)
b = BitVec('b', 32)

Answer 1

For extending, we use ZeroExt or SignExt. The ZeroExt will add "zeros", and SignExt will "copy" the sign bit (i.e., the most significant bit). For truncation we use Extract, it can extract any subsequence of bits. Here is a small example (also available online at rise4fun).

a = BitVec('a', 1)
b = BitVec('b', 32)
solve(ZeroExt(31, a) == b)
solve(b > 10, Extract(0,0,b) == a)

EDIT: we can use p == (x == 1) to 'assign' a Boolean variable p with the value of a Bit-vector x of size 1, and vice-versa. The formula p == (x == 1) is just stating that p is true if and only if x is 1. Here is an example (also available online here)

x = BitVec('x', 1)
p = Bool('p')

solve(p == (x == 1), x == 0)
solve(p == (x == 1), x == 1)
solve(p == (x == 1), Not(p))
solve(p == (x == 1), p)