0

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?

John Smith
  • 771
  • 8
  • 25

1 Answers1

3

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.

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
  • Great. Then my first problem was the scope of `exists`. I modified the assertion to `solver.add(Exists(x, And(f(x) == 4, x >= 0, x < 10)))` and the SMT solver now returns a `sat` or `unsat` depending on my input correctly. Still, I cannot get the solver to give me a hint of the `x` that satisfied the assertion. How can you do that? The solution you mentioned above is correct, as it does what you say, but I want to use quantifiers in another context (model checking) and need the result. – John Smith Aug 24 '17 at 10:21
  • 1
    The best way to achieve that is to skolemize the formula yourself, i.e., insert new function symbols that replace the existentials, and which depend on the universals in scope. That way you are in control of the names of those functions and they will have a function interpretation in the model. – Christoph Wintersteiger Aug 24 '17 at 11:20