datatype_update_field method

Z3_ast datatype_update_field(
  1. Z3_context c,
  2. Z3_func_decl field_access,
  3. Z3_ast t,
  4. Z3_ast value,
)

\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,
  );
}