Function Z3_model_eval

pub unsafe extern "C" fn Z3_model_eval(
    c: Z3_context,
    m: Z3_model,
    t: Z3_ast,
    model_completion: bool,
    v: *mut Z3_ast,
) -> bool

Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.

If model_completion is true, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in m. These constants and functions were essentially don’t cares.

If model_completion is false, then Z3 will not assign interpretations to constants for functions that do not have interpretations in m. Evaluation behaves as the identify function in this case.

The evaluation may fail for the following reasons:

• t contains a quantifier.
• the model m is partial, that is, it doesn’t have a complete interpretation for uninterpreted functions. That is, the option MODEL_PARTIAL=true was used.
• t is type incorrect.
• Z3_interrupt was invoked during evaluation.