datatype_update_field method
\brief Update record field with a value.
This corresponds to the 'with' construct in OCaml. It has the effect of updating a record field with a given value. The remaining fields are left unchanged. It is the record equivalent of an array store (see \sa Z3_mk_store). If the datatype has more than one constructor, then the update function behaves as identity if there is a mismatch between the accessor and constructor. For example ((_ update-field car) nil 1) is nil, while ((_ update-field car) (cons 2 nil) 1) is (cons 1 nil).
\pre Z3_get_sort_kind(Z3_get_sort(c, t)) == Z3_get_domain(c, field_access, 1) == Z3_DATATYPE_SORT \pre Z3_get_sort(c, value) == Z3_get_range(c, field_access)
def_API('Z3_datatype_update_field', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(AST), _in(AST)))
Implementation
Z3_ast datatype_update_field(
Z3_context c,
Z3_func_decl field_access,
Z3_ast t,
Z3_ast value,
) {
return _datatype_update_field(
c,
field_access,
t,
value,
);
}