[−][src]Function z3_sys::Z3_is_as_array
pub unsafe extern "C" fn Z3_is_as_array(c: Z3_context, a: Z3_ast) -> bool
The (_ as-array f) AST node is a construct for assigning interpretations
for arrays in Z3.
It is the array such that forall indices i we have that
(select (_ as-array f) i) is equal to (f i). This procedure
returns true if the a is an as-array AST node.
Z3 current solvers have minimal support for as_array nodes.