mk_const_array method

Z3_ast mk_const_array(
  1. Z3_context c,
  2. Z3_sort domain,
  3. Z3_ast v
)

\brief Create the constant array.

The resulting term is an array, such that a \c select on an arbitrary index produces the value \c v.

\param c logical context. \param domain domain sort for the array. \param v value that the array maps to.

def_API('Z3_mk_const_array', AST, (_in(CONTEXT), _in(SORT), _in(AST)))

Implementation

Z3_ast mk_const_array(
  Z3_context c,
  Z3_sort domain,
  Z3_ast v,
) {
  return _mk_const_array(
    c,
    domain,
    v,
  );
}