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

This PR makes two simultaneous changes:

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

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

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

45 files changed, 438 insertions, 2526 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f6c5187c7..c55c29ed4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1032,7 +1032,6 @@ install(FILES
           expr/array.h
           expr/array_store_all.h
           expr/ascription_type.h
-          expr/datatype.h
           expr/emptyset.h
           expr/expr_iomanip.h
           expr/record.h
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 150f84301..0a35981d2 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -38,6 +38,7 @@
 
 #include "base/check.h"
 #include "base/configuration.h"
+#include "expr/dtype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
@@ -927,7 +928,7 @@ bool Sort::isDatatype() const { return d_type->isDatatype(); }
 bool Sort::isParametricDatatype() const
 {
   if (!d_type->isDatatype()) return false;
-  return DatatypeType(*d_type).isParametric();
+  return TypeNode::fromType(*d_type).isParametricDatatype();
 }
 
 bool Sort::isConstructor() const { return d_type->isConstructor(); }
@@ -965,25 +966,33 @@ bool Sort::isComparableTo(Sort s) const
 
 Datatype Sort::getDatatype() const
 {
+  NodeManagerScope scope(d_solver->getNodeManager());
   CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
-  return Datatype(d_solver, DatatypeType(*d_type).getDatatype());
+  return Datatype(d_solver, TypeNode::fromType(*d_type).getDType());
 }
 
 Sort Sort::instantiate(const std::vector<Sort>& params) const
 {
+  NodeManagerScope scope(d_solver->getNodeManager());
   CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
-  std::vector<Type> tparams;
+  std::vector<TypeNode> tparams;
   for (const Sort& s : params)
   {
-    tparams.push_back(*s.d_type.get());
+    tparams.push_back(TypeNode::fromType(*s.d_type.get()));
   }
   if (d_type->isDatatype())
   {
-    return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams));
+    return Sort(d_solver,
+                TypeNode::fromType(*d_type)
+                    .instantiateParametricDatatype(tparams)
+                    .toType());
   }
   Assert(d_type->isSortConstructor());
-  return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams));
+  return Sort(d_solver,
+              d_solver->getNodeManager()
+                  ->mkSort(TypeNode::fromType(*d_type), tparams)
+                  .toType());
 }
 
 std::string Sort::toString() const { return d_type->toString(); }
@@ -996,20 +1005,20 @@ CVC4::Type Sort::getType(void) const { return *d_type; }
 
 size_t Sort::getConstructorArity() const
 {
-  CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
+  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
   return ConstructorType(*d_type).getArity();
 }
 
 std::vector<Sort> Sort::getConstructorDomainSorts() const
 {
-  CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
+  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
   std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
   return typeVectorToSorts(d_solver, types);
 }
 
 Sort Sort::getConstructorCodomainSort() const
 {
-  CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
+  CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
   return Sort(d_solver, ConstructorType(*d_type).getRangeType());
 }
 
@@ -1126,14 +1135,20 @@ uint32_t Sort::getFPSignificandSize() const
 std::vector<Sort> Sort::getDatatypeParamSorts() const
 {
   CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
-  std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes();
-  return typeVectorToSorts(d_solver, types);
+  std::vector<CVC4::TypeNode> typeNodes =
+      TypeNode::fromType(*d_type).getParamTypes();
+  std::vector<Sort> sorts;
+  for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++)
+  {
+    sorts.push_back(Sort(d_solver, typeNodes[i].toType()));
+  }
+  return sorts;
 }
 
 size_t Sort::getDatatypeArity() const
 {
   CVC4_API_CHECK(isDatatype()) << "Not a datatype sort.";
-  return DatatypeType(*d_type).getArity();
+  return TypeNode::fromType(*d_type).getNumChildren() - 1;
 }
 
 /* Tuple sort ---------------------------------------------------------- */
@@ -1141,14 +1156,20 @@ size_t Sort::getDatatypeArity() const
 size_t Sort::getTupleLength() const
 {
   CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
-  return DatatypeType(*d_type).getTupleLength();
+  return TypeNode::fromType(*d_type).getTupleLength();
 }
 
 std::vector<Sort> Sort::getTupleSorts() const
 {
   CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
-  std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes();
-  return typeVectorToSorts(d_solver, types);
+  std::vector<CVC4::TypeNode> typeNodes =
+      TypeNode::fromType(*d_type).getTupleTypes();
+  std::vector<Sort> sorts;
+  for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++)
+  {
+    sorts.push_back(Sort(d_solver, typeNodes[i].toType()));
+  }
+  return sorts;
 }
 
 /* --------------------------------------------------------------------- */
@@ -1472,7 +1493,8 @@ Kind Term::getKindHelper() const
         break;
     }
   }
-
+  // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
+  // INTERNAL_KIND.
   return intToExtKind(d_node->getKind());
 }
 
@@ -1604,7 +1626,7 @@ Op Term::getOp() const
     return Op(d_solver, intToExtKind(d_node->getKind()), op);
   }
   // Notice this is the only case where getKindHelper is used, since the
-  // cases above do have special cases for intToExtKind.
+  // cases above do not have special cases for intToExtKind.
   return Op(d_solver, getKindHelper());
 }
 
@@ -1938,20 +1960,31 @@ DatatypeConstructorDecl::DatatypeConstructorDecl()
 
 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
                                                  const std::string& name)
-    : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name))
+    : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name))
+{
+}
+DatatypeConstructorDecl::~DatatypeConstructorDecl()
 {
+  if (d_ctor != nullptr)
+  {
+    // ensure proper node manager is in scope
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_ctor.reset();
+  }
 }
 
 void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort)
 {
+  NodeManagerScope scope(d_solver->getNodeManager());
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort)
       << "non-null range sort for selector";
-  d_ctor->addArg(name, *sort.d_type);
+  d_ctor->addArg(name, TypeNode::fromType(*sort.d_type));
 }
 
 void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
 {
-  d_ctor->addArg(name, DatatypeSelfType());
+  NodeManagerScope scope(d_solver->getNodeManager());
+  d_ctor->addArgSelf(name);
 }
 
 std::string DatatypeConstructorDecl::toString() const
@@ -1963,8 +1996,8 @@ std::string DatatypeConstructorDecl::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-const CVC4::DatatypeConstructor&
-DatatypeConstructorDecl::getDatatypeConstructor(void) const
+const CVC4::DTypeConstructor& DatatypeConstructorDecl::getDatatypeConstructor(
+    void) const
 {
   return *d_ctor;
 }
@@ -1990,8 +2023,7 @@ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
 DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            bool isCoDatatype)
-    : d_solver(slv),
-      d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
+    : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype))
 {
 }
 
@@ -2000,10 +2032,10 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            Sort param,
                            bool isCoDatatype)
     : d_solver(slv),
-      d_dtype(new CVC4::Datatype(slv->getExprManager(),
-                                 name,
-                                 std::vector<Type>{*param.d_type},
-                                 isCoDatatype))
+      d_dtype(new CVC4::DType(
+          name,
+          std::vector<TypeNode>{TypeNode::fromType(*param.d_type)},
+          isCoDatatype))
 {
 }
 
@@ -2013,23 +2045,32 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            bool isCoDatatype)
     : d_solver(slv)
 {
-  std::vector<Type> tparams;
+  std::vector<TypeNode> tparams;
   for (const Sort& p : params)
   {
-    tparams.push_back(*p.d_type);
+    tparams.push_back(TypeNode::fromType(*p.d_type));
   }
-  d_dtype = std::shared_ptr<CVC4::Datatype>(
-      new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype));
+  d_dtype = std::shared_ptr<CVC4::DType>(
+      new CVC4::DType(name, tparams, isCoDatatype));
 }
 
 bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
 
-DatatypeDecl::~DatatypeDecl() {}
+DatatypeDecl::~DatatypeDecl()
+{
+  if (d_dtype != nullptr)
+  {
+    // ensure proper node manager is in scope
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_dtype.reset();
+  }
+}
 
 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
 {
+  NodeManagerScope scope(d_solver->getNodeManager());
   CVC4_API_CHECK_NOT_NULL;
-  d_dtype->addConstructor(*ctor.d_ctor);
+  d_dtype->addConstructor(ctor.d_ctor);
 }
 
 size_t DatatypeDecl::getNumConstructors() const
@@ -2062,7 +2103,7 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); }
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
+CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
 
 std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 {
@@ -2075,13 +2116,21 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
 
 DatatypeSelector::DatatypeSelector(const Solver* slv,
-                                   const CVC4::DatatypeConstructorArg& stor)
-    : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor))
+                                   const CVC4::DTypeSelector& stor)
+    : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor))
 {
   CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
 }
 
-DatatypeSelector::~DatatypeSelector() {}
+DatatypeSelector::~DatatypeSelector()
+{
+  if (d_stor != nullptr)
+  {
+    // ensure proper node manager is in scope
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_stor.reset();
+  }
+}
 
 std::string DatatypeSelector::getName() const { return d_stor->getName(); }
 
@@ -2093,7 +2142,7 @@ Term DatatypeSelector::getSelectorTerm() const
 
 Sort DatatypeSelector::getRangeSort() const
 {
-  return Sort(d_solver, d_stor->getRangeType());
+  return Sort(d_solver, d_stor->getRangeType().toType());
 }
 
 std::string DatatypeSelector::toString() const
@@ -2105,8 +2154,7 @@ std::string DatatypeSelector::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg(
-    void) const
+CVC4::DTypeSelector DatatypeSelector::getDatatypeConstructorArg(void) const
 {
   return *d_stor;
 }
@@ -2124,14 +2172,22 @@ DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
 }
 
 DatatypeConstructor::DatatypeConstructor(const Solver* slv,
-                                         const CVC4::DatatypeConstructor& ctor)
-    : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor))
+                                         const CVC4::DTypeConstructor& ctor)
+    : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor))
 {
   CVC4_API_CHECK(d_ctor->isResolved())
       << "Expected resolved datatype constructor";
 }
 
-DatatypeConstructor::~DatatypeConstructor() {}
+DatatypeConstructor::~DatatypeConstructor()
+{
+  if (d_ctor != nullptr)
+  {
+    // ensure proper node manager is in scope
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_ctor.reset();
+  }
+}
 
 std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
 
@@ -2143,15 +2199,22 @@ Term DatatypeConstructor::getConstructorTerm() const
 
 Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const
 {
+  NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_CHECK(d_ctor->isResolved())
+      << "Expected resolved datatype constructor";
+  CVC4_API_CHECK(retSort.isDatatype())
+      << "Cannot get specialized constructor type for non-datatype type "
+      << retSort;
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   
   NodeManager* nm = d_solver->getNodeManager();
-  Node ret = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                           nm->mkConst(AscriptionType(
-                               d_ctor
-                                   ->getSpecializedConstructorType(
-                                       retSort.getType()))),
-                           d_ctor->getConstructor());
+  Node ret = nm->mkNode(
+      kind::APPLY_TYPE_ASCRIPTION,
+      nm->mkConst(AscriptionType(d_ctor
+                                     ->getSpecializedConstructorType(
+                                         TypeNode::fromType(retSort.getType()))
+                                     .toType())),
+      d_ctor->getConstructor());
   (void)ret.getType(true); /* kick off type checking */
   // apply type ascription to the operator
   Term sctor =
@@ -2205,20 +2268,19 @@ DatatypeConstructor::const_iterator DatatypeConstructor::end() const
 }
 
 DatatypeConstructor::const_iterator::const_iterator(
-    const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin)
+    const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin)
 {
   d_solver = slv;
-  d_int_stors = ctor.getArgs();
+  d_int_stors = &ctor.getArgs();
 
-  const std::vector<CVC4::DatatypeConstructorArg>* sels =
-      static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
-          d_int_stors);
-  for (const auto& s : *sels)
+  const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels =
+      ctor.getArgs();
+  for (const std::shared_ptr<CVC4::DTypeSelector>& s : sels)
   {
     /* Can not use emplace_back here since constructor is private. */
-    d_stors.push_back(DatatypeSelector(d_solver, s));
+    d_stors.push_back(DatatypeSelector(d_solver, *s.get()));
   }
-  d_idx = begin ? 0 : sels->size();
+  d_idx = begin ? 0 : sels.size();
 }
 
 DatatypeConstructor::const_iterator::const_iterator()
@@ -2283,7 +2345,7 @@ std::string DatatypeConstructor::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor(
+const CVC4::DTypeConstructor& DatatypeConstructor::getDatatypeConstructor(
     void) const
 {
   return *d_ctor;
@@ -2303,8 +2365,18 @@ DatatypeSelector DatatypeConstructor::getSelectorForName(
       break;
     }
   }
-  CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
-                           << getName() << " exists";
+  if (!foundSel)
+  {
+    std::stringstream snames;
+    snames << "{ ";
+    for (size_t i = 0, ncons = getNumSelectors(); i < ncons; i++)
+    {
+      snames << (*d_ctor)[i].getName() << " ";
+    }
+    snames << "} ";
+    CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
+                             << getName() << " exists among " << snames.str();
+  }
   return DatatypeSelector(d_solver, (*d_ctor)[index]);
 }
 
@@ -2316,15 +2388,23 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 
 /* Datatype ----------------------------------------------------------------- */
 
-Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype)
-    : d_solver(slv), d_dtype(new CVC4::Datatype(dtype))
+Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype)
+    : d_solver(slv), d_dtype(new CVC4::DType(dtype))
 {
   CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
 }
 
 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
 
-Datatype::~Datatype() {}
+Datatype::~Datatype()
+{
+  if (d_dtype != nullptr)
+  {
+    // ensure proper node manager is in scope
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_dtype.reset();
+  }
+}
 
 DatatypeConstructor Datatype::operator[](size_t idx) const
 {
@@ -2383,7 +2463,7 @@ Datatype::const_iterator Datatype::end() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; }
+const CVC4::DType& Datatype::getDatatype(void) const { return *d_dtype; }
 
 DatatypeConstructor Datatype::getConstructorForName(
     const std::string& name) const
@@ -2399,24 +2479,34 @@ DatatypeConstructor Datatype::getConstructorForName(
       break;
     }
   }
-  CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
-                            << getName() << " exists";
+  if (!foundCons)
+  {
+    std::stringstream snames;
+    snames << "{ ";
+    for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
+    {
+      snames << (*d_dtype)[i].getName() << " ";
+    }
+    snames << "}";
+    CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
+                              << getName() << " exists, among " << snames.str();
+  }
   return DatatypeConstructor(d_solver, (*d_dtype)[index]);
 }
 
 Datatype::const_iterator::const_iterator(const Solver* slv,
-                                         const CVC4::Datatype& dtype,
+                                         const CVC4::DType& dtype,
                                          bool begin)
-    : d_solver(slv), d_int_ctors(dtype.getConstructors())
+    : d_solver(slv), d_int_ctors(&dtype.getConstructors())
 {
-  const std::vector<CVC4::DatatypeConstructor>* cons =
-      static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
-  for (const auto& c : *cons)
+  const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
+      dtype.getConstructors();
+  for (const std::shared_ptr<DTypeConstructor>& c : cons)
   {
     /* Can not use emplace_back here since constructor is private. */
-    d_ctors.push_back(DatatypeConstructor(d_solver, c));
+    d_ctors.push_back(DatatypeConstructor(d_solver, *c.get()));
   }
-  d_idx = begin ? 0 : cons->size();
+  d_idx = begin ? 0 : cons.size();
 }
 
 Datatype::const_iterator::const_iterator()
@@ -2662,8 +2752,8 @@ Sort Grammar::resolve()
         Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
   }
 
-  std::vector<CVC4::Datatype> datatypes;
-  std::set<Type> unresTypes;
+  std::vector<CVC4::DType> datatypes;
+  std::set<TypeNode> unresTypes;
 
   datatypes.reserve(d_ntSyms.size());
 
