CODEWITHSUNDEEP
pythonz3smtz3pybitvector
Sharad
Sharad

Reputation: 553

Or of bitvectors in z3Py

Ideally it is possible to 'Or' two numbers represented as bitvectors but I am not able to it. Please tell if there is some error in the code or something else

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

The error given is

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)

From this error I understand that Or can be done only for bool variables. My question is how to Or for BitVectors

Upvotes: 2

Views: 614

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

Yes, Or(a,b) is a boolean disjunction, you probably want a bitwise or since you're trying to compare bitvectors, which can be done in the Python API using | from the documentation (here's a z3py link for the example: 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]

I updated your example so that line1 and line2 are longer than 1 bit (which would be equivalent to the boolean case, but is a different type, hence the error).

Note that this is bvor in the SMT-LIB standard, see http://smtlib.cs.uiowa.edu/logics/V1/QF_BV.smt

Upvotes: 5

Related Questions