[Question] How can I get a model from formula with quantifier?

[hagozaebii]

Hi, recently I solved a formula with quantifier using z3. But I encountered results that I cannot understand.

First, a model that I got from the formula was empty. For example, z3 gives an empty model about the below formula.

>>> p
ForAll(x, x < x + 1)
>>> solver = Solver()
>>> solver.add(p)
>>> solver.check()
sat
>>> model = solver.model()
>>> model
[]

Why is the model an empty list? I am curious about what it means(the meaning of the empty list).

Second, I cannot evaluate another formula based on the model. Let's assume a situation where we have a very trivial formula.

>>> simple
1 == x
>>> model.evaluate(simple)
1 == x

the model that I used is what I got from the formula 'ForAll(x, x < x + 1)'. In my humble opinion, I think the result of the evaluation should be 'true'. However, z3 did not do anything in the evaluation. I hope to know the reason why z3 does not support evaluation based on the model got from the formula with quantifier.

To summarize my question,
a) What is the meaning of an empty list as a model?
b) How can I evaluate another formula with a model from a formula with quantifier?

Thanks for your time.

[NikolajBjorner]

1. the empty list means the model does not assign values to any (free) variables/functions. Your example only had bound variables.
2. the evaluate function does not perform any quantifier reasoning. It just substitutes in values from models and does constant folding. A quantified formula is similar to a program. The halting problem is undecidable, similar with respect to quantifier evaluation.