Retrieve a value in Z3Py yields unexpected result

问题:

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.

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

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

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

回答1:

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

1/5000

You should write:

1.0/5000.0

You can see the generated expression by:

print s.sexpr()

which would have alerted you to the issue.

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