Add support for datatype update (#6449)

This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.

Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.

1 files changed, 10 insertions, 46 deletions

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index f7658412c..0375b5e60 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1918,11 +1918,11 @@ enum CVC5_EXPORT Kind : int32_t
    */
   APPLY_CONSTRUCTOR,
   /**
-   * Datatype selector application.
+   * Datatype selector application, which is undefined if misapplied.
    *
    * Parameters:
    *   - 1: Selector (operator)
-   *   - 2: Datatype term (undefined if mis-applied)
+   *   - 2: Datatype term
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
@@ -1940,56 +1940,20 @@ enum CVC5_EXPORT Kind : int32_t
    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
   APPLY_TESTER,
-#if 0
-  /* Parametric datatype term.  */
-  PARAMETRIC_DATATYPE,
-  /* type ascription, for datatype constructor applications;
-   * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor
-   * application being ascribed */
-  APPLY_TYPE_ASCRIPTION,
-#endif
-  /**
-   * Operator for a tuple update.
-   *
-   * Parameters:
-   *   - 1: Index of the tuple to be updated
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
-   *
-   * Apply tuple update.
-   *
-   * Parameters:
-   *   - 1: Op of kind TUPLE_UPDATE (which references an index)
-   *   - 2: Tuple
-   *   - 3: Element to store in the tuple at the given index
-   *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
-   */
-  TUPLE_UPDATE,
   /**
-   * Operator for a record update.
+   * Datatype update application, which does not change the argument if
+   * misapplied.
    *
    * Parameters:
-   *   - 1: Name of the field to be updated
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, const std::string& param) const`
-   *
-   * Record update.
-   *
-   * Parameters:
-   *   - 1: Op of kind RECORD_UPDATE (which references a field)
-   *   - 2: Record term to update
-   *   - 3: Element to store in the record in the given field
+   *   - 1: Updater (operator)
+   *   - 2: Datatype term
+   *   - 3: Value to update a field of the datatype term with
    *
    * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op,, const std::vector<Term>& children) const`
+   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
-  RECORD_UPDATE,
+  APPLY_UPDATER,
   /**
    * Match expressions.
    * For example, the smt2 syntax match term