Function z3_sys::Z3_is_as_array
[−]
[src]
pub unsafe extern "C" fn Z3_is_as_array(c: Z3_context, a: Z3_ast) -> Z3_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 Z3_TRUE
if the a
is an as
-array AST node.
Z3 current solvers have minimal support for as_array
nodes.
See also: