Retrieve a value in Z3Py yields unexpected result

Question

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.

alias · Accepted Answer · 2018-06-20 00:05:28Z

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

edited Jun 20, 2018 at 0:05

answered Jun 19, 2018 at 23:59

alias

30.9k2 gold badges31 silver badges51 bronze badges

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

3 Comments

yokke Over a year ago

Ok, that was a problem. The formula seems to be wrong anyway, given that I want the max value: it gives 1/4. Setting delta = RealVal('1/4') returns x = 1/2 (true in fact). Setting it to 1/2 returns 3/4 and so on (should be 1). Adjusting the < and > to <=, >= doesn't help. Trying with ForAll x... and !Exists x ... also doesn't produce the expected value.

alias Over a year ago

Not sure what you make of your comment. Are you saying z3 is computing an incorrect model? If so, please formulate a new question and post it separately. (Note: I didn’t actually check your program for details, other than noticing that the constants were incorrectly coded.)

yokke Over a year ago

Yes. Ok, here we go: stackoverflow.com/questions/50947472/…

Collectives™ on Stack Overflow

Retrieve a value in Z3Py yields unexpected result

1 Answer 1

3 Comments

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

3 Comments

Linked

Related