这是Z3中的一个bug吗？应用了Real和ForAll的答案不正确

Question

我试图找到抛物线y=(x+2)**2-3的最小值，显然，当x==-2时，答案应该是y==-3。但是z3给出了x= 0，y= 1的答案，这不符合ForAll断言。

我是不是在某些方面假设错误了？

以下是python代码：

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

结果是：

[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]

结果表明，'qe‘策略消除了ForAll断言为真，尽管它并不总是正确的。这是求解器给出错误答案的原因吗？我应该编写什么代码来找到这样一个表达式的最小值(或最大值)？

顺便说一句，Mac的Z3版本是4.3.2。

Answer 1

我参考了How does Z3 handle non-linear integer arithmetic?，并使用“qfnra-nlsat”和“smt”策略找到了部分解决方案。

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

结果是：

sat
[x = -2, y = -3]
sat
[x = 0, y = 1]

尽管如此，“量化宽松”策略和默认求解器看起来还是有问题的。他们不会给出正确的结果。还需要进一步的评论和讨论。