Function z3_sys::Z3_mk_rec_func_decl

pub unsafe extern "C" fn Z3_mk_rec_func_decl(
    c: Z3_context,
    s: Z3_symbol,
    domain_size: c_uint,
    domain: *const Z3_sort,
    range: Z3_sort
) -> Z3_func_decl

Declare a recursive function

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

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

See also:

• Z3_mk_app
• Z3_add_rec_def