Values of Existential Quantifiers in Z3

Question

Say, I write a simple code with quantifiers as below:

from z3 import *
s = SolverFor("LIA")
x1, y1 = Ints('x1 y1')
s.add(ForAll(x1, Implies(x1>=0, Exists(y1, (y1>x1)))))

print(s.check()) print(s.model())

The result is :

sat
[ ]

Shouldn't this output a value of y1 for which it is satisfiable?

alias alias · Accepted Answer · 2019-12-17T16:37:57

And what would that value be? Note that the value of y1 depends on x1 in your formula, so it wouldn't make sense to print y1 only.

In general, once you go under a universal quantifier z3 can no longer print the value of variables. To do so meaningfully, it would have to print all the prefix universals, and unless all your domains are finite this wouldn't make sense. (Nor it would be useful.)

Values of Existential Quantifiers in Z3

1 Answers