Function z3_sys::Z3_datatype_update_field

pub unsafe extern "C" fn Z3_datatype_update_field(
    c: Z3_context,
    field_access: Z3_func_decl,
    t: Z3_ast,
    value: Z3_ast
) -> Z3_ast

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 Z3_mk_store). If the datatype has more than one constructor, then the update function behaves as identity if there is a miss-match 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).

Preconditions:

• Z3_get_sort_kind(Z3_get_sort(c, t)) == Z3_get_domain(c, field_access, 1) == SortKind::Datatype
• Z3_get_sort(c, value) == Z3_get_range(c, field_access)