Решатель z3 и решить дают разные результаты

Question

Я экспериментировал с z3 (версия 4.8.7, полученная через pip3) и обнаружил это (очевидное) расхождение.

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()

Это дает неправильный вывод для s, хотя он получает v правильно.

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

s должно быть (1/2) * (981/100) * 100, что является результатом решения.

Я упускаю что-то очевидное в Solver в z3 или это ошибка? Спасибо.

Answer 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 используется, если вы хотите проверить достоверность только при некоторых дополнительных предположениях.