z3 Solver 解决方案问题

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()

返回sat，并给出解决方案

[p = 0, q = 0]

不满足约束。如果我删除最终约束，它会返回 满足前两个（平凡）约束的合理对。怎么回事？

在线试用的固定链接：http://rise4fun.com/Z3Py/fk4

---

编辑：我是 z3 的新手，所以我有可能做错了什么，请告诉我。

Answer 1

Z3 不支持使用 Python 的比较链，即 a < b < c 与 a < b and b < c 相同。如果不重载and，则无法使 Z3 支持它，这在 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] 是其中一种解决方案。