z3 Solver 和 solve 给出不同的结果答案

【问题标题】：z3 Solver and solve give different resultsz3 Solver 和 solve 给出不同的结果
【发布时间】：2020-02-19 04:52:35
【问题描述】：

我一直在试验 z3（通过 pip3 获得的版本“4.8.7”）并发现了这个（明显的）差异。


t, s0, s, u, a, v = Reals('t s0 s u a v')
equations = [v == u + a*t, s == s0 + u*t + a*t**2/2,
             v**2 - u**2 == 2*a*s]
problem = [t == 10, s0 == 0, u == 0, a == 9.81]
solve(equations+problem)

这给出了 s 的正确输出：

[a = 981/100, u = 0, s0 = 0, t = 10, s = 981/2, v = 981/10]

但是当我使用 Solver 时，结果就不同了：

solver = Solver()
solver.check(equations+problem)
solver.model()

这给出了 s 的错误输出，尽管它使 v 正确。

[t = 10, u = 0, s0 = 0, s = 0, a = 981/100, v = 981/10]

s 应该是 (1/2) * (981/100) * 100，这是求解的结果。

我是否在 z3 的 Solver 中遗漏了一些明显的东西，或者这是一个错误？谢谢。

【问题讨论】：

标签： z3 z3py

【解决方案1】：

这里的问题是solver.check 的参数是求解器在求解约束时可以做出的额外假设，而不是要检查的实际约束。请参阅此处的文档：https://z3prover.github.io/api/html/z3py_8py_source.html#l06628

正确的调用是：

solver = Solver()
solver.add(equations+problem)
print solver.check()
print solver.model()

也就是说，你 add 约束，然后在没有参数的情况下调用 check。这将匹配 solve 所做的。如果您只想在一些额外的假设下检查有效性，则使用 check 的参数。

【讨论】：