z3求解器和求解器给出不同的结果

Question

我一直在尝试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.check(equations+problem)
solver.model()

尽管v正确，但这给s提供了错误的输出。

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

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

我是在z3的Solver中缺少明显的东西还是这是一个bug？谢谢。

Answer 1

这里的问题是，将solver.check的参数视为要满足的假设，而不是要检查的约束。请参阅此处的文档：https://z3prover.github.io/api/html/z3py_8py_source.html#l06628