Function z3_sys::Z3_is_as_array [−][src]
pub unsafe extern "C" fn Z3_is_as_array(
c: Z3_context,
a: Z3_ast
) -> bool
Expand description
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.