Replace Expr-level datatype with Node-level DType (#4875)

This PR makes two simultaneous changes:

The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :

ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.

This PR will enable further removal of other datatype-specific things in the Expr layer.

1 files changed, 12 insertions, 8 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index bcddc23f5..0f2db7869 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -207,6 +207,8 @@ size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
 
 const DType& NodeManager::getDTypeForIndex(size_t index) const
 {
+  // if this assertion fails, it is likely due to not managing datatypes
+  // properly w.r.t. multiple NodeManagers.
   Assert(index < d_registeredDTypes.size());
   return *d_registeredDTypes[index];
 }
@@ -635,18 +637,19 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto
       for (unsigned i = 0; i < types.size(); ++ i) {
         sst << "_" << types[i];
       }
-      Datatype dt(nm->toExprManager(), sst.str());
+      DType dt(sst.str());
       dt.setTuple();
       std::stringstream ssc;
       ssc << sst.str() << "_ctor";
-      DatatypeConstructor c(ssc.str());
+      std::shared_ptr<DTypeConstructor> c =
+          std::make_shared<DTypeConstructor>(ssc.str());
       for (unsigned i = 0; i < types.size(); ++ i) {
         std::stringstream ss;
         ss << sst.str() << "_stor_" << i;
-        c.addArg(ss.str().c_str(), types[i].toType());
+        c->addArg(ss.str().c_str(), types[i]);
       }
       dt.addConstructor(c);
-      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      d_data = nm->mkDatatypeType(dt);
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
     return d_data;
@@ -664,16 +667,17 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
         sst << "_" << (*i).first << "_" << (*i).second;
       }
-      Datatype dt(nm->toExprManager(), sst.str());
+      DType dt(sst.str());
       dt.setRecord();
       std::stringstream ssc;
       ssc << sst.str() << "_ctor";
-      DatatypeConstructor c(ssc.str());
+      std::shared_ptr<DTypeConstructor> c =
+          std::make_shared<DTypeConstructor>(ssc.str());
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-        c.addArg((*i).first, (*i).second);
+        c->addArg((*i).first, TypeNode::fromType((*i).second));
       }
       dt.addConstructor(c);
-      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      d_data = nm->mkDatatypeType(dt);
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
     return d_data;