Function z3_sys::Z3_mk_map [−][src]
pub unsafe extern "C" fn Z3_mk_map(
c: Z3_context,
f: Z3_func_decl,
n: c_uint,
args: *const Z3_ast
) -> Z3_ast
Expand description
Map f on the argument arrays.
The n
nodes args
must be of array sorts [domain_i -> range_i]
.
The function declaration f
must have type range_1 .. range_n -> range
.
v
must have sort range. The sort of the result is [domain_i -> range]
.