检索 Z3Py 中的值会产生意外结果

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

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

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 = 2]。这肯定不是真的（采取x = 1）。怎么了？

另外：通过指定delta = RealVal('1')，一个反例是x = 0，即使当x = 0应该避免。

您的常量被强制为整数。而不是写：

1/5000

你应该写：

1.0/5000.0

您可以通过以下方式查看生成的表达式：

print s.sexpr()

这会提醒您注意这个问题。

注意。编写常量时，明确类型始终很重要。请参阅此答案，了解该主题的变体，该变体可能会导致进一步的问题：https://stackoverflow.com/a/46860633/936310 https://stackoverflow.com/a/46860633/936310