python - z3Py：将 BoolRef 转换为一位 BitVecRef

Question

是否可以在 z3Py 中转换BoolRef为一位长？BitVecRef在我的设计中，要求 aBitVecRef从两个其他的比较中返回BitVecRef。这类似于将 pythonbool转换为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)is的类型Boolref，它会引发“排序不匹配”错误。有没有办法将结果转换为可以(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)