或z3Py中的bitvectors

Question

理想情况下,可以将'或'两个数字表示为位向量,但我无法做到.请告诉我们代码中是否有错误或其他错误

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变量做.我的问题是如何或为BitVectors

Answer 1

是的,Or(a,b)是一个布尔析取,你可能想要一点点,或者你想要比较bitvectors,这可以|在文档中使用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]

我更新了你的例子,使得line1和line2长于1位(这相当于布尔情况,但是是一个不同的类型,因此错误).

请注意,这是bvorSMT-LIB标准,请参阅http://smtlib.cs.uiowa.edu/logics/V1/QF_BV.smt