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.

5 files changed, 122 insertions, 92 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 6ee1409d6..18db5d5ab 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -243,8 +243,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {APPLY_SELECTOR, cvc5::Kind::APPLY_SELECTOR},
     {APPLY_CONSTRUCTOR, cvc5::Kind::APPLY_CONSTRUCTOR},
     {APPLY_TESTER, cvc5::Kind::APPLY_TESTER},
-    {TUPLE_UPDATE, cvc5::Kind::TUPLE_UPDATE},
-    {RECORD_UPDATE, cvc5::Kind::RECORD_UPDATE},
+    {APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER},
     {DT_SIZE, cvc5::Kind::DT_SIZE},
     {TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT},
     /* Separation Logic ---------------------------------------------------- */
@@ -550,10 +549,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
         {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND},
         {cvc5::Kind::APPLY_TESTER, APPLY_TESTER},
-        {cvc5::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE},
-        {cvc5::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
-        {cvc5::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
-        {cvc5::Kind::RECORD_UPDATE, RECORD_UPDATE},
+        {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER},
         {cvc5::Kind::DT_SIZE, DT_SIZE},
         {cvc5::Kind::TUPLE_PROJECT, TUPLE_PROJECT},
         /* Separation Logic ------------------------------------------------ */
@@ -661,8 +657,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
 
 /* Set of kinds for indexed operators */
 const static std::unordered_set<Kind> s_indexed_kinds(
-    {RECORD_UPDATE,
-     DIVISIBLE,
+    {DIVISIBLE,
      IAND,
      BITVECTOR_REPEAT,
      BITVECTOR_ZERO_EXTEND,
@@ -672,7 +667,6 @@ const static std::unordered_set<Kind> s_indexed_kinds(
      INT_TO_BITVECTOR,
      FLOATINGPOINT_TO_UBV,
      FLOATINGPOINT_TO_SBV,
-     TUPLE_UPDATE,
      BITVECTOR_EXTRACT,
      FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
      FLOATINGPOINT_TO_FP_FLOATINGPOINT,
@@ -718,7 +712,8 @@ bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
 bool isApplyKind(cvc5::Kind k)
 {
   return (k == cvc5::Kind::APPLY_UF || k == cvc5::Kind::APPLY_CONSTRUCTOR
-          || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER);
+          || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER
+          || k == cvc5::Kind::APPLY_UPDATER);
 }
 
 #ifdef CVC5_ASSERTIONS
@@ -1194,6 +1189,15 @@ bool Sort::isTester() const
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Sort::isUpdater() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isUpdater();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 bool Sort::isFunction() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -1852,7 +1856,6 @@ size_t Op::getNumIndices() const
   switch (k)
   {
     case DIVISIBLE: size = 1; break;
-    case RECORD_UPDATE: size = 1; break;
     case BITVECTOR_REPEAT: size = 1; break;
     case BITVECTOR_ZERO_EXTEND: size = 1; break;
     case BITVECTOR_SIGN_EXTEND: size = 1; break;
@@ -1862,7 +1865,6 @@ size_t Op::getNumIndices() const
     case IAND: size = 1; break;
     case FLOATINGPOINT_TO_UBV: size = 1; break;
     case FLOATINGPOINT_TO_SBV: size = 1; break;
-    case TUPLE_UPDATE: size = 1; break;
     case REGEXP_REPEAT: size = 1; break;
     case BITVECTOR_EXTRACT: size = 2; break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break;
@@ -1892,12 +1894,10 @@ std::string Op::getIndices() const
   CVC5_API_CHECK(!d_node->isNull())
       << "Expecting a non-null internal expression. This Op is not indexed.";
   Kind k = intToExtKind(d_node->getKind());
-  CVC5_API_CHECK(k == DIVISIBLE || k == RECORD_UPDATE)
-      << "Can't get string index from"
-      << " kind " << kindToString(k);
+  CVC5_API_CHECK(k == DIVISIBLE) << "Can't get string index from"
+                                 << " kind " << kindToString(k);
   //////// all checks before this line
-  return k == DIVISIBLE ? d_node->getConst<Divisible>().k.toString()
-                        : d_node->getConst<RecordUpdate>().getField();
+  return d_node->getConst<Divisible>().k.toString();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -1938,7 +1938,6 @@ uint32_t Op::getIndices() const
     case FLOATINGPOINT_TO_SBV:
       i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size;
       break;
-    case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
     case REGEXP_REPEAT:
       i = d_node->getConst<RegExpRepeat>().d_repeatAmount;
       break;
@@ -3062,6 +3061,15 @@ Term DatatypeSelector::getSelectorTerm() const
   ////////
   CVC5_API_TRY_CATCH_END;
 }
+Term DatatypeSelector::getUpdaterTerm() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return Term(d_solver, d_stor->getUpdater());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
 
 Sort DatatypeSelector::getRangeSort() const
 {
@@ -3424,7 +3432,17 @@ Term Datatype::getConstructorTerm(const std::string& name) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
-  return getConstructor(name).getConstructorTerm();
+  return getConstructorForName(name).getConstructorTerm();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+DatatypeSelector Datatype::getSelector(const std::string& name) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return getSelectorForName(name);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -3579,6 +3597,30 @@ DatatypeConstructor Datatype::getConstructorForName(
   return DatatypeConstructor(d_solver, (*d_dtype)[index]);
 }
 
+DatatypeSelector Datatype::getSelectorForName(const std::string& name) const
+{
+  bool foundSel = false;
+  size_t index = 0;
+  size_t sindex = 0;
+  for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
+  {
+    int si = (*d_dtype)[i].getSelectorIndexForName(name);
+    if (si >= 0)
+    {
+      sindex = static_cast<size_t>(si);
+      index = i;
+      foundSel = true;
+      break;
+    }
+  }
+  if (!foundSel)
+  {
+    CVC5_API_CHECK(foundSel)
+        << "No select " << name << " for datatype " << getName() << " exists";
+  }
+  return DatatypeSelector(d_solver, (*d_dtype)[index][sindex]);
+}
+
 Datatype::const_iterator::const_iterator(const Solver* slv,
                                          const cvc5::DType& dtype,
                                          bool begin)
@@ -5806,29 +5848,18 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
-  CVC5_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE),
-                               kind)
-      << "RECORD_UPDATE or DIVISIBLE";
+  CVC5_API_KIND_CHECK_EXPECTED((kind == DIVISIBLE), kind) << "DIVISIBLE";
   //////// all checks before this line
   Op res;
-  if (kind == RECORD_UPDATE)
-  {
-    res = Op(this,
-             kind,
-             *mkValHelper<cvc5::RecordUpdate>(cvc5::RecordUpdate(arg)).d_node);
-  }
-  else
-  {
-    /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-     * throws an std::invalid_argument exception. For consistency, we treat it
-     * as invalid. */
-    CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg)
-        << "a string representing an integer, real or rational value.";
-    res = Op(this,
-             kind,
-             *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg)))
-                  .d_node);
-  }
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg)
+      << "a string representing an integer, real or rational value.";
+  res = Op(this,
+           kind,
+           *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg)))
+                .d_node);
   return res;
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -5905,11 +5936,6 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
           *mkValHelper<cvc5::FloatingPointToSBV>(cvc5::FloatingPointToSBV(arg))
                .d_node);
       break;
