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()
返回 sat，并给出解决方案
[p = 0, q = 0]
不满足约束。如果我删除最后一个约束，它会返回一个满足前两个（平凡）约束的合理对。这是怎么回事？
在线尝试的永久链接：http ://rise4fun.com/Z3Py/fk4
编辑：我是 z3 的新手，所以我有可能做错了什么，请告诉我。
Z3 不支持使用 Python 的比较链，即a < b < c与a < b and b < c. Z3 不能在没有重载的情况下支持它，and这在 Python 中目前是不可能的。所以a < b < c应该写成：
b_ = b
Z3.And(a < b_, b_ < c)
只计算b一次表达式。
将s.add行替换为：
s.add(1<=p, p<=9, 1<=q, q<=19, 5<(3*p-4*q), (3*p-4*q)<10)
我得到：
[p = 6, q = 3]
所以你必须像我上面为求解器所做的那样将它们分开。
Python 扩展1<=p<=9为1<=p and p<=9，当它被解释p<=9为原样bool(1 <= p)时True，问题中的代码导致求解：
s.add(p<=9, q<=19, (3*p-4*q)<10)
这[p = 0, q = 0]是解决方案之一。