Z3::Model

The declarations of the variables the model assigned - #each_const is what yields the variables themselves

Constants first, then functions - so what's yielded is a variable and its value, or a declaration and its interpretation, and both halves are unions

Yields each constant in the model as a {variable, value} pair, sorted by name

Yields each function as a {declaration, interpretation} pair, sorted by name

The uninterpreted functions the model decided the meaning of.

Recursive definitions are left out. Z3 puts every one made in the context into every model, of every solver, whether or not the query so much as mentioned it - define-fun-rec is context-global the way it is in an SMT-LIB script. It isn't something this model decided, it's the definition handed straight back, and its else branch is a body over de Bruijn variables which no Expr can hold.

Whether the model says anything at all about this variable or function. It's the question #model_eval can't answer: without completion an unassigned variable evaluates to itself, and with it Z3 invents a value rather than telling you it had to.

#eval without the sort coming back with it, for the cases where the expression's class isn't known statically - an argument of a FuncDecl, say

A formula asserting the model must differ somewhere - useful for enumerating all solutions.

Only constants are negated. Saying "some function differs somewhere" needs a quantifier, so a model with functions in it can repeat under this.

This needs to go eventually