또는 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에서 |를 사용하여 파이썬 API에서 수행 할 수 있습니다 bitvectors을 비교하기 위해 노력하고 이후 때문이다 (이다 예를위한 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