14 files changed, 63 insertions, 2257 deletions

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];
 }