Search code examples
pythoncastingz3z3pybitvector

z3Py: Cast BoolRef to one-bit BitVecRef

Is it possible to cast BoolRef to a one-bit-long BitVecRef in z3Py? In my design, it is required that a BitVecRef is returned from a comparison between two other BitVecRef's. This would be similar to casting a python bool to an int. Here is an example of its use:

bv1, bv2, added = z3.BitVecs('bv1 bv2 added', 4)
res = z3.BitVec('res', 1)
s = z3.Solver()
s.add(res == (bv1 < bv2))
s.add(added == added + z3.ZeroExt(3, res))

This would be ideal, but the type of (bv1 < bv2) is Boolref, and it throws a "sort mismatch" error. Is there a way to cast the result of (bv1 < bv2) so that res can asserted equal to it?

Solution

  • Bit-vectors can't be casted to Boolean automatically. The usual approach is to wrap them in if-then-elses, e.g., in this example, instead of 

    s.add(res == (bv1 < bv2))

    we can say

    c = If(bv1 < bv2, BitVecVal(1, 1), BitVecVal(0, 1))
s.add(res == c)