Eliminate Expr-level calls in TypeNode (#3562)

2 files changed, 18 insertions, 16 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 4727ab0b0..8c005bd3c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -49,7 +49,7 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
     if (!gv.isNull())
     {
       TypeNode tn = gv.getType();
-      if (tn.isDatatype() && tn.getDatatype().isSygus())
+      if (tn.isDatatype() && tn.getDType().isSygus())
       {
         return true;
       }
@@ -137,9 +137,9 @@ Node CegGrammarConstructor::process(Node q,
     std::stringstream ss;
     ss << sf;
     Node sfvl;
-    if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus())
+    if (preGrammarType.isDatatype() && preGrammarType.getDType().isSygus())
     {
-      sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList());
+      sfvl = preGrammarType.getDType().getSygusVarList();
       tn = preGrammarType;
     }else{
       sfvl = getSygusVarList(sf);
@@ -260,7 +260,7 @@ Node CegGrammarConstructor::process(Node q,
     }
     tds->registerSygusType(tn);
     Assert(tn.isDatatype());
-    const Datatype& dt = tn.getDatatype();
+    const DType& dt = tn.getDType();
     Assert(dt.isSygus());
     if( !dt.getSygusAllowAll() ){
       d_is_syntax_restricted = true;
@@ -427,13 +427,13 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
       Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
       types.push_back( range );
       if( range.isDatatype() ){
-        const Datatype& dt = range.getDatatype();
+        const DType& dt = range.getDType();
         for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
         {
           for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
                ++j)
           {
-            TypeNode tn = TypeNode::fromType(dt[i][j].getRangeType());
+            TypeNode tn = dt[i][j].getRangeType();
             collectSygusGrammarTypesFor(tn, types);
           }
         }
@@ -817,11 +817,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     else if (types[i].isDatatype())
     {
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
-      const Datatype& dt = types[i].getDatatype();
+      const DType& dt = types[i].getDType();
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
         Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
-        Node cop = Node::fromExpr(dt[k].getConstructor());
+        Node cop = dt[k].getConstructor();
         if (dt[k].getNumArgs() == 0)
         {
           // Nullary constructors are interpreted as terms, not operators.
@@ -834,7 +834,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         {
           Trace("sygus-grammar-def")
               << "...for " << dt[k][j].getName() << std::endl;
-          TypeNode crange = TypeNode::fromType(dt[k][j].getRangeType());
+          TypeNode crange = dt[k][j].getRangeType();
           Assert(type_to_unres.find(crange) != type_to_unres.end());
           cargsCons.push_back(type_to_unres[crange]);
           // add to the selector type the selector operator
@@ -842,12 +842,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           Assert(std::find(types.begin(), types.end(), crange) != types.end());
           unsigned i_selType = std::distance(
               types.begin(), std::find(types.begin(), types.end(), crange));
-          TypeNode arg_type = TypeNode::fromType(dt[k][j].getType());
+          TypeNode arg_type = dt[k][j].getType();
           arg_type = arg_type.getSelectorDomainType();
           Assert(type_to_unres.find(arg_type) != type_to_unres.end());
           std::vector<TypeNode> cargsSel;
           cargsSel.push_back(type_to_unres[arg_type]);
-          Node sel = Node::fromExpr(dt[k][j].getSelector());
+          Node sel = dt[k][j].getSelector();
           sdts[i_selType].addConstructor(sel, dt[k][j].getName(), cargsSel);
         }
         sdts[i].addConstructor(cop, dt[k].getName(), cargsCons);
@@ -1175,14 +1175,16 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       //add for testers
       Trace("sygus-grammar-def") << "...add for testers" << std::endl;
-      const Datatype& dt = types[i].getDatatype();
+      const DType& dt = types[i].getDType();
       std::vector<TypeNode> cargsTester;
       cargsTester.push_back(unres_types[iuse]);
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
-        Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
-        sdtBool.addConstructor(
-            dt[k].getTester(), dt[k].getTesterName(), cargsTester);
+        Trace("sygus-grammar-def")
+            << "...for " << dt[k].getTester() << std::endl;
+        std::stringstream sst;
+        sst << dt[k].getTester();
+        sdtBool.addConstructor(dt[k].getTester(), sst.str(), cargsTester);
       }
     }
   }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 019abc28a..c7c1d820f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -599,7 +599,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
     return tn;
   }
   /* Collect all operators for normalization */
-  const Datatype& dt = tn.getDatatype();
+  const Datatype& dt = DatatypeType(tn.toType()).getDatatype();
   if (!dt.isSygus())
   {
     // datatype but not sygus datatype case