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.

8 files changed, 8 insertions, 98 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 28cf23f57..9bf63dcfc 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -112,8 +112,6 @@ libcvc5_add_sources(
   dtype_cons.cpp
   dtype_selector.h
   dtype_selector.cpp
-  record.cpp
-  record.h
   sequence.cpp
   sequence.h
   subs.cpp
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 07b8aa5f1..c1893d3f4 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -109,7 +109,7 @@ const DType& DType::datatypeOf(Node item)
 size_t DType::indexOf(Node item)
 {
   Assert(item.getType().isConstructor() || item.getType().isTester()
-         || item.getType().isSelector());
+         || item.getType().isSelector() || item.getType().isUpdater());
   return indexOfInternal(item);
 }
 
@@ -125,7 +125,7 @@ size_t DType::indexOfInternal(Node item)
 
 size_t DType::cindexOf(Node item)
 {
-  Assert(item.getType().isSelector());
+  Assert(item.getType().isSelector() || item.getType().isUpdater());
   return cindexOfInternal(item);
 }
 size_t DType::cindexOfInternal(Node item)
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0a0781819..780fda9ab 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -724,7 +724,7 @@ TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range)
       domain.isDatatype(), domain, "cannot create non-datatype upater type");
   // It is a function type domain x range -> domain, we store only the
   // arguments
-  return mkTypeNode(kind::DT_UPDATE_TYPE, domain, range);
+  return mkTypeNode(kind::UPDATER_TYPE, domain, range);
 }
 
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8b99f5743..9952baf89 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -34,6 +34,8 @@
 
 namespace cvc5 {
 
+using Record = std::vector<std::pair<std::string, TypeNode>>;
+
 namespace api {
 class Solver;
 }
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
deleted file mode 100644
index 0792de20c..000000000
--- a/src/expr/record.cpp
+++ /dev/null
@@ -1,27 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class representing a record definition.
- */
-
-#include "expr/record.h"
-
-#include "base/check.h"
-#include "base/output.h"
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
-  return out << "[" << t.getField() << "]";
-}
-
-}  // namespace cvc5
diff --git a/src/expr/record.h b/src/expr/record.h
deleted file mode 100644
index ecf6c8d32..000000000
--- a/src/expr/record.h
+++ /dev/null
@@ -1,60 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Mathias Preiner, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class representing a Record definition.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__RECORD_H
-#define CVC5__RECORD_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <utility>
-
-// Forward Declarations
-namespace cvc5 {
-// This forward delcartion is required to resolve a cicular dependency with
-// Record which is a referenced in a Kind file.
-class TypeNode;
-}  // namespace cvc5
-
-namespace cvc5 {
-
-// operators for record update
-class RecordUpdate
-{
-  std::string d_field;
-
- public:
-  RecordUpdate(const std::string& field) : d_field(field) {}
-  std::string getField() const { return d_field; }
-  bool operator==(const RecordUpdate& t) const { return d_field == t.d_field; }
-  bool operator!=(const RecordUpdate& t) const { return d_field != t.d_field; }
-}; /* class RecordUpdate */
-
-struct RecordUpdateHashFunction
-{
-  inline size_t operator()(const RecordUpdate& t) const {
-    return std::hash<std::string>()(t.getField());
-  }
-}; /* struct RecordUpdateHashFunction */
-
-std::ostream& operator<<(std::ostream& out, const RecordUpdate& t);
-
-using Record = std::vector<std::pair<std::string, TypeNode>>;
-
-}  // namespace cvc5
-
-#endif /* CVC5__RECORD_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 483983e6e..bd435a392 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -249,7 +249,7 @@ bool TypeNode::isClosedEnumerable()
 bool TypeNode::isFirstClass() const
 {
   return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
-         && getKind() != kind::TESTER_TYPE && getKind() != kind::DT_UPDATE_TYPE
+         && getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE
          && (getKind() != kind::TYPE_CONSTANT
              || (getConst<TypeConstant>() != REGEXP_TYPE
                  && getConst<TypeConstant>() != SEXPR_TYPE));
@@ -633,10 +633,7 @@ bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; }
 
 bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; }
 
-bool TypeNode::isDatatypeUpdater() const
-{
-  return getKind() == kind::DT_UPDATE_TYPE;
-}
+bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; }
 
 bool TypeNode::isCodatatype() const
 {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index d73d64b43..0ab1d0217 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -652,7 +652,7 @@ public:
   bool isTester() const;
 
   /** Is this a datatype updater type */
-  bool isDatatypeUpdater() const;
+  bool isUpdater() const;
 
   /** Get the internal Datatype specification from a datatype type */
   const DType& getDType() const;