@@ -2684,8 +2774,8 @@ Sort Grammar::resolve()
     }
 
     bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
-    Type btt = ntSym.d_node->getType().toType();
-    dtDecl.d_dtype->setSygus(btt, bvl.d_node->toExpr(), aci, false);
+    TypeNode btt = ntSym.d_node->getType();
+    dtDecl.d_dtype->setSygus(btt, *bvl.d_node, aci, false);
 
     // We can be in a case where the only rule specified was (Variable T)
     // and there are no variables of type T, in which case this is a bogus
@@ -2695,15 +2785,15 @@ Sort Grammar::resolve()
         << " produced an empty rule list";
 
     datatypes.push_back(*dtDecl.d_dtype);
-    unresTypes.insert(*ntsToUnres[ntSym].d_type);
+    unresTypes.insert(TypeNode::fromType(*ntsToUnres[ntSym].d_type));
   }
 
-  std::vector<DatatypeType> datatypeTypes =
-      d_solver->getExprManager()->mkMutualDatatypeTypes(
-          datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+  std::vector<TypeNode> datatypeTypes =
+      d_solver->getNodeManager()->mkMutualDatatypeTypes(
+          datatypes, unresTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
 
   // return is the first datatype
-  return Sort(d_solver, datatypeTypes[0]);
+  return Sort(d_solver, datatypeTypes[0].toType());
 }
 
 void Grammar::addSygusConstructorTerm(
@@ -2735,8 +2825,12 @@ void Grammar::addSygusConstructorTerm(
         d_solver->getExprManager()->mkExpr(
             CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
   }
-  dt.d_dtype->addSygusConstructor(
-      op.d_node->toExpr(), ssCName.str(), sortVectorToTypes(cargs));
+  std::vector<TypeNode> cargst;
+  for (const Sort& s : cargs)
+  {
+    cargst.push_back(TypeNode::fromType(s.getType()));
+  }
+  dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
 }
 
 Term Grammar::purifySygusGTerm(
@@ -2801,9 +2895,8 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
     {
       std::stringstream ss;
       ss << v;
-      std::vector<Sort> cargs;
-      dt.d_dtype->addSygusConstructor(
-          v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs));
+      std::vector<TypeNode> cargs;
+      dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs);
     }
   }
 }
@@ -3048,9 +3141,10 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
     std::vector<DatatypeDecl>& dtypedecls,
     std::set<Sort>& unresolvedSorts) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  std::vector<CVC4::Datatype> datatypes;
+  std::vector<CVC4::DType> datatypes;
   for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
@@ -3069,13 +3163,18 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   {
     CVC4_API_SOLVER_CHECK_SORT(sort);
   }
-  std::set<Type> utypes = sortSetToTypes(unresolvedSorts);
-  std::vector<CVC4::DatatypeType> dtypes =
-      d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes);
+  
+  std::set<TypeNode> utypes;
+  for (const Sort& s : unresolvedSorts)
+  {
+    utypes.insert(TypeNode::fromType(s.getType()));
+  }
+  std::vector<CVC4::TypeNode> dtypes =
+      getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
   std::vector<Sort> retTypes;
-  for (CVC4::DatatypeType t : dtypes)
+  for (CVC4::TypeNode t : dtypes)
   {
-    retTypes.push_back(Sort(this, t));
+    retTypes.push_back(Sort(this, t.toType()));
   }
   return retTypes;
 
@@ -3224,13 +3323,15 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 
 Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(this == dtypedecl.d_solver)
       << "Given datatype declaration is not associated with this solver";
   CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
       << "a datatype declaration with at least one constructor";
 
-  return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype));
+  return Sort(this,
+              getNodeManager()->mkDatatypeType(*dtypedecl.d_dtype).toType());
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3238,14 +3339,18 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
 std::vector<Sort> Solver::mkDatatypeSorts(
     std::vector<DatatypeDecl>& dtypedecls) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   std::set<Sort> unresolvedSorts;
   return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 std::vector<Sort> Solver::mkDatatypeSorts(std::vector<DatatypeDecl>& dtypedecls,
                                           std::set<Sort>& unresolvedSorts) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
@@ -3332,6 +3437,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
 Sort Solver::mkRecordSort(
     const std::vector<std::pair<std::string, Sort>>& fields) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   std::vector<std::pair<std::string, Type>> f;
   size_t i = 0;
@@ -3347,7 +3453,7 @@ Sort Solver::mkRecordSort(
     f.emplace_back(p.first, *p.second.d_type);
   }
 
-  return Sort(this, d_exprMgr->mkRecordType(Record(f)));
+  return Sort(this, getNodeManager()->mkRecordType(Record(f)).toType());
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3409,9 +3515,12 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
         !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
         << "non-function-like sort as parameter sort for tuple sort";
   }
-  std::vector<Type> types = sortVectorToTypes(sorts);
-
-  return Sort(this, d_exprMgr->mkTupleType(types));
+  std::vector<TypeNode> typeNodes;
+  for (const Sort& s : sorts)
+  {
+    typeNodes.push_back(TypeNode::fromType(*s.d_type));
+  }
+  return Sort(this, getNodeManager()->mkTupleType(typeNodes).toType());
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3789,6 +3898,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
 DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
     const std::string& name)
 {
+  NodeManagerScope scope(getNodeManager());
   return DatatypeConstructorDecl(this, name);
 }
 
@@ -3797,6 +3907,7 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
 
 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype)
 {
+  NodeManagerScope scope(getNodeManager());
   return DatatypeDecl(this, name, isCoDatatype);
 }
 
@@ -3804,6 +3915,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
                                     Sort param,
                                     bool isCoDatatype)
 {
+  NodeManagerScope scope(getNodeManager());
   return DatatypeDecl(this, name, param, isCoDatatype);
 }
 
@@ -3811,6 +3923,7 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
                                     const std::vector<Sort>& params,
                                     bool isCoDatatype)
 {
+  NodeManagerScope scope(getNodeManager());
   return DatatypeDecl(this, name, params, isCoDatatype);
 }
 
@@ -4018,6 +4131,7 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 Term Solver::mkTuple(const std::vector<Sort>& sorts,
                      const std::vector<Term>& terms) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(sorts.size() == terms.size())
       << "Expected the same number of sorts and elements";
@@ -4395,7 +4509,7 @@ Sort Solver::declareDatatype(
         << "datatype constructor declaration associated to this solver object";
     dtdecl.addConstructor(ctors[i]);
   }
-  return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
+  return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl.d_dtype).toType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 6c84b73bc..0c322d7da 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -40,9 +40,9 @@ template <bool ref_count>
 class NodeTemplate;
 typedef NodeTemplate<true> Node;
 class Expr;
-class Datatype;
-class DatatypeConstructor;
-class DatatypeConstructorArg;
+class DType;
+class DTypeConstructor;
+class DTypeSelector;
 class ExprManager;
 class GetAbductCommand;
 class GetInterpolCommand;
@@ -1242,6 +1242,11 @@ class CVC4_PUBLIC DatatypeConstructorDecl
   DatatypeConstructorDecl();
 
   /**
+   * Destructor.
+   */
+  ~DatatypeConstructorDecl();
+
+  /**
    * Add datatype selector declaration.
    * @param name the name of the datatype selector declaration to add
    * @param sort the range sort of the datatype selector declaration to add
@@ -1260,7 +1265,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
+  const CVC4::DTypeConstructor& getDatatypeConstructor(void) const;
 
  private:
   /**
@@ -1280,9 +1285,9 @@ class CVC4_PUBLIC DatatypeConstructorDecl
    * The internal (intermediate) datatype constructor wrapped by this
    * datatype constructor declaration.
    * This is a shared_ptr rather than a unique_ptr since
-   * CVC4::DatatypeConstructor is not ref counted.
+   * CVC4::DTypeConstructor is not ref counted.
    */
-  std::shared_ptr<CVC4::DatatypeConstructor> d_ctor;
+  std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
 };
 
 class Solver;
@@ -1333,7 +1338,7 @@ class CVC4_PUBLIC DatatypeDecl
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::Datatype& getDatatype(void) const;
+  CVC4::DType& getDatatype(void) const;
 
  private:
   /**
@@ -1386,10 +1391,10 @@ class CVC4_PUBLIC DatatypeDecl
 
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
-   * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
+   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
    * not ref counted.
    */
-  std::shared_ptr<CVC4::Datatype> d_dtype;
+  std::shared_ptr<CVC4::DType> d_dtype;
 };
 
 /**
@@ -1414,7 +1419,7 @@ class CVC4_PUBLIC DatatypeSelector
    * @param stor the internal datatype selector to be wrapped
    * @return the DatatypeSelector
    */
-  DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor);
+  DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor);
 
   /**
    * Destructor.
@@ -1440,7 +1445,7 @@ class CVC4_PUBLIC DatatypeSelector
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const;
+  CVC4::DTypeSelector getDatatypeConstructorArg(void) const;
 
  private:
   /**
@@ -1450,10 +1455,10 @@ class CVC4_PUBLIC DatatypeSelector
 
   /**
    * The internal datatype selector wrapped by this datatype selector.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
+   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
    * not ref counted.
    */
-  std::shared_ptr<CVC4::DatatypeConstructorArg> d_stor;
+  std::shared_ptr<CVC4::DTypeSelector> d_stor;
 };
 
 /**
@@ -1477,7 +1482,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param ctor the internal datatype constructor to be wrapped
    * @return the DatatypeConstructor
    */
-  DatatypeConstructor(const Solver* slv, const CVC4::DatatypeConstructor& ctor);
+  DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor);
 
   /**
    * Destructor.
@@ -1620,7 +1625,7 @@ class CVC4_PUBLIC DatatypeConstructor
      * @param true if this is a begin() iterator
      */
     const_iterator(const Solver* slv,
-                   const CVC4::DatatypeConstructor& ctor,
+                   const CVC4::DTypeConstructor& ctor,
                    bool begin);
 
     /**
@@ -1652,7 +1657,7 @@ class CVC4_PUBLIC DatatypeConstructor
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
+  const CVC4::DTypeConstructor& getDatatypeConstructor(void) const;
 
  private:
   /**
@@ -1669,10 +1674,10 @@ class CVC4_PUBLIC DatatypeConstructor
 
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
+   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
    * not ref counted.
    */
-  std::shared_ptr<CVC4::DatatypeConstructor> d_ctor;
+  std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
 };
 
 /*
@@ -1691,7 +1696,7 @@ class CVC4_PUBLIC Datatype
    * @param dtype the internal datatype to be wrapped
    * @return the Datatype
    */
-  Datatype(const Solver* slv, const CVC4::Datatype& dtype);
+  Datatype(const Solver* slv, const CVC4::DType& dtype);
 
   // Nullary constructor for Cython
   Datatype();
@@ -1835,7 +1840,7 @@ class CVC4_PUBLIC Datatype
      * @param dtype the internal datatype to iterate over
      * @param true if this is a begin() iterator
      */
-    const_iterator(const Solver* slv, const CVC4::Datatype& dtype, bool begin);
+    const_iterator(const Solver* slv, const CVC4::DType& dtype, bool begin);
 
     /**
      * The associated solver object.
@@ -1866,7 +1871,7 @@ class CVC4_PUBLIC Datatype
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  const CVC4::Datatype& getDatatype(void) const;
+  const CVC4::DType& getDatatype(void) const;
 
  private:
   /**
@@ -1883,10 +1888,10 @@ class CVC4_PUBLIC Datatype
 
   /**
    * The internal datatype wrapped by this datatype.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
+   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
    * not ref counted.
    */
