model_get_func_interp method

Z3_func_interp model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)

\brief Return the interpretation of the function \c f in the model \c m. Return \c NULL, if the model does not assign an interpretation for \c f. That should be interpreted as: the \c f does not matter.

\pre Z3_get_arity(c, f) > 0

\remark Reference counting must be used to manage Z3_func_interp objects, even when the Z3_context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

def_API('Z3_model_get_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))

Implementation

Z3_func_interp model_get_func_interp(
  Z3_context c,
  Z3_model m,
  Z3_func_decl f,
) {
  return _model_get_func_interp(
    c,
    m,
    f,
  );
}