z3 Solver solution issues

Question

p = Int('p')
q = Int('q')

s = Solver()
s.add(1<=p<=9, 1<=q<=19, 5<(3*p-4*q)<10)
s.check() 
print s.model()

returns sat, and gives the solution

[p = 0, q = 0]

which does not satisfy the constraints. If I remove the final constraint, it returns a sensible pair that satisfies the first two (trivial) constraints. What's going on?

Permalink to try this online: http://rise4fun.com/Z3Py/fk4

---

EDIT : I'm new to z3, so there's a chance I'm doing something horribly wrong, do let me know.

Answer 1

Z3 does not support using Python's comparison chaining i.e. that a < b < c is the same as a < b and b < c. Z3 can not be made to support it without overloading and which is currently not possible in Python. So a < b < c should be written as:

b_ = b
Z3.And(a < b_, b_ < c)

to only evaluate the expression b once.

---

After replacing the s.add line with:

s.add(1<=p, p<=9, 1<=q, q<=19, 5<(3*p-4*q), (3*p-4*q)<10)

I get:

[p = 6, q = 3]

So you have to split them up as I did above for the solver.

---

Python expands 1<=p<=9 to 1<=p and p<=9, when that is interpreted this results in p<=9 as bool(1 <= p) is True, the code in the question results in solving for:

s.add(p<=9, q<=19, (3*p-4*q)<10)

for which [p = 0, q = 0] is one of the solutions.