add_rec_def method

void add_rec_def(
  1. Z3_context c,
  2. Z3_func_decl f,
  3. int n,
  4. Pointer<Z3_ast> args,
  5. Z3_ast body,
)

\brief Define the body of a recursive function.

\param c logical context. \param f function declaration. \param n number of arguments to the function \param args constants that are used as arguments to the recursive function in the definition. \param body body of the recursive function

After declaring a recursive function or a collection of mutually recursive functions, use this function to provide the definition for the recursive function.

\sa Z3_mk_rec_func_decl

def_API('Z3_add_rec_def', VOID, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST), _in(AST)))

Implementation

void add_rec_def(
  Z3_context c,
  Z3_func_decl f,
  int n,
  ffi.Pointer<Z3_ast> args,
  Z3_ast body,
) {
  return _add_rec_def(
    c,
    f,
    n,
    args,
    body,
  );
}