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

问题描述 投票:0回答:1

我一直在尝试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?谢谢。

z3 z3py
1个回答
0
投票

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

© www.soinside.com 2019 - 2024. All rights reserved.