model_eval method

bool model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Pointer<Z3_ast> v,)

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

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

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

The evaluation may fail for the following reasons:

• \c t contains a quantifier.

• the model \c m is partial, that is, it doesn't have a complete interpretation for uninterpreted functions. That is, the option \ccode{MODEL_PARTIAL=true} was used.

• \c t is type incorrect.

• \c Z3_interrupt was invoked during evaluation.

def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))

Implementation

bool model_eval(
  Z3_context c,
  Z3_model m,
  Z3_ast t,
  bool model_completion,
  ffi.Pointer<Z3_ast> v,
) {
  return _model_eval(
    c,
    m,
    t,
    model_completion,
    v,
  );
}