Function z3_sys::Z3_mk_func_decl [−][src]
pub unsafe extern "C" fn Z3_mk_func_decl(
c: Z3_context,
s: Z3_symbol,
domain_size: c_uint,
domain: *const Z3_sort,
range: Z3_sort
) -> Z3_func_decl
Expand description
Declare a constant or function.
c
: logical context.s
: name of the constant or function.domain_size
: number of arguments. It is 0 when declaring a constant.domain
: array containing the sort of each argument. The array must contain domain_size elements. It is 0 when declaring a constant.range
: sort of the constant or the return sort of the function.
After declaring a constant or function, the function
Z3_mk_app
can be used to create a constant or function
application.