mk_array_sort method

Z3_sort mk_array_sort(
  1. Z3_context c,
  2. Z3_sort domain,
  3. Z3_sort range
)

\brief Create an array type.

We usually represent the array type as: \ccode{domain -> range}. Arrays are usually used to model the heap/memory in software verification.

\sa Z3_mk_select \sa Z3_mk_store

def_API('Z3_mk_array_sort', SORT, (_in(CONTEXT), _in(SORT), _in(SORT)))

Implementation

Z3_sort mk_array_sort(
  Z3_context c,
  Z3_sort domain,
  Z3_sort range,
) {
  return _mk_array_sort(
    c,
    domain,
    range,
  );
}