Incorrect model of max value in Z3Py

问题:

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

Which outputs [d = 1/4].

To check it, I set delta = RealVal('1/4'), drop the ForAll quantifier from f and I get x = 1/2. I replace delta with 1/2 and get 3/4, then 7/8 and so on. The bound should be 1. Can I get Z3 to output that immediately?

回答1:

If you do the math yourself, you can see that the solution is x != 0, x < 1. Or you can simply ask Wolfram Alpha to do it for you. So, there's no such delta.

The issue you're having is that you're asserting:

s.add(Not(f))

This turns the universal quantification on x into an existential; asking z3 to find a delta such that there is some x that fits the bill. (That is, you're negating your whole formula.) Instead, you should do:

s.add(delta > 0, f)

which also makes sure that delta is positive. With that change, z3 will correctly respond:

unsat

(And then you'll get an error for the call to s.model(), you should only call s.model() if the previous call to s.check() returns sat.)