[−][src]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)