Updates not related to creation for eliminating Expr-level datatype (#4838)

This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.

This required updating a unit test from Expr -> Node.

7 files changed, 18 insertions, 32 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 9ec3ac5fd..f8712e20e 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -304,6 +304,7 @@ void Datatype::setRecord() {
   PrettyCheckArgument(
       !isResolved(), this, "cannot set record to a finalized Datatype");
   d_isRecord = true;
+  d_internal->setRecord();
 }
 
 Cardinality Datatype::getCardinality(Type t) const
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 85e07866b..c64814ed6 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -66,7 +66,7 @@ void DTypeConstructor::addArgSelf(std::string selectorName)
 {
   Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
   std::shared_ptr<DTypeSelector> a =
-      std::make_shared<DTypeSelector>(selectorName, Node::null());
+      std::make_shared<DTypeSelector>(selectorName + '\0', Node::null());
   addArg(a);
 }
 
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 68d3904d3..1da60eb05 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -26,6 +26,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "expr/dtype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
@@ -212,11 +213,10 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
           Trace("parser-overloading")
               << "Parametric overloaded datatype selector " << name << " "
               << tna << std::endl;
-          DatatypeType tnd = static_cast<DatatypeType>(argTypes[i]);
-          const Datatype& dt = tnd.getDatatype();
+          const DType& dt = TypeNode::fromType(argTypes[i]).getDType();
           // tng is the "generalized" version of the instantiated parametric
           // type tna
-          Type tng = dt.getDatatypeType();
+          Type tng = dt.getTypeNode().toType();
           itc = tat->d_children.find(tng);
           if (itc != tat->d_children.end())
           {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 7696d9d7a..8232ef339 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -331,8 +331,7 @@ bool Type::isTuple() const {
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getKind() == kind::DATATYPE_TYPE
-         && DatatypeType(*this).getDatatype().isRecord();
+  return d_typeNode->isRecord();
 }
 
 /** Is this a symbolic expression type? */
@@ -586,7 +585,8 @@ std::vector<Type> ConstructorType::getArgTypes() const {
   return args;
 }
 
-const Datatype& DatatypeType::getDatatype() const {
+const Datatype& DatatypeType::getDatatype() const
+{
   NodeManagerScope nms(d_nodeManager);
   Assert(isDatatype());
   if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
@@ -602,10 +602,6 @@ bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }
 
-Expr DatatypeType::getConstructor(std::string name) const {
-  return getDatatype().getConstructor(name);
-}
-
 bool DatatypeType::isInstantiated() const {
   return d_typeNode->isInstantiatedDatatype();
 }
@@ -662,14 +658,6 @@ std::vector<Type> DatatypeType::getTupleTypes() const {
   return vect;
 }
 
-/** Get the description of the record type */
-const Record& DatatypeType::getRecord() const {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isRecord());
-  const Datatype& dt = getDatatype();
-  return *(dt.getRecord());
-}
-
 DatatypeType SelectorType::getDomain() const {
   return DatatypeType(makeType((*d_typeNode)[0]));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 61cb7eabf..0067ba7e7 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -621,13 +621,6 @@ class CVC4_PUBLIC DatatypeType : public Type {
 
   /** Is this datatype parametric? */
   bool isParametric() const;
-
-  /**
-   * Get the constructor operator associated to the given constructor
-   * name in this datatype.
-   */
-  Expr getConstructor(std::string name) const;
-
   /**
    * Has this datatype been fully instantiated ?
    *
@@ -654,9 +647,6 @@ class CVC4_PUBLIC DatatypeType : public Type {
   /** Get the constituent types of a tuple type */
   std::vector<Type> getTupleTypes() const;
 
-  /** Get the description of the record type */
-  const Record& getRecord() const;
-
 };/* class DatatypeType */
 
 /** Class encapsulating the constructor type. */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index c97a24d6d..7e38fac3d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -396,12 +396,16 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
-
-/** Is this a tuple type? */
-bool TypeNode::isTuple() const {
+bool TypeNode::isTuple() const
+{
   return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
 }
 
+bool TypeNode::isRecord() const
+{
+  return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord());
+}
+
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
   const DType& dt = getDType();
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0d0c17edf..b836e5069 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -599,6 +599,9 @@ public:
   /** Is this a tuple type? */
   bool isTuple() const;
 
+  /** Is this a record type? */
+  bool isRecord() const;
+
   /** Get the length of a tuple type */
   size_t getTupleLength() const;