Function z3_sys::Z3_mk_const_array [−][src]
pub unsafe extern "C" fn Z3_mk_const_array(
c: Z3_context,
domain: Z3_sort,
v: Z3_ast
) -> Z3_ast
Expand description
Create the constant array.
The resulting term is an array, such that a select
on an arbitrary index
produces the value v
.
c
: logical context.domain
: domain sort for the array.v
: value that the array maps to.