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, 11 insertions, 11 deletions

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index d0ebe5f19..b34ff59f5 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -241,7 +241,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
   Trace("srs-input") << "Construct unresolved types..." << std::endl;
   // each canonical subterm corresponds to a grammar type
-  std::set<Type> unres;
+  std::set<TypeNode> unres;
   std::vector<SygusDatatype> sdts;
   // make unresolved types for each canonical term
   std::map<Node, TypeNode> cterm_to_utype;
@@ -253,7 +253,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     std::string tname = ss.str();
     TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER);
     cterm_to_utype[ct] = tnu;
-    unres.insert(tnu.toType());
+    unres.insert(tnu);
     sdts.push_back(SygusDatatype(tname));
   }
   Trace("srs-input") << "...finished." << std::endl;
@@ -369,19 +369,19 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   Trace("srs-input") << "Make mutual datatype types for subterms..."
                      << std::endl;
   // extract the datatypes
-  std::vector<Datatype> datatypes;
+  std::vector<DType> datatypes;
   for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
   {
     datatypes.push_back(sdts[i].getDatatype());
   }
-  std::vector<DatatypeType> types = nm->toExprManager()->mkMutualDatatypeTypes(
-      datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+  std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(
+      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
   Trace("srs-input") << "...finished." << std::endl;
   Assert(types.size() == unres.size());
   std::map<Node, TypeNode> subtermTypes;
   for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
   {
-    subtermTypes[cterms[i]] = TypeNode::fromType(types[i]);
+    subtermTypes[cterms[i]] = types[i];
   }
 
   Trace("srs-input") << "Construct the top-level types..." << std::endl;
@@ -418,12 +418,12 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     }
     // set that this is a sygus datatype
     sdttl.initializeDatatype(t, sygusVarList, false, false);
-    Datatype dttl = sdttl.getDatatype();
-    DatatypeType tlt = nm->toExprManager()->mkDatatypeType(
-        dttl, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-    tlGrammarTypes[t] = TypeNode::fromType(tlt);
+    DType dttl = sdttl.getDatatype();
+    TypeNode tlt =
+        nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+    tlGrammarTypes[t] = tlt;
     Trace("srs-input") << "Grammar is: " << std::endl;
-    Trace("srs-input") << tlt.getDatatype() << std::endl;
+    Trace("srs-input") << tlt.getDType() << std::endl;
   }
   Trace("srs-input") << "...finished." << std::endl;