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, 4 insertions, 6 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 8120d1d88..89b516511 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -211,17 +211,15 @@ void CvcPrinter::toStream(
       break;
 
     case kind::DATATYPE_TYPE: {
-      const Datatype& dt =
-          NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
-              n.getConst<DatatypeIndexConstant>().getIndex());
-
+      const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
+          n.getConst<DatatypeIndexConstant>().getIndex());
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
           if (i > 0) {
             out << ", ";
           }
-          Type t = dt[0][i].getRangeType();
+          TypeNode t = dt[0][i].getRangeType();
           out << t;
         }
         out << ']';
@@ -233,7 +231,7 @@ void CvcPrinter::toStream(
           if (i > 0) {
             out << ", ";
           }
-          Type t = dt[0][i].getRangeType();
+          TypeNode t = dt[0][i].getRangeType();
           out << dt[0][i].getSelector() << ":" << t;
         }
         out << " #]";