时间戳

首页 > 解决方案 > z3 Solver 和 solve 给出不同的结果

z3 - z3 Solver 和 solve 给出不同的结果

问题描述

我一直在试验 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 中遗漏了一些明显的东西，或者这是一个错误？谢谢你。

标签： z3z3py

解决方案

这里的问题是，参数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如果您只想在一些额外的假设下检查有效性，则使用参数 to 。

推荐阅读