python - 或z3Py中的位向量

理想情况下，可以将两个数字“或”表示为位向量，但我不能这样做。请告诉我代码中是否有错误

line1 = BitVec('line1', 1)
line2 = BitVec('line2', 1)
s = Solver()
s.add(Or(line1, line2) == 0)
print s.check()

给出的错误是

error: 'type error'
WARNING: invalid function application for or, sort mismatch on argument at position 1,         expected Bool but given (_ BitVec 1)
WARNING: (declare-fun or (Bool Bool) Bool) applied to:
line1 of sort (_ BitVec 1)
line2 of sort (_ BitVec 1)

从这个错误中，我了解或者只能对bool变量执行。我的问题是如何或为位向量

最佳答案

是的，Or(a,b)是一个布尔析取，您可能需要按位或因为您正在尝试比较位向量，这可以使用documentation中的|在Python API中完成（这里有一个z3py链接，例如：http://rise4fun.com/Z3Py/1l0）：

line1 = BitVec('line1', 2)
line2 = BitVec('line2', 2)
s = Solver()
P = (line1 | line2) != 0
print P
s.add(P)
print s.check()
print s.model() # [line2 = 0, line1 = 3]

我更新了您的示例，使第1行和第2行的长度超过1位（这相当于布尔值大小写，但类型不同，因此出错）。
请注意，这是SMT-LIB标准中的bvor，请参见http://smtlib.cs.uiowa.edu/logics/V1/QF_BV.smt

关于python - 或z3Py中的位向量，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/22357609/