z3Py：将 BoolRef 转换为一位 BitVecRef

Question

是否可以在 z3Py 中将 BoolRef 转换为一位长的 BitVecRef？在我的设计中，需要从其他两个 BitVecRef 之间的比较返回 BitVecRef。这类似于将 python bool 转换为 int。这是一个使用示例：

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

这很理想，但是 (bv1 < bv2) 的类型是 Boolref，它会抛出 "sort mismatch" 错误。有没有办法转换 (bv1 < bv2) 的结果，以便 res 可以断言等于它？

Answer 1

位向量无法自动转换为布尔值。通常的方法是将它们包装在 if-then-elses 中，例如，在这个例子中，而不是

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

我们可以说

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

z3Py：将 BoolRef 转换为一位 BitVecRef

z3Py: Cast BoolRef to one-bit BitVecRef

python

casting

bitvector

z3

z3py