is_as_array method

bool is_as_array(
  1. Z3_context c,
  2. Z3_ast a
)

\brief The \ccode{(_ as-array f)} AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices \c i we have that \ccode{(select (_ as-array f) i)} is equal to \ccode{(f i)}. This procedure returns \c true if the \c a is an \c as-array AST node.

Z3 current solvers have minimal support for \c as_array nodes.

\sa Z3_get_as_array_func_decl

def_API('Z3_is_as_array', BOOL, (_in(CONTEXT), _in(AST)))

Implementation

bool is_as_array(
  Z3_context c,
  Z3_ast a,
) {
  return _is_as_array(
    c,
    a,
  );
}