是否可以在z3Py中将BoolRef其转换为一位长BitVecRef？在我的设计中，要求BitVecRef从其他两个之间的比较中返回a 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)为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)
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句