Merge pull request #8500 from Z3Prover/copilot/update-functional-datatype

Add datatype_update_field to C++, Python, TypeScript, and OCaml bindings

src/api/c++/z3++.h

@@ -1296,6 +1296,17 @@ namespace z3 {
         */
         expr update(expr_vector const& args) const;
 
+        /**
+           \brief Update a datatype field.
+           Return a new datatype expression with the specified field updated to the new value.
+           The remaining fields are unchanged.
+
+           \pre is_datatype()
+           \param field_access The accessor function declaration for the field to update
+           \param new_value The new value for the field
+        */
+        expr update_field(func_decl const& field_access, expr const& new_value) const;
+
         /**
            \brief Return the 'body' of this quantifier.
 
@@ -4471,6 +4482,13 @@ namespace z3 {
         return expr(ctx(), r);
     }
 
+    inline expr expr::update_field(func_decl const& field_access, expr const& new_value) const {
+        assert(is_datatype());
+        Z3_ast r = Z3_datatype_update_field(ctx(), field_access, m_ast, new_value);
+        check_error();
+        return expr(ctx(), r);
+    }
+
     typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t;
 
     class on_clause {

src/api/js/src/high-level/high-level.ts

@@ -4819,6 +4819,13 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return _toExpr(check(Z3.substitute_funs(contextPtr, t.ast, from, to)));
     }
 
+    function updateField(t: DatatypeExpr<Name>, fieldAccessor: FuncDecl<Name>, newValue: Expr<Name>): DatatypeExpr<Name> {
+      _assertContext(t);
+      _assertContext(fieldAccessor);
+      _assertContext(newValue);
+      return _toExpr(check(Z3.datatype_update_field(contextPtr, fieldAccessor.ptr, t.ast, newValue.ast))) as DatatypeExpr<Name>;
+    }
+
     function ast_from_string(s: string): Ast<Name> {
       const sort_names: Z3_symbol[] = [];
       const sorts: Z3_sort[] = [];
@@ -4998,6 +5005,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       substitute,
       substituteVars,
       substituteFuns,
+      updateField,
       simplify,
 
       /////////////

src/api/js/src/high-level/types.ts

@@ -808,6 +808,9 @@ export interface Context<Name extends string = 'main'> {
   /** @category Operations */
   substituteFuns(t: Expr<Name>, ...substitutions: [FuncDecl<Name>, Expr<Name>][]): Expr<Name>;
 
+  /** @category Operations */
+  updateField(t: DatatypeExpr<Name>, fieldAccessor: FuncDecl<Name>, newValue: Expr<Name>): DatatypeExpr<Name>;
+
   simplify(expr: Expr<Name>): Promise<Expr<Name>>;
 
   /** @category Operations */

src/api/ml/z3.ml

@@ -961,6 +961,9 @@ struct
       let g j = Z3native.get_datatype_sort_constructor_accessor (Sort.gc x) x i j in
       List.init ds g) in
     List.init n f
+
+  let update_field (ctx:context) (field_access:FuncDecl.func_decl) (t:Expr.expr) (v:Expr.expr) =
+    Z3native.datatype_update_field ctx field_access t v
 end
 
 

src/api/ml/z3.mli

@@ -1130,6 +1130,12 @@ sig
 
   (** The constructor accessors. *)
   val get_accessors : Sort.sort -> FuncDecl.func_decl list list
+
+  (** Update a datatype field at expression [t] with value [v].
+      The function performs a record update at [t]. The field
+      that is passed in as argument is updated with value [v],
+      the remaining fields of [t] are unchanged. *)
+  val update_field : context -> FuncDecl.func_decl -> Expr.expr -> Expr.expr -> Expr.expr
 end
 
 (** Functions to manipulate Enumeration expressions *)

src/api/python/z3/z3.py

@@ -5523,6 +5523,32 @@ class DatatypeRef(ExprRef):
         """Return the datatype sort of the datatype expression `self`."""
         return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 
+    def update_field(self, field_accessor, new_value):
+        """Return a new datatype expression with the specified field updated.
+        
+        Args:
+            field_accessor: The accessor function declaration for the field to update
+            new_value: The new value for the field
+            
+        Returns:
+            A new datatype expression with the field updated, other fields unchanged
+            
+        Example:
+            >>> Person = Datatype('Person')
+            >>> Person.declare('person', ('name', StringSort()), ('age', IntSort()))
+            >>> Person = Person.create()
+            >>> person_age = Person.accessor(0, 1)  # age accessor
+            >>> p = Const('p', Person)
+            >>> p2 = p.update_field(person_age, IntVal(30))
+        """
+        if z3_debug():
+            _z3_assert(is_func_decl(field_accessor), "Z3 function declaration expected")
+            _z3_assert(is_expr(new_value), "Z3 expression expected")
+        return _to_expr_ref(
+            Z3_datatype_update_field(self.ctx_ref(), field_accessor.ast, self.as_ast(), new_value.as_ast()),
+            self.ctx
+        )
+
 def DatatypeSort(name, params=None, ctx=None):
     """Create a reference to a sort that was declared, or will be declared, as a recursive datatype.