mk_rec_func_decl method

Z3_func_decl mk_rec_func_decl(
  1. Z3_context c,
  2. Z3_symbol s,
  3. int domain_size,
  4. Pointer<Z3_sort> domain,
  5. Z3_sort range,
)

\brief Declare a recursive function

\param c logical context. \param s name of the function. \param domain_size number of arguments. It should be greater than 0. \param domain array containing the sort of each argument. The array must contain domain_size elements. \param range sort of the constant or the return sort of the function.

After declaring recursive function, it should be associated with a recursive definition #Z3_add_rec_def. The function #Z3_mk_app can be used to create a constant or function application.

\sa Z3_add_rec_def \sa Z3_mk_app \sa Z3_mk_func_decl

def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))

Implementation

Z3_func_decl mk_rec_func_decl(
  Z3_context c,
  Z3_symbol s,
  int domain_size,
  ffi.Pointer<Z3_sort> domain,
  Z3_sort range,
) {
  return _mk_rec_func_decl(
    c,
    s,
    domain_size,
    domain,
    range,
  );
}