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

是否可以在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，并且会引发“排序不匹配”错误。有没有一种方法可以强制转换(bv1 < bv2)的结果，使res可以断言等于它的值？

最佳答案

位向量不能自动转换为布尔值。通常的方法是将它们包装在if-then-els中，例如在本示例中，而不是

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

我们可以说

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

关于python - z3Py:将BoolRef转换为一位BitVecRef，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/39380560/