-  std::shared_ptr<CVC4::Datatype> d_dtype;
+  std::shared_ptr<CVC4::DType> d_dtype;
 };
 
 /**
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 0092b78c6..8bc732314 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -73,8 +73,6 @@ libcvc4_add_sources(
   type_node.cpp
   type_node.h
   variable_type_map.h
-  datatype.h
-  datatype.cpp
   datatype_index.h
   datatype_index.cpp
   dtype.h
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
deleted file mode 100644
index a9ac3fbbf..000000000
--- a/src/expr/datatype.cpp
+++ /dev/null
@@ -1,970 +0,0 @@
-/*********************                                                        */
-/*! \file datatype.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A class representing a Datatype definition
- **
- ** A class representing a Datatype definition for the theory of
- ** inductive datatypes.
- **/
-#include "expr/datatype.h"
-
-#include <string>
-#include <sstream>
-
-#include "base/check.h"
-#include "expr/attribute.h"
-#include "expr/datatype.h"
-#include "expr/dtype.h"
-#include "expr/expr_manager.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/node.h"
-#include "expr/node_algorithm.h"
-#include "expr/node_manager.h"
-#include "expr/type.h"
-#include "expr/type_matcher.h"
-#include "options/datatypes_options.h"
-#include "options/set_language.h"
-#include "theory/type_enumerator.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-Datatype::~Datatype()
-{
-  ExprManagerScope ems(*d_em);
-  d_internal.reset();
-  d_constructors.clear();
-}
-
-Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
-    : d_em(em),
-      d_internal(nullptr),
-      d_record(NULL),
-      d_isRecord(false),
-      d_constructors()
-{
-  ExprManagerScope ems(*d_em);
-  d_internal = std::make_shared<DType>(name, isCo);
-}
-
-Datatype::Datatype(ExprManager* em,
-                   std::string name,
-                   const std::vector<Type>& params,
-                   bool isCo)
-    : d_em(em),
-      d_internal(nullptr),
-      d_record(NULL),
-      d_isRecord(false),
-      d_constructors()
-{
-  ExprManagerScope ems(*d_em);
-  std::vector<TypeNode> paramsn;
-  for (const Type& t : params)
-  {
-    paramsn.push_back(TypeNode::fromType(t));
-  }
-  d_internal = std::make_shared<DType>(name, paramsn, isCo);
-}
-
-const Datatype& Datatype::datatypeOf(Expr item) {
-  ExprManagerScope ems(item);
-  TypeNode t = Node::fromExpr(item).getType();
-  switch(t.getKind()) {
-  case kind::CONSTRUCTOR_TYPE:
-    return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype();
-  case kind::SELECTOR_TYPE:
-  case kind::TESTER_TYPE:
-    return DatatypeType(t[0].toType()).getDatatype();
-  default:
-    Unhandled() << "arg must be a datatype constructor, selector, or tester";
-  }
-}
-
-size_t Datatype::indexOf(Expr item) {
-  ExprManagerScope ems(item);
-  PrettyCheckArgument(item.getType().isConstructor() ||
-                item.getType().isTester() ||
-                item.getType().isSelector(),
-                item,
-                "arg must be a datatype constructor, selector, or tester");
-  return indexOfInternal(item);
-}
-
-size_t Datatype::indexOfInternal(Expr item)
-{
-  TNode n = Node::fromExpr(item);
-  if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
-    return indexOf( item[0] );
-  }else{
-    Assert(n.hasAttribute(DTypeIndexAttr()));
-    return n.getAttribute(DTypeIndexAttr());
-  }
-}
-
-size_t Datatype::cindexOf(Expr item) {
-  ExprManagerScope ems(item);
-  PrettyCheckArgument(item.getType().isSelector(),
-                item,
-                "arg must be a datatype selector");
-  return cindexOfInternal(item);
-}
-size_t Datatype::cindexOfInternal(Expr item)
-{
-  TNode n = Node::fromExpr(item);
-  if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
-    return cindexOf( item[0] );
-  }else{
-    Assert(n.hasAttribute(DTypeConsIndexAttr()));
-    return n.getAttribute(DTypeConsIndexAttr());
-  }
-}
-
-void Datatype::resolve(const std::map<std::string, DatatypeType>& resolutions,
-                       const std::vector<Type>& placeholders,
-                       const std::vector<Type>& replacements,
-                       const std::vector<SortConstructorType>& paramTypes,
-                       const std::vector<DatatypeType>& paramReplacements)
-{
-  PrettyCheckArgument(!isResolved(), this, "cannot resolve a Datatype twice");
-  PrettyCheckArgument(resolutions.find(getName()) != resolutions.end(),
-                      resolutions,
-                      "Datatype::resolve(): resolutions doesn't contain me!");
-  PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
-                "placeholders and replacements must be the same size");
-  PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
-                "paramTypes and paramReplacements must be the same size");
-  PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
-
-  // we're using some internals, so we have to make sure that the Datatype's
-  // ExprManager is active
-  ExprManagerScope ems(*d_em);
-
-  Trace("datatypes") << "Datatype::resolve: " << getName()
-                     << ", #placeholders=" << placeholders.size() << std::endl;
-
-  std::map<std::string, TypeNode> resolutionsn;
-  std::vector<TypeNode> placeholdersn;
-  std::vector<TypeNode> replacementsn;
-  std::vector<TypeNode> paramTypesn;
-  std::vector<TypeNode> paramReplacementsn;
-  for (const std::pair<const std::string, DatatypeType>& r : resolutions)
-  {
-    resolutionsn[r.first] = TypeNode::fromType(r.second);
-  }
-  for (const Type& t : placeholders)
-  {
-    placeholdersn.push_back(TypeNode::fromType(t));
-  }
-  for (const Type& t : replacements)
-  {
-    replacementsn.push_back(TypeNode::fromType(t));
-  }
-  for (const Type& t : paramTypes)
-  {
-    paramTypesn.push_back(TypeNode::fromType(t));
-  }
-  for (const Type& t : paramReplacements)
-  {
-    paramReplacementsn.push_back(TypeNode::fromType(t));
-  }
-  bool res = d_internal->resolve(resolutionsn,
-                                 placeholdersn,
-                                 replacementsn,
-                                 paramTypesn,
-                                 paramReplacementsn);
-  if (!res)
-  {
-    IllegalArgument(*this,
-                    "could not resolve datatype that is not well formed");
-  }
-  Trace("dt-debug") << "Datatype::resolve: finished " << getName() << " "
-                    << d_constructors.size() << std::endl;
-  AlwaysAssert(isResolved());
-  //
-  d_self = d_internal->getTypeNode().toType();
-  for (DatatypeConstructor& c : d_constructors)
-  {
-    AlwaysAssert(c.isResolved());
-    c.d_constructor = c.d_internal->getConstructor().toExpr();
-    for (size_t i = 0, nargs = c.getNumArgs(); i < nargs; i++)
-    {
-      AlwaysAssert(c.d_args[i].isResolved());
-      c.d_args[i].d_selector = c.d_args[i].d_internal->getSelector().toExpr();
-    }
-  }
-
-  if( d_isRecord ){
-    std::vector< std::pair<std::string, Type> > fields;
-    for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
-      fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
-    }
-    d_record.reset(new Record(fields));
-  }
-}
-
-void Datatype::addConstructor(const DatatypeConstructor& c) {
-  Trace("dt-debug") << "Datatype::addConstructor" << std::endl;
-  PrettyCheckArgument(
-      !isResolved(), this, "cannot add a constructor to a finalized Datatype");
-  d_constructors.push_back(c);
-  d_internal->addConstructor(c.d_internal);
-  Trace("dt-debug") << "Datatype::addConstructor: finished" << std::endl;
-}
-
-
-void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
-  PrettyCheckArgument(
-      !isResolved(), this, "cannot set sygus type to a finalized Datatype");
-  // We can be in a case where the only rule specified was
-  // (Constant T), in which case we have not yet added a constructor. We
-  // ensure an arbitrary constant is added in this case. We additionally
-  // add a constant if the grammar has only non-nullary constructors, since this
-  // ensures the datatype is well-founded (see 3423).
-  // Notice we only want to do this for sygus datatypes that are user-provided.
-  // At the moment, the condition !allow_all implies the grammar is
-  // user-provided and hence may require a default constant.
-  // TODO (https://github.com/CVC4/cvc4-projects/issues/38):
-  // In an API for SyGuS, it probably makes more sense for the user to
-  // explicitly add the "any constant" constructor with a call instead of
-  // passing a flag. This would make the block of code unnecessary.
-  if (allow_const && !allow_all)
-  {
-    // if i don't already have a constant (0-ary constructor)
-    bool hasConstant = false;
-    for (unsigned i = 0, ncons = getNumConstructors(); i < ncons; i++)
-    {
-      if ((*this)[i].getNumArgs() == 0)
-      {
-        hasConstant = true;
-        break;
-      }
-    }
-    if (!hasConstant)
-    {
-      // add an arbitrary one
-      Expr op = st.mkGroundTerm();
-      std::stringstream cname;
-      cname << op;
-      std::vector<Type> cargs;
-      addSygusConstructor(op, cname.str(), cargs);
-    }
-  }
-
-  TypeNode stn = TypeNode::fromType(st);
-  Node bvln = Node::fromExpr(bvl);
-  d_internal->setSygus(stn, bvln, allow_const, allow_all);
-}
-
-void Datatype::addSygusConstructor(Expr op,
-                                   const std::string& cname,
-                                   const std::vector<Type>& cargs,
-                                   int weight)
-{
-  // avoid name clashes
-  std::stringstream ss;
-  ss << getName() << "_" << getNumConstructors() << "_" << cname;
-  std::string name = ss.str();
-  unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
-  DatatypeConstructor c(name, cweight);
-  c.setSygus(op);
-  for( unsigned j=0; j<cargs.size(); j++ ){
-    Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
-    std::stringstream sname;
-    sname << name << "_" << j;
-    c.addArg(sname.str(), cargs[j]);
-  }
-  addConstructor(c);
-}
-
-void Datatype::addSygusConstructor(Kind k,
-                                   const std::string& cname,
-                                   const std::vector<Type>& cargs,
-                                   int weight)
-{
-  ExprManagerScope ems(*d_em);
-  Expr op = d_em->operatorOf(k);
-  addSygusConstructor(op, cname, cargs, weight);
-}
-
-void Datatype::setTuple() {
-  PrettyCheckArgument(
-      !isResolved(), this, "cannot set tuple to a finalized Datatype");
-  d_internal->setTuple();
-}
-
-void Datatype::setRecord() {
-  PrettyCheckArgument(
-      !isResolved(), this, "cannot set record to a finalized Datatype");
-  d_isRecord = true;
-  d_internal->setRecord();
-}
-
-Cardinality Datatype::getCardinality(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->getCardinality(tn);
-}
-
-Cardinality Datatype::getCardinality() const
-{
-  PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->getCardinality();
-}
-
-bool Datatype::isRecursiveSingleton(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->isRecursiveSingleton(tn);
-}
-
-bool Datatype::isRecursiveSingleton() const
-{
-  PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->isRecursiveSingleton();
-}
-
-unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
-{
-  Assert(isRecursiveSingleton(t));
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->getNumRecursiveSingletonArgTypes(tn);
-}
-
-unsigned Datatype::getNumRecursiveSingletonArgTypes() const
-{
-  PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->getNumRecursiveSingletonArgTypes();
-}
-
-Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
-{
-  Assert(isRecursiveSingleton(t));
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->getRecursiveSingletonArgType(tn, i).toType();
-}
-
-Type Datatype::getRecursiveSingletonArgType(unsigned i) const
-{
-  PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->getRecursiveSingletonArgType(i).toType();
-}
-
-bool Datatype::isFinite(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->isFinite(tn);
-}
-bool Datatype::isFinite() const
-{
-  PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->isFinite();
-}
-
-bool Datatype::isInterpretedFinite(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->isInterpretedFinite(tn);
-}
-bool Datatype::isInterpretedFinite() const
-{
-  PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
-  ExprManagerScope ems(d_self);
-  return d_internal->isInterpretedFinite();
-}
-
-bool Datatype::isWellFounded() const
-{
-  ExprManagerScope ems(d_self);
-  return d_internal->isWellFounded();
-}
-
-bool Datatype::hasNestedRecursion() const
-{
-  ExprManagerScope ems(d_self);
-  return d_internal->hasNestedRecursion();
-}
-
-Expr Datatype::mkGroundTerm(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  Node gterm = d_internal->mkGroundTerm(tn);
-  PrettyCheckArgument(
-      !gterm.isNull(),
-      this,
-      "datatype is not well-founded, cannot construct a ground term!");
-  return gterm.toExpr();
-}
-
-Expr Datatype::mkGroundValue(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  ExprManagerScope ems(d_self);
-  TypeNode tn = TypeNode::fromType(t);
-  Node gvalue = d_internal->mkGroundValue(tn);
-  PrettyCheckArgument(
-      !gvalue.isNull(),
-      this,
-      "datatype is not well-founded, cannot construct a ground value!");
-  return gvalue.toExpr();
-}
-
-DatatypeType Datatype::getDatatypeType() const
-{
-  PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  ExprManagerScope ems(d_self);
-  Type self = d_internal->getTypeNode().toType();
-  PrettyCheckArgument(!self.isNull(), *this);
-  return DatatypeType(self);
-}
-
-DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const
-{
-  PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  ExprManagerScope ems(d_self);
-  Type self = d_internal->getTypeNode().toType();
-  PrettyCheckArgument(!self.isNull() && DatatypeType(self).isParametric(),
-                      this);
-  return DatatypeType(self).instantiate(params);
-}
-
-bool Datatype::operator==(const Datatype& other) const
-{
-  // two datatypes are == iff the name is the same and they have
-  // exactly matching constructors (in the same order)
-
-  if(this == &other) {
-    return true;
-  }
-  return true;
-}
-
-const DatatypeConstructor& Datatype::operator[](size_t index) const {
-  PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
-  return d_constructors[index];
-}
-
-const DatatypeConstructor& Datatype::operator[](std::string name) const {
-  for(const_iterator i = begin(); i != end(); ++i) {
-    if((*i).getName() == name) {
-      return *i;
-    }
-  }
-  std::string dname = getName();
-  IllegalArgument(name,
-                  "No such constructor `%s' of datatype `%s'",
-                  name.c_str(),
-                  dname.c_str());
-}
-
-Expr Datatype::getConstructor(std::string name) const {
-  return (*this)[name].getConstructor();
-}
-
-Type Datatype::getSygusType() const {
-  return d_internal->getSygusType().toType();
-}
-
-Expr Datatype::getSygusVarList() const {
-  return d_internal->getSygusVarList().toExpr();
-}
-
-bool Datatype::getSygusAllowConst() const {
-  return d_internal->getSygusAllowConst();
-}
-
-bool Datatype::getSygusAllowAll() const {
-  return d_internal->getSygusAllowAll();
-}
-
-bool Datatype::involvesExternalType() const{
-  return d_internal->involvesExternalType();
-}
-
-bool Datatype::involvesUninterpretedType() const{
-  return d_internal->involvesUninterpretedType();
-}
-
-const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
-{
-  return &d_constructors;
-}
-
-DatatypeConstructor::DatatypeConstructor(std::string name, unsigned weight)
-    : d_internal(nullptr)
-{
-  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  d_internal = std::make_shared<DTypeConstructor>(name, weight);
-}
-
-void DatatypeConstructor::setSygus(Expr op)
-{
-  PrettyCheckArgument(
-      !isResolved(), this, "cannot modify a finalized Datatype constructor");
-  Node opn = Node::fromExpr(op);
-  d_internal->setSygus(op);
-}
-
-const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
-    const
-{
-  return &d_args;
-}
-
-void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
-  // We don't want to introduce a new data member, because eventually
-  // we're going to be a constant stuffed inside a node.  So we stow
-  // the selector type away inside a var until resolution (when we can
-  // create the proper selector type)
-  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
-
-  // we're using some internals, so we have to set up this library context
-  ExprManagerScope ems(selectorType);
-
-  Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-  Debug("datatypes") << type << endl;
-  d_args.push_back(DatatypeConstructorArg(selectorName, type));
-  d_internal->addArg(d_args.back().d_internal);
-}
-
-void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
-  // We don't want to introduce a new data member, because eventually
-  // we're going to be a constant stuffed inside a node.  So we stow
-  // the selector type away after a NUL in the name string until
-  // resolution (when we can create the proper selector type)
-  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
-  d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
-  d_internal->addArg(d_args.back().d_internal);
-}
-
-void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
-  // We don't want to introduce a new data member, because eventually
-  // we're going to be a constant stuffed inside a node.  So we mark
-  // the name string with a NUL to indicate that we have a
-  // self-selecting selector until resolution (when we can create the
-  // proper selector type)
-  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
-  d_internal->addArg(d_args.back().d_internal);
-}
-
-std::string DatatypeConstructor::getName() const
-{
-  return d_internal->getName();
-}
-
-Expr DatatypeConstructor::getConstructor() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_constructor;
-}
-
-Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type");
-  ExprManagerScope ems(d_constructor);
-  TypeNode tn = TypeNode::fromType(returnType);
-  return d_internal->getSpecializedConstructorType(tn).toType();
-}
-
-Expr DatatypeConstructor::getTester() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  return d_internal->getTester().toExpr();
-}
-
-Expr DatatypeConstructor::getSygusOp() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  return d_internal->getSygusOp().toExpr();
-}
-
-bool DatatypeConstructor::isSygusIdFunc() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  return d_internal->isSygusIdFunc();
-}
-
-unsigned DatatypeConstructor::getWeight() const
-{
-  PrettyCheckArgument(
-      isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  return d_internal->getWeight();
-}
-
-Cardinality DatatypeConstructor::getCardinality(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->getCardinality(tn);
-}
-
-bool DatatypeConstructor::isFinite(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->isFinite(tn);
-}
-
-bool DatatypeConstructor::isInterpretedFinite(Type t) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  ExprManagerScope ems(d_constructor);
-  TypeNode tn = TypeNode::fromType(t);
-  return d_internal->isInterpretedFinite(tn);
-}
-
-const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
-  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
-  return d_args[index];
-}
-
-const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
-  for(const_iterator i = begin(); i != end(); ++i) {
-    if((*i).getName() == name) {
-      return *i;
-    }
-  }
-  std::string dname = getName();
-  IllegalArgument(name,
-                  "No such arg `%s' of constructor `%s'",
-                  name.c_str(),
-                  dname.c_str());
-}
-
-Expr DatatypeConstructor::getSelector(std::string name) const {
-  return (*this)[name].d_selector;
-}
-
-Type DatatypeConstructor::getArgType(unsigned index) const
-{
-  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
-  ExprManagerScope ems(d_constructor);
-  return d_internal->getArgType(index).toType();
-}
-
-bool DatatypeConstructor::involvesExternalType() const{
-  ExprManagerScope ems(d_constructor);
-  return d_internal->involvesExternalType();
-}
-
-bool DatatypeConstructor::involvesUninterpretedType() const{
-  ExprManagerScope ems(d_constructor);
-  return d_internal->involvesUninterpretedType();
-}
-
-DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
-    : d_internal(nullptr)
-{
-  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
-  d_internal = std::make_shared<DTypeSelector>(name, Node::fromExpr(selector));
-}
-
-std::string DatatypeConstructorArg::getName() const
-{
-  string name = d_internal->getName();
-  const size_t nul = name.find('\0');
-  if(nul != string::npos) {
-    name.resize(nul);
-  }
-  return name;
-}
-
-Expr DatatypeConstructorArg::getSelector() const {
-  PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
-  return d_selector;
-}
-
-Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const {
-  PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor");
-  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
-  ExprManagerScope ems(d_constructor);
-  TypeNode dtn = TypeNode::fromType(domainType);
-  return d_internal->getSelectorInternal(dtn, index).toExpr();
-}
-
-int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
-  PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
-  ExprManagerScope ems(d_constructor);
-  Node seln = Node::fromExpr(sel);
-  return d_internal->getSelectorIndexInternal(seln);
-}
-
-Expr DatatypeConstructorArg::getConstructor() const {
-  PrettyCheckArgument(isResolved(), this,
-                "cannot get a associated constructor for argument of an unresolved datatype constructor");
-  ExprManagerScope ems(d_selector);
-  return d_internal->getConstructor().toExpr();
-}
-
-SelectorType DatatypeConstructorArg::getType() const {
-  return d_selector.getType();
-}
-
-Type DatatypeConstructorArg::getRangeType() const {
-  return getType().getRangeType();
-}
-
-bool DatatypeConstructorArg::isUnresolvedSelf() const
-{
-  return d_selector.isNull();
-}
-
-bool DatatypeConstructorArg::isResolved() const
-{
-  // We could just write:
-  //
-  //   return !d_selector.isNull() && d_selector.getType().isSelector();
-  //
-  // HOWEVER, this causes problems in ExprManager tear-down, because
-  // the attributes are removed before the pool is purged.  When the
-  // pool is purged, this triggers an equality test between Datatypes,
-  // and this triggers a call to isResolved(), which breaks because
-  // d_selector has no type after attributes are stripped.
-  //
-  // This problem, coupled with the fact that this function is called
-  // _often_, means we should just use a boolean flag.
-  //
-  return d_internal->isResolved();
-}
-
-std::ostream& operator<<(std::ostream& os, const Datatype& dt)
-{
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
-  dt.toStream(os);
-  return os;
-}
-
-void Datatype::toStream(std::ostream& out) const
-{
-  out << "DATATYPE " << getName();
-  if (isParametric())
-  {
-    out << '[';
-    for (size_t i = 0; i < getNumParameters(); ++i)
-    {
-      if(i > 0) {
-        out << ',';
-      }
-      out << getParameter(i);
-    }
-    out << ']';
-  }
-  out << " =" << endl;
-  Datatype::const_iterator i = begin(), i_end = end();
-  if(i != i_end) {
-    out << "  ";
-    do {
-      out << *i << endl;
-      if(++i != i_end) {
-        out << "| ";
-      }
-    } while(i != i_end);
-  }
-  out << "END;" << endl;
-}
-
-std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
-  ctor.toStream(os);
-  return os;
-}
-
-void DatatypeConstructor::toStream(std::ostream& out) const
-{
-  out << getName();
-
-  DatatypeConstructor::const_iterator i = begin(), i_end = end();
-  if(i != i_end) {
-    out << "(";
-    do {
-      out << *i;
-      if(++i != i_end) {
-        out << ", ";
-      }
-    } while(i != i_end);
-    out << ")";
-  }
-}
-
-std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
-  arg.toStream(os);
-  return os;
-}
-
-void DatatypeConstructorArg::toStream(std::ostream& out) const
-{
-  std::string name = getName();
-  out << name << ": ";
-
-  Type t;
-  if (isResolved())
-  {
-    t = getRangeType();
-  }
-  else if (d_selector.isNull())
-  {
-    string typeName = name.substr(name.find('\0') + 1);
-    out << ((typeName == "") ? "[self]" : typeName);
-    return;
-  }
-  else
-  {
-    t = d_selector.getType();
-  }
-  out << t;
-}
-
-std::string Datatype::getName() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->getName();
-}
-size_t Datatype::getNumConstructors() const { return d_constructors.size(); }
-
-bool Datatype::isParametric() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->isParametric();
-}
-size_t Datatype::getNumParameters() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->getNumParameters();
-}
-Type Datatype::getParameter(unsigned int i) const
-{
-  CheckArgument(isParametric(),
-                this,
-                "Cannot get type parameter of a non-parametric datatype.");
-  CheckArgument(i < getNumParameters(),
-                i,
-                "Type parameter index out of range for datatype.");
-  ExprManagerScope ems(*d_em);
-  return d_internal->getParameter(i).toType();
-}
-
-std::vector<Type> Datatype::getParameters() const
-{
-  CheckArgument(isParametric(),
-                this,
-                "Cannot get type parameters of a non-parametric datatype.");
-  std::vector<Type> params;
-  std::vector<TypeNode> paramsn = d_internal->getParameters();
-  // convert to type
-  for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++)
-  {
-    params.push_back(paramsn[i].toType());
-  }
-  return params;
-}
-
-bool Datatype::isCodatatype() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->isCodatatype();
-}
-
-bool Datatype::isSygus() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->isSygus();
-}
-
-bool Datatype::isTuple() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->isTuple();
-}
-
-bool Datatype::isRecord() const { return d_isRecord; }
-
-Record* Datatype::getRecord() const { return d_record.get(); }
-bool Datatype::operator!=(const Datatype& other) const
-{
-  return !(*this == other);
-}
-
-bool Datatype::isResolved() const
-{
-  ExprManagerScope ems(*d_em);
-  return d_internal->isResolved();
-}
-Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); }
-
-Datatype::iterator Datatype::end() { return iterator(d_constructors, false); }
-
-Datatype::const_iterator Datatype::begin() const
-{
-  return const_iterator(d_constructors, true);
-}
-
-Datatype::const_iterator Datatype::end() const
-{
-  return const_iterator(d_constructors, false);
-}
-
-bool DatatypeConstructor::isResolved() const
-{
-  return d_internal->isResolved();
-}
-
-size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
-
-DatatypeConstructor::iterator DatatypeConstructor::begin()
-{
-  return iterator(d_args, true);
-}
-
-DatatypeConstructor::iterator DatatypeConstructor::end()
-{
-  return iterator(d_args, false);
-}
-
-DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
-{
-  return const_iterator(d_args, true);
-}
-
-DatatypeConstructor::const_iterator DatatypeConstructor::end() const
-{
-  return const_iterator(d_args, false);
-}
-}/* CVC4 namespace */
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
deleted file mode 100644
index 0deb20d8f..000000000
--- a/src/expr/datatype.h
+++ /dev/null
@@ -1,933 +0,0 @@
-/*********************                                                        */
-/*! \file datatype.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A class representing a Datatype definition
- **
- ** A class representing a Datatype definition for the theory of
- ** inductive datatypes.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__DATATYPE_H
-#define CVC4__DATATYPE_H
-
-#include <functional>
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-
-namespace CVC4 {
-  // messy; Expr needs Datatype (because it's the payload of a
-  // CONSTANT-kinded expression), and Datatype needs Expr.
-  //class CVC4_PUBLIC Datatype;
-  class CVC4_PUBLIC DatatypeIndexConstant;
-}/* CVC4 namespace */
-
-#include "base/exception.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/datatype_index.h"
-#include "util/hash.h"
-
-
-namespace CVC4 {
-
-class CVC4_PUBLIC ExprManager;
-
-class CVC4_PUBLIC DatatypeConstructor;
-class CVC4_PUBLIC DatatypeConstructorArg;
-
-class CVC4_PUBLIC DatatypeConstructorIterator {
-  const std::vector<DatatypeConstructor>* d_v;
-  size_t d_i;
-
-  friend class Datatype;
-
-  DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
-  }
-
-public:
-  typedef const DatatypeConstructor& value_type;
-  const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; }
-  const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; }
-  DatatypeConstructorIterator& operator++() { ++d_i; return *this; }
-  DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; }
-  bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
-  bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
-};/* class DatatypeConstructorIterator */
-
-class CVC4_PUBLIC DatatypeConstructorArgIterator {
-  const std::vector<DatatypeConstructorArg>* d_v;
-  size_t d_i;
-
-  friend class DatatypeConstructor;
-
-  DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
-  }
-
-public:
-  typedef const DatatypeConstructorArg& value_type;
-  const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; }
-  const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; }
-  DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; }
-  DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; }
-  bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
-  bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
-};/* class DatatypeConstructorArgIterator */
-
-/**
- * An exception that is thrown when a datatype resolution fails.
- */
-class CVC4_PUBLIC DatatypeResolutionException : public Exception {
- public:
-  inline DatatypeResolutionException(std::string msg);
-};/* class DatatypeResolutionException */
-
-/**
- * A holder type (used in calls to DatatypeConstructor::addArg())
- * to allow a Datatype to refer to itself.  Self-typed fields of
- * Datatypes will be properly typed when a Type is created for the
- * Datatype by the ExprManager (which calls Datatype::resolve()).
- */
-class CVC4_PUBLIC DatatypeSelfType {
-};/* class DatatypeSelfType */
-
-class DTypeSelector;
-
-/**
- * An unresolved type (used in calls to
- * DatatypeConstructor::addArg()) to allow a Datatype to refer to
- * itself or to other mutually-recursive Datatypes.  Unresolved-type
- * fields of Datatypes will be properly typed when a Type is created
- * for the Datatype by the ExprManager (which calls
- * Datatype::resolve()).
- */
-class CVC4_PUBLIC DatatypeUnresolvedType {
-  std::string d_name;
-public:
-  inline DatatypeUnresolvedType(std::string name);
-  inline std::string getName() const;
-};/* class DatatypeUnresolvedType */
-
-/**
- * A Datatype constructor argument (i.e., a Datatype field).
- */
-class CVC4_PUBLIC DatatypeConstructorArg {
-  friend class DatatypeConstructor;
-  friend class Datatype;
-
- public:
-  /** Get the name of this constructor argument. */
-  std::string getName() const;
-
-  /**
-   * Get the selector for this constructor argument; this call is
-   * only permitted after resolution.
-   */
-  Expr getSelector() const;
-
-  /**
-   * Get the associated constructor for this constructor argument;
-   * this call is only permitted after resolution.
-   */
-  Expr getConstructor() const;
-
-  /**
-   * Get the type of the selector for this constructor argument;
-   * this call is only permitted after resolution.
-   */
-  SelectorType getType() const;
-
-  /**
-   * Get the range type of this argument.
-   */
-  Type getRangeType() const;
-
-  /**
-   * Returns true iff this constructor argument has been resolved.
-   */
-  bool isResolved() const;
-
-  /** prints this datatype constructor argument to stream */
-  void toStream(std::ostream& out) const;
-
- private:
-  /** The internal representation */
-  std::shared_ptr<DTypeSelector> d_internal;
-  /** The selector */
-  Expr d_selector;
-  /** is this selector unresolved? */
-  bool isUnresolvedSelf() const;
-  /** constructor */
-  DatatypeConstructorArg(std::string name, Expr selector);
-};/* class DatatypeConstructorArg */
-
-class DTypeConstructor;
-
-/**
- * A constructor for a Datatype.
- */
-class CVC4_PUBLIC DatatypeConstructor {
-  friend class Datatype;
-
- public:
-  /** The type for iterators over constructor arguments. */
-  typedef DatatypeConstructorArgIterator iterator;
-  /** The (const) type for iterators over constructor arguments. */
-  typedef DatatypeConstructorArgIterator const_iterator;
-
-  /**
-   * Create a new Datatype constructor with the given name for the
-   * constructor.  The actual constructor and tester (meaning, the Exprs
-   * representing operators for these entities) aren't created until
-   * resolution time.
-   * weight is the value that this constructor carries when computing size.
-   * For example, if A, B, C have weights 0, 1, and 3 respectively, then
-   * C( B( A() ), B( A() ) ) has size 5.
-   */
-  explicit DatatypeConstructor(std::string name, unsigned weight = 1);
-
-  ~DatatypeConstructor() {}
-  /**
-   * Add an argument (i.e., a data field) of the given name and type
-   * to this Datatype constructor.  Selector names need not be unique;
-   * they are for convenience and pretty-printing only.
-   */
-  void addArg(std::string selectorName, Type selectorType);
-
-  /**
-   * Add an argument (i.e., a data field) of the given name to this
-   * Datatype constructor that refers to an as-yet-unresolved
-   * Datatype (which may be mutually-recursive).  Selector names need
-   * not be unique; they are for convenience and pretty-printing only.
-   */
-  void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
-
-  /**
-   * Add a self-referential (i.e., a data field) of the given name
-   * to this Datatype constructor that refers to the enclosing
-   * Datatype.  For example, using the familiar "nat" Datatype, to
-   * create the "pred" field for "succ" constructor, one uses
-   * succ::addArg("pred", DatatypeSelfType())---the actual Type
-   * cannot be passed because the Datatype is still under
-   * construction.  Selector names need not be unique; they are for
-   * convenience and pretty-printing only.
-   *
-   * This is a special case of
-   * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType).
-   */
-  void addArg(std::string selectorName, DatatypeSelfType);
-
-  /** Get the name of this Datatype constructor. */
-  std::string getName() const;
-
-  /**
-   * Get the constructor operator of this Datatype constructor.  The
-   * Datatype must be resolved.
-   */
-  Expr getConstructor() const;
-
-  /**
-   * Get the tester operator of this Datatype constructor.  The
-   * Datatype must be resolved.
-   */
-  Expr getTester() const;
-
-  /** get sygus op
-   *
-   * This method returns the operator or
-   * term that this constructor represents
-   * in the sygus encoding. This may be a
-   * builtin operator, defined function, variable,
-   * or constant that this constructor encodes in this
-   * deep embedding.
-   */
-  Expr getSygusOp() const;
-  /** is this a sygus identity function?
-   *
-   * This returns true if the sygus operator of this datatype constructor is
-   * of the form (lambda (x) x).
-   */
-  bool isSygusIdFunc() const;
-  /** get weight
-   *
-   * Get the weight of this constructor. This value is used when computing the
-   * size of datatype terms that involve this constructor.
-   */
-  unsigned getWeight() const;
-
-  /**
-   * Get the number of arguments (so far) of this Datatype constructor.
-   */
-  size_t getNumArgs() const;
-
-  /**
-   * Get the specialized constructor type for a parametric
-   * constructor; this call is only permitted after resolution.
-   * Given a (concrete) returnType, the constructor's concrete
-   * type in this parametric datatype is returned.
-   *
-   * For instance, if the datatype is list[T], with constructor
-   * "cons[T]" of type "T -> list[T] -> list[T]", then calling
-   * this function with "list[int]" will return the concrete
-   * "cons" constructor type for lists of int---namely,
-   * "int -> list[int] -> list[int]".
-   */
-  Type getSpecializedConstructorType(Type returnType) const;
-
-  /**
-   * Return the cardinality of this constructor (the product of the
-   * cardinalities of its arguments).
-   */
-  Cardinality getCardinality(Type t) const;
-
-  /**
-   * Return true iff this constructor is finite (it is nullary or
-   * each of its argument types are finite).  This function can
-   * only be called for resolved constructors.
-   */
-  bool isFinite(Type t) const;
-  /**
-   * Return true iff this constructor is finite (it is nullary or
-   * each of its argument types are finite) under assumption
-   * uninterpreted sorts are finite.  This function can
-   * only be called for resolved constructors.
-   */
-  bool isInterpretedFinite(Type t) const;
-
-  /**
-   * Returns true iff this Datatype constructor has already been
-   * resolved.
-   */
-  bool isResolved() const;
-
-  /** Get the beginning iterator over DatatypeConstructor args. */
-  iterator begin();
-  /** Get the ending iterator over DatatypeConstructor args. */
-  iterator end();
-  /** Get the beginning const_iterator over DatatypeConstructor args. */
-  const_iterator begin() const;
-  /** Get the ending const_iterator over DatatypeConstructor args. */
-  const_iterator end() const;
-
-  /** Get the ith DatatypeConstructor arg. */
-  const DatatypeConstructorArg& operator[](size_t index) const;
-
-  /**
-   * Get the DatatypeConstructor arg named.  This is a linear search
-   * through the arguments, so in the case of multiple,
-   * similarly-named arguments, the first is returned.
-   */
-  const DatatypeConstructorArg& operator[](std::string name) const;
-
-  /**
-   * Get the selector named.  This is a linear search
-   * through the arguments, so in the case of multiple,
-   * similarly-named arguments, the selector for the first
-   * is returned.
-   */
-  Expr getSelector(std::string name) const;
-  /**
-   * Get argument type. Returns the return type of the i^th selector of this
-   * constructor.
-   */
-  Type getArgType(unsigned i) const;
-
-  /** get selector internal
-   *
-   * This gets selector for the index^th argument
-   * of this constructor. The type dtt is the datatype
-   * type whose datatype is the owner of this constructor,
-   * where this type may be an instantiated parametric datatype.
-   *
-   * If shared selectors are enabled,
-   * this returns a shared (constructor-agnotic) selector, which
-   * in the terminology of "Datatypes with Shared Selectors", is:
-   *   sel_{dtt}^{T,atos(T,C,index)}
-   * where C is this constructor, and T is the type
-   * of the index^th field of this constructor.
-   * The semantics of sel_{dtt}^{T,n}( t ) is the n^th field of
-   * type T of constructor term t if one exists, or is
-   * unconstrained otherwise.
-   */
-  Expr getSelectorInternal(Type dtt, size_t index) const;
-
-  /** get selector index internal
-   *
-   * This gets the argument number of this constructor
-   * that the selector sel accesses. It returns -1 if the
-   * selector sel is not a selector for this constructor.
-   *
-   * In the terminology of "Datatypes with Shared Selectors",
-   * if sel is sel_{dtt}^{T,index} for some (T, index), where
-   * dtt is the datatype type whose datatype is the owner
-   * of this constructor, then this method returns
-   *   stoa(T,C,index)
-   */
-  int getSelectorIndexInternal( Expr sel ) const;
-
-  /** involves external type
-   *
-   * Get whether this constructor has a subfield
-   * in any constructor that is not a datatype type.
-   */
-  bool involvesExternalType() const;
-  /** involves external type
-   *
-   * Get whether this constructor has a subfield
-   * in any constructor that is an uninterpreted type.
-   */
-  bool involvesUninterpretedType() const;
-
-  /** set sygus
-   *
-   * Set that this constructor is a sygus datatype constructor that encodes
-   * operator op. spc is the sygus callback of this datatype constructor,
-   * which is stored in a shared pointer.
-   */
-  void setSygus(Expr op);
-
-  /**
-   * Get the list of arguments to this constructor.
-   */
-  const std::vector<DatatypeConstructorArg>* getArgs() const;
-
-  /** prints this datatype constructor to stream */
-  void toStream(std::ostream& out) const;
-
- private:
-  /** The internal representation */
-  std::shared_ptr<DTypeConstructor> d_internal;
-  /** The constructor */
-  Expr d_constructor;
-  /** the arguments of this constructor */
-  std::vector<DatatypeConstructorArg> d_args;
-};/* class DatatypeConstructor */
-
-class DType;
-
-/**
- * The representation of an inductive datatype.
- *
- * This is far more complicated than it first seems.  Consider this
- * datatype definition:
- *
- *   DATATYPE nat =
- *     succ(pred: nat)
- *   | zero
- *   END;
- *
- * You cannot define "nat" until you have a Type for it, but you
- * cannot have a Type for it until you fill in the type of the "pred"
- * selector, which needs the Type.  So we have a chicken-and-egg
- * problem.  It's even more complicated when we have mutual recursion
- * between datatypes, since the CVC presentation language does not
- * require forward-declarations.  Here, we define trees of lists that
- * contain trees of lists (etc):
- *
- *   DATATYPE
- *     tree = node(left: tree, right: tree) | leaf(list),
- *     list = cons(car: tree, cdr: list) | nil
- *   END;
- *
- * Note that while parsing the "tree" definition, we have to take it
- * on faith that "list" is a valid type.  We build Datatype objects to
- * describe "tree" and "list", and their constructors and constructor
- * arguments, but leave any unknown types (including self-references)
- * in an "unresolved" state.  After parsing the whole DATATYPE block,
- * we create a DatatypeType through
- * ExprManager::mkMutualDatatypeTypes().  The ExprManager creates a
- * DatatypeType for each, but before "releasing" this type into the
- * wild, it does a round of in-place "resolution" on each Datatype by
- * calling Datatype::resolve() with a map of string -> DatatypeType to
- * allow the datatype to construct the necessary testers and
- * selectors.
- *
- * An additional point to make is that we want to ease the burden on
- * both the parser AND the users of the CVC4 API, so this class takes
- * on the task of generating its own selectors and testers, for
- * instance.  That means that, after reifying the Datatype with the
- * ExprManager, the parser needs to go through the (now-resolved)
- * Datatype and request the constructor, selector, and tester terms.
- * See src/parser/parser.cpp for how this is done.  For API usage
- * ideas, see test/unit/util/datatype_black.h.
- *
- * Datatypes may also be defined parametrically, such as this example:
- *
- *  DATATYPE
- *    list[T] = cons(car : T, cdr : list[T]) | null,
- *    tree = node(children : list[tree]) | leaf
- *  END;
- *
- * Here, the definition of the parametric datatype list, where T is a type variable.
- * In other words, this defines a family of types list[C] where C is any concrete
- * type.  Datatypes can be parameterized over multiple type variables using the
- * syntax sym[ T1, ..., Tn ] = ...,
- *
- */
-class CVC4_PUBLIC Datatype {
-  friend class DatatypeConstructor;
-  friend class ExprManager;  // for access to resolve()
-  friend class NodeManager;  // temporary, for access to d_internal
- public:
-  /**
-   * Get the datatype of a constructor, selector, or tester operator.
-   */
-  static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
-
-  /**
-   * Get the index of a constructor or tester in its datatype, or the
-   * index of a selector in its constructor.  (Zero is always the
-   * first index.)
-   */
-  static size_t indexOf(Expr item) CVC4_PUBLIC;
-
-  /**
-   * Get the index of constructor corresponding to selector.  (Zero is
-   * always the first index.)
-   */
-  static size_t cindexOf(Expr item) CVC4_PUBLIC;
-
-  /**
-   * Same as above, but without checks. These methods should be used by
-   * internal (Node-level) code.
-   */
-  static size_t indexOfInternal(Expr item);
-  static size_t cindexOfInternal(Expr item);
-
-  /** The type for iterators over constructors. */
-  typedef DatatypeConstructorIterator iterator;
-  /** The (const) type for iterators over constructors. */
-  typedef DatatypeConstructorIterator const_iterator;
-
-  /** Create a new Datatype of the given name. */
-  explicit Datatype(ExprManager* em, std::string name, bool isCo = false);
-
-  /**
-   * Create a new Datatype of the given name, with the given
-   * parameterization.
-   */
-  Datatype(ExprManager* em,
-           std::string name,
-           const std::vector<Type>& params,
-           bool isCo = false);
-
-  ~Datatype();
-
-  /** Add a constructor to this Datatype.
-   *
-   * Notice that constructor names need not
-   * be unique; they are for convenience and pretty-printing only.
-   */
-  void addConstructor(const DatatypeConstructor& c);
-
-  /** set sygus
-   *
-   * This marks this datatype as a sygus datatype.
-   * A sygus datatype is one that represents terms of type st
-   * via a deep embedding described in Section 4 of
-   * Reynolds et al. CAV 2015. We say that this sygus datatype
-   * "encodes" its sygus type st in the following.
-   *
-   * st : the type this datatype encodes (this can be Int, Bool, etc.),
-   * bvl : the list of arguments for the synth-fun
-   * allow_const : whether all constants are (implicitly) allowed by the
-   * datatype
-   * allow_all : whether all terms are (implicitly) allowed by the datatype
-   *
-   * Notice that allow_const/allow_all do not reflect the constructors
-   * for this datatype, and instead are used solely for relaxing constraints
-   * when doing solution reconstruction (Figure 5 of Reynolds et al.
-   * CAV 2015).
-   */
-  void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
-  /** add sygus constructor
-   *
-   * This adds a sygus constructor to this datatype, where
-   * this datatype should be currently unresolved.
-   *
-   * op : the builtin operator, constant, or variable that
-   *      this constructor encodes
-   * cname : the name of the constructor (for printing only)
-   * cargs : the arguments of the constructor
-   *
-   * It should be the case that cargs are sygus datatypes that
-   * encode the arguments of op. For example, a sygus constructor
-   * with op = PLUS should be such that cargs.size()>=2 and
-   * the sygus type of cargs[i] is Real/Int for each i.
-   *
-   * weight denotes the value added by the constructor when computing the size
-   * of datatype terms. Passing a value <0 denotes the default weight for the
-   * constructor, which is 0 for nullary constructors and 1 for non-nullary
-   * constructors.
-   */
-  void addSygusConstructor(Expr op,
-                           const std::string& cname,
-                           const std::vector<Type>& cargs,
-                           int weight = -1);
-  /**
-   * Same as above, with builtin kind k.
-   */
-  void addSygusConstructor(Kind k,
-                           const std::string& cname,
-                           const std::vector<Type>& cargs,
-                           int weight = -1);
-
-  /** set that this datatype is a tuple */
-  void setTuple();
-
-  /** set that this datatype is a record */
-  void setRecord();
-
-  /** Get the name of this Datatype. */
-  std::string getName() const;
-
-  /** Get the number of constructors (so far) for this Datatype. */
-  size_t getNumConstructors() const;
-
-  /** Is this datatype parametric? */
-  bool isParametric() const;
-
-  /** Get the nubmer of type parameters */
-  size_t getNumParameters() const;
-
-  /** Get parameter */
-  Type getParameter(unsigned int i) const;
-
-  /** Get parameters */
-  std::vector<Type> getParameters() const;
-
-  /** is this a co-datatype? */
-  bool isCodatatype() const;
-
-  /** is this a sygus datatype? */
-  bool isSygus() const;
-
-  /** is this a tuple datatype? */
-  bool isTuple() const;
-
-  /** is this a record datatype? */
-  bool isRecord() const;
-
-  /** get the record representation for this datatype */
-  Record* getRecord() const;
-
-  /**
-   * Return the cardinality of this datatype.
-   * The Datatype must be resolved.
-   *
-   * The version of this method that takes Type t is required
-   * for parametric datatypes, where t is an instantiated
-   * parametric datatype type whose datatype is this class.
-   */
-  Cardinality getCardinality(Type t) const;
-  Cardinality getCardinality() const;
-
-  /**
-   * Return true iff this Datatype has finite cardinality. If the
-   * datatype is not well-founded, this method returns false. The
-   * Datatype must be resolved or an exception is thrown.
-   *
-   * The version of this method that takes Type t is required
-   * for parametric datatypes, where t is an instantiated
-   * parametric datatype type whose datatype is this class.
-   */
-  bool isFinite(Type t) const;
-  bool isFinite() const;
-
-  /**
-   * Return true iff this  Datatype is finite (all constructors are
-   * finite, i.e., there  are finitely  many ground terms) under the
-   * assumption unintepreted sorts are finite. If the
-   * datatype is  not well-founded, this method returns false.  The
-   * Datatype must be resolved or an exception is thrown.
-   *
-   * The versions of these methods that takes Type t is required
-   * for parametric datatypes, where t is an instantiated
-   * parametric datatype type whose datatype is this class.
-   */
-  bool isInterpretedFinite(Type t) const;
-  bool isInterpretedFinite() const;
-
-  /** is well-founded
-   *
-   * Return true iff this datatype is well-founded (there exist finite
-   * values of this type).
-   * This datatype must be resolved or an exception is thrown.
-   */
-  bool isWellFounded() const;
-  /** has nested recursion
-   *
-   * Return true iff this datatype has nested recursion.
-   * This datatype must be resolved or an exception is thrown.
-   */
-  bool hasNestedRecursion() const;
-
-  /** is recursive singleton
-   *
-   * Return true iff this datatype is a recursive singleton
-   * (a recursive singleton is a recursive datatype with only
-   * one infinite value). For details, see Reynolds et al. CADE 2015.
-   *
-   * The versions of these methods that takes Type t is required
-   * for parametric datatypes, where t is an instantiated
-   * parametric datatype type whose datatype is this class.
-   */
-  bool isRecursiveSingleton(Type t) const;
-  bool isRecursiveSingleton() const;
-
-  /** recursive single arguments
-   *
-   * Get recursive singleton argument types (uninterpreted sorts that the
-   * cardinality of this datatype is dependent upon). For example, for :
-   *   stream :=  cons( head1 : U1, head2 : U2, tail : stream )
-   * Then, the recursive singleton argument types of stream are { U1, U2 },
-   * since if U1 and U2 have cardinality one, then stream has cardinality
-   * one as well.
-   *
-   * The versions of these methods that takes Type t is required
-   * for parametric datatypes, where t is an instantiated
-   * parametric datatype type whose datatype is this class.
-  */
-  unsigned getNumRecursiveSingletonArgTypes(Type t) const;
-  Type getRecursiveSingletonArgType(Type t, unsigned i) const;
-  unsigned getNumRecursiveSingletonArgTypes() const;
-  Type getRecursiveSingletonArgType(unsigned i) const;
-
-  /**
-   * Construct and return a ground term of this Datatype.  The
-   * Datatype must be both resolved and well-founded, or else an
-   * exception is thrown.
-   *
-   * This method takes a Type t, which is a datatype type whose
-   * datatype is this class, which may be an instantiated datatype
-   * type if this datatype is parametric.
-   */
-  Expr mkGroundTerm(Type t) const;
-  /** Make ground value
-   *
-   * Same as above, but constructs a constant value instead of a ground term.
-   * These two notions typically coincide. However, for uninterpreted sorts,
-   * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns
-   * an uninterpreted constant. The motivation for mkGroundTerm is that
-   * unintepreted constants should never appear in lemmas. The motivation for
-   * mkGroundValue is for things like type enumeration and model construction.
-   */
-  Expr mkGroundValue(Type t) const;
-
-  /**
-   * Get the DatatypeType associated to this Datatype.  Can only be
-   * called post-resolution.
-   */
-  DatatypeType getDatatypeType() const;
-
-  /**
-   * Get the DatatypeType associated to this (parameterized) Datatype.  Can only be
-   * called post-resolution.
-   */
-  DatatypeType getDatatypeType(const std::vector<Type>& params) const;
-
-  /**
-   * Return true iff the two Datatypes are the same.
-   *
-   * We need == for mkConst(Datatype) to properly work---since if the
-   * Datatype Expr requested is the same as an already-existing one,
-   * we need to return that one.  For that, we have a hash and
-   * operator==.  We provide != for symmetry.  We don't provide
-   * operator<() etc. because given two Datatype Exprs, you could
-   * simply compare those rather than the (bare) Datatypes.  This
-   * means, though, that Datatype cannot be stored in a sorted list or
-   * RB tree directly, so maybe we can consider adding these
-   * comparison operators later on.
-   */
-  bool operator==(const Datatype& other) const;
-  /** Return true iff the two Datatypes are not the same. */
-  bool operator!=(const Datatype& other) const;
-
-  /** Return true iff this Datatype has already been resolved. */
-  bool isResolved() const;
-
-  /** Get the beginning iterator over DatatypeConstructors. */
-  iterator begin();
-  /** Get the ending iterator over DatatypeConstructors. */
-  iterator end();
-  /** Get the beginning const_iterator over DatatypeConstructors. */
-  const_iterator begin() const;
-  /** Get the ending const_iterator over DatatypeConstructors. */
-  const_iterator end() const;
-
-  /** Get the ith DatatypeConstructor. */
-  const DatatypeConstructor& operator[](size_t index) const;
-
-  /**
-   * Get the DatatypeConstructor named.  This is a linear search
-   * through the constructors, so in the case of multiple,
-   * similarly-named constructors, the first is returned.
-   */
-  const DatatypeConstructor& operator[](std::string name) const;
- 
-  /**
-   * Get the constructor operator for the named constructor.
-   * This is a linear search through the constructors, so in
-   * the case of multiple, similarly-named constructors, the
-   * first is returned.
-   *
-   * This Datatype must be resolved.
-   */
-  Expr getConstructor(std::string name) const;
-
-  /** get sygus type
-   * This gets the built-in type associated with
-   * this sygus datatype, i.e. the type of the
-   * term that this sygus datatype encodes.
-   */
-  Type getSygusType() const;
-
-  /** get sygus var list
-   * This gets the variable list of the function
-   * to synthesize using this sygus datatype.
-   * For example, if we are synthesizing a binary
-   * function f where solutions are of the form:
-   *   f = (lambda (xy) t[x,y])
-   * In this case, this method returns the
-   * bound variable list containing x and y.
-   */
-  Expr getSygusVarList() const;
-  /** get sygus allow constants
-   *
-   * Does this sygus datatype allow constants?
-   * Notice that this is not a property of the
-   * constructors of this datatype. Instead, it is
-   * an auxiliary flag (provided in the call
-   * to setSygus).
-   */
-  bool getSygusAllowConst() const;
-  /** get sygus allow all
-   *
-   * Does this sygus datatype allow all terms?
-   * Notice that this is not a property of the
-   * constructors of this datatype. Instead, it is
-   * an auxiliary flag (provided in the call
-   * to setSygus).
-   */
-  bool getSygusAllowAll() const;
-
-  /** involves external type
-   * Get whether this datatype has a subfield
-   * in any constructor that is not a datatype type.
-   */
-  bool involvesExternalType() const;
-  /** involves uninterpreted type
-   * Get whether this datatype has a subfield
-   * in any constructor that is an uninterpreted type.
-   */
-  bool involvesUninterpretedType() const;
-
-  /**
-   * Get the list of constructors.
-   */
-  const std::vector<DatatypeConstructor>* getConstructors() const;
-
-  /** prints this datatype to stream */
-  void toStream(std::ostream& out) const;
-
- private:
-  /** The expression manager that created this datatype */
-  ExprManager* d_em;
-  /** The internal representation */
-  std::shared_ptr<DType> d_internal;
-  /** self type */
-  Type d_self;
-  /** the data of the record for this datatype (if applicable) */
-  std::shared_ptr<Record> d_record;
-  /** whether the datatype is a record */
-  bool d_isRecord;
-  /** the constructors of this datatype */
-  std::vector<DatatypeConstructor> d_constructors;
-  /**
-   * Datatypes refer to themselves, recursively, and we have a
-   * chicken-and-egg problem.  The DatatypeType around the Datatype
-   * cannot exist until the Datatype is finalized, and the Datatype
-   * cannot refer to the DatatypeType representing itself until it
-   * exists.  resolve() is called by the ExprManager when a Type is
-   * ultimately requested of the Datatype specification (that is, when
-   * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes()
-   * is called).  Has the effect of freezing the object, too; that is,
-   * addConstructor() will fail after a call to resolve().
-   *
-   * The basic goal of resolution is to assign constructors, selectors,
-   * and testers.  To do this, any UnresolvedType/SelfType references
-   * must be cleared up.  This is the purpose of the "resolutions" map;
-   * it includes any mutually-recursive datatypes that are currently
-   * under resolution.  The four vectors come in two pairs (so, really
-   * they are two maps).  placeholders->replacements give type variables
-   * that should be resolved in the case of parametric datatypes.
-   *
-   * @param resolutions a map of strings to DatatypeTypes currently under
-   * resolution
-   * @param placeholders the types in these Datatypes under resolution that must
-   * be replaced
-   * @param replacements the corresponding replacements
-   * @param paramTypes the sort constructors in these Datatypes under resolution
-   * that must be replaced
-   * @param paramReplacements the corresponding (parametric) DatatypeTypes
-   */
-  void resolve(const std::map<std::string, DatatypeType>& resolutions,
-               const std::vector<Type>& placeholders,
-               const std::vector<Type>& replacements,
-               const std::vector<SortConstructorType>& paramTypes,
-               const std::vector<DatatypeType>& paramReplacements);
-};/* class Datatype */
-
-/**
- * A hash function for Datatypes.  Needed to store them in hash sets
- * and hash maps.
- */
-struct CVC4_PUBLIC DatatypeHashFunction {
-  inline size_t operator()(const Datatype& dt) const {
-    return std::hash<std::string>()(dt.getName());
-  }
-  inline size_t operator()(const Datatype* dt) const {
-    return std::hash<std::string>()(dt->getName());
-  }
-  inline size_t operator()(const DatatypeConstructor& dtc) const {
-    return std::hash<std::string>()(dtc.getName());
-  }
-  inline size_t operator()(const DatatypeConstructor* dtc) const {
-    return std::hash<std::string>()(dtc->getName());
-  }
-};/* struct DatatypeHashFunction */
-
-
-// FUNCTION DECLARATIONS FOR OUTPUT STREAMS
-
-std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
-
-// INLINE FUNCTIONS
-
-inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) :
-  Exception(msg) {
-}
-
-inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
-  d_name(name) {
-}
-
-inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
-
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__DATATYPE_H */
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index bfc33ef87..fa9bb9793 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -245,6 +245,45 @@ void DType::addSygusConstructor(Node op,
 void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll)
 {
   Assert(!d_resolved);
+  // We can be in a case where the only rule specified was
+  // (Constant T), in which case we have not yet added a constructor. We
+  // ensure an arbitrary constant is added in this case. We additionally
+  // add a constant if the grammar has only non-nullary constructors, since this
+  // ensures the datatype is well-founded (see 3423).
+  // Notice we only want to do this for sygus datatypes that are user-provided.
+  // At the moment, the condition !allow_all implies the grammar is
+  // user-provided and hence may require a default constant.
+  // TODO (https://github.com/CVC4/cvc4-projects/issues/38):
+  // In an API for SyGuS, it probably makes more sense for the user to
+  // explicitly add the "any constant" constructor with a call instead of
+  // passing a flag. This would make the block of code unnecessary.
+  if (allowConst && !allowAll)
+  {
+    // if I don't already have a constant (0-ary constructor)
+    bool hasConstant = false;
+    for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
+    {
+      if ((*this)[i].getNumArgs() == 0)
+      {
+        hasConstant = true;
+        break;
+      }
+    }
+    if (!hasConstant)
+    {
+      // add an arbitrary one
+      Node op = st.mkGroundTerm();
+      // use same naming convention as SygusDatatype
+      std::stringstream ss;
+      ss << getName() << "_" << getNumConstructors() << "_" << op;
+      // it has zero weight
+      std::shared_ptr<DTypeConstructor> c =
+          std::make_shared<DTypeConstructor>(ss.str(), 0);
+      c->setSygus(op);
+      addConstructor(c);
+    }
+  }
+
   d_sygusType = st;
   d_sygusBvl = bvl;
   d_sygusAllowConst = allowConst || allowAll;
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index f48997748..44482c6cf 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -77,7 +77,6 @@ typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
 class NodeManager;
-class Datatype;
 
 /**
  * The Node-level representation of an inductive datatype, which currently
@@ -141,7 +140,6 @@ class Datatype;
  */
 class DType
 {
-  friend class Datatype;
   friend class DTypeConstructor;
   friend class NodeManager;  // for access to resolve()
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 66824c07a..0d22a3c41 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -114,8 +114,6 @@ ExprManager::~ExprManager()
       }
     }
 #endif
