python - 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相同.不重载就不能让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]是解决方案之一。