2

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?

Improve this question

1 Answer 1

Reset to default
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.)

Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

What's different between s.add(d > 0, f) and f = ForAll(x, Implies(d > 0, ...) in Z3?
Former is conjunction, latter is implication. With the former, you are telling z3 to find you a model making sure d is strictly positive and also f holds too. With the latter, you are telling z3 to find a model where you only care f holding when d is positive. That is, it can find you a model with d <= 0 and completely ignore what happens with f, which isn't what you want. Note that this has nothing to do with z3 in particular, but just regular predicate logic. The difference between p /\ forall x. q and forall x. p => q, when p does not mention x.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.