Z3py: how to expand and reset variables?

Question

I have two variables “a” and “b” of different sizes, see below. I have few questions:

(1) How do I copy the value of "a" to "b"? (i.e. continuation operation)

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

Thanks.

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

Answer 1

To continue, we use ZeroExt or SignExt . ZeroExt will add zeros, and SignExt will “copy” the sign bit (ie, the most significant bit). For truncation, we use Extract , it can extract any subsequence of bits. Here is a small example (also available on the Internet 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 logical variable p with a value of bit vector x size 1 and vice versa. The formula p == (x == 1) simply states 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)