或位矢量z3Py

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) 

從這個錯誤我明白，或者可用於布爾變量只是做。我的問題是如何或爲BitVectors

Answer 1

是，Or(a,b)是一個布爾脫節，你可能想按位或因爲你試圖從documentation比較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] 

我更新您的示例，使得第1行和第2行是大於1位（這將等同於布爾情況，但是是不同的類型，因此誤差更長）。

注意，這是在SMT-LIB標準bvor，看到http://smtlib.cs.uiowa.edu/logics/V1/QF_BV.smt