-    // clear the datatypes
-    d_ownedDatatypes.clear();
 
     delete d_nodeManager;
     d_nodeManager = NULL;
@@ -597,20 +595,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
 }
 
-DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) {
-  NodeManagerScope nms(d_nodeManager);
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
-     typeNodes.push_back(*types[i].d_typeNode);
-  }
-  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
-}
-
-DatatypeType ExprManager::mkRecordType(const Record& rec) {
-  NodeManagerScope nms(d_nodeManager);
-  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
-}
-
 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
   std::vector<TypeNode> typeNodes;
@@ -648,195 +632,6 @@ SequenceType ExprManager::mkSequenceType(Type elementType) const
       new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode))));
 }
 
-DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags)
-{
-  // Not worth a special implementation; this doesn't need to be fast
-  // code anyway.
-  vector<Datatype> datatypes;
-  datatypes.push_back(datatype);
-  std::vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes, flags);
-  Assert(result.size() == 1);
-  return result.front();
-}
-
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
-    std::vector<Datatype>& datatypes, uint32_t flags)
-{
-  std::set<Type> unresolvedTypes;
-  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags);
-}
-
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
-    std::vector<Datatype>& datatypes,
-    std::set<Type>& unresolvedTypes,
-    uint32_t flags)
-{
-  NodeManagerScope nms(d_nodeManager);
-  std::map<std::string, DatatypeType> nameResolutions;
-  std::vector<DatatypeType> dtts;
-
-  // have to build deep copy so that datatypes will live in this class
-  std::vector< Datatype* > dt_copies;
-  for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
-    d_ownedDatatypes.push_back(std::unique_ptr<Datatype>(new Datatype(*i)));
-    dt_copies.push_back(d_ownedDatatypes.back().get());
-  }
-
-  // First do some sanity checks, set up the final Type to be used for
-  // each datatype, and set up the "named resolutions" used to handle
-  // simple self- and mutual-recursion, for example in the definition
-  // "nat = succ(pred:nat) | zero", a named resolution can handle the
-  // pred selector.
-  for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) {
-    TypeNode* typeNode;
-    // register datatype with the node manager
-    size_t index = d_nodeManager->registerDatatype((*i)->d_internal);
-    if( (*i)->getNumParameters() == 0 ) {
-      typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)));
-      //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
-    } else {
-      TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
-      //TypeNode cons = d_nodeManager->mkTypeConst(*i);
-      std::vector< TypeNode > params;
-      params.push_back( cons );
-      for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) {
-        params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) );
-      }
-
-      typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
-    }
-    Type type(d_nodeManager, typeNode);
-    DatatypeType dtt(type);
-    PrettyCheckArgument(
-        nameResolutions.find((*i)->getName()) == nameResolutions.end(),
-        dt_copies,
-        "cannot construct two datatypes at the same time "
-        "with the same name `%s'",
-        (*i)->getName().c_str());
-    nameResolutions.insert(std::make_pair((*i)->getName(), dtt));
-    dtts.push_back(dtt);
-  }
-
-  // Second, set up the type substitution map for complex type
-  // resolution (e.g. if "list" is the type we're defining, and it has
-  // a selector of type "ARRAY INT OF list", this can't be taken care
-  // of using the named resolutions that we set up above.  A
-  // preliminary array type was set up, and now needs to have "list"
-  // substituted in it for the correct type.
-  //
-  // @TODO get rid of named resolutions altogether and handle
-  // everything with these resolutions?
-  std::vector< SortConstructorType > paramTypes;
-  std::vector< DatatypeType > paramReplacements;
-  std::vector<Type> placeholders;// to hold the "unresolved placeholders"
-  std::vector<Type> replacements;// to hold our final, resolved types
-  for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) {
-    std::string name;
-    if( (*i).isSort() ) {
-      name = SortType(*i).getName();
-    } else {
-      Assert((*i).isSortConstructor());
-      name = SortConstructorType(*i).getName();
-    }
-    std::map<std::string, DatatypeType>::const_iterator resolver =
-      nameResolutions.find(name);
-    PrettyCheckArgument(
-        resolver != nameResolutions.end(),
-        unresolvedTypes,
-        "cannot resolve type `%s'; it's not among "
-        "the datatypes being defined", name.c_str());
-    // We will instruct the Datatype to substitute "*i" (the
-    // unresolved SortType used as a placeholder in complex types)
-    // with "(*resolver).second" (the DatatypeType we created in the
-    // first step, above).
-    if( (*i).isSort() ) {
-      placeholders.push_back(*i);
-      replacements.push_back( (*resolver).second );
-    } else {
-      Assert((*i).isSortConstructor());
-      paramTypes.push_back( SortConstructorType(*i) );
-      paramReplacements.push_back( (*resolver).second );
-    }
-  }
-
-  // Lastly, perform the final resolutions and checks.
-  std::vector<TypeNode> tns;
-  for(std::vector<DatatypeType>::iterator i = dtts.begin(),
-        i_end = dtts.end();
-      i != i_end;
-      ++i) {
-    const Datatype& dt = (*i).getDatatype();
-    if(!dt.isResolved()) {
-      const_cast<Datatype&>(dt).resolve(nameResolutions,
-                                        placeholders,
-                                        replacements,
-                                        paramTypes,
-                                        paramReplacements);
-    }
-
-    // Now run some checks, including a check to make sure that no
-    // selector is function-valued.
-    checkResolvedDatatype(*i);
-    tns.push_back(TypeNode::fromType(*i));
-  }
-
-  for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewDatatypes(tns, flags);
-  }
-  
-  return dtts;
-}
-
-void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
-  const Datatype& dt = dtt.getDatatype();
-
-  AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
-
-  // for all constructors...
-  for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
-      i != i_end;
-      ++i) {
-    const DatatypeConstructor& c = *i;
-    Type testerType CVC4_UNUSED = c.getTester().getType();
-    Assert(c.isResolved() && testerType.isTester()
-           && TesterType(testerType).getDomain() == dtt
-           && TesterType(testerType).getRangeType() == booleanType())
-        << "malformed tester in datatype post-resolution";
-    Type ctorType CVC4_UNUSED = c.getConstructor().getType();
-    Assert(ctorType.isConstructor()
-           && ConstructorType(ctorType).getArity() == c.getNumArgs()
-           && ConstructorType(ctorType).getRangeType() == dtt)
-        << "malformed constructor in datatype post-resolution";
-    // for all selectors...
-    for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
-        j != j_end;
-        ++j) {
-      const DatatypeConstructorArg& a = *j;
-      Type selectorType = a.getType();
-      Assert(a.isResolved() && selectorType.isSelector()
-             && SelectorType(selectorType).getDomain() == dtt)
-          << "malformed selector in datatype post-resolution";
-      // This next one's a "hard" check, performed in non-debug builds
-      // as well; the other ones should all be guaranteed by the
-      // CVC4::Datatype class, but this actually needs to be checked.
-      AlwaysAssert(!SelectorType(selectorType)
-                        .getRangeType()
-                        .d_typeNode->isFunctionLike())
-          << "cannot put function-like things in datatypes";
-    }
-  }
-}
-
-SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
-}
-
-TesterType ExprManager::mkTesterType(Type domain) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
-}
-
 SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const {
   NodeManagerScope nms(d_nodeManager);
   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags))));
@@ -1110,13 +905,6 @@ Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapColle
               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
 }
 
-const Datatype& ExprManager::getDatatypeForIndex(unsigned index) const
-{
-  // when the Node-level API is in place, this function will be deleted.
-  Assert(index < d_ownedDatatypes.size());
-  return *d_ownedDatatypes[index];
-}
-
 ${mkConst_implementations}
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 2b9a85aca..a6fce56a2 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -65,11 +65,6 @@ class CVC4_PUBLIC ExprManager {
   NodeManager* getNodeManager() const;
 
   /**
-   * Check some things about a newly-created DatatypeType.
-   */
-  void checkResolvedDatatype(DatatypeType dtt) const;
-
-  /**
    * SmtEngine will use all the internals, so it will grab the
    * NodeManager.
    */
@@ -84,10 +79,6 @@ class CVC4_PUBLIC ExprManager {
   // undefined, private copy constructor and assignment op (disallow copy)
   ExprManager(const ExprManager&) = delete;
   ExprManager& operator=(const ExprManager&) = delete;
-
-  /** A list of datatypes owned by this expr manager. */
-  std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
-
   /** Creates an expression manager. */
   ExprManager();
  public:
@@ -346,18 +337,6 @@ class CVC4_PUBLIC ExprManager {
   FunctionType mkPredicateType(const std::vector<Type>& sorts);
 
   /**
-   * Make a tuple type with types from
-   * <code>types[0..types.size()-1]</code>.  <code>types</code> must
-   * have at least one element.
-   */
-  DatatypeType mkTupleType(const std::vector<Type>& types);
-
-  /**
-   * Make a record type with types from the rec parameter.
-   */
-  DatatypeType mkRecordType(const Record& rec);
-
-  /**
    * Make a symbolic expressiontype with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> may
    * have any number of elements.
@@ -379,68 +358,6 @@ class CVC4_PUBLIC ExprManager {
   /** Make the type of sequence with the given parameterization. */
   SequenceType mkSequenceType(Type elementType) const;
 
-  /** Bits for use in mkDatatypeType() flags.
-   *
-   * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
-   * out as a definition, for example, in models or during dumping.
-   */
-  enum
-  {
-    DATATYPE_FLAG_NONE = 0,
-    DATATYPE_FLAG_PLACEHOLDER = 1
-  }; /* enum */
-
-  /** Make a type representing the given datatype. */
-  DatatypeType mkDatatypeType(Datatype& datatype,
-                              uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /**
-   * Make a set of types representing the given datatypes, which may be
-   * mutually recursive.
-   */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(
-      std::vector<Datatype>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /**
-   * Make a set of types representing the given datatypes, which may
-   * be mutually recursive.  unresolvedTypes is a set of SortTypes
-   * that were used as placeholders in the Datatypes for the Datatypes
-   * of the same name.  This is just a more complicated version of the
-   * above mkMutualDatatypeTypes() function, but is required to handle
-   * complex types.
-   *
-   * For example, unresolvedTypes might contain the single sort "list"
-   * (with that name reported from SortType::getName()).  The
-   * datatypes list might have the single datatype
-   *
-   *   DATATYPE
-   *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
-   *   END;
-   *
-   * To represent the Type of the array, the user had to create a
-   * placeholder type (an uninterpreted sort) to stand for "list" in
-   * the type of "car".  It is this placeholder sort that should be
-   * passed in unresolvedTypes.  If the datatype was of the simpler
-   * form:
-   *
-   *   DATATYPE
-   *     list = cons(car:list, cdr:list) | nil;
-   *   END;
-   *
-   * then no complicated Type needs to be created, and the above,
-   * simpler form of mkMutualDatatypeTypes() is enough.
-   */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(
-      std::vector<Datatype>& datatypes,
-      std::set<Type>& unresolvedTypes,
-      uint32_t flags = DATATYPE_FLAG_NONE);
-
-  /** Make a type representing a selector with the given parameterization. */
-  SelectorType mkSelectorType(Type domain, Type range) const;
-
-  /** Make a type representing a tester with the given parameterization. */
-  TesterType mkTesterType(Type domain) const;
-
   /** Bits for use in mkSort() flags. */
   enum {
     SORT_FLAG_NONE = 0,
@@ -573,13 +490,6 @@ class CVC4_PUBLIC ExprManager {
    * maximal arity as the maximal possible number of children of a node.
    **/
   static bool isNAryKind(Kind fun);
-
-  /**
-   * Return the datatype at the given index owned by this class. Type nodes are
-   * associated with datatypes through the DatatypeIndexConstant class. The
-   * argument index is intended to be a value taken from that class.
-   */
-  const Datatype& getDatatypeForIndex(unsigned index) const;
 };/* class ExprManager */
 
 ${mkConst_instantiations}
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index bcddc23f5..0f2db7869 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -207,6 +207,8 @@ size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
 
 const DType& NodeManager::getDTypeForIndex(size_t index) const
 {
+  // if this assertion fails, it is likely due to not managing datatypes
+  // properly w.r.t. multiple NodeManagers.
   Assert(index < d_registeredDTypes.size());
   return *d_registeredDTypes[index];
 }
@@ -635,18 +637,19 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto
       for (unsigned i = 0; i < types.size(); ++ i) {
         sst << "_" << types[i];
       }
-      Datatype dt(nm->toExprManager(), sst.str());
+      DType dt(sst.str());
       dt.setTuple();
       std::stringstream ssc;
       ssc << sst.str() << "_ctor";
-      DatatypeConstructor c(ssc.str());
+      std::shared_ptr<DTypeConstructor> c =
+          std::make_shared<DTypeConstructor>(ssc.str());
       for (unsigned i = 0; i < types.size(); ++ i) {
         std::stringstream ss;
         ss << sst.str() << "_stor_" << i;
-        c.addArg(ss.str().c_str(), types[i].toType());
+        c->addArg(ss.str().c_str(), types[i]);
       }
       dt.addConstructor(c);
-      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      d_data = nm->mkDatatypeType(dt);
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
     return d_data;
@@ -664,16 +667,17 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
         sst << "_" << (*i).first << "_" << (*i).second;
       }
-      Datatype dt(nm->toExprManager(), sst.str());
+      DType dt(sst.str());
       dt.setRecord();
       std::stringstream ssc;
       ssc << sst.str() << "_ctor";
-      DatatypeConstructor c(ssc.str());
+      std::shared_ptr<DTypeConstructor> c =
+          std::make_shared<DTypeConstructor>(ssc.str());
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-        c.addArg((*i).first, (*i).second);
+        c->addArg((*i).first, TypeNode::fromType((*i).second));
       }
       dt.addConstructor(c);
-      d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+      d_data = nm->mkDatatypeType(dt);
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
     return d_data;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index cfe771ca5..592b5e7e9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -91,10 +91,6 @@ class NodeManager {
   friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
   friend Expr ExprManager::mkVar(Type, uint32_t flags);
 
-  // friend so it can access NodeManager's d_listeners and notify clients
-  friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
-      std::vector<Datatype>&, std::set<Type>&, uint32_t);
-
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
@@ -380,8 +376,8 @@ class NodeManager {
   /** Create a variable with the given type. */
   Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
   Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-  
-public:
+
+ public:
 
   explicit NodeManager(ExprManager* exprManager);
   ~NodeManager();
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 1efea4e15..d6004e7cb 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -18,10 +18,7 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-SygusDatatype::SygusDatatype(const std::string& name)
-    : d_dt(Datatype(NodeManager::currentNM()->toExprManager(), name))
-{
-}
+SygusDatatype::SygusDatatype(const std::string& name) : d_dt(DType(name)) {}
 
 std::string SygusDatatype::getName() const { return d_dt.getName(); }
 
@@ -79,25 +76,19 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
   Assert(!d_cons.empty());
   /* Use the sygus type to not lose reference to the original types (Bool,
    * Int, etc) */
-  d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll);
+  d_dt.setSygus(sygusType, sygusVars, allowConst, allowAll);
   for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i)
   {
-    // must convert to type now
-    std::vector<Type> cargs;
-    for (TypeNode& ct : d_cons[i].d_argTypes)
-    {
-      cargs.push_back(ct.toType());
-    }
     // add (sygus) constructor
-    d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(),
+    d_dt.addSygusConstructor(d_cons[i].d_op,
                              d_cons[i].d_name,
-                             cargs,
+                             d_cons[i].d_argTypes,
                              d_cons[i].d_weight);
   }
   Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
 }
 
-const Datatype& SygusDatatype::getDatatype() const
+const DType& SygusDatatype::getDatatype() const
 {
   // should have initialized by this point
   Assert(isInitialized());
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 4342aa291..6fe0531fb 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -20,7 +20,7 @@
 #include <vector>
 
 #include "expr/attribute.h"
-#include "expr/datatype.h"
+#include "expr/dtype.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 
@@ -122,7 +122,7 @@ class SygusDatatype
                           bool allowConst,
                           bool allowAll);
   /** Get the sygus datatype initialized by this class */
-  const Datatype& getDatatype() const;
+  const DType& getDatatype() const;
 
   /** is initialized */
   bool isInitialized() const;
@@ -131,7 +131,7 @@ class SygusDatatype
   /** Information for each constructor. */
   std::vector<SygusDatatypeConstructor> d_cons;
   /** Datatype to represent type's structure */
-  Datatype d_dt;
+  DType d_dt;
 };
 
 }  // namespace CVC4
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8232ef339..5dd15dd37 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -585,19 +585,6 @@ std::vector<Type> ConstructorType::getArgTypes() const {
   return args;
 }
 
-const Datatype& DatatypeType::getDatatype() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isDatatype());
-  if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
-  {
-    DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>();
-    return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex());
-  }
-  Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE);
-  return DatatypeType((*d_typeNode)[0].toType()).getDatatype();
-}
-
 bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 0067ba7e7..d58643811 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -616,9 +616,6 @@ class CVC4_PUBLIC DatatypeType : public Type {
   /** Construct from the base type */
   DatatypeType(const Type& type = Type());
 
-  /** Get the underlying datatype */
-  const Datatype& getDatatype() const;
-
   /** Is this datatype parametric? */
   bool isParametric() const;
   /**
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index b836e5069..2c5be80aa 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1011,7 +1011,8 @@ inline TypeNode TypeNode::getRangeType() const {
   if(isTester()) {
     return NodeManager::currentNM()->booleanType();
   }
-  Assert(isFunction() || isConstructor() || isSelector());
+  Assert(isFunction() || isConstructor() || isSelector())
+      << "Cannot get range type of " << *this;
   return (*this)[getNumChildren() - 1];
 }
 
diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index 89c90a8c4..4b2bde810 100644
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -20,7 +20,7 @@
 
 #include <cvc4/base/configuration.h>
 #include <cvc4/base/exception.h>
-#include <cvc4/expr/datatype.h>
+#include <cvc4/expr/datatype_index.h>
 #include <cvc4/expr/expr.h>
 #include <cvc4/expr/expr_manager.h>
 #include <cvc4/options/options.h>
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 354f2d472..4bb253603 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1463,13 +1463,14 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
           {
             PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
           }
-          Expr ef = f.getExpr();
-          if (Datatype::datatypeOf(ef).isParametric())
+          api::Datatype dt = type.getConstructorCodomainSort().getDatatype();
+          if (dt.isParametric())
           {
-            type = api::Sort(
-                SOLVER,
-                Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
-                    .getSpecializedConstructorType(expr.getSort().getType()));
+            // lookup constructor by name
+            api::DatatypeConstructor dc = dt.getConstructor(f.toString());
+            api::Term scons = dc.getSpecializedConstructorTerm(expr.getSort());
+            // take the type of the specialized constructor instead
+            type = scons.getSort();
           }
           argTypes = type.getConstructorDomainSorts();
         }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fa0f8af43..1e5d2155a 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1149,11 +1149,9 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       ss << "tuple is of length " << length << "; cannot access index " << n;
       parseError(ss.str());
     }
-    const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
-    api::Term ret =
-        d_solver->mkTerm(api::APPLY_SELECTOR,
-                         api::Term(d_solver, dt[0][n].getSelector()),
-                         args[0]);
+    const api::Datatype& dt = t.getDatatype();
+    api::Term ret = d_solver->mkTerm(
+        api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
     Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
     return ret;
   }
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index d0ebe5f19..b34ff59f5 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -241,7 +241,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
   Trace("srs-input") << "Construct unresolved types..." << std::endl;
   // each canonical subterm corresponds to a grammar type
-  std::set<Type> unres;
+  std::set<TypeNode> unres;
   std::vector<SygusDatatype> sdts;
   // make unresolved types for each canonical term
   std::map<Node, TypeNode> cterm_to_utype;
@@ -253,7 +253,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     std::string tname = ss.str();
     TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER);
     cterm_to_utype[ct] = tnu;
-    unres.insert(tnu.toType());
+    unres.insert(tnu);
     sdts.push_back(SygusDatatype(tname));
   }
   Trace("srs-input") << "...finished." << std::endl;
@@ -369,19 +369,19 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   Trace("srs-input") << "Make mutual datatype types for subterms..."
                      << std::endl;
   // extract the datatypes
-  std::vector<Datatype> datatypes;
+  std::vector<DType> datatypes;
   for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
   {
     datatypes.push_back(sdts[i].getDatatype());
   }
-  std::vector<DatatypeType> types = nm->toExprManager()->mkMutualDatatypeTypes(
-      datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+  std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(
+      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
   Trace("srs-input") << "...finished." << std::endl;
   Assert(types.size() == unres.size());
   std::map<Node, TypeNode> subtermTypes;
   for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
   {
-    subtermTypes[cterms[i]] = TypeNode::fromType(types[i]);
+    subtermTypes[cterms[i]] = types[i];
   }
 
   Trace("srs-input") << "Construct the top-level types..." << std::endl;
@@ -418,12 +418,12 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     }
     // set that this is a sygus datatype
     sdttl.initializeDatatype(t, sygusVarList, false, false);
-    Datatype dttl = sdttl.getDatatype();
-    DatatypeType tlt = nm->toExprManager()->mkDatatypeType(
-        dttl, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-    tlGrammarTypes[t] = TypeNode::fromType(tlt);
+    DType dttl = sdttl.getDatatype();
+    TypeNode tlt =
+        nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+    tlGrammarTypes[t] = tlt;
     Trace("srs-input") << "Grammar is: " << std::endl;
-    Trace("srs-input") << tlt.getDatatype() << std::endl;
+    Trace("srs-input") << tlt.getDType() << std::endl;
   }
   Trace("srs-input") << "...finished." << std::endl;
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 8120d1d88..89b516511 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -211,17 +211,15 @@ void CvcPrinter::toStream(
       break;
 
     case kind::DATATYPE_TYPE: {
-      const Datatype& dt =
-          NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
-              n.getConst<DatatypeIndexConstant>().getIndex());
-
+      const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
+          n.getConst<DatatypeIndexConstant>().getIndex());
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
           if (i > 0) {
             out << ", ";
           }
-          Type t = dt[0][i].getRangeType();
+          TypeNode t = dt[0][i].getRangeType();
           out << t;
         }
         out << ']';
@@ -233,7 +231,7 @@ void CvcPrinter::toStream(
           if (i > 0) {
             out << ", ";
           }
-          Type t = dt[0][i].getRangeType();
+          TypeNode t = dt[0][i].getRangeType();
           out << dt[0][i].getSelector() << ":" << t;
         }
         out << " #]";
diff --git a/src/smt/command.h b/src/smt/command.h
index 95274884f..a0e591269 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -29,7 +29,6 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "expr/variable_type_map.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 41602dab2..539d6ba2f 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -62,7 +62,7 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
 void SmtNodeManagerListener::nmNotifyNewDatatypes(
     const std::vector<TypeNode>& dtts, uint32_t flags)
 {
-  if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+  if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
   {
     std::vector<Type> types;
     for (const TypeNode& dt : dtts)
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 26bff20b7..ef8dd47f1 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -41,7 +41,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is
 constant DATATYPE_TYPE \
     ::CVC4::DatatypeIndexConstant \
     "::CVC4::DatatypeIndexConstantHashFunction" \
-    "expr/datatype.h" \
+    "expr/datatype_index.h" \
     "a datatype type index"
 cardinality DATATYPE_TYPE \
     "%TYPE%.getDType().getCardinality(%TYPE%)" \
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index bd14f8a2c..0aa44e170 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -648,7 +648,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
 
   // must convert all constructors to version with variables in "vars"
   std::vector<SygusDatatype> sdts;
-  std::set<Type> unres;
+  std::set<TypeNode> unres;
 
   Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
   Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;
@@ -662,7 +662,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
   ssutn0 << sdtd.getName() << "_s";
   TypeNode abdTNew =
       nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
-  unres.insert(abdTNew.toType());
+  unres.insert(abdTNew);
   dtProcessed[sdt] = abdTNew;
 
   // We must convert all symbols in the sygus datatype type sdt to
@@ -706,7 +706,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
                 nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
             Trace("dtsygus-gen-debug") << "    ...unresolved type " << argtNew
                                        << " for " << argt << std::endl;
-            unres.insert(argtNew.toType());
+            unres.insert(argtNew);
             dtProcessed[argt] = argtNew;
             dtNextToProcess.push_back(argt);
           }
@@ -736,22 +736,21 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
   Trace("dtsygus-gen-debug")
       << "Make " << sdts.size() << " datatype types..." << std::endl;
   // extract the datatypes
-  std::vector<Datatype> datatypes;
+  std::vector<DType> datatypes;
   for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
   {
     datatypes.push_back(sdts[i].getDatatype());
   }
   // make the datatype types
-  std::vector<DatatypeType> datatypeTypes =
-      nm->toExprManager()->mkMutualDatatypeTypes(
-          datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-  TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]);
+  std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
+      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+  TypeNode sdtS = datatypeTypes[0];
   if (Trace.isOn("dtsygus-gen-debug"))
   {
     Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl;
     for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
     {
-      const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType();
+      const DType& dtj = datatypeTypes[j].getDType();
       Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl;
       for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
       {
diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 0c475a8e0..e2b36c463 100644
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -25,7 +25,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
-#include "expr/datatype.h"
+#include "expr/dtype.h"
 #include "expr/node.h"
 #include "theory/datatypes/sygus_simple_sym.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 6dd990b30..e9a0ba052 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -24,7 +24,6 @@
 
 #include "context/cdlist.h"
 #include "expr/attribute.h"
-#include "expr/datatype.h"
 #include "expr/node_trie.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/sygus_extension.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 176f275f0..d971a373d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -14,7 +14,6 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
-#include "expr/datatype.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 0fe6bef00..f5c13b183 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -21,7 +21,6 @@
 #include <unordered_set>
 
 #include "context/cdhashmap.h"
-#include "expr/datatype.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/quant_util.h"
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 9126aad94..8595ab673 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -14,7 +14,6 @@
 
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 
-#include "expr/datatype.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 582fa067d..d0536a1ea 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -465,8 +465,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       std::string veName("_virtual_enum_grammar");
       SygusDatatype sdt(veName);
       TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER);
-      std::set<Type> unresolvedTypes;
-      unresolvedTypes.insert(u.toType());
+      std::set<TypeNode> unresolvedTypes;
+      unresolvedTypes.insert(u);
       std::vector<TypeNode> cargsEmpty;
       Node cr = nm->mkConst(Rational(1));
       sdt.addConstructor(cr, "1", cargsEmpty);
@@ -475,15 +475,11 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       cargsPlus.push_back(u);
       sdt.addConstructor(PLUS, cargsPlus);
       sdt.initializeDatatype(nm->integerType(), bvl, false, false);
-      std::vector<Datatype> datatypes;
+      std::vector<DType> datatypes;
       datatypes.push_back(sdt.getDatatype());
-      std::vector<DatatypeType> dtypes =
-          nm->toExprManager()->mkMutualDatatypeTypes(
-              datatypes,
-              unresolvedTypes,
-              ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-      TypeNode vtn = TypeNode::fromType(dtypes[0]);
-      d_virtual_enum = nm->mkSkolem("_ve", vtn);
+      std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
+          datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
+      d_virtual_enum = nm->mkSkolem("_ve", dtypes[0]);
       d_tds->registerEnumerator(
           d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
     }
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index ee37d7b4b..f31a9a977 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -15,7 +15,6 @@
 
 #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"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index bd5f7ae50..b89b94fc8 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -16,7 +16,6 @@
 
 #include <stack>
 
-#include "expr/datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -378,10 +377,11 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
   return visited[n];
 }
 
-
-TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set<Type>& unres) {
+TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
+                                                 std::set<TypeNode>& unres)
+{
   TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
-  unres.insert( unresolved.toType() );
+  unres.insert(unresolved);
   return unresolved;
 }
 
@@ -529,7 +529,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         include_cons,
     std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
     std::vector<SygusDatatypeGenerator>& sdts,
-    std::set<Type>& unres)
+    std::set<TypeNode>& unres)
 {
   NodeManager* nm = NodeManager::currentNM();
   Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
@@ -1389,7 +1389,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
   {
     Trace("sygus-grammar-def") << "    ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
   }
-  std::set<Type> unres;
+  std::set<TypeNode> unres;
   std::vector<SygusDatatypeGenerator> sdts;
   mkSygusDefaultGrammar(range,
                         bvl,
@@ -1401,19 +1401,18 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
                         sdts,
                         unres);
   // extract the datatypes from the sygus datatype generator objects
-  std::vector<Datatype> datatypes;
+  std::vector<DType> datatypes;
   for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
   {
     datatypes.push_back(sdts[i].d_sdt.getDatatype());
   }
   Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
   Assert(!datatypes.empty());
-  std::vector<DatatypeType> types =
-      NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
-          datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+  std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
+      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
   Trace("sygus-grammar-def") << "...finished" << std::endl;
   Assert(types.size() == datatypes.size());
-  return TypeNode::fromType( types[0] );
+  return types[0];
 }
 
 TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
@@ -1423,7 +1422,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
     return templ_arg_sygus_type;
   }else{
     tcount++;
-    std::set<Type> unres;
+    std::set<TypeNode> unres;
     std::vector<SygusDatatype> sdts;
     std::stringstream ssd;
     ssd << fun << "_templ_" << tcount;
@@ -1450,16 +1449,16 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
     sdts.back().addConstructor(op, ssdc.str(), argTypes);
     sdts.back().initializeDatatype(templ.getType(), bvl, true, true);
     // extract the datatypes from the sygus datatype objects
-    std::vector<Datatype> datatypes;
+    std::vector<DType> datatypes;
     for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
     {
       datatypes.push_back(sdts[i].getDatatype());
     }
-    std::vector<DatatypeType> types =
-        NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
-            datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+    std::vector<TypeNode> types =
+        NodeManager::currentNM()->mkMutualDatatypeTypes(
+            datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
     Assert(types.size() == 1);
-    return TypeNode::fromType( types[0] );
+    return types[0];
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index fd7f84484..c0113b31c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -222,7 +222,8 @@ public:
   };
 
   // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
-  static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
+  static TypeNode mkUnresolvedType(const std::string& name,
+                                   std::set<TypeNode>& unres);
   // collect the list of types that depend on type range
   static void collectSygusGrammarTypesFor(TypeNode range,
                                           std::vector<TypeNode>& types);
@@ -243,7 +244,7 @@ public:
           include_cons,
       std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
       std::vector<SygusDatatypeGenerator>& sdts,
-      std::set<Type>& unres);
+      std::set<TypeNode>& unres);
 
   // helper function for mkSygusTemplateType
   static TypeNode mkSygusTemplateTypeRec(Node templ,
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 939256b2b..d9deb78f5 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -15,7 +15,6 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 
-#include "expr/datatype.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
@@ -122,7 +121,7 @@ void SygusGrammarNorm::TypeObject::initializeDatatype(
       << "...built datatype " << d_sdt.getDatatype() << " ";
   /* Add to global accumulators */
   sygus_norm->d_dt_all.push_back(d_sdt.getDatatype());
-  sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
+  sygus_norm->d_unres_t_all.insert(d_unres_tn);
   Trace("sygus-grammar-normalize") << "---------------------------------\n";
 }
 
@@ -463,7 +462,6 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
   // Remaining operators are rebuilt as they are.
   // Notice that we must extract the Datatype here to get the (Expr-layer)
   // sygus print callback.
-  const Datatype& dtt = DatatypeType(tn.toType()).getDatatype();
   for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
   {
     unsigned oi = op_pos[i];
@@ -520,22 +518,21 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
       Trace("sygus-grammar-normalize-build") << d_dt_all[i];
     }
     Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
-    for (const Type& unres_t : d_unres_t_all)
+    for (const TypeNode& unres_t : d_unres_t_all)
     {
       Trace("sygus-grammar-normalize-build") << unres_t << " ";
     }
     Trace("sygus-grammar-normalize-build") << "\n";
   }
   Assert(d_dt_all.size() == d_unres_t_all.size());
-  std::vector<DatatypeType> types =
-      NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
-          d_dt_all, d_unres_t_all, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+  std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
+      d_dt_all, d_unres_t_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
   Assert(types.size() == d_dt_all.size());
   /* Clear accumulators */
   d_dt_all.clear();
   d_unres_t_all.clear();
   /* By construction the normalized type node will be the last one considered */
-  return TypeNode::fromType(types.back());
+  return types.back();
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 5994d0e7d..8ffa81e9e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -22,7 +22,6 @@
 #include <string>
 #include <vector>
 
-#include "expr/datatype.h"
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
 #include "expr/type.h"
@@ -376,9 +375,9 @@ class SygusGrammarNorm
    */
   TNode d_sygus_vars;
   /* Datatypes to be resolved */
-  std::vector<Datatype> d_dt_all;
+  std::vector<DType> d_dt_all;
   /* Types to be resolved */
-  std::set<Type> d_unres_t_all;
+  std::set<TypeNode> d_unres_t_all;
   /* Associates type nodes with OpPosTries */
   std::map<TypeNode, OpPosTrie> d_tries;
   /* Map of type nodes into their identity operators (\lambda x. x) */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 361226678..9bb2c977c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -20,7 +20,6 @@
 #include <map>
 #include <vector>
 
-#include "expr/datatype.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 0ecd888e0..c2ca83e41 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -16,16 +16,12 @@
 
 #include "theory/quantifiers/sygus/sygus_interpol.h"
 
-#include "expr/datatype.h"
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
-#include "expr/sygus_datatype.h"
 #include "options/smt_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -188,15 +184,14 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
     getIncludeCons(axioms, conj, include_cons);
     std::unordered_set<Node, NodeHashFunction> terms_irrelevant;
-    itpGTypeS =
-        CVC4::theory::quantifiers::CegGrammarConstructor::mkSygusDefaultType(
-            NodeManager::currentNM()->booleanType(),
-            d_ibvlShared,
-            "interpolation_grammar",
-            extra_cons,
-            exclude_cons,
-            include_cons,
-            terms_irrelevant);
+    itpGTypeS = CegGrammarConstructor::mkSygusDefaultType(
+        NodeManager::currentNM()->booleanType(),
+        d_ibvlShared,
+        "interpolation_grammar",
+        extra_cons,
+        exclude_cons,
+        include_cons,
+        terms_irrelevant);
   }
   Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl;
   return itpGTypeS;
@@ -235,10 +230,10 @@ void SygusInterpol::mkSygusConjecture(Node itp,
 
   // set the sygus bound variable list
   Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
-  itp.setAttribute(theory::SygusSynthFunVarListAttribute(), d_ibvlShared);
+  itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared);
   // sygus attribute
   Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
-  theory::SygusAttribute ca;
+  SygusAttribute ca;
   sygusVar.setAttribute(ca, true);
   Node instAttr = nm->mkNode(kind::INST_ATTRIBUTE, sygusVar);
   std::vector<Node> iplc;
@@ -265,7 +260,7 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   constraint = constraint.substitute(
       d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end());
   Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl;
-  constraint = theory::Rewriter::rewrite(constraint);
+  constraint = Rewriter::rewrite(constraint);
 
   d_sygusConj = constraint;
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 0921fba30..573db99c7 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -14,7 +14,6 @@
  **/
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 
-#include "expr/datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 6df8619f7..729a12c66 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -16,7 +16,6 @@
 
 #include <stack>
 
-#include "expr/datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 9608de743..5b7ad2049 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -14,7 +14,6 @@
  **/
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
-#include "expr/datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index f657062ed..42b560c59 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -14,7 +14,6 @@
 
 #include "theory/quantifiers/term_util.h"
 
-#include "expr/datatype.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 82f32337e..c8eeece4a 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -15,7 +15,6 @@
  **/
 
 #include "theory/sets/theory_sets_rels.h"
-#include "expr/datatype.h"
 #include "theory/sets/theory_sets_private.h"
 #include "theory/sets/theory_sets.h"
 
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index c86408a52..f1b25515c 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -20,6 +20,7 @@
 #include <unordered_set>
 
 #include "expr/array_store_all.h"
+#include "expr/dtype.h"
 #include "expr/expr_manager.h"
 #include "expr/kind.h"
 #include "expr/node_manager.h"
@@ -145,51 +146,66 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT( ! te.isFinished() );
   }
 
-  void testDatatypesFinite() {
-    Datatype dt(d_em, "Colors");
-    dt.addConstructor(DatatypeConstructor("red"));
-    dt.addConstructor(DatatypeConstructor("orange"));
-    dt.addConstructor(DatatypeConstructor("yellow"));
-    dt.addConstructor(DatatypeConstructor("green"));
-    dt.addConstructor(DatatypeConstructor("blue"));
-    dt.addConstructor(DatatypeConstructor("violet"));
-    TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
+  void testDTypesFinite()
+  {
+    DType dt("Colors");
+    dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+    TypeNode datatype = d_nm->mkDatatypeType(dt);
+    const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
+        datatype.getDType().getConstructors();
     TypeEnumerator te(datatype);
-    TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red")));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange")));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow")));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green")));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")));
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet")));
+    TS_ASSERT_EQUALS(
+        *te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()));
+    TS_ASSERT_EQUALS(
+        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()));
+    TS_ASSERT_EQUALS(
+        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()));
+    TS_ASSERT_EQUALS(
+        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor()));
+    TS_ASSERT_EQUALS(
+        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor()));
+    TS_ASSERT_EQUALS(
+        *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor()));
     TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
     TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
     TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
   }
 
-  void testDatatypesInfinite1() {
-    Datatype colors(d_em, "Colors");
-    colors.addConstructor(DatatypeConstructor("red"));
-    colors.addConstructor(DatatypeConstructor("orange"));
-    colors.addConstructor(DatatypeConstructor("yellow"));
-    colors.addConstructor(DatatypeConstructor("green"));
-    colors.addConstructor(DatatypeConstructor("blue"));
-    colors.addConstructor(DatatypeConstructor("violet"));
-    TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors));
-    Datatype listColors(d_em, "ListColors");
-    DatatypeConstructor consC("cons");
-    consC.addArg("car", colorsType.toType());
-    consC.addArg("cdr", DatatypeSelfType());
+  void testDTypesInfinite1()
+  {
+    DType colors("Colors");
+    colors.addConstructor(std::make_shared<DTypeConstructor>("red"));
+    colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+    colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+    colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
+    colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+    colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+    TypeNode colorsType = d_nm->mkDatatypeType(colors);
+    const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
+        colorsType.getDType().getConstructors();
+    DType listColors("ListColors");
+    std::shared_ptr<DTypeConstructor> consC =
+        std::make_shared<DTypeConstructor>("cons");
+    consC->addArg("car", colorsType);
+    consC->addArgSelf("cdr");
     listColors.addConstructor(consC);
-    listColors.addConstructor(DatatypeConstructor("nil"));
-    TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors));
+    listColors.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+    TypeNode listColorsType = d_nm->mkDatatypeType(listColors);
+    const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons =
+        listColorsType.getDType().getConstructors();
 
     TypeEnumerator te(listColorsType);
     TS_ASSERT( ! te.isFinished() );
-    Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons"));
-    Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil"));
-    Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red"));
-    Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange"));
-    Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow"));
+    Node cons = lctCons[0]->getConstructor();
+    Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor());
+    Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor());
+    Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor());
+    Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor());
     TS_ASSERT_EQUALS(*te, nil);
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
     TS_ASSERT( ! te.isFinished() );
@@ -212,7 +228,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT( ! te.isFinished() );
   }
 
-  void NOTYETtestDatatypesInfinite2() {
+  void NOTYETtestDTypesInfinite2()
+  {
     //TypeNode datatype;
     //TypeEnumerator te(datatype);
     //TS_ASSERT( ! te.isFinished() );