Function z3_sys::Z3_mk_fresh_func_decl

pub unsafe extern "C" fn Z3_mk_fresh_func_decl(
    c: Z3_context, 
    prefix: Z3_string, 
    domain_size: c_uint, 
    domain: *const Z3_sort, 
    range: Z3_sort
) -> Z3_func_decl

Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration. If prefix is different from NULL, then the name generate by Z3 will start with prefix.

NOTE: If prefix is NULL, then it is assumed to be the empty string.

See also:

• Z3_mk_func_decl