Use the node-level datatypes API (#3556)

28 files changed, 271 insertions, 309 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 6c4f2c620..9fd682aaf 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -57,16 +59,14 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
           << "...try based on constructor term " << n << std::endl;
       std::vector<Node> children;
       children.push_back(n.getOperator());
-      const Datatype& dt =
-          static_cast<DatatypeType>(d_type.toType()).getDatatype();
-      unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+      const DType& dt = d_type.getDType();
+      unsigned cindex = datatypes::utils::indexOf(n.getOperator());
       // now must solve for selectors applied to pv
       for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
       {
-        Node c = nm->mkNode(
-            APPLY_SELECTOR_TOTAL,
-            Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)),
-            pv);
+        Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
+                            dt[cindex].getSelectorInternal(d_type, j),
+                            pv);
         ci->pushStackVariable(c);
         children.push_back(c);
       }
@@ -146,15 +146,13 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
     else
     {
       NodeManager* nm = NodeManager::currentNM();
-      unsigned cindex = Datatype::indexOf(a.getOperator().toExpr());
+      unsigned cindex = DType::indexOf(a.getOperator().toExpr());
       TypeNode tn = a.getType();
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
       {
         Node nn = nm->mkNode(
-            APPLY_SELECTOR_TOTAL,
-            Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
-            sb);
+            APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
         Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
         if (!s.isNull())
         {
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index bed382e28..1d4a23af1 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -341,13 +341,12 @@ CegHandledStatus CegInstantiator::isCbqiSort(
     // we initialize to handled, we remain handled as long as all subfields
     // of this datatype are not unhandled.
     ret = CEG_HANDLED;
-    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    const DType& dt = tn.getDType();
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
       {
-        TypeNode crange = TypeNode::fromType(
-            static_cast<SelectorType>(dt[i][j].getType()).getRangeType());
+        TypeNode crange = dt[i].getArgType(j);
         CegHandledStatus cret = isCbqiSort(crange, visited, qe);
         if (cret == CEG_UNHANDLED)
         {
@@ -520,15 +519,12 @@ void CegInstantiator::registerTheoryIds(TypeNode tn,
     registerTheoryId(tid);
     if (tn.isDatatype())
     {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      const DType& dt = tn.getDType();
       for (unsigned i = 0; i < dt.getNumConstructors(); i++)
       {
         for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
         {
-          registerTheoryIds(
-              TypeNode::fromType(
-                  ((SelectorType)dt[i][j].getType()).getRangeType()),
-              visited);
+          registerTheoryIds(dt[i].getArgType(j), visited);
         }
       }
     }
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 3a075ec8a..8e09ef6a2 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
+#include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
@@ -208,7 +209,7 @@ CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(
     : CandidateGeneratorQE(qe, mpat)
 {
   Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
-  d_mpat_type = static_cast<DatatypeType>(mpat.getType().toType());
+  d_mpat_type = mpat.getType();
 }
 
 void CandidateGeneratorConsExpand::reset(Node eqc)
@@ -222,7 +223,7 @@ void CandidateGeneratorConsExpand::reset(Node eqc)
   {
     d_eqc = eqc;
     d_mode = cand_term_ident;
-    Assert(d_eqc.getType().toType() == d_mpat_type);
+    Assert(d_eqc.getType() == d_mpat_type);
   }
 }
 
@@ -237,15 +238,13 @@ Node CandidateGeneratorConsExpand::getNextCandidate()
   // expand it
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> children;
-  const Datatype& dt = d_mpat_type.getDatatype();
+  const DType& dt = d_mpat_type.getDType();
   Assert(dt.getNumConstructors() == 1);
   children.push_back(d_op);
   for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
   {
-    Node sel =
-        nm->mkNode(APPLY_SELECTOR_TOTAL,
-                   Node::fromExpr(dt[0].getSelectorInternal(d_mpat_type, i)),
-                   curr);
+    Node sel = nm->mkNode(
+        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
     children.push_back(sel);
   }
   return nm->mkNode(APPLY_CONSTRUCTOR, children);
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 8cff12477..51c5ffa0b 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -203,7 +203,7 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE
 
  protected:
   /** the (datatype) type of the input match pattern */
-  DatatypeType d_mpat_type;
+  TypeNode d_mpat_type;
   /** we don't care about the operator of n */
   bool isLegalOpCandidate(Node n) override;
 };
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index e639dc446..6fdd6d67a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -17,6 +17,7 @@
 #include "expr/datatype.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/instantiate.h"
@@ -203,7 +204,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       {
         // 1-constructors have a trivial way of generating candidates in a
         // given equivalence class
-        const Datatype& dt = d_match_pattern.getType().getDatatype();
+        const DType& dt = d_match_pattern.getType().getDType();
         if (dt.getNumConstructors() == 1)
         {
           d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
@@ -226,11 +227,11 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }
     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
-        Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
-        size_t selectorIndex = Datatype::cindexOf(selectorExpr);
-        const Datatype& dt = Datatype::datatypeOf(selectorExpr);
-        const DatatypeConstructor& c = dt[selectorIndex];
-        Node cOp = Node::fromExpr(c.getConstructor());
+        Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+        size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
+        const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
+        const DTypeConstructor& c = dt[selectorIndex];
+        Node cOp = c.getConstructor();
         Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
         d_cg = new inst::CandidateGeneratorQE( qe, cOp );
       }else{
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index c6800b092..cfff64f15 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -737,14 +738,17 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
         return Node::null();
       }
     }
-    const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() );
-    unsigned index = Datatype::indexOf( t.getOperator().toExpr() );
+    NodeManager* nm = NodeManager::currentNM();
+    const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
+    unsigned index = datatypes::utils::indexOf(t.getOperator());
     for( unsigned i=0; i<t.getNumChildren(); i++ ){
       Node u;
       if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
         u = matchBoundVar( v, t[i], e[i] );
       }else{
-        Node se = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index].getSelectorInternal( e.getType().toType(), i ) ), e );
+        Node se = nm->mkNode(APPLY_SELECTOR_TOTAL,
+                             dt[index].getSelectorInternal(e.getType(), i),
+                             e);
         u = matchBoundVar( v, t[i], se );
       }
       if( !u.isNull() ){
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index e425cd345..32bd2b0e8 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -47,16 +47,19 @@ void QuantDSplit::checkOwnership(Node q)
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
     if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      if( dt.isRecursiveSingleton( tn.toType() ) ){
+      const DType& dt = tn.getDType();
+      if (dt.isRecursiveSingleton(tn))
+      {
         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
-      }else{
+      }
+      else
+      {
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
           // split if it is a finite datatype
-          doSplit = dt.isInterpretedFinite(tn.toType());
+          doSplit = dt.isInterpretedFinite(tn);
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
-            if (dt.isInterpretedFinite(tn.toType()))
+            if (dt.isInterpretedFinite(tn))
             {
               // split if goes from being unhandled -> handled by finite
               // instantiation. An example is datatypes with uninterpreted sort
@@ -144,20 +147,20 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
       TypeNode tn = svar.getType();
       Assert(tn.isDatatype());
       std::vector<Node> cons;
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
       {
         std::vector<Node> vars;
         for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
         {
-          TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType());
+          TypeNode tns = dt[j][k].getRangeType();
           Node v = nm->mkBoundVar(tns);
           vars.push_back(v);
         }
         std::vector<Node> bvs_cmb;
         bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
         bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
-        vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor()));
+        vars.insert(vars.begin(), dt[j].getConstructor());
         Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
         TNode ct = c;
         Node body = q[1].substitute(svar, ct);
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0039ec845..8d65523e1 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -14,9 +14,11 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -308,8 +310,8 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
       Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
       computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
     }else{
-      Expr testerExpr = n[0].getOperator().toExpr();
-      int index = Datatype::indexOf( testerExpr );
+      Node tester = n[0].getOperator();
+      int index = datatypes::utils::indexOf(tester);
       std::map< int, Node >::iterator itn = ncons[x].find( index );
       if( itn!=ncons[x].end() ){
         Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
@@ -328,6 +330,7 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
       }
     }
   }else{
+    NodeManager* nm = NodeManager::currentNM();
     Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
     std::vector< Node > children;
     children.push_back( n );
@@ -343,7 +346,7 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
       //only if we haven't settled on a positive tester
       if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
         //check if we have exhausted all options but one
-        const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype();
+        const DType& dt = x.getType().getDType();
         std::vector< Node > nchildren;
         int pos_cons = -1;
         for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
@@ -355,9 +358,8 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
           }
         }
         if( pos_cons>=0 ){
-          const DatatypeConstructor& c = dt[pos_cons];
-          Expr tester = c.getTester();
-          children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() );
+          Node tester = dt[pos_cons].getTester();
+          children.push_back(nm->mkNode(APPLY_TESTER, tester, x).negate());
         }else{
           children.insert( children.end(), nchildren.begin(), nchildren.end() );
         }
@@ -454,20 +456,21 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
   }
   if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
     if( n.getKind()==APPLY_TESTER ){
-      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-      unsigned index = Datatype::indexOf(n.getOperator().toExpr());
+      NodeManager* nm = NodeManager::currentNM();
+      const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
+      unsigned index = datatypes::utils::indexOf(n.getOperator());
       Assert(dt.getNumConstructors() > 1);
       if( pol ){
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           if( i!=index ){
-            Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
+            Node t = nm->mkNode(APPLY_TESTER, dt[i].getTester(), n[0]);
             addEntailedCond( t, false, currCond, new_cond, conflict );
           }
         }
       }else{
         if( dt.getNumConstructors()==2 ){
           int oindex = 1-index;
-          Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
+          Node t = nm->mkNode(APPLY_TESTER, dt[oindex].getTester(), n[0]);
           addEntailedCond( t, true, currCond, new_cond, conflict );
         }
       }
@@ -1011,16 +1014,16 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
     if (ita != args.end())
     {
       vars.push_back(lit[0]);
-      Expr testerExpr = lit.getOperator().toExpr();
-      int index = Datatype::indexOf(testerExpr);
-      const Datatype& dt = Datatype::datatypeOf(testerExpr);
-      const DatatypeConstructor& c = dt[index];
+      Node tester = lit.getOperator();
+      int index = datatypes::utils::indexOf(tester);
+      const DType& dt = datatypes::utils::datatypeOf(tester);
+      const DTypeConstructor& c = dt[index];
       std::vector<Node> newChildren;
-      newChildren.push_back(Node::fromExpr(c.getConstructor()));
+      newChildren.push_back(c.getConstructor());
       std::vector<Node> newVars;
       for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
       {
-        TypeNode tn = TypeNode::fromType(c[j].getRangeType());
+        TypeNode tn = c[j].getRangeType();
         Node v = nm->mkBoundVar(tn);
         newChildren.push_back(v);
         newVars.push_back(v);
@@ -1081,8 +1084,8 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
   {
     Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
                          << std::endl;
-    Expr testerExpr = lit.getOperator().toExpr();
-    unsigned index = Datatype::indexOf(testerExpr);
+    Node tester = lit.getOperator();
+    unsigned index = datatypes::utils::indexOf(tester);
     Node s = datatypeExpand(index, lit[0], args);
     if (!s.isNull())
     {
@@ -1179,16 +1182,15 @@ Node QuantifiersRewriter::datatypeExpand(unsigned index,
   {
     return Node::null();
   }
-  const Datatype& dt =
-      static_cast<DatatypeType>(v.getType().toType()).getDatatype();
+  const DType& dt = v.getType().getDType();
   Assert(index < dt.getNumConstructors());
-  const DatatypeConstructor& c = dt[index];
+  const DTypeConstructor& c = dt[index];
   std::vector<Node> newChildren;
-  newChildren.push_back(Node::fromExpr(c.getConstructor()));
+  newChildren.push_back(c.getConstructor());
   std::vector<Node> newVars;
   for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
   {
-    TypeNode tn = TypeNode::fromType(c.getArgType(j));
+    TypeNode tn = c.getArgType(j);
     Node vn = NodeManager::currentNM()->mkBoundVar(tn);
     newChildren.push_back(vn);
     newVars.push_back(vn);
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 1d2b869c4..a83303454 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -73,8 +73,8 @@ Node Skolemize::getSkolemConstant(Node q, unsigned i)
   return Node::null();
 }
 
-void Skolemize::getSelfSel(const Datatype& dt,
-                           const DatatypeConstructor& dc,
+void Skolemize::getSelfSel(const DType& dt,
+                           const DTypeConstructor& dc,
                            Node n,
                            TypeNode ntn,
                            std::vector<Node>& selfSel)
@@ -82,14 +82,14 @@ void Skolemize::getSelfSel(const Datatype& dt,
   TypeNode tspec;
   if (dt.isParametric())
   {
-    tspec = TypeNode::fromType(
-        dc.getSpecializedConstructorType(n.getType().toType()));
+    tspec = dc.getSpecializedConstructorType(n.getType());
     Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
                           << std::endl;
     Assert(tspec.getNumChildren() == dc.getNumArgs());
   }
   Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
                         << dt.getName() << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
   for (unsigned j = 0; j < dc.getNumArgs(); j++)
   {
     std::vector<Node> ssc;
@@ -104,32 +104,17 @@ void Skolemize::getSelfSel(const Datatype& dt,
     }
     else
     {
-      TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
+      TypeNode tn = dc[j].getRangeType();
       Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
       if (tn == ntn)
       {
         ssc.push_back(n);
       }
     }
-    /* TODO: more than weak structural induction
-    else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
-    )==visited.end() ){
-      visited.push_back( tn );
-      const Datatype& dt =
-    ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
-      std::vector< Node > disj;
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        getSelfSel( dt[i], n, ntn, ssc );
-      }
-      visited.pop_back();
-    }
-    */
     for (unsigned k = 0; k < ssc.size(); k++)
     {
-      Node ss = NodeManager::currentNM()->mkNode(
-          APPLY_SELECTOR_TOTAL,
-          dc.getSelectorInternal(n.getType().toType(), j),
-          n);
+      Node ss = nm->mkNode(
+          APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
       if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
       {
         selfSel.push_back(ss);
@@ -146,6 +131,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
                                  Node& sub,
                                  std::vector<unsigned>& sub_vars)
 {
+  NodeManager* nm = NodeManager::currentNM();
   Assert(sk.empty() || sk.size() == f[0].getNumChildren());
   // calculate the variables and substitution
   std::vector<TNode> ind_vars;
@@ -220,17 +206,14 @@ Node Skolemize::mkSkolemizedBody(Node f,
     // the following constructs ~( R( x, k ) => ~P( x ) )
     if (options::dtStcInduction() && tn.isDatatype())
     {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      const DType& dt = tn.getDType();
       std::vector<Node> disj;
       for (unsigned i = 0; i < dt.getNumConstructors(); i++)
       {
         std::vector<Node> selfSel;
         getSelfSel(dt, dt[i], k, tn, selfSel);
         std::vector<Node> conj;
-        conj.push_back(
-            NodeManager::currentNM()
-                ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
-                .negate());
+        conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate());
         for (unsigned j = 0; j < selfSel.size(); j++)
         {
           conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
@@ -346,7 +329,7 @@ bool Skolemize::isInductionTerm(Node n)
   TypeNode tn = n.getType();
   if (options::dtStcInduction() && tn.isDatatype())
   {
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    const DType& dt = tn.getDType();
     return !dt.isCodatatype();
   }
   if (options::intWfInduction() && n.getType().isInteger())
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index f07bbdfd3..86af1ee1b 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -123,8 +123,8 @@ class Skolemize
    * applied to term n, whose return type in ntn, and stores
    * them in the vector selfSel.
    */
-  static void getSelfSel(const Datatype& dt,
-                         const DatatypeConstructor& dc,
+  static void getSelfSel(const DType& dt,
+                         const DTypeConstructor& dc,
                          Node n,
                          TypeNode ntn,
                          std::vector<Node>& selfSel);
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 61d891f75..69e0ef70a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -467,8 +467,8 @@ Node CegSingleInv::getSolution(unsigned sol_index,
                                bool rconsSygus)
 {
   Assert(d_sol != NULL);
-  const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
-  Node varList = Node::fromExpr( dt.getSygusVarList() );
+  const DType& dt = stn.getDType();
+  Node varList = dt.getSygusVarList();
   Node prog = d_quant[0][sol_index];
   std::vector< Node > vars;
   Node s;
@@ -478,8 +478,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
       || d_inst.empty())
   {
     Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
-    s = d_qe->getTermEnumeration()->getEnumerateTerm(
-        TypeNode::fromType(dt.getSygusType()), 0);
+    s = d_qe->getTermEnumeration()->getEnumerateTerm(dt.getSygusType(), 0);
   }
   else
   {
@@ -548,7 +547,7 @@ Node CegSingleInv::reconstructToSyntax(Node s,
                                        bool rconsSygus)
 {
   d_solution = s;
-  const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+  const DType& dt = stn.getDType();
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
@@ -621,7 +620,7 @@ Node CegSingleInv::reconstructToSyntax(Node s,
   }
   //make into lambda
   if( !dt.getSygusVarList().isNull() ){
-    Node varList = Node::fromExpr( dt.getSygusVarList() );
+    Node varList = dt.getSygusVarList();
     return NodeManager::currentNM()->mkNode( LAMBDA, varList, sol );
   }else{
     return sol;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 811210628..113da2acb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
 #include "expr/datatype.h"
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
@@ -27,7 +28,6 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -132,7 +132,7 @@ Node CegSingleInvSol::reconstructSolution(Node sol,
     {
       TypeNode tn = it->first;
       Assert(tn.isDatatype());
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName()
                          << " : " << std::endl;
       for (std::map<Node, int>::iterator it2 = it->second.begin();
@@ -225,7 +225,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     d_rcons_to_status[stn][t] = -1;
     TypeNode tn = t.getType();
     Assert(stn.isDatatype());
-    const Datatype& dt = stn.getDatatype();
+    const DType& dt = stn.getDType();
     TermDbSygus* tds = d_qe->getTermDatabaseSygus();
     SygusTypeInfo& sti = tds->getTypeInfo(stn);
     Assert(dt.isSygus());
@@ -240,7 +240,8 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     carg = sti.getOpConsNum(min_t);
     if( carg!=-1 ){
       Trace("csi-rcons-debug") << "  Type has operator." << std::endl;
-      d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
+      d_reconstruct[id] = NodeManager::currentNM()->mkNode(
+          APPLY_CONSTRUCTOR, dt[carg].getConstructor());
       status = 0;
     }else{
       //check if kind is in syntax sort
@@ -266,7 +267,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
         if( tchildren.size()==dt[karg].getNumArgs() ){
           Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
           status = 0;
-          Node cons = Node::fromExpr( dt[karg].getConstructor() );
+          Node cons = dt[karg].getConstructor();
           if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
             Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
             d_reconstruct_op[id].erase( cons );
@@ -295,10 +296,10 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
             //try to directly reconstruct from single argument
             std::vector< Node > tchildren;
             tchildren.push_back( min_t );
-            TypeNode stnc = TypeNode::fromType( ((SelectorType)dt[ii][0].getType()).getRangeType() );
+            TypeNode stnc = dt[ii][0].getRangeType();
             Trace("csi-rcons-debug") << "...try identity function " << dt[ii].getSygusOp() << ", child type is " << stnc << std::endl;
             status = 0;
-            Node cons = Node::fromExpr( dt[ii].getConstructor() );
+            Node cons = dt[ii].getConstructor();
             if( !collectReconstructNodes( id, tchildren, dt[ii], d_reconstruct_op[id][cons], status ) ){
               d_reconstruct_op[id].erase( cons );
               status = 1;
@@ -320,7 +321,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
               {
                 success = true;
                 status = 0;
-                Node cons = Node::fromExpr( dt[index_found].getConstructor() );
+                Node cons = dt[index_found].getConstructor();
                 Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
                 for( unsigned i=0; i<args.size(); i++ ){
                   Trace("csi-rcons-debug") << "  " << args[i] << std::endl;
@@ -429,7 +430,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
 
 bool CegSingleInvSol::collectReconstructNodes(int pid,
                                               std::vector<Node>& ts,
-                                              const DatatypeConstructor& dtc,
+                                              const DTypeConstructor& dtc,
                                               std::vector<int>& ids,
                                               int& status)
 {
@@ -510,7 +511,7 @@ int CegSingleInvSol::allocate(Node n, TypeNode stn)
   if( it==d_rcons_to_id[stn].end() ){
     int ret = d_id_count;
     if( Trace.isOn("csi-rcons-debug") ){
-      const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+      const DType& dt = stn.getDType();
       Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " <<  dt.getName() << std::endl;
     }
     d_id_node[d_id_count] = n;
@@ -696,7 +697,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
     d_builtin_const_to_sygus[tn][c] = c;
     return c;
   }
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
                            << dt.getName() << std::endl;
   if (!dt.isSygus())
@@ -716,8 +717,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
     int carg = ti.getOpConsNum(c);
     if (carg != -1)
     {
-      sc = nm->mkNode(APPLY_CONSTRUCTOR,
-                      Node::fromExpr(dt[carg].getConstructor()));
+      sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[carg].getConstructor());
     }
     else
     {
@@ -734,8 +734,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
         Node n = builtinToSygusConst(c, tnc, rcons_depth);
         if (!n.isNull())
         {
-          sc = nm->mkNode(
-              APPLY_CONSTRUCTOR, Node::fromExpr(dt[ii].getConstructor()), n);
+          sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[ii].getConstructor(), n);
           break;
         }
       }
@@ -744,16 +743,14 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
         if (rcons_depth < 1000)
         {
           // accelerated, recursive reconstruction of constants
-          Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
+          Kind pk = getPlusKind(dt.getSygusType());
           if (pk != UNDEFINED_KIND)
           {
             int arg = ti.getKindConsNum(pk);
             if (arg != -1)
             {
-              Kind ck =
-                  getComparisonKind(TypeNode::fromType(dt.getSygusType()));
-              Kind pkm =
-                  getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
+              Kind ck = getComparisonKind(dt.getSygusType());
+              Kind pkm = getPlusKind(dt.getSygusType(), true);
               // get types
               Assert(dt[arg].getNumArgs() == 2);
               TypeNode tn1 = tds->getArgType(dt[arg], 0);
@@ -780,7 +777,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
                       Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth);
                       Assert(!sc1.isNull());
                       sc = nm->mkNode(APPLY_CONSTRUCTOR,
-                                      Node::fromExpr(dt[arg].getConstructor()),
+                                      dt[arg].getConstructor(),
                                       sc1,
                                       sc2);
                       break;
@@ -819,9 +816,9 @@ void CegSingleInvSol::registerType(TypeNode tn)
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   // ensure it is registered
   tds->registerSygusType(tn);
-  const Datatype& dt = tn.getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
-  TypeNode btn = TypeNode::fromType(dt.getSygusType());
+  TypeNode btn = dt.getSygusType();
   // for constant reconstruction
   Kind ck = getComparisonKind(btn);
   Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
@@ -829,7 +826,7 @@ void CegSingleInvSol::registerType(TypeNode tn)
   // iterate over constructors
   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
   {
-    Node n = Node::fromExpr(dt[i].getSygusOp());
+    Node n = dt[i].getSygusOp();
     if (n.getKind() != kind::BUILTIN && n.isConst())
     {
       d_const_list[tn].push_back(n);
@@ -927,7 +924,7 @@ bool CegSingleInvSol::getMatch(Node t,
                                int index_start)
 {
   Assert(st.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(st.toType()).getDatatype();
+  const DType& dt = st.getDType();
   Assert(dt.isSygus());
   std::map<Kind, std::vector<Node> > kgens;
   std::vector<Node> gens;
@@ -975,7 +972,7 @@ bool CegSingleInvSol::getMatch(Node t,
   return false;
 }
 
-Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c)
+Node CegSingleInvSol::getGenericBase(TypeNode tn, const DType& dt, int c)
 {
   std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
   if (it != d_generic_base[tn].end())
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index c319080af..ed84c81b2 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -106,7 +106,11 @@ private:
   int allocate( Node n, TypeNode stn );
   // term t with sygus type st, returns inducted templated form of t
   int collectReconstructNodes( Node t, TypeNode stn, int& status );
-  bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
+  bool collectReconstructNodes(int pid,
+                               std::vector<Node>& ts,
+                               const DTypeConstructor& dtc,
+                               std::vector<int>& ids,
+                               int& status);
   bool getPathToRoot( int id );
   void setReconstructed( int id, Node n );
   //get equivalent terms to n with top symbol k
@@ -140,7 +144,7 @@ private:
    * This returns the builtin term that is the analog of an application of the
    * c^th constructor of dt to fresh variables.
    */
-  Node getGenericBase(TypeNode tn, const Datatype& dt, int c);
+  Node getGenericBase(TypeNode tn, const DType& dt, int c);
   /** cache for the above function */
   std::map<TypeNode, std::map<int, Node> > d_generic_base;
   /** get match
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 0b9dd3b48..573e11426 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -197,7 +197,7 @@ bool CegisCoreConnective::processInitialize(Node conj,
   // candidate has the production rule gt -> AND( gt, gt ). Similarly for
   // precondition and OR.
   Assert(gt.isDatatype());
-  const Datatype& gdt = gt.getDatatype();
+  const DType& gdt = gt.getDType();
   SygusTypeInfo& gti = d_tds->getTypeInfo(gt);
   for (unsigned r = 0; r < 2; r++)
   {
@@ -211,12 +211,12 @@ bool CegisCoreConnective::processInitialize(Node conj,
     Kind rk = r == 0 ? OR : AND;
     int i = gti.getKindConsNum(rk);
     if (i != -1 && gdt[i].getNumArgs() == 2
-        && TypeNode::fromType(gdt[i].getArgType(0)) == gt
-        && TypeNode::fromType(gdt[i].getArgType(1)) == gt)
+        && gdt[i].getArgType(0) == gt
+        && gdt[i].getArgType(1) == gt)
     {
       Trace("sygus-ccore-init") << "  will do " << (r == 0 ? "pre" : "post")
                                 << "condition." << std::endl;
-      Node cons = Node::fromExpr(gdt[i].getConstructor());
+      Node cons = gdt[i].getConstructor();
       c.initialize(f, cons);
       // Register the symmetry breaking lemma: do not do top-level solutions
       // with this constructor (e.g. we want to enumerate literals, not
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 0cdfe4307..dd9af2c43 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -45,7 +45,7 @@ void EnumStreamPermutation::reset(Node value)
   d_value = value;
   // get variables in value's type
   TypeNode tn = value.getType();
-  Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+  Node var_list = tn.getDType().getSygusVarList();
   NodeManager* nm = NodeManager::currentNM();
   // get subtypes in value's type
   SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
@@ -58,10 +58,10 @@ void EnumStreamPermutation::reset(Node value)
     // collect constructors for variable in all subtypes
     for (const TypeNode& stn : sf_types)
     {
-      const Datatype& dt = stn.getDatatype();
+      const DType& dt = stn.getDType();
       for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
       {
-        if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+        if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
         {
           Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
           d_var_tn_cons[v][stn] = cons;
@@ -337,7 +337,7 @@ void EnumStreamSubstitution::initialize(TypeNode tn)
 {
   d_tn = tn;
   // get variables in value's type
-  Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+  Node var_list = tn.getDType().getSygusVarList();
   // get subtypes in value's type
   NodeManager* nm = NodeManager::currentNM();
   SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
@@ -349,10 +349,10 @@ void EnumStreamSubstitution::initialize(TypeNode tn)
     // collect constructors for variable in all subtypes
     for (const TypeNode& stn : sf_types)
     {
-      const Datatype& dt = stn.getDatatype();
+      const DType& dt = stn.getDType();
       for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
       {
-        if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+        if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
         {
           d_var_tn_cons[v][stn] =
               nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 0396aba86..a58c5d841 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -16,9 +16,11 @@
 #include "theory/quantifiers/sygus/sygus_abduct.h"
 
 #include "expr/datatype.h"
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "printer/sygus_print_callback.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -85,13 +87,13 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   // if provided, we will associate it with the function-to-synthesize
   if (!abdGType.isNull())
   {
-    Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus());
+    Assert(abdGType.isDatatype() && abdGType.getDType().isSygus());
     // must convert all constructors to version with bound variables in "vars"
     std::vector<SygusDatatype> sdts;
     std::set<Type> unres;
 
     Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
-    Trace("sygus-abduct-debug") << abdGType.getDatatype() << std::endl;
+    Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl;
 
     // datatype types we need to process
     std::vector<TypeNode> dtToProcess;
@@ -99,7 +101,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
     std::map<TypeNode, TypeNode> dtProcessed;
     dtToProcess.push_back(abdGType);
     std::stringstream ssutn0;
-    ssutn0 << abdGType.getDatatype().getName() << "_s";
+    ssutn0 << abdGType.getDType().getName() << "_s";
     TypeNode abdTNew =
         nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
     unres.insert(abdTNew.toType());
@@ -126,8 +128,8 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
       std::vector<TypeNode> dtNextToProcess;
       for (const TypeNode& curr : dtToProcess)
       {
-        Assert(curr.isDatatype() && curr.getDatatype().isSygus());
-        const Datatype& dtc = curr.getDatatype();
+        Assert(curr.isDatatype() && curr.getDType().isSygus());
+        const DType& dtc = curr.getDType();
         std::stringstream ssdtn;
         ssdtn << dtc.getName() << "_s";
         sdts.push_back(SygusDatatype(ssdtn.str()));
@@ -136,7 +138,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
             << std::endl;
         for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
         {
-          Node op = Node::fromExpr(dtc[j].getSygusOp());
+          Node op = dtc[j].getSygusOp();
           // apply the substitution to the argument
           Node ops = op.substitute(
               syms.begin(), syms.end(), varlist.begin(), varlist.end());
@@ -145,14 +147,14 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
           std::vector<TypeNode> cargs;
           for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
           {
-            TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k));
+            TypeNode argt = dtc[j].getArgType(k);
             std::map<TypeNode, TypeNode>::iterator itdp =
                 dtProcessed.find(argt);
             TypeNode argtNew;
             if (itdp == dtProcessed.end())
             {
               std::stringstream ssutn;
-              ssutn << argt.getDatatype().getName() << "_s";
+              ssutn << argt.getDType().getName() << "_s";
               argtNew =
                   nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
               Trace("sygus-abduct-debug")
@@ -196,7 +198,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
         }
         Trace("sygus-abduct-debug")
             << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
-        TypeNode stn = TypeNode::fromType(dtc.getSygusType());
+        TypeNode stn = dtc.getSygusType();
         sdts.back().initializeDatatype(
             stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
       }
@@ -222,7 +224,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
       Trace("sygus-abduct-debug") << "Made datatype types:" << std::endl;
       for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
       {
-        const Datatype& dtj = datatypeTypes[j].getDatatype();
+        const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType();
         Trace("sygus-abduct-debug") << "#" << j << ": " << dtj << std::endl;
         for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
         {
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index e4c23977e..f6ec58f56 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -35,7 +35,7 @@ void SygusEnumerator::initialize(Node e)
   d_enum = e;
   d_etype = d_enum.getType();
   Assert(d_etype.isDatatype());
-  Assert(d_etype.getDatatype().isSygus());
+  Assert(d_etype.getDType().isSygus());
   d_tlEnum = getMasterEnumForType(d_etype);
   d_abortSize = options::sygusAbortSize();
 
@@ -50,7 +50,7 @@ void SygusEnumerator::initialize(Node e)
   TNode agt = ag;
   TNode truent = truen;
   Assert(d_tcache.find(d_etype) != d_tcache.end());
-  const Datatype& dt = d_etype.getDatatype();
+  const DType& dt = d_etype.getDType();
   for (const Node& lem : sbl)
   {
     if (!d_tds->isSymBreakLemmaTemplate(lem))
@@ -86,7 +86,7 @@ void SygusEnumerator::initialize(Node e)
           {
             if (a == e)
             {
-              Node cons = Node::fromExpr(dt[tst].getConstructor());
+              Node cons = dt[tst].getConstructor();
               Trace("sygus-enum") << "  ...unit exclude constructor #" << tst
                                   << ", constructor " << cons << std::endl;
               d_sbExcTlCons.insert(cons);
@@ -168,7 +168,7 @@ void SygusEnumerator::TermCache::initialize(Node e,
     // not a datatype, finish
     return;
   }
-  const Datatype& dt = tn.getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     // not a sygus datatype, finish
@@ -200,7 +200,7 @@ void SygusEnumerator::TermCache::initialize(Node e,
     // record type information
     for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
     {
-      TypeNode tn = TypeNode::fromType(dt[i].getArgType(j));
+      TypeNode tn = dt[i].getArgType(j);
       argTypes[i].push_back(tn);
     }
   }
@@ -544,7 +544,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn)
 
 SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
 {
-  if (tn.isDatatype() && tn.getDatatype().isSygus())
+  if (tn.isDatatype() && tn.getDType().isSygus())
   {
     std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn);
     if (it != d_masterEnum.end())
@@ -627,11 +627,11 @@ Node SygusEnumerator::TermEnumMaster::getCurrent()
   d_currTermSet = true;
   // construct based on the children
   std::vector<Node> children;
-  const Datatype& dt = d_tn.getDatatype();
+  const DType& dt = d_tn.getDType();
   Assert(d_consNum > 0 && d_consNum <= d_ccCons.size());
   // get the current constructor number
   unsigned cnum = d_ccCons[d_consNum - 1];
-  children.push_back(Node::fromExpr(dt[cnum].getConstructor()));
+  children.push_back(dt[cnum].getConstructor());
   // add the current of each child to children
   for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++)
   {
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 42ddbbb7d..0cc57e0ec 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -47,7 +47,7 @@ void SygusEvalUnfold::registerEvalTerm(Node n)
   TypeNode tn = n[0].getType();
   // since n[0] is an evaluation head, we know tn is a sygus datatype
   Assert(tn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
   if (n[0].getKind() == APPLY_CONSTRUCTOR)
   {
@@ -57,7 +57,7 @@ void SygusEvalUnfold::registerEvalTerm(Node n)
   }
   // register this evaluation term with its head
   d_evals[n[0]].push_back(n);
-  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  Node var_list = dt.getSygusVarList();
   d_eval_args[n[0]].push_back(std::vector<Node>());
   for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
   {
@@ -109,7 +109,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
       bool hasSymCons = sti.hasSubtermSymbolicCons();
       // n occurs as an evaluation head, thus it has sygus datatype type
       Assert(tn.isDatatype());
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       Assert(dt.isSygus());
       Trace("sygus-eval-unfold")
           << "SygusEvalUnfold: Register model value : " << vn << " for " << n
@@ -121,7 +121,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
       Node bTerm = d_tds->sygusToBuiltin(vn, tn);
       Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
       std::vector<Node> vars;
-      Node var_list = Node::fromExpr(dt.getSygusVarList());
+      Node var_list = dt.getSygusVarList();
       for (const Node& v : var_list)
       {
         vars.push_back(v);
@@ -240,22 +240,20 @@ Node SygusEvalUnfold::unfold(Node en,
   }
 
   TypeNode headType = en[0].getType();
-  Type headTypeT = headType.toType();
   NodeManager* nm = NodeManager::currentNM();
-  const Datatype& dt = headType.getDatatype();
+  const DType& dt = headType.getDType();
   unsigned i = datatypes::utils::indexOf(ev.getOperator());
   if (track_exp)
   {
     // explanation
-    Node ee =
-        nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
+    Node ee = nm->mkNode(APPLY_TESTER, dt[i].getTester(), en[0]);
     if (std::find(exp.begin(), exp.end(), ee) == exp.end())
     {
       exp.push_back(ee);
     }
   }
   // if we are a symbolic constructor, unfolding returns the subterm itself
-  Node sop = Node::fromExpr(dt[i].getSygusOp());
+  Node sop = dt[i].getSygusOp();
   if (sop.getAttribute(SygusAnyConstAttribute()))
   {
     Trace("sygus-eval-unfold-debug")
@@ -272,7 +270,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       Node ret = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]);
+          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
       Trace("sygus-eval-unfold-debug")
           << "...return (from constructor) " << ret << std::endl;
       return ret;
@@ -295,7 +293,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       s = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]);
+          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
     }
     cc.push_back(s);
     if (track_exp)
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index cf1993efb..8fb7cf2e7 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_explain.h"
 
+#include "expr/dtype.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
@@ -138,7 +139,7 @@ void SygusExplain::getExplanationForEquality(Node n,
     return;
   }
   Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR);
-  const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   int i = datatypes::utils::indexOf(vn.getOperator());
   Node tst = datatypes::utils::mkTester(n, i, dt);
   exp.push_back(tst);
@@ -147,9 +148,7 @@ void SygusExplain::getExplanationForEquality(Node n,
     if (cexc.find(j) == cexc.end())
     {
       Node sel = NodeManager::currentNM()->mkNode(
-          kind::APPLY_SELECTOR_TOTAL,
-          Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)),
-          n);
+          kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
       getExplanationForEquality(sel, vn[j], exp);
     }
   }
@@ -227,7 +226,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
       trb.replaceChild(i, vn[i]);
     }
   }
-  const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
+  const DType& dt = ntn.getDType();
   int cindex = datatypes::utils::indexOf(vn.getOperator());
   Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
   Node tst = datatypes::utils::mkTester(n, cindex, dt);
@@ -245,9 +244,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
   for (unsigned i = 0; i < vn.getNumChildren(); i++)
   {
     Node sel = NodeManager::currentNM()->mkNode(
-        kind::APPLY_SELECTOR_TOTAL,
-        Node::fromExpr(dt[cindex].getSelectorInternal(ntn.toType(), i)),
-        n);
+        kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
     Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
     if (cexc.find(i) == cexc.end())
     {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index b1b1ea62c..d9ce08d49 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 
+#include "expr/dtype.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -35,14 +36,14 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
   Assert(tn.isDatatype());
   TermDbSygus* tds = qe->getTermDatabaseSygus();
   tds->registerSygusType(tn);
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
-  TypeNode btn = TypeNode::fromType(dt.getSygusType());
+  TypeNode btn = dt.getSygusType();
   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
   {
     Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
                        << std::endl;
-    Node sop = Node::fromExpr(dt[i].getSygusOp());
+    Node sop = dt[i].getSygusOp();
     if (sop.getAttribute(SygusAnyConstAttribute()))
     {
       // the any constant constructor is never redundant
@@ -101,7 +102,7 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
 
 void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
 {
-  const Datatype& dt = static_cast<DatatypeType>(d_type.toType()).getDatatype();
+  const DType& dt = d_type.getDType();
   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
   {
     if (isRedundant(i))
@@ -118,7 +119,7 @@ bool SygusRedundantCons::isRedundant(unsigned i)
 }
 
 void SygusRedundantCons::getGenericList(TermDbSygus* tds,
-                                        const Datatype& dt,
+                                        const DType& dt,
                                         unsigned c,
                                         unsigned index,
                                         std::map<int, Node>& pre,
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 317892723..f0743027e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -113,7 +113,7 @@ class SygusRedundantCons
    * to terms.
    */
   void getGenericList(TermDbSygus* tds,
-                      const Datatype& dt,
+                      const DType& dt,
                       unsigned c,
                       unsigned index,
                       std::map<int, Node>& pre,
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 5511adb18..9ab94d1bc 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -70,7 +70,7 @@ void SygusRepairConst::registerSygusType(TypeNode tn,
       // "any constant" constructors
       return;
     }
-    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    const DType& dt = tn.getDType();
     if (!dt.isSygus())
     {
       // may have recursed to a non-sygus-datatype
@@ -83,7 +83,7 @@ void SygusRepairConst::registerSygusType(TypeNode tn,
     }
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
-      const DatatypeConstructor& dtc = dt[i];
+      const DTypeConstructor& dtc = dt[i];
       // recurse on all subfields
       for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
       {
@@ -366,14 +366,14 @@ bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
   }
   TypeNode tn = n.getType();
   Assert(tn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     return false;
   }
   Node op = n.getOperator();
   unsigned cindex = datatypes::utils::indexOf(op);
-  Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+  Node sygusOp = dt[cindex].getSygusOp();
   if (sygusOp.getAttribute(SygusAnyConstAttribute()))
   {
     // if it represents "any constant" then it is repairable
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index f87b906e1..052546c0e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
+#include "expr/dtype.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
@@ -141,8 +142,7 @@ void SygusUnifStrategy::registerStrategyPoint(Node et,
   if (d_einfo.find(et) == d_einfo.end())
   {
     Trace("sygus-unif-debug")
-        << "...register " << et << " for "
-        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
+        << "...register " << et << " for " << tn.getDType().getName();
     Trace("sygus-unif-debug") << ", role = " << enum_role
                               << ", in search = " << inSearch << std::endl;
     d_einfo[et].initialize(enum_role);
@@ -196,8 +196,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     ee = nm->mkSkolem("ee", tn);
     eti.d_enum[erole] = ee;
     Trace("sygus-unif-debug")
-        << "...enumerator " << ee << " for "
-        << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+        << "...enumerator " << ee << " for " << tn.getDType().getName()
         << ", role = " << erole << std::endl;
   }
   else
@@ -217,7 +216,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
   // we know this is a sygus datatype since it is either the top-level type
   // in the strategy graph, or was recursed by a strategy we inferred.
   Assert(tn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
 
   std::map<Node, std::vector<StrategyType> > cop_to_strat;
@@ -232,8 +231,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
   bool search_this = false;
   for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
   {
-    Node cop = Node::fromExpr(dt[j].getConstructor());
-    Node op = Node::fromExpr(dt[j].getSygusOp());
+    Node cop = dt[j].getConstructor();
+    Node op = dt[j].getSygusOp();
     Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
                               << " with sygus op " << op << "..." << std::endl;
 
@@ -244,8 +243,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     std::vector<TypeNode> sktns;
     for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
     {
-      Type t = dt[j][k].getRangeType();
-      TypeNode ttn = TypeNode::fromType(t);
+      TypeNode ttn = dt[j][k].getRangeType();
       Node kv = nm->mkSkolem("ut", ttn);
       sks.push_back(kv);
       cop_to_sks[cop].push_back(kv);
@@ -255,7 +253,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
     std::vector<Node> echildren;
     echildren.push_back(ut);
-    Node sbvl = Node::fromExpr(dt.getSygusVarList());
+    Node sbvl = dt.getSygusVarList();
     for (const Node& sbv : sbvl)
     {
       echildren.push_back(sbv);
@@ -482,10 +480,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
       for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
       {
         TypeNode ctn = sktns[cop_to_carg_list[cop][k]];
-        Trace("sygus-unif-debug")
-            << "   Child type " << k << " : "
-            << static_cast<DatatypeType>(ctn.toType()).getDatatype().getName()
-            << std::endl;
+        Trace("sygus-unif-debug") << "   Child type " << k << " : "
+                                  << ctn.getDType().getName() << std::endl;
         cop_to_child_types[cop].push_back(ctn);
       }
       // if there are checks on the consistency of child types wrt strategies,
@@ -578,14 +574,10 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
           {
             // it is templated, allocate a fresh variable
             et = nm->mkSkolem("et", ct);
-            Trace("sygus-unif-debug")
-                << "...enumerate " << et << " of type "
-                << ((DatatypeType)ct.toType()).getDatatype().getName();
+            Trace("sygus-unif-debug") << "...enumerate " << et << " of type "
+                                      << ct.getDType().getName();
             Trace("sygus-unif-debug") << " for arg " << j << " of "
-                                      << static_cast<DatatypeType>(tn.toType())
-                                             .getDatatype()
-                                             .getName()
-                                      << std::endl;
+                                      << tn.getDType().getName() << std::endl;
             registerStrategyPoint(et, ct, erole_c, true);
             d_einfo[et].d_template = cop_to_child_templ[cop][j];
             d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
@@ -595,8 +587,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
           else
           {
             Trace("sygus-unif-debug")
-                << "...child type enumerate "
-                << ((DatatypeType)ct.toType()).getDatatype().getName()
+                << "...child type enumerate " << ct.getDType().getName()
                 << ", node role = " << nrole_c << std::endl;
             // otherwise use the previous
             Assert(d_tinfo[ct].d_enum.find(erole_c)
@@ -631,9 +622,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
         {
           Trace("sygus-unif") << "Initialized strategy " << strat;
           Trace("sygus-unif")
-              << " for "
-              << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
-              << ", operator " << cop;
+              << " for " << tn.getDType().getName() << ", operator " << cop;
           Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
                               << ", solution template = (lambda ( ";
           for (const Node& targ : cons_strat->d_sol_templ_args)
@@ -707,10 +696,8 @@ void SygusUnifStrategy::staticLearnRedundantOps(
     std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
     Assert(itn != d_einfo.end());
     // see if there is anything we can eliminate
-    Trace("sygus-unif")
-        << "* Search enumerator #" << i << " : type "
-        << ((DatatypeType)e.getType().toType()).getDatatype().getName()
-        << " : ";
+    Trace("sygus-unif") << "* Search enumerator #" << i << " : type "
+                        << e.getType().getDType().getName() << " : ";
     Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
                         << " slaves:" << std::endl;
     for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
@@ -734,8 +721,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
   {
     Node em = nce.first;
-    const Datatype& dt =
-        static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+    const DType& dt = em.getType().getDType();
     std::vector<Node> lemmas;
     for (std::pair<const unsigned, bool>& nc : nce.second)
     {
@@ -819,21 +805,18 @@ void SygusUnifStrategy::staticLearnRedundantOps(
     // arguments of ITE are the same BOOL type
     if (restrictions.d_iteReturnBoolConst)
     {
-      const Datatype& dt =
-          static_cast<DatatypeType>(etn.toType()).getDatatype();
-      Node op = Node::fromExpr(dt[cindex].getSygusOp());
-      TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+      const DType& dt = etn.getDType();
+      Node op = dt[cindex].getSygusOp();
+      TypeNode sygus_tn = dt.getSygusType();
       if (op.getKind() == kind::BUILTIN
-          && NodeManager::operatorToKind(op) == ITE
-          && sygus_tn.isBoolean()
-          && (TypeNode::fromType(dt[cindex].getArgType(1))
-              == TypeNode::fromType(dt[cindex].getArgType(2))))
+          && NodeManager::operatorToKind(op) == ITE && sygus_tn.isBoolean()
+          && (dt[cindex].getArgType(1) == dt[cindex].getArgType(2)))
       {
         unsigned ncons = dt.getNumConstructors(), indexT = ncons,
                  indexF = ncons;
         for (unsigned k = 0; k < ncons; ++k)
         {
-          Node op_arg = Node::fromExpr(dt[k].getSygusOp());
+          Node op_arg = dt[k].getSygusOp();
           if (dt[k].getNumArgs() > 0 || !op_arg.isConst())
           {
             continue;
@@ -867,14 +850,14 @@ void SygusUnifStrategy::staticLearnRedundantOps(
     }
   }
   // get the current datatype
-  const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
+  const DType& dt = etn.getDType();
   // do not use recursive Boolean connectives for conditions of ITEs
   if (nrole == role_ite_condition && restrictions.d_iteCondOnlyAtoms)
   {
-    TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+    TypeNode sygus_tn = dt.getSygusType();
     for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
     {
-      Node op = Node::fromExpr(dt[j].getSygusOp());
+      Node op = dt[j].getSygusOp();
       Trace("sygus-strat-slearn")
           << "...for ite condition, look at operator : " << op << std::endl;
       if (op.isConst() && dt[j].getNumArgs() == 0)
@@ -894,7 +877,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(
           bool type_ok = true;
           for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
           {
-            TypeNode tn = TypeNode::fromType(dt[j].getArgType(k));
+            TypeNode tn = dt[j].getArgType(k);
             if (tn != etn)
             {
               type_ok = false;
@@ -991,8 +974,7 @@ void SygusUnifStrategy::debugPrint(
 
   indent(c, ind);
   Trace(c) << e << " :: node role : " << nrole;
-  Trace(c) << ", type : "
-           << static_cast<DatatypeType>(etn.toType()).getDatatype().getName();
+  Trace(c) << ", type : " << etn.getDType().getName();
   if (ei.isConditional())
   {
     Trace(c) << ", conditional";
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ca4feda32..e30f9771c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1050,7 +1050,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
       Node prog = d_embed_quant[0][i];
       int status = statuses[i];
       TypeNode tn = prog.getType();
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       std::stringstream ss;
       ss << prog;
       std::string f(ss.str());
@@ -1113,7 +1113,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
         // pvs stores the variables that will be printed in the argument list
         // below.
         std::vector<Node> pvs;
-        Node vl = Node::fromExpr(dt.getSygusVarList());
+        Node vl = dt.getSygusVarList();
         if (!vl.isNull())
         {
           Assert(vl.getKind() == BOUND_VAR_LIST);
@@ -1176,9 +1176,9 @@ bool SynthConjecture::getSynthSolutions(
     }
     // convert to lambda
     TypeNode tn = d_embed_quant[0][i].getType();
-    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    const DType& dt = tn.getDType();
     Node fvar = d_quant[0][i];
-    Node bvl = Node::fromExpr(dt.getSygusVarList());
+    Node bvl = dt.getSygusVarList();
     if (!bvl.isNull())
     {
       // since we don't have function subtyping, this assertion should only
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 08fb58e40..bce46fb6b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -67,9 +67,9 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
   TypeNode vtn = tn;
   if( useSygusType ){
     if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      const DType& dt = tn.getDType();
       if( !dt.getSygusType().isNull() ){
-        vtn = TypeNode::fromType( dt.getSygusType() );
+        vtn = dt.getSygusType();
         sindex = 1;
       } 
     }
@@ -77,7 +77,7 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
   while( i>=(int)d_fv[sindex][tn].size() ){
     std::stringstream ss;
     if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      const DType& dt = tn.getDType();
       ss << "fv_" << dt.getName() << "_" << i;
     }else{
       ss << "fv_" << tn << "_" << i;
@@ -126,11 +126,8 @@ bool TermDbSygus::hasFreeVar( Node n ) {
 Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
 {
   Assert(tn.isDatatype());
-  Assert(static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus());
-  Assert(
-      TypeNode::fromType(
-          static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
-          .isComparableTo(c.getType()));
+  Assert(tn.getDType().isSygus());
+  Assert(tn.getDType().getSygusType().isComparableTo(c.getType()));
 
   std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
   if (it == d_proxy_vars[tn].end())
@@ -146,9 +143,9 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
     }
     else
     {
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       k = NodeManager::currentNM()->mkNode(
-          APPLY_CONSTRUCTOR, Node::fromExpr(dt[anyC].getConstructor()), c);
+          APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
     }
     d_proxy_vars[tn][c] = k;
     return k;
@@ -161,7 +158,7 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   return d_fv_stype[v];
 }
 
-Node TermDbSygus::mkGeneric(const Datatype& dt,
+Node TermDbSygus::mkGeneric(const DType& dt,
                             unsigned c,
                             std::map<TypeNode, int>& var_count,
                             std::map<int, Node>& pre,
@@ -181,7 +178,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
       a = it->second;
       Trace("sygus-db-debug") << "From pre: " << a << std::endl;
     }else{
-      TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
+      TypeNode tna = dt[c].getArgType(i);
       a = getFreeVarInc( tna, var_count, true );
     }
     Trace("sygus-db-debug")
@@ -194,7 +191,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
   return ret;
 }
 
-Node TermDbSygus::mkGeneric(const Datatype& dt,
+Node TermDbSygus::mkGeneric(const DType& dt,
                             int c,
                             std::map<int, Node>& pre,
                             bool doBetaRed)
@@ -203,7 +200,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt,
   return mkGeneric(dt, c, var_count, pre, doBetaRed);
 }
 
-Node TermDbSygus::mkGeneric(const Datatype& dt, int c, bool doBetaRed)
+Node TermDbSygus::mkGeneric(const DType& dt, int c, bool doBetaRed)
 {
   std::map<int, Node> pre;
   return mkGeneric(dt, c, pre, doBetaRed);
@@ -294,7 +291,7 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
   }
   Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
                           << ", type = " << tn << std::endl;
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     return n;
@@ -306,7 +303,7 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
     std::map<int, Node> pre;
     for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
     {
-      pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
+      pre[j] = sygusToBuiltin(n[j], dt[i].getArgType(j));
       Trace("sygus-db-debug")
           << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
     }
@@ -326,7 +323,7 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
   // map to builtin variable type
   int fv_num = getVarNum(n);
   Assert(!dt.getSygusType().isNull());
-  TypeNode vtn = TypeNode::fromType(dt.getSygusType());
+  TypeNode vtn = dt.getSygusType();
   Node ret = getFreeVar(vtn, fv_num);
   return ret;
 }
@@ -341,7 +338,7 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){
   {
     sum += getSygusTermSize(n[i]);
   }
-  const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+  const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
   int cindex = datatypes::utils::indexOf(n.getOperator());
   Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
   unsigned weight = dt[cindex].getWeight();
@@ -362,7 +359,7 @@ bool TermDbSygus::registerSygusType(TypeNode tn)
   {
     return false;
   }
-  const Datatype& dt = tn.getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     return false;
@@ -407,12 +404,10 @@ void TermDbSygus::registerEnumerator(Node e,
     TypeNode stn = sf_types[i];
     Assert(stn.isDatatype());
     SygusTypeInfo& sti = getTypeInfo(stn);
-    const Datatype& dt = stn.getDatatype();
+    const DType& dt = stn.getDType();
     int anyC = sti.getAnyConstantConsNum();
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
-      Expr sop = dt[i].getSygusOp();
-      Assert(!sop.isNull());
       bool isAnyC = static_cast<int>(i) == anyC;
       if (isAnyC && !useSymbolicCons)
       {
@@ -497,7 +492,7 @@ void TermDbSygus::registerEnumerator(Node e,
         // sygus stream are to find many solutions to an easy problem, where
         // the bottleneck often becomes the large number of "exclude the current
         // solution" clauses.
-        const Datatype& dt = et.getDatatype();
+        const DType& dt = et.getDType();
         if (options::sygusStream()
             || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
         {
@@ -767,8 +762,7 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
   {
     d_sel_weight[tn].clear();
     itsw = d_sel_weight.find(tn);
-    Type t = tn.toType();
-    const Datatype& dt = static_cast<DatatypeType>(t).getDatatype();
+    const DType& dt = tn.getDType();
     Trace("sygus-db") << "Compute selector weights for " << dt.getName()
                       << std::endl;
     for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
@@ -776,7 +770,7 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
       unsigned cw = dt[i].getWeight();
       for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
       {
-        Node csel = Node::fromExpr(dt[i].getSelectorInternal(t, j));
+        Node csel = dt[i].getSelectorInternal(tn, j);
         std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
         if (its == itsw->second.end() || cw < its->second)
         {
@@ -790,14 +784,15 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
   return itsw->second[sel];
 }
 
-TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
+TypeNode TermDbSygus::getArgType(const DTypeConstructor& c, unsigned i) const
 {
   Assert(i < c.getNumArgs());
-  return TypeNode::fromType(
-      static_cast<SelectorType>(c[i].getType()).getRangeType());
+  return c.getArgType(i);
 }
 
-bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ) {
+bool TermDbSygus::isTypeMatch(const DTypeConstructor& c1,
+                              const DTypeConstructor& c2)
+{
   if( c1.getNumArgs()!=c2.getNumArgs() ){
     return false;
   }else{
@@ -818,10 +813,10 @@ bool TermDbSygus::isSymbolicConsApp(Node n) const
   }
   TypeNode tn = n.getType();
   Assert(tn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
   unsigned cindex = datatypes::utils::indexOf(n.getOperator());
-  Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+  Node sygusOp = dt[cindex].getSygusOp();
   // it is symbolic if it represents "any constant"
   return sygusOp.getAttribute(SygusAnyConstAttribute());
 }
@@ -834,12 +829,12 @@ bool TermDbSygus::canConstructKind(TypeNode tn,
   Assert(isRegistered(tn));
   SygusTypeInfo& ti = getTypeInfo(tn);
   int c = ti.getKindConsNum(k);
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   if (c != -1)
   {
     for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
     {
-      argts.push_back(TypeNode::fromType(dt[c].getArgType(i)));
+      argts.push_back(dt[c].getArgType(i));
     }
     return true;
   }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 76b5039f6..6d328ddca 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -19,6 +19,7 @@
 
 #include <unordered_set>
 
+#include "expr/dtype.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/quantifiers/fun_def_evaluator.h"
@@ -229,18 +230,18 @@ class TermDbSygus {
    * If doBetaRed is true, then lambda operators are eagerly eliminated via
    * beta reduction.
    */
-  Node mkGeneric(const Datatype& dt,
+  Node mkGeneric(const DType& dt,
                  unsigned c,
                  std::map<TypeNode, int>& var_count,
                  std::map<int, Node>& pre,
                  bool doBetaRed = true);
   /** same as above, but with empty var_count */
-  Node mkGeneric(const Datatype& dt,
+  Node mkGeneric(const DType& dt,
                  int c,
                  std::map<int, Node>& pre,
                  bool doBetaRed = true);
   /** same as above, but with empty pre */
-  Node mkGeneric(const Datatype& dt, int c, bool doBetaRed = true);
+  Node mkGeneric(const DType& dt, int c, bool doBetaRed = true);
   /** makes a symbolic term concrete
    *
    * Given a sygus datatype term n of type tn with holes (symbolic constructor
@@ -413,9 +414,9 @@ class TermDbSygus {
   /** get the weight of the selector, where tn is the domain of sel */
   unsigned getSelectorWeight(TypeNode tn, Node sel);
   /** get arg type */
-  TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
+  TypeNode getArgType(const DTypeConstructor& c, unsigned i) const;
   /** Do constructors c1 and c2 have the same type? */
-  bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
+  bool isTypeMatch(const DTypeConstructor& c1, const DTypeConstructor& c2);
   /** return whether n is an application of a symbolic constructor */
   bool isSymbolicConsApp(Node n) const;
   /** can construct kind
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 71ccd60c9..a17a60927 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/type_info.h"
 
 #include "base/check.h"
+#include "expr/dtype.h"
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -37,14 +38,14 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
 {
   d_this = tn;
   Assert(tn.isDatatype());
-  const Datatype& dt = tn.getDatatype();
+  const DType& dt = tn.getDType();
   Assert(dt.isSygus());
   Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
-  TypeNode btn = TypeNode::fromType(dt.getSygusType());
+  TypeNode btn = dt.getSygusType();
   d_btype = btn;
   Assert(!d_btype.isNull());
   // get the sygus variable list
-  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  Node var_list = dt.getSygusVarList();
   if (!var_list.isNull())
   {
     for (unsigned j = 0; j < var_list.getNumChildren(); j++)
@@ -77,7 +78,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
   {
     for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
     {
-      TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+      TypeNode ctn = dt[i].getArgType(j);
       Trace("sygus-db") << "  register subfield type " << ctn << std::endl;
       if (tds->registerSygusType(ctn))
       {
@@ -93,13 +94,12 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
   // iterate over constructors
   for (unsigned i = 0; i < dt.getNumConstructors(); i++)
   {
-    Expr sop = dt[i].getSygusOp();
+    Node sop = dt[i].getSygusOp();
     Assert(!sop.isNull());
-    Node n = Node::fromExpr(sop);
     Trace("sygus-db") << "  Operator #" << i << " : " << sop;
     if (sop.getKind() == kind::BUILTIN)
     {
-      Kind sk = NodeManager::operatorToKind(n);
+      Kind sk = NodeManager::operatorToKind(sop);
       Trace("sygus-db") << ", kind = " << sk;
       d_kinds[sk] = i;
       d_arg_kind[i] = sk;
@@ -112,8 +112,8 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     else if (sop.isConst() && dt[i].getNumArgs() == 0)
     {
       Trace("sygus-db") << ", constant";
-      d_consts[n] = i;
-      d_arg_const[i] = n;
+      d_consts[sop] = i;
+      d_arg_const[i] = sop;
     }
     else if (sop.getKind() == LAMBDA)
     {
@@ -121,9 +121,9 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
       Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
       for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
       {
-        TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+        TypeNode ct = dt[i].getArgType(j);
         TypeNode cbt = tds->sygusToBuiltinType(ct);
-        TypeNode lat = TypeNode::fromType(sop[0][j].getType());
+        TypeNode lat = sop[0][j].getType();
         AlwaysAssert(cbt.isSubtypeOf(lat))
             << "In sygus datatype " << dt.getName()
             << ", argument to a lambda constructor is not " << lat << std::endl;
@@ -135,13 +135,13 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
       }
     }
     // symbolic constructors
-    if (n.getAttribute(SygusAnyConstAttribute()))
+    if (sop.getAttribute(SygusAnyConstAttribute()))
     {
       d_sym_cons_any_constant = i;
       d_has_subterm_sym_cons = true;
     }
-    d_ops[n] = i;
-    d_arg_ops[i] = n;
+    d_ops[sop] = i;
+    d_arg_ops[i] = sop;
     Trace("sygus-db") << std::endl;
     // We must properly catch type errors in sygus grammars for arguments of
     // builtin operators. The challenge is that we easily ask for expected
@@ -170,7 +170,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
       csize = 1;
       for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
       {
-        TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+        TypeNode ct = dt[i].getArgType(j);
         if (ct == tn)
         {
           csize += d_min_term_size;
@@ -182,7 +182,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
         }
         else
         {
-          Assert(!ct.isDatatype() || !ct.getDatatype().isSygus());
+          Assert(!ct.isDatatype() || !ct.getDType().isSygus());
         }
       }
     }
@@ -219,12 +219,11 @@ void SygusTypeInfo::initializeVarSubclasses()
     std::vector<unsigned> rm_indices;
     TypeNode stn = sf_types[i];
     Assert(stn.isDatatype());
-    const Datatype& dt = stn.getDatatype();
+    const DType& dt = stn.getDType();
     for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
     {
-      Expr sop = dt[j].getSygusOp();
-      Assert(!sop.isNull());
-      Node sopn = Node::fromExpr(sop);
+      Node sopn = dt[j].getSygusOp();
+      Assert(!sopn.isNull());
       if (type_occurs.find(sopn) != type_occurs.end())
       {
         // if it is a variable, store that it occurs in stn
@@ -272,7 +271,7 @@ void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
     // do not recurse to non-datatype types
     return;
   }
-  const Datatype& dt = tn.getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     // do not recurse to non-sygus datatype types
@@ -284,7 +283,7 @@ void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
   {
     for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
     {
-      TypeNode at = TypeNode::fromType(dt[i].getArgType(j));
+      TypeNode at = dt[i].getArgType(j);
       computeMinTypeDepthInternal(at, type_depth + 1);
     }
   }
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 834ca1975..10af0d703 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus_sampler.h"
 
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
@@ -92,7 +93,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds,
   d_is_valid = true;
   d_ftn = f.getType();
   Assert(d_ftn.isDatatype());
-  const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
+  const DType& dt = d_ftn.getDType();
   Assert(dt.isSygus());
 
   Trace("sygus-sample") << "Register sampler for " << f << std::endl;
@@ -105,7 +106,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds,
   d_rvalue_null_cindices.clear();
   d_var_sygus_types.clear();
   // get the sygus variable list
-  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  Node var_list = dt.getSygusVarList();
   if (!var_list.isNull())
   {
     for (const Node& sv : var_list)
@@ -659,7 +660,7 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
   {
     return getRandomValue(tn);
   }
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  const DType& dt = tn.getDType();
   if (!dt.isSygus())
   {
     return getRandomValue(tn);
@@ -685,7 +686,7 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
         << "Recurse constructor index #" << index << std::endl;
     unsigned cindex = cindices[index];
     Assert(cindex < dt.getNumConstructors());
-    const DatatypeConstructor& dtc = dt[cindex];
+    const DTypeConstructor& dtc = dt[cindex];
     // more likely to terminate in recursive calls
     double rchance_new = rchance + (1.0 - rchance) * rinc;
     std::map<int, Node> pre;
@@ -718,7 +719,7 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn,
   }
   Trace("sygus-sample-grammar") << "...resort to random value" << std::endl;
   // if we did not generate based on the grammar, pick a random value
-  return getRandomValue(TypeNode::fromType(dt.getSygusType()));
+  return getRandomValue(dt.getSygusType());
 }
 
 // recursion depth bounded by number of types in grammar (small)
@@ -731,15 +732,15 @@ void SygusSampler::registerSygusType(TypeNode tn)
     {
       return;
     }
-    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    const DType& dt = tn.getDType();
     if (!dt.isSygus())
     {
       return;
     }
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
-      const DatatypeConstructor& dtc = dt[i];
-      Node sop = Node::fromExpr(dtc.getSygusOp());
+      const DTypeConstructor& dtc = dt[i];
+      Node sop = dtc.getSygusOp();
       bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end();
       if (isVar)
       {