mk_store method

Z3_ast mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v,)

\brief Array update.

The node \c a must have an array sort \ccode{domain -> range}, \c i must have sort \c domain, \c v must have sort range. The sort of the result is \ccode{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 \c a (with respect to \c select) on all indices except for \c i, where it maps to \c v (and the \c select of \c a with respect to \c i may be a different value).

\sa Z3_mk_array_sort \sa Z3_mk_select

def_API('Z3_mk_store', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))

Implementation

Z3_ast mk_store(
  Z3_context c,
  Z3_ast a,
  Z3_ast i,
  Z3_ast v,
) {
  return _mk_store(
    c,
    a,
    i,
    v,
  );
}