Function z3_sys::Z3_mk_store

pub unsafe extern "C" fn Z3_mk_store(
    c: Z3_context, 
    a: Z3_ast, 
    i: Z3_ast, 
    v: Z3_ast
) -> Z3_ast

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).

See also:

• Z3_mk_array_sort
• Z3_mk_select