-    case TUPLE_UPDATE:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::TupleUpdate>(cvc5::TupleUpdate(arg)).d_node);
-      break;
     case REGEXP_REPEAT:
       res =
           Op(this,
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 1e857085b..16f58ee80 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -399,6 +399,11 @@ class CVC5_EXPORT Sort
    */
   bool isTester() const;
   /**
+   * Is this a datatype updater sort?
+   * @return true if the sort is a datatype updater sort
+   */
+  bool isUpdater() const;
+  /**
    * Is this a function sort?
    * @return true if the sort is a function sort
    */
@@ -1575,6 +1580,7 @@ class CVC5_EXPORT DatatypeDecl
  */
 class CVC5_EXPORT DatatypeSelector
 {
+  friend class Datatype;
   friend class DatatypeConstructor;
   friend class Solver;
 
@@ -1598,6 +1604,12 @@ class CVC5_EXPORT DatatypeSelector
    */
   Term getSelectorTerm() const;
 
+  /**
+   * Get the upater operator of this datatype selector.
+   * @return the updater term
+   */
+  Term getUpdaterTerm() const;
+
   /** @return the range sort of this argument. */
   Sort getRangeSort() const;
 
@@ -1908,6 +1920,15 @@ class CVC5_EXPORT Datatype
    */
   Term getConstructorTerm(const std::string& name) const;
 
+  /**
+   * Get the datatype constructor with the given name.
+   * This is a linear search through the constructors and their selectors, so
+   * in case of multiple, similarly-named selectors, the first is returned.
+   * @param name the name of the datatype selector
+   * @return the datatype selector with the given name
+   */
+  DatatypeSelector getSelector(const std::string& name) const;
+
   /** @return the name of this Datatype. */
   std::string getName() const;
 
@@ -2070,6 +2091,13 @@ class CVC5_EXPORT Datatype
   DatatypeConstructor getConstructorForName(const std::string& name) const;
 
   /**
+   * Return selector for name.
+   * @param name The name of selector to find
+   * @return the selector object for the name
+   */
+  DatatypeSelector getSelectorForName(const std::string& name) const;
+
+  /**
    * Helper for isNull checks. This prevents calling an API function with
    * CVC5_API_CHECK_NOT_NULL
    */
@@ -2890,7 +2918,6 @@ class CVC5_EXPORT Solver
 
   /**
    * Create operator of kind:
-   *   - RECORD_UPDATE
    *   - DIVISIBLE (to support arbitrary precision integers)
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
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
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 6302b7e43..e4c0eb915 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -32,6 +32,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         DatatypeConstructor operator[](const string& name) except +
         DatatypeConstructor getConstructor(const string& name) except +
         Term getConstructorTerm(const string& name) except +
+        DatatypeSelector getSelector(const string& name) except +
         size_t getNumConstructors() except +
         bint isParametric() except +
         bint isCodatatype() except +
@@ -89,6 +90,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         DatatypeSelector() except +
         string getName() except +
         Term getSelectorTerm() except +
+        Term getUpdaterTerm() except +
         Sort getRangeSort() except +
         string toString() except +
 
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 135eeb165..11742ca08 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -109,6 +109,12 @@ cdef class Datatype:
         term.cterm = self.cd.getConstructorTerm(name.encode())
         return term
 
+    def getSelector(self, str name):
+        """Return a selector by name."""
+        cdef DatatypeSelector ds = DatatypeSelector(self.solver)
+        ds.cds = self.cd.getSelector(name.encode())
+        return ds
+
     def getNumConstructors(self):
         """:return: number of constructors."""
         return self.cd.getNumConstructors()
@@ -267,6 +273,11 @@ cdef class DatatypeSelector:
         term.cterm = self.cds.getSelectorTerm()
         return term
 
+    def getUpdaterTerm(self):
+        cdef Term term = Term(self.solver)
+        term.cterm = self.cds.getUpdaterTerm()
+        return term
+
     def getRangeSort(self):
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.cds.getRangeSort()