CODEWITHSUNDEEP
z3z3py
user4562262
user4562262

Reputation: 170

z3 Solver and solve give different results

I have been experimenting with z3 (version '4.8.7' obtained through pip3) and found this (apparent) discrepancy.


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)

This gives the correct output for s:

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

But when I use the Solver, the result is different:

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

This gives a wrong output for s, though it gets v right.

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

s should be (1/2) * (981/100) * 100 which is the result in solve.

Am I missing something obvious in z3's Solver or is this a bug? Thank you.

Upvotes: 0

Views: 301

Answers (1)

alias
alias

Reputation: 30525

The issue here is that the argument to solver.check are extra assumptions the solver can make as it solves the constraints, not the actual constraints to check. See the documentation here: https://z3prover.github.io/api/html/z3py_8py_source.html#l06628

The correct call would be:

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

that is, you add the constraints, and then call check with no arguments. This would match what solve does. The argument to check are used if you want to check validity under some extra assumptions only.

Upvotes: 3

Related Questions