add_func_interp method

Z3_func_interp add_func_interp(
  1. Z3_context c,
  2. Z3_model m,
  3. Z3_func_decl f,
  4. Z3_ast default_value,
)

\brief Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.

\param c context \param m model \param f function declaration \param default_value default value for function interpretation

def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))

Implementation

Z3_func_interp add_func_interp(
  Z3_context c,
  Z3_model m,
  Z3_func_decl f,
  Z3_ast default_value,
) {
  return _add_func_interp(
    c,
    m,
    f,
    default_value,
  );
}