CODEWITHSUNDEEP
z3z3pyquantifiers
John Smith
John Smith

Reputation: 781

z3py: Usage of existential quantifier

This script

from z3 import *
solver = z3.Solver()
x = Int('x')
def f(y):
    return y+y
solver.add(x >= 0, x < 10, Exists(x, f(x) == 4) )
print solver.check()
print solver.model()

gives me 

sat
[x = 0]

as an answer. This is not what I want or expect. As an answer I would like to see 

sat
[x = 2]

I found two other posts going in a similar direction((Z3Py) declaring function and Quantifier in Z3), but something doesn't work out.

How do you use the existantial quantifier in this case to get an adequate answer?

Upvotes: 0

Views: 1354

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

The existential binds a different x whose scope is limited to the body of the formula. Hence, your constraints are effectively (0 ≤ x < 10) ∧ (∃ x' . f(x') == 4). Both conjuncts are satisfied by a model in which x = 0; in particular, the second conjunct is satisfied in this model because x' could be 2.

It seems that you want to constrain x further, not only by the inequality. Try the following (not tested)

solver.add(x >= 0, x < 10, f(x) == 4)

and then print the model.

Upvotes: 3

Related Questions