Z3Py 中最大值的模型不正确

我想找到一个表达式的最大间隔e对于所有 x 都成立。编写这样的公式的方法应该是：Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e.

为了得到这样一个d， 公式f在 Z3 中（看上面的）可能是以下内容：

from __future__ import division
from z3 import *

x = Real('x')
delta = Real('d')
s = Solver()

e = And(1/10000*x**2 > 0, 1/5000*x**3 + -1/5000*x**2 < 0)

f = ForAll(x,
And(Implies(And(delta > 0,
                -delta < x, x < delta, 
                x != 0),
            e),
    Implies(And(delta > 0,
                Or(x > delta, x < -delta),
                x != 0),
            Not(e))
    )
)

s.add(Not(f))
s.check()
print s.model()

哪个输出[d = 1/4].

为了检查它，我设置了delta = RealVal('1/4')，删除ForAll量词来自f我得到x = 1/2。我替换delta with 1/2并得到3/4, then 7/8等等。界限应该是1。我可以让Z3立即输出吗？

如果你自己算一下，你会发现解决方案是x != 0, x < 1。或者你可以简单地询问沃尔夫勒姆·阿尔法 http://www.wolframalpha.com/input/?i=1%2F10000*x**2%20%3E%200%20%26%26%20(1%2F5000*x**3%20%2B%20-1%2F5000*x**2%20%3C%200)为你做这件事。所以，不存在这样的delta.

您遇到的问题是您断言：

s.add(Not(f))

这将开启通用量化x进入存在主义；询问z3找到一个delta such 有一些x这符合要求。 （也就是说，你否定了整个公式。）相反，你应该这样做：

s.add(delta > 0, f)

这也确保了delta是积极的。进行此更改后，z3 将正确响应：

unsat

（然后你会收到一个错误，调用s.model()，你应该只调用s.model()如果之前的调用s.check()回报sat.)