在 Z3Py 中检索值会产生意外结果 [英] Retrieve a value in Z3Py yields unexpected result

问题描述

我想找到一个最大区间，其中表达式 e 对所有 x 都为真.编写这样一个公式的方法应该是: Exists d : ForAll x in (-d,d) .e 和 ForAll x 不在 (-d,d) 中.!e.

I want to find a maximal interval in which an expression e is true for all x. A way to write such a formula should be: Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e.

要得到这样的 d，Z3 中的公式 f(看上面的那个)可能如下:

To get such a d, the formula f in Z3 (looking at the one above) could be the following:

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).怎么了?

It prints: [d = 2]. This is surely not true (take x = 1). What's wrong?

另外:通过指定 delta = RealVal('1')，反例是 x = 0，即使 x = 0 应该避免.

Also: by specifying delta = RealVal('1'), a counterexample is x = 0, even when x = 0 should be avoided.

推荐答案

您的常量被强制为整数.而不是写:

Your constants are getting coerced to integers. Instead of writing:

1/5000

你应该写:

1.0/5000.0

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

You can see the generated expression by:

print s.sexpr()

这会提醒您注意该问题.

which would have alerted you to the issue.

注意.在编写常量时，明确类型总是很重要的.有关此主题的变体，可能会导致更多问题，请参阅此答案:https://stackoverflow.com/a/46860633/936310

NB. Being explicit about types is always important when writing constants. See this answer for a variation on this theme that can lead to further problems: https://stackoverflow.com/a/46860633/936310

这篇关于在 Z3Py 中检索值会产生意外结果的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！