Function z3_sys::Z3_model_eval [−] [src]

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

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

If model_completion is Z3_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 Z3_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.