Function Z3_mk_func_decl

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

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.

See also:

• Z3_mk_app
• Z3_mk_fresh_func_decl
• Z3_mk_rec_func_decl