Is this a bug in Z3? Wrong answer on Real and ForAll
I'm trying to find the minimum value of the parabola y = (x + 2) ** 2-3, apparently the answer should be y == - 3 when x == - 2. But z3 gives the answer [x = 0, y = 1], which does not match the ForAll statement.
Am I mistakenly assuming something?
Here is the python code:
from z3 import *
x, y, z = Reals('x y z')
print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3,
ForAll([z], y <= (z + 2) ** 2 - 3))))
solve(y == x * x + 4 * x +1,
ForAll([z], y <= z * z + 4 * z +1))
And the result:
[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]
The result shows that the "qe" tactic removes this ForAll to True, although it is NOT always true. Is this the reason the solver is giving the wrong answer? What should I code to find the minimum (or maximum) value of such an expression?
BTW version Z3 for Mac is 4.3.2.
source to share
I titled How does Z3 handle non-linear integer arithmetic? and found a partial solution using the "qfnra-nlsat" and "smt" tactics.
from z3 import *
x, y, z = Reals('x y z')
s1 = Then('qfnra-nlsat','smt').solver()
print s1.check(And(y == (x + 2) ** 2 - 3,
ForAll([z], y <= (z + 2) ** 2 - 3)))
print s1.model()
s2 = Then('qe', 'qfnra-nlsat','smt').solver()
print s2.check(And(y == (x + 2) ** 2 - 3,
ForAll([z], y <= (z + 2) ** 2 - 3)))
print s2.model()
And the result:
sat
[x = -2, y = -3]
sat
[x = 0, y = 1]
However, the "qe" tactic and the default solver seem to be errors. They don't give the correct result. Further comments and discussion are needed.
source to share