[−][src]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.