CODEWITHSUNDEEP
z3z3py
Xenia Galinskaya
Xenia Galinskaya

Reputation: 25

Z3Py: add constraint of two vectors inequality

(Subj)

Here is my attempt:

#!/usr/bin/python
from z3 import *

s=Solver()

veclen=3

tmp_false=BoolVector ('tmp_false', veclen)
for x in range(veclen):
    s.add(tmp_false[x]==False)

tmp=BoolVector ('tmp', veclen)

s.add(tmp!=tmp_false) # not working

# I want here tmp equals to anything except False,False,False

print s.check()
print s.model()

I would use tuples, but length of vector is set during runtime. Should I use arrays? Or LISP-like cons-cells within tuples, as described in Z3 manuals?

Upvotes: 0

Views: 311

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The BoolVector function just creates a list structure. The != operator on python lists does not create an expression. It just evaluates to "true". So you are not really sending an expression to Z3. To create tuple expressions you can use algebraic data-types. A record type is a special case of an algebraic data-type, and Z3 understands how to reason about these. So for example, you can write:

from z3 import *

s=Solver()

Bv = Datatype("record")
Bv.declare('mk', ('1', BoolSort()), ('2', BoolSort()), ('3', BoolSort()))   
Bv = Bv.create()

tmp_false = Bv.mk(False, False, False)
tmp = Const('tmp', Bv)

print tmp != tmp_false
s.add(tmp!=tmp_false) 

# I want here tmp equals to anything except False,False,False

print s.check()
print s.model()

Upvotes: 2

Related Questions