Function z3_sys::Z3_mk_const_array

source · 
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.