What is the correct way to handle quantified formulas with respect to empty models?

Question

I'm playing with uninterpreted sorts and functions and cannot quite understand how quantified formulas interact with empty models. Here (also here http://rise4fun.com/Z3Py/6ets) are some simple examples that somewhat confuse me:

1. [∀v : False] is unsat, while "intuitively" it holds for an empty model.
2. Checking [∃v : v = v] yields an empty model while that does not have a satisfying assignment.
3. Some formulas, seemingly equivalent to [∃v : v = v], somehow prevent z3 from producing empty models. [∃v, v1 : v = v1] is one such example. E.g., if we add such formula to a solver and then try to create something resembling an allsat procedure (adding more and more constraints to rule out more and more models), we would run into unsat before getting an empty model.

So, could you please refer me to any documents/papers describing how z3 handles quantifiers and empty models? Also, if I choose to restrict my attention to nonempty models only, what is the correct way to ask z3 for that? Things like [∃v, v1 : v = v1] seem to do the trick, but is there a better way?

Answer 1

Z3 does not consider empty models. This is a standard assumption in first-order logic. For more details search "first-order logic empty models", you will get many links explaining the motivation for this convention. The wikipedia page for first-order logic has a brief description (section "Empty domains").

Moreover, we should not confuse [] with the empty model. It is just saying that for satisfying the input formulas, Z3 does not need to assign an interpretation to any uninterpreted symbol in the input formula. Z3 displays only the interpretation of symbols that are needed to satisfy the formula. For example, the formula [∃v : v = v] does not contain any uninterpreted symbol, then Z3 just displays the empty assignment [].