Function z3_sys::Z3_mk_store [−][src]
pub unsafe extern "C" fn Z3_mk_store(
c: Z3_context,
a: Z3_ast,
i: Z3_ast,
v: Z3_ast
) -> Z3_ast
Expand description
Array update.
The node a
must have an array sort [domain -> range]
, i
must have sort domain
,
v
must have sort range. The sort of the result is [domain -> range]
.
The semantics of this function is given by the theory of arrays described in the SMT-LIB
standard. See http://smtlib.org for more details.
The result of this function is an array that is equal to a
(with respect to select
)
on all indices except for i
, where it maps to v
(and the select
of a
with
respect to i
may be a different value).