Function z3_sys::Z3_mk_fresh_func_decl
source · 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
Expand description
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.