Activate node-level datatype API (#3540)

4 files changed, 399 insertions, 1197 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 07af9617d..14b21a96a 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -37,42 +37,23 @@ using namespace std;
 
 namespace CVC4 {
 
-namespace expr {
-  namespace attr {
-    struct DatatypeIndexTag {};
-    struct DatatypeConsIndexTag {};
-    struct DatatypeFiniteTag {};
-    struct DatatypeFiniteComputedTag {};
-    struct DatatypeUFiniteTag {};
-    struct DatatypeUFiniteComputedTag {};
-  }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
-typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
+Datatype::~Datatype()
+{
+  ExprManagerScope ems(*d_em);
+  d_internal.reset();
+  d_constructors.clear();
+  delete d_record;
+}
 
 Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
     : d_em(em),
-      d_name(name),
-      d_params(),
-      d_isCo(isCo),
-      d_isTuple(false),
-      d_isRecord(false),
+      d_internal(nullptr),
       d_record(NULL),
-      d_constructors(),
-      d_resolved(false),
-      d_self(),
-      d_involvesExt(false),
-      d_involvesUt(false),
-      d_sygus_allow_const(false),
-      d_sygus_allow_all(false),
-      d_card(CardinalityUnknown()),
-      d_well_founded(0)
+      d_isRecord(false),
+      d_constructors()
 {
+  ExprManagerScope ems(*d_em);
+  d_internal = std::make_shared<DType>(name, isCo);
 }
 
 Datatype::Datatype(ExprManager* em,
@@ -80,26 +61,18 @@ Datatype::Datatype(ExprManager* em,
                    const std::vector<Type>& params,
                    bool isCo)
     : d_em(em),
-      d_name(name),
-      d_params(params),
-      d_isCo(isCo),
-      d_isTuple(false),
-      d_isRecord(false),
+      d_internal(nullptr),
       d_record(NULL),
-      d_constructors(),
-      d_resolved(false),
-      d_self(),
-      d_involvesExt(false),
-      d_involvesUt(false),
-      d_sygus_allow_const(false),
-      d_sygus_allow_all(false),
-      d_card(CardinalityUnknown()),
-      d_well_founded(0)
+      d_isRecord(false),
+      d_constructors()
 {
-}
-
-Datatype::~Datatype(){
-  delete d_record;
+  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) {
@@ -132,8 +105,8 @@ size_t Datatype::indexOfInternal(Expr item)
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return indexOf( item[0] );
   }else{
-    Assert(n.hasAttribute(DatatypeIndexAttr()));
-    return n.getAttribute(DatatypeIndexAttr());
+    Assert(n.hasAttribute(DTypeIndexAttr()));
+    return n.getAttribute(DTypeIndexAttr());
   }
 }
 
@@ -150,46 +123,82 @@ size_t Datatype::cindexOfInternal(Expr item)
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return cindexOf( item[0] );
   }else{
-    Assert(n.hasAttribute(DatatypeConsIndexAttr()));
-    return n.getAttribute(DatatypeConsIndexAttr());
+    Assert(n.hasAttribute(DTypeConsIndexAttr()));
+    return n.getAttribute(DTypeConsIndexAttr());
   }
 }
 
-void Datatype::resolve(ExprManager* em,
-                       const std::map<std::string, DatatypeType>& resolutions,
+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)
+                       const std::vector<SortConstructorType>& paramTypes,
+                       const std::vector<DatatypeType>& paramReplacements)
 {
-  PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
-  PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
-  PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
-                "Datatype::resolve(): resolutions doesn't contain me!");
+  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");
-  DatatypeType self = (*resolutions.find(d_name)).second;
-  PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
-  d_resolved = true;
-  size_t index = 0;
-  for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
-    (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
-    Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
-    Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
-  }
-  d_self = self;
 
-  d_involvesExt =  false;
-  d_involvesUt =  false;
-  for(const_iterator i = begin(); i != end(); ++i) {
-    if( (*i).involvesExternalType() ){
-      d_involvesExt =  true;
-    }
-    if( (*i).involvesUninterpretedType() ){
-      d_involvesUt =  true;
+  // 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();
     }
   }
 
@@ -200,52 +209,24 @@ void Datatype::resolve(ExprManager* em,
     }
     d_record = new Record(fields);
   }
-
-  if (isSygus())
-  {
-    // all datatype constructors should be sygus and have sygus operators whose
-    // free variables are subsets of sygus bound var list.
-    Node sbvln = Node::fromExpr(d_sygus_bvl);
-    std::unordered_set<Node, NodeHashFunction> svs;
-    for (const Node& sv : sbvln)
-    {
-      svs.insert(sv);
-    }
-    for (unsigned i = 0, ncons = d_constructors.size(); i < ncons; i++)
-    {
-      Expr sop = d_constructors[i].getSygusOp();
-      PrettyCheckArgument(!sop.isNull(),
-                          this,
-                          "Sygus datatype contains a non-sygus constructor");
-      Node sopn = Node::fromExpr(sop);
-      std::unordered_set<Node, NodeHashFunction> fvs;
-      expr::getFreeVariables(sopn, fvs);
-      for (const Node& v : fvs)
-      {
-        PrettyCheckArgument(
-            svs.find(v) != svs.end(),
-            this,
-            "Sygus constructor has an operator with a free variable that is "
-            "not in the formal argument list of the function-to-synthesize");
-      }
-    }
-  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
-  PrettyCheckArgument(!d_resolved, this,
-                "cannot add a constructor to a finalized Datatype");
+  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(!d_resolved, this,
-                      "cannot set sygus type to a finalized Datatype");        
-  d_sygus_type = st;
-  d_sygus_bvl = bvl;
-  d_sygus_allow_const = allow_const || allow_all;
-  d_sygus_allow_all = allow_all;
+  PrettyCheckArgument(
+      !isResolved(), this, "cannot set sygus type to a finalized Datatype");
+  TypeNode stn = TypeNode::fromType(st);
+  Node bvln = Node::fromExpr(bvl);
+  d_internal->setSygus(stn, bvln, allow_const, allow_all);
 }
 
 void Datatype::addSygusConstructor(Expr op,
@@ -254,8 +235,6 @@ void Datatype::addSygusConstructor(Expr op,
                                    std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
-  Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
-  Debug("dt-sygus") << "    sygus op : " << op << std::endl;
   // avoid name clashes
   std::stringstream ss;
   ss << getName() << "_" << getNumConstructors() << "_" << cname;
@@ -275,12 +254,14 @@ void Datatype::addSygusConstructor(Expr op,
 }
                                     
 void Datatype::setTuple() {
-  PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
-  d_isTuple = true;
+  PrettyCheckArgument(
+      !isResolved(), this, "cannot set tuple to a finalized Datatype");
+  d_internal->setTuple();
 }
 
 void Datatype::setRecord() {
-  PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
+  PrettyCheckArgument(
+      !isResolved(), this, "cannot set record to a finalized Datatype");
   d_isRecord = true;
 }
 
@@ -288,347 +269,143 @@ Cardinality Datatype::getCardinality(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
-  std::vector< Type > processing;
-  computeCardinality( t, processing );
-  return d_card;
+  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");
-  return getCardinality( d_self );
-}
-
-Cardinality Datatype::computeCardinality(Type t,
-                                         std::vector<Type>& processing) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
-    d_card = Cardinality::INTEGERS;
-  }else{
-    processing.push_back( d_self );
-    Cardinality c = 0;
-    for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-      c += (*i).computeCardinality( t, processing );
-    }
-    d_card = c;
-    processing.pop_back();
-  }
-  return d_card;
+  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);
-  if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){
-    if( isCodatatype() ){
-      Assert(d_card_u_assume[t].empty());
-      std::vector< Type > processing;
-      if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
-        d_card_rec_singleton[t] = 1;
-      }else{
-        d_card_rec_singleton[t] = -1;
-      }
-      if( d_card_rec_singleton[t]==1 ){
-        Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume[t].size() << " uninterpreted sorts: " << std::endl;
-        for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
-          Trace("dt-card") << "  " << d_card_u_assume[t][i] << std::endl;
-        }
-        Trace("dt-card") << std::endl;
-      }
-    }else{
-      d_card_rec_singleton[t] = -1;
-    }
-  }
-  return d_card_rec_singleton[t]==1;
+  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");
-  return isRecursiveSingleton( d_self );
+  ExprManagerScope ems(d_self);
+  return d_internal->isRecursiveSingleton();
 }
 
 unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
 {
-  Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
   Assert(isRecursiveSingleton(t));
-  return d_card_u_assume[t].size();
+  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");
-  return getNumRecursiveSingletonArgTypes( d_self );
+  ExprManagerScope ems(d_self);
+  return d_internal->getNumRecursiveSingletonArgTypes();
 }
 
 Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
 {
-  Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
   Assert(isRecursiveSingleton(t));
-  return d_card_u_assume[t][i];
+  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");
-  return getRecursiveSingletonArgType( d_self, i );
-}
-
-bool Datatype::computeCardinalityRecSingleton(Type t,
-                                              std::vector<Type>& processing,
-                                              std::vector<Type>& u_assume) const
-{
-  if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
-    return true;
-  }else{
-    if( d_card_rec_singleton[t]==0 ){
-      //if not yet computed
-      if( d_constructors.size()==1 ){
-        bool success = false;
-        processing.push_back( d_self );
-        for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) {
-          Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
-          //if it is an uninterpreted sort, then we depend on it having cardinality one
-          if( tc.isSort() ){
-            if( std::find( u_assume.begin(), u_assume.end(), tc )==u_assume.end() ){
-              u_assume.push_back( tc );
-            }
-          //if it is a datatype, recurse
-          }else if( tc.isDatatype() ){
-            const Datatype & dt = ((DatatypeType)tc).getDatatype();
-            if( !dt.computeCardinalityRecSingleton( t, processing, u_assume ) ){
-              return false;
-            }else{
-              success = true;
-            }
-          //if it is a builtin type, it must have cardinality one
-          }else if( !tc.getCardinality().isOne() ){
-            return false;
-          }
-        }
-        processing.pop_back();
-        return success;
-      }else{
-        return false;
-      }
-    }else if( d_card_rec_singleton[t]==-1 ){
-      return false;
-    }else{
-      for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
-        if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[t][i] )==u_assume.end() ){
-          u_assume.push_back( d_card_u_assume[t][i] );
-        }
-      }
-      return true;
-    }
-  }
+  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);
-
-  // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
-  TypeNode self = TypeNode::fromType(d_self);
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeFiniteComputedAttr())) {
-    return self.getAttribute(DatatypeFiniteAttr());
-  }
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isFinite( t )) {
-      self.setAttribute(DatatypeFiniteComputedAttr(), true);
-      self.setAttribute(DatatypeFiniteAttr(), false);
-      return false;
-    }
-  }
-  self.setAttribute(DatatypeFiniteComputedAttr(), true);
-  self.setAttribute(DatatypeFiniteAttr(), true);
-  return true;
+  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");
-  return isFinite( d_self );
+  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);
-  // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
-  TypeNode self = TypeNode::fromType(d_self);
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
-    return self.getAttribute(DatatypeUFiniteAttr());
-  }
-  //start by assuming it is not
-  self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-  self.setAttribute(DatatypeUFiniteAttr(), false);
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isInterpretedFinite( t )) {
-      return false;
-    }
-  }
-  self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-  self.setAttribute(DatatypeUFiniteAttr(), true);
-  return true;
+  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");
-  return isInterpretedFinite( d_self );
+  ExprManagerScope ems(d_self);
+  return d_internal->isInterpretedFinite();
 }
 
 bool Datatype::isWellFounded() const
 {
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  if( d_well_founded==0 ){
-    // we're using some internals, so we have to set up this library context
-    ExprManagerScope ems(d_self);
-    std::vector< Type > processing;
-    if( computeWellFounded( processing ) ){
-      d_well_founded = 1;
-    }else{
-      d_well_founded = -1;
-    }
-  }
-  return d_well_founded==1;
-}
-
-bool Datatype::computeWellFounded(std::vector<Type>& processing) const
-{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
-    return d_isCo;
-  }else{
-    processing.push_back( d_self );
-    for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-      if( (*i).computeWellFounded( processing ) ){
-        processing.pop_back();
-        return true;
-      }else{
-        Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl;
-      }
-    }
-    processing.pop_back();
-    Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl;
-    return false;
-  }
+  ExprManagerScope ems(d_self);
+  return d_internal->isWellFounded();
 }
 
 Expr Datatype::mkGroundTerm(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  return mkGroundTermInternal(t, false);
+  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");
-  return mkGroundTermInternal(t, true);
-}
-
-Expr Datatype::mkGroundTermInternal(Type t, bool isValue) const
-{
   ExprManagerScope ems(d_self);
-  Debug("datatypes") << "mkGroundTerm of type " << t
-                     << ", isValue = " << isValue << std::endl;
-  // is this already in the cache ?
-  std::map<Type, Expr>& cache = isValue ? d_ground_value : d_ground_term;
-  std::map<Type, Expr>::iterator it = cache.find(t);
-  if (it != cache.end())
-  {
-    Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
-    return it->second;
-  }
-  std::vector<Type> processing;
-  Expr groundTerm = computeGroundTerm(t, processing, isValue);
-  if (!groundTerm.isNull())
-  {
-    // we found a ground-term-constructing constructor!
-    cache[t] = groundTerm;
-    Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm
-                       << std::endl;
-  }
-  if (groundTerm.isNull())
-  {
-    if (!d_isCo)
-    {
-      // if we get all the way here, we aren't well-founded
-      IllegalArgument(
-          *this,
-          "datatype is not well-founded, cannot construct a ground term!");
-    }
-  }
-  return groundTerm;
-}
-
-Expr getSubtermWithType( Expr e, Type t, bool isTop ){
-  if( !isTop && e.getType()==t ){
-    return e;
-  }else{
-    for( unsigned i=0; i<e.getNumChildren(); i++ ){
-      Expr se = getSubtermWithType( e[i], t, false );
-      if( !se.isNull() ){
-        return se;
-      }
-    }
-    return Expr();
-  }
-}
-
-Expr Datatype::computeGroundTerm(Type t,
-                                 std::vector<Type>& processing,
-                                 bool isValue) const
-{
-  if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
-    processing.push_back( t );
-    for( unsigned r=0; r<2; r++ ){
-      for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-        //do nullary constructors first
-        if( ((*i).getNumArgs()==0)==(r==0)){
-          Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
-          Expr e =
-              (*i).computeGroundTerm(t, processing, d_ground_term, isValue);
-          if( !e.isNull() ){
-            //must check subterms for the same type to avoid infinite loops in type enumeration
-            Expr se = getSubtermWithType( e, t, true );
-            if( !se.isNull() ){
-              Debug("datatypes") << "Take subterm " << se << std::endl;
-              e = se;
-            }
-            processing.pop_back();
-            return e;
-          }else{
-            Debug("datatypes") << "...failed." << std::endl;
-          }
-        }
-      }
-    }
-    processing.pop_back();
-  }else{
-    Debug("datatypes") << "...already processing " << t << " " << d_self << std::endl;
-  }
-  return Expr();
+  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");
-  PrettyCheckArgument(!d_self.isNull(), *this);
-  return DatatypeType(d_self);
+  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");
-  PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
-  return DatatypeType(d_self).instantiate(params);
+  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
@@ -639,70 +416,6 @@ bool Datatype::operator==(const Datatype& other) const
   if(this == &other) {
     return true;
   }
-
-  if(isResolved() != other.isResolved()) {
-    return false;
-  }
-
-  if( d_name != other.d_name ||
-      getNumConstructors() != other.getNumConstructors() ) {
-    return false;
-  }
-  for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
-    Assert(j != other.end());
-    // two constructors are == iff they have the same name, their
-    // constructors and testers are equal and they have exactly
-    // matching args (in the same order)
-    if((*i).getName() != (*j).getName() ||
-       (*i).getNumArgs() != (*j).getNumArgs()) {
-      return false;
-    }
-    // testing equivalence of constructors and testers is harder b/c
-    // this constructor might not be resolved yet; only compare them
-    // if they are both resolved
-    Assert(isResolved() == !(*i).d_constructor.isNull()
-           && isResolved() == !(*i).d_tester.isNull()
-           && (*i).d_constructor.isNull() == (*j).d_constructor.isNull()
-           && (*i).d_tester.isNull() == (*j).d_tester.isNull());
-    if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
-      return false;
-    }
-    if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
-      return false;
-    }
-    for(DatatypeConstructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
-      Assert(l != (*j).end());
-      if((*k).getName() != (*l).getName()) {
-        return false;
-      }
-      // testing equivalence of selectors is harder b/c args might not
-      // be resolved yet
-      Assert(isResolved() == (*k).isResolved()
-             && (*k).isResolved() == (*l).isResolved());
-      if((*k).isResolved()) {
-        // both are resolved, so simply compare the selectors directly
-        if((*k).d_selector != (*l).d_selector) {
-          return false;
-        }
-      } else {
-        // neither is resolved, so compare their (possibly unresolved)
-        // types; we don't know if they'll be resolved the same way,
-        // so we can't ever say unresolved types are equal
-        if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) {
-          if((*k).d_selector.getType() != (*l).d_selector.getType()) {
-            return false;
-          }
-        } else {
-          if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) {
-            // Fine, the selectors are equal if the rest of the
-            // enclosing datatypes are equal...
-          } else {
-            return false;
-          }
-        }
-      }
-    }
-  }
   return true;
 }
 
@@ -717,31 +430,11 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const {
       return *i;
     }
   }
-  IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
-}
-
-
-Expr Datatype::getSharedSelector( Type dtt, Type t, unsigned index ) const{
-  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  std::map< Type, std::map< Type, std::map< unsigned, Expr > > >::iterator itd = d_shared_sel.find( dtt );
-  if( itd!=d_shared_sel.end() ){
-    std::map< Type, std::map< unsigned, Expr > >::iterator its = itd->second.find( t );
-    if( its!=itd->second.end() ){
-      std::map< unsigned, Expr >::iterator it = its->second.find( index );
-      if( it!=its->second.end() ){
-        return it->second;
-      }
-    }
-  }
-  //make the shared selector
-  Expr s;
-  NodeManager* nm = NodeManager::fromExprManager( d_self.getExprManager() );
-  std::stringstream ss;
-  ss << "sel_" << index;
-  s = nm->mkSkolem(ss.str(), nm->mkSelectorType(TypeNode::fromType(dtt), TypeNode::fromType(t)), "is a shared selector", NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-  d_shared_sel[dtt][t][index] = s;
-  Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl;
-  return s; 
+  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 {
@@ -749,27 +442,27 @@ Expr Datatype::getConstructor(std::string name) const {
 }
 
 Type Datatype::getSygusType() const {
-  return d_sygus_type;
+  return d_internal->getSygusType().toType();
 }
 
 Expr Datatype::getSygusVarList() const {
-  return d_sygus_bvl;
+  return d_internal->getSygusVarList().toExpr();
 }
 
 bool Datatype::getSygusAllowConst() const {
-  return d_sygus_allow_const;
+  return d_internal->getSygusAllowConst();
 }
 
 bool Datatype::getSygusAllowAll() const {
-  return d_sygus_allow_all;
+  return d_internal->getSygusAllowAll();
 }
 
 bool Datatype::involvesExternalType() const{
-  return d_involvesExt;
+  return d_internal->involvesExternalType();
 }
 
 bool Datatype::involvesUninterpretedType() const{
-  return d_involvesUt;
+  return d_internal->involvesUninterpretedType();
 }
 
 const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
@@ -777,136 +470,22 @@ const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
   return &d_constructors;
 }
 
-void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
-                                  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, size_t cindex)
-{
-  PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
-  PrettyCheckArgument(!isResolved(),
-                "cannot resolve a Datatype constructor twice; "
-                "perhaps the same constructor was added twice, "
-                "or to two datatypes?");
-
-  // we're using some internals, so we have to set up this library context
-  ExprManagerScope ems(*em);
-
-  NodeManager* nm = NodeManager::fromExprManager(em);
-  TypeNode selfTypeNode = TypeNode::fromType(self);
-  size_t index = 0;
-  for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
-    if((*i).d_selector.isNull()) {
-      // the unresolved type wasn't created here; do name resolution
-      string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
-      (*i).d_name.resize((*i).d_name.find('\0'));
-      if(typeName == "") {
-        (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-      } else {
-        map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
-        if(j == resolutions.end()) {
-          stringstream msg;
-          msg << "cannot resolve type \"" << typeName << "\" "
-              << "in selector \"" << (*i).d_name << "\" "
-              << "of constructor \"" << d_name << "\"";
-          throw DatatypeResolutionException(msg.str());
-        } else {
-          (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-        }
-      }
-    } else {
-      // the type for the selector already exists; may need
-      // complex-type substitution
-      Type range = (*i).d_selector.getType();
-      if(!placeholders.empty()) {
-        range = range.substitute(placeholders, replacements);
-      }
-      if(!paramTypes.empty() ) {
-        range = doParametricSubstitution( range, paramTypes, paramReplacements );
-      }
-      (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-    }
-    Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
-    Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
-    (*i).d_resolved = true;
-  }
-
-  Assert(index == getNumArgs());
-
-  // Set constructor/tester last, since DatatypeConstructor::isResolved()
-  // returns true when d_tester is not the null Expr.  If something
-  // fails above, we want Constuctor::isResolved() to remain "false".
-  // Further, mkConstructorType() iterates over the selectors, so
-  // should get the results of any resolutions we did above.
-  d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-  d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
-  // associate constructor with all selectors
-  for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
-    (*i).d_constructor = d_constructor;
-  }
-}
-
-Type DatatypeConstructor::doParametricSubstitution( Type range,
-                                  const std::vector< SortConstructorType >& paramTypes,
-                                  const std::vector< DatatypeType >& paramReplacements ) {
-  TypeNode typn = TypeNode::fromType( range );
-  if(typn.getNumChildren() == 0) {
-    return range;
-  } else {
-    std::vector< Type > origChildren;
-    std::vector< Type > children;
-    for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) {
-      origChildren.push_back( (*i).toType() );
-      children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
-    }
-    for( unsigned i = 0; i < paramTypes.size(); ++i ) {
-      if( paramTypes[i].getArity() == origChildren.size() ) {
-        Type tn = paramTypes[i].instantiate( origChildren );
-        if( range == tn ) {
-          return paramReplacements[i].instantiate( children );
-        }
-      }
-    }
-    NodeBuilder<> nb(typn.getKind());
-    for( unsigned i = 0; i < children.size(); ++i ) {
-      nb << TypeNode::fromType( children[i] );
-    }
-    return nb.constructTypeNode().toType();
-  }
-}
-
 DatatypeConstructor::DatatypeConstructor(std::string name)
-    :  // 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 tester name away inside the constructor name until
-       // resolution.
-      d_internal(nullptr),  // until the Node-level datatype API is activated
-      d_name(name + '\0' + "is_" + name),  // default tester name is "is_FOO"
-      d_tester(),
-      d_args(),
-      d_sygus_pc(nullptr),
-      d_weight(1)
+    : d_internal(nullptr),
+      d_testerName("is_" + name)  // default tester name is "is_FOO"
 {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  d_internal = std::make_shared<DTypeConstructor>(name, 1);
 }
 
 DatatypeConstructor::DatatypeConstructor(std::string name,
                                          std::string tester,
                                          unsigned weight)
-    :  // 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 tester name away inside the constructor name until
-       // resolution.
-      d_internal(nullptr),  // until the Node-level datatype API is activated
-      d_name(name + '\0' + tester),
-      d_tester(),
-      d_args(),
-      d_sygus_pc(nullptr),
-      d_weight(weight)
+    : d_internal(nullptr), d_testerName(tester)
 {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+  d_internal = std::make_shared<DTypeConstructor>(name, weight);
 }
 
 void DatatypeConstructor::setSygus(Expr op,
@@ -914,7 +493,9 @@ void DatatypeConstructor::setSygus(Expr op,
 {
   PrettyCheckArgument(
       !isResolved(), this, "cannot modify a finalized Datatype constructor");
-  d_sygus_op = op;
+  Node opn = Node::fromExpr(op);
+  d_internal->setSygus(op);
+  // print callback lives at the expression level currently
   d_sygus_pc = spc;
 }
 
@@ -938,6 +519,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type 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) {
@@ -948,6 +530,7 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedTyp
   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) {
@@ -958,16 +541,18 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
   // 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_name.substr(0, d_name.find('\0'));
+  return d_internal->getName();
 }
 
 std::string DatatypeConstructor::getTesterName() const
 {
-  return d_name.substr(d_name.find('\0') + 1);
+  // not stored internally, since tester names only pertain to parsing
+  return d_testerName;
 }
 
 Expr DatatypeConstructor::getConstructor() const {
@@ -979,44 +564,34 @@ 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);
-  const Datatype& dt = Datatype::datatypeOf(d_constructor);
-  PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
-  TypeNode dtt = TypeNode::fromType(dt.getDatatypeType());
-  TypeMatcher m(dtt);
-  m.doMatching(dtt, TypeNode::fromType(returnType));
-  std::vector<TypeNode> sns;
-  m.getMatches(sns);
-  std::vector<Type> subst;
-  for (TypeNode& s : sns)
-  {
-    subst.push_back(s.toType());
-  }
-  vector<Type> params = dt.getParameters();
-  return d_constructor.getType().substitute(params, subst);
+  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");
-  return d_tester;
+  ExprManagerScope ems(d_constructor);
+  return d_internal->getTester().toExpr();
 }
 
 Expr DatatypeConstructor::getSygusOp() const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_op;
+  ExprManagerScope ems(d_constructor);
+  return d_internal->getSygusOp().toExpr();
 }
 
 bool DatatypeConstructor::isSygusIdFunc() const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return (d_sygus_op.getKind() == kind::LAMBDA
-          && d_sygus_op[0].getNumChildren() == 1
-          && d_sygus_op[0][0] == d_sygus_op[1]);
+  ExprManagerScope ems(d_constructor);
+  return d_internal->isSygusIdFunc();
 }
 
 unsigned DatatypeConstructor::getWeight() const
 {
   PrettyCheckArgument(
       isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_weight;
+  ExprManagerScope ems(d_constructor);
+  return d_internal->getWeight();
 }
 
 std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
@@ -1029,214 +604,27 @@ std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback()
 Cardinality DatatypeConstructor::getCardinality(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
-  Cardinality c = 1;
-
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality();
-  }
-
-  return c;
-}
-
-/** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality(
-    Type t, std::vector<Type>& processing) const
-{
-  Cardinality c = 1;
-  std::vector< Type > instTypes;
-  std::vector< Type > paramTypes;
-  if( DatatypeType(t).isParametric() ){
-    paramTypes = DatatypeType(t).getDatatype().getParameters();
-    instTypes = DatatypeType(t).getParamTypes();
-  }  
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type tc = SelectorType((*i).getSelector().getType()).getRangeType();
-    if( DatatypeType(t).isParametric() ){
-      tc = tc.substitute( paramTypes, instTypes );
-    }
-    if( tc.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)tc).getDatatype();
-      c *= dt.computeCardinality( t, processing );
-    }else{
-      c *= tc.getCardinality();
-    }
-  }
-  return c;
-}
-
-bool DatatypeConstructor::computeWellFounded(
-    std::vector<Type>& processing) const
-{
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = SelectorType((*i).getSelector().getType()).getRangeType();
-    if( t.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)t).getDatatype();
-      if( !dt.computeWellFounded( processing ) ){
-        return false;
-      }
-    }
-  }
-  return true;
+  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");
-
-  // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
-  TNode self = Node::fromExpr(d_constructor);
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeFiniteComputedAttr())) {
-    return self.getAttribute(DatatypeFiniteAttr());
-  }
-  std::vector< Type > instTypes;
-  std::vector< Type > paramTypes;
-  if( DatatypeType(t).isParametric() ){
-    paramTypes = DatatypeType(t).getDatatype().getParameters();
-    instTypes = DatatypeType(t).getParamTypes();
-  }  
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type tc = (*i).getRangeType();
-    if( DatatypeType(t).isParametric() ){
-      tc = tc.substitute( paramTypes, instTypes );
-    }
-    if (!tc.isFinite())
-    {
-      self.setAttribute(DatatypeFiniteComputedAttr(), true);
-      self.setAttribute(DatatypeFiniteAttr(), false);
-      return false;
-    }
-  }
-  self.setAttribute(DatatypeFiniteComputedAttr(), true);
-  self.setAttribute(DatatypeFiniteAttr(), true);
-  return true;
+  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");
-  // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
-  TNode self = Node::fromExpr(d_constructor);
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
-    return self.getAttribute(DatatypeUFiniteAttr());
-  }
-  std::vector< Type > instTypes;
-  std::vector< Type > paramTypes;
-  if( DatatypeType(t).isParametric() ){
-    paramTypes = DatatypeType(t).getDatatype().getParameters();
-    instTypes = DatatypeType(t).getParamTypes();
-  }  
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type tc = (*i).getRangeType();
-    if( DatatypeType(t).isParametric() ){
-      tc = tc.substitute( paramTypes, instTypes );
-    }
-    TypeNode tcn = TypeNode::fromType( tc );
-    if(!tcn.isInterpretedFinite()) {
-      self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-      self.setAttribute(DatatypeUFiniteAttr(), false);
-      return false;
-    }
-  }
-  self.setAttribute(DatatypeUFiniteComputedAttr(), true);
-  self.setAttribute(DatatypeUFiniteAttr(), true);
-  return true;
+  TypeNode tn = TypeNode::fromType(t);
+  return d_internal->isInterpretedFinite(tn);
 }
 
-Expr DatatypeConstructor::computeGroundTerm(Type t,
-                                            std::vector<Type>& processing,
-                                            std::map<Type, Expr>& gt,
-                                            bool isValue) const
-{
-  // we're using some internals, so we have to set up this library context
-  ExprManagerScope ems(d_constructor);
-
-  std::vector<Expr> groundTerms;
-  groundTerms.push_back(getConstructor());
-
-  // for each selector, get a ground term
-  std::vector< Type > instTypes;
-  std::vector< Type > paramTypes;
-  bool isParam = static_cast<DatatypeType>(t).isParametric();
-  if (isParam)
-  {
-    paramTypes = DatatypeType(t).getDatatype().getParameters();
-    instTypes = DatatypeType(t).getParamTypes();
-  }
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
-    if (isParam)
-    {
-      selType = selType.substitute( paramTypes, instTypes );
-    }
-    Expr arg;
-    if( selType.isDatatype() ){
-      std::map< Type, Expr >::iterator itgt = gt.find( selType );
-      if( itgt != gt.end() ){
-        arg = itgt->second;
-      }else{
-        const Datatype & dt = DatatypeType(selType).getDatatype();
-        arg = dt.computeGroundTerm(selType, processing, isValue);
-      }
-    }
-    else
-    {
-      // call mkGroundValue or mkGroundTerm based on isValue
-      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
-    }
-    if( arg.isNull() ){
-      Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
-      return Expr();
-    }else{
-      Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl;
-      groundTerms.push_back(arg);
-    }
-  }
-
-  Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
-  if (isParam)
-  {
-    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
-    // type is parametric, must apply type ascription
-    Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
-    groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
-                       getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
-                       groundTerms[0]);
-    groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
-  }
-  return groundTerm;
-}
-
-void DatatypeConstructor::computeSharedSelectors( Type domainType ) const {
-  if( d_shared_selectors[domainType].size()<getNumArgs() ){
-    TypeNode ctype;
-    if( DatatypeType(domainType).isParametric() ){
-      ctype = TypeNode::fromType( getSpecializedConstructorType( domainType ) );
-    }else{
-      ctype = TypeNode::fromType( d_constructor.getType() );
-    }
-    Assert(ctype.isConstructor());
-    Assert(ctype.getNumChildren() - 1 == getNumArgs());
-    //compute the shared selectors
-    const Datatype& dt = Datatype::datatypeOf(d_constructor);
-    std::map< TypeNode, unsigned > counter;
-    for( unsigned j=0; j<ctype.getNumChildren()-1; j++ ){
-      TypeNode t = ctype[j];
-      Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] );
-      d_shared_selectors[domainType].push_back( ss );
-      Assert(d_shared_selector_index[domainType].find(ss)
-             == d_shared_selector_index[domainType].end());
-      d_shared_selector_index[domainType][ss] = j;
-      counter[t]++;
-    }
-  }
-}
-
-
 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
   return d_args[index];
@@ -1248,49 +636,44 @@ const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name)
       return *i;
     }
   }
-  IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+  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].getSelector();
+  return (*this)[name].d_selector;
 }
 
 Type DatatypeConstructor::getArgType(unsigned index) const
 {
   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
-  return static_cast<SelectorType>((*this)[index].getType()).getRangeType();
+  ExprManagerScope ems(d_constructor);
+  return d_internal->getArgType(index).toType();
 }
 
 bool DatatypeConstructor::involvesExternalType() const{
-  for(const_iterator i = begin(); i != end(); ++i) {
-    if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
-      return true;
-    }
-  }
-  return false;
+  ExprManagerScope ems(d_constructor);
+  return d_internal->involvesExternalType();
 }
 
 bool DatatypeConstructor::involvesUninterpretedType() const{
-  for(const_iterator i = begin(); i != end(); ++i) {
-    if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) {
-      return true;
-    }
-  }
-  return false;
+  ExprManagerScope ems(d_constructor);
+  return d_internal->involvesUninterpretedType();
 }
 
 DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
-    : d_internal(nullptr),  // until the Node-level datatype API is activated
-      d_name(name),
-      d_selector(selector),
-      d_resolved(false)
+    : 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_name;
+  string name = d_internal->getName();
   const size_t nul = name.find('\0');
   if(nul != string::npos) {
     name.resize(nul);
@@ -1306,42 +689,27 @@ Expr DatatypeConstructorArg::getSelector() const {
 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");
-  if( options::dtSharedSelectors() ){
-    computeSharedSelectors( domainType );
-    Assert(d_shared_selectors[domainType].size() == getNumArgs());
-    return d_shared_selectors[domainType][index];
-  }else{
-    return d_args[index].getSelector();
-  }
+  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");
-  if( options::dtSharedSelectors() ){
-    Assert(sel.getType().isSelector());
-    Type domainType = ((SelectorType)sel.getType()).getDomain();
-    computeSharedSelectors( domainType );
-    std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel );
-    if( its!=d_shared_selector_index[domainType].end() ){
-      return (int)its->second;
-    }
-  }else{
-    unsigned sindex = Datatype::indexOf(sel);
-    if( getNumArgs() > sindex && d_args[sindex].getSelector() == sel ){
-      return (int)sindex;
-    }
-  }
-  return -1;
+  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");
-  return d_constructor;
+  ExprManagerScope ems(d_selector);
+  return d_internal->getConstructor().toExpr();
 }
 
 SelectorType DatatypeConstructorArg::getType() const {
-  return getSelector().getType();
+  return d_selector.getType();
 }
 
 Type DatatypeConstructorArg::getRangeType() const {
@@ -1350,7 +718,25 @@ Type DatatypeConstructorArg::getRangeType() const {
 
 bool DatatypeConstructorArg::isUnresolvedSelf() const
 {
-  return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
+  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)
@@ -1423,7 +809,8 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
 
 void DatatypeConstructorArg::toStream(std::ostream& out) const
 {
-  out << getName() << ": ";
+  std::string name = getName();
+  out << name << ": ";
 
   Type t;
   if (isResolved())
@@ -1432,7 +819,7 @@ void DatatypeConstructorArg::toStream(std::ostream& out) const
   }
   else if (d_selector.isNull())
   {
-    string typeName = d_name.substr(d_name.find('\0') + 1);
+    string typeName = name.substr(name.find('\0') + 1);
     out << ((typeName == "") ? "[self]" : typeName);
     return;
   }
@@ -1448,4 +835,119 @@ std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
   return out << "index_" << dic.getIndex();
 }
 
+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; }
+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
index c9191aadf..dccda5ad4 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -163,14 +163,8 @@ class CVC4_PUBLIC DatatypeConstructorArg {
  private:
   /** The internal representation */
   std::shared_ptr<DTypeSelector> d_internal;
-  /** the name of this selector */
-  std::string d_name;
-  /** the selector expression */
+  /** The selector */
   Expr d_selector;
-  /** the constructor associated with this selector */
-  Expr d_constructor;
-  /** whether this class has been resolved */
-  bool d_resolved;
   /** is this selector unresolved? */
   bool isUnresolvedSelf() const;
   /** constructor */
@@ -323,7 +317,7 @@ class CVC4_PUBLIC DatatypeConstructor {
   /**
    * Get the number of arguments (so far) of this Datatype constructor.
    */
-  inline size_t getNumArgs() const;
+  size_t getNumArgs() const;
 
   /**
    * Get the specialized constructor type for a parametric
@@ -363,16 +357,16 @@ class CVC4_PUBLIC DatatypeConstructor {
    * Returns true iff this Datatype constructor has already been
    * resolved.
    */
-  inline bool isResolved() const;
+  bool isResolved() const;
 
   /** Get the beginning iterator over DatatypeConstructor args. */
-  inline iterator begin();
+  iterator begin();
   /** Get the ending iterator over DatatypeConstructor args. */
-  inline iterator end();
+  iterator end();
   /** Get the beginning const_iterator over DatatypeConstructor args. */
-  inline const_iterator begin() const;
+  const_iterator begin() const;
   /** Get the ending const_iterator over DatatypeConstructor args. */
-  inline const_iterator end() const;
+  const_iterator end() const;
 
   /** Get the ith DatatypeConstructor arg. */
   const DatatypeConstructorArg& operator[](size_t index) const;
@@ -462,102 +456,14 @@ class CVC4_PUBLIC DatatypeConstructor {
  private:
   /** The internal representation */
   std::shared_ptr<DTypeConstructor> d_internal;
-  /** the name of the constructor */
-  std::string d_name;
-  /** the constructor expression */
+  /** the name of the tester */
+  std::string d_testerName;
+  /** The constructor */
   Expr d_constructor;
-  /** the tester for this constructor */
-  Expr d_tester;
   /** the arguments of this constructor */
   std::vector<DatatypeConstructorArg> d_args;
-  /** sygus operator */
-  Expr d_sygus_op;
   /** sygus print callback */
   std::shared_ptr<SygusPrintCallback> d_sygus_pc;
-  /** weight */
-  unsigned d_weight;
-
-  /** shared selectors for each type
-   *
-   * This stores the shared (constructor-agnotic)
-   * selectors that access the fields of this datatype.
-   * In the terminology of "Datatypes with Shared Selectors",
-   * this stores:
-   *   sel_{dtt}^{T1,atos(T1,C,1)}, ...,
-   *   sel_{dtt}^{Tn,atos(Tn,C,n)}
-   * where C is this constructor, which has type
-   * T1 x ... x Tn -> dtt above.
-   * We store this information for (possibly multiple)
-   * datatype types dtt, since this constructor may be
-   * for a parametric datatype, where dtt is an instantiated
-   * parametric datatype.
-   */
-  mutable std::map<Type, std::vector<Expr> > d_shared_selectors;
-  /** for each type, a cache mapping from shared selectors to
-   * its argument index for this constructor.
-   */
-  mutable std::map<Type, std::map<Expr, unsigned> > d_shared_selector_index;
-  /** resolve
-   *
-   * This resolves (initializes) the constructor. For details
-   * on how datatypes and their constructors are resolved, see
-   * documentation for Datatype::resolve.
-   */
-  void resolve(ExprManager* em,
-               DatatypeType self,
-               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,
-               size_t cindex);
-
-  /** Helper function for resolving parametric datatypes.
-   *
-   * This replaces instances of the SortConstructorType produced for unresolved
-   * parametric datatypes, with the corresponding resolved DatatypeType.  For
-   * example, take the parametric definition of a list,
-   *    list[T] = cons(car : T, cdr : list[T]) | null.
-   * If "range" is the unresolved parametric datatype:
-   *   DATATYPE list =
-   *    cons(car: SORT_TAG_1,
-   *         cdr: SORT_TAG_2(SORT_TAG_1)) | null END;,
-   * this function will return the resolved type:
-   *   DATATYPE list =
-   *    cons(car: SORT_TAG_1,
-   *         cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END;
-   */
-  Type doParametricSubstitution(
-      Type range,
-      const std::vector<SortConstructorType>& paramTypes,
-      const std::vector<DatatypeType>& paramReplacements);
-
-  /** compute the cardinality of this datatype */
-  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
-  /** compute whether this datatype is well-founded */
-  bool computeWellFounded(std::vector<Type>& processing) const;
-  /** compute ground term
-   *
-   * This method is used for constructing a term that is an application
-   * of this constructor whose type is t.
-   *
-   * The argument processing is the set of datatype types we are currently
-   * traversing. This is used to avoid infinite loops.
-   *
-   * The argument gt caches the ground terms we have computed so far.
-   *
-   * The argument isValue is whether we are constructing a constant value. If
-   * this flag is false, we are constructing a canonical ground term that is
-   * not necessarily constant.
-   */
-  Expr computeGroundTerm(Type t,
-                         std::vector<Type>& processing,
-                         std::map<Type, Expr>& gt,
-                         bool isValue) const;
-  /** compute shared selectors
-   * This computes the maps d_shared_selectors and d_shared_selector_index.
-   */
-  void computeSharedSelectors(Type domainType) const;
 };/* class DatatypeConstructor */
 
 class DType;
@@ -623,6 +529,7 @@ class DType;
  */
 class CVC4_PUBLIC Datatype {
   friend class DatatypeConstructor;
+  friend class ExprManager;  // for access to resolve()
   friend class NodeManager;  // temporary, for access to d_internal
  public:
   /**
@@ -731,37 +638,37 @@ class CVC4_PUBLIC Datatype {
   void setRecord();
 
   /** Get the name of this Datatype. */
-  inline std::string getName() const;
+  std::string getName() const;
 
   /** Get the number of constructors (so far) for this Datatype. */
-  inline size_t getNumConstructors() const;
+  size_t getNumConstructors() const;
 
   /** Is this datatype parametric? */
-  inline bool isParametric() const;
+  bool isParametric() const;
 
   /** Get the nubmer of type parameters */
-  inline size_t getNumParameters() const;
+  size_t getNumParameters() const;
 
   /** Get parameter */
-  inline Type getParameter( unsigned int i ) const;
+  Type getParameter(unsigned int i) const;
 
   /** Get parameters */
-  inline std::vector<Type> getParameters() const;
+  std::vector<Type> getParameters() const;
 
   /** is this a co-datatype? */
-  inline bool isCodatatype() const;
+  bool isCodatatype() const;
 
   /** is this a sygus datatype? */
-  inline bool isSygus() const;
+  bool isSygus() const;
 
   /** is this a tuple datatype? */
-  inline bool isTuple() const;
+  bool isTuple() const;
 
   /** is this a record datatype? */
-  inline bool isRecord() const;
+  bool isRecord() const;
 
   /** get the record representation for this datatype */
-  inline Record * getRecord() const;
+  Record* getRecord() const;
 
   /**
    * Return the cardinality of this datatype.
@@ -887,19 +794,19 @@ class CVC4_PUBLIC Datatype {
    */
   bool operator==(const Datatype& other) const;
   /** Return true iff the two Datatypes are not the same. */
-  inline bool operator!=(const Datatype& other) const;
+  bool operator!=(const Datatype& other) const;
 
   /** Return true iff this Datatype has already been resolved. */
-  inline bool isResolved() const;
+  bool isResolved() const;
 
   /** Get the beginning iterator over DatatypeConstructors. */
-  inline iterator begin();
+  iterator begin();
   /** Get the ending iterator over DatatypeConstructors. */
-  inline iterator end();
+  iterator end();
   /** Get the beginning const_iterator over DatatypeConstructors. */
-  inline const_iterator begin() const;
+  const_iterator begin() const;
   /** Get the ending const_iterator over DatatypeConstructors. */
-  inline const_iterator end() const;
+  const_iterator end() const;
 
   /** Get the ith DatatypeConstructor. */
   const DatatypeConstructor& operator[](size_t index) const;
@@ -981,67 +888,14 @@ class CVC4_PUBLIC Datatype {
   ExprManager* d_em;
   /** The internal representation */
   std::shared_ptr<DType> d_internal;
-  /** name of this datatype */
-  std::string d_name;
-  /** the type parameters of this datatype (if this is a parametric datatype)
-   */
-  std::vector<Type> d_params;
-  /** whether the datatype is a codatatype. */
-  bool d_isCo;
-  /** whether the datatype is a tuple */
-  bool d_isTuple;
-  /** whether the datatype is a record */
-  bool d_isRecord;
+  /** self type */
+  Type d_self;
   /** the data of the record for this datatype (if applicable) */
   Record* d_record;
+  /** whether the datatype is a record */
+  bool d_isRecord;
   /** the constructors of this datatype */
   std::vector<DatatypeConstructor> d_constructors;
-  /** whether this datatype has been resolved */
-  bool d_resolved;
-  Type d_self;
-  /** cache for involves external type */
-  bool d_involvesExt;
-  /** cache for involves uninterpreted type */
-  bool d_involvesUt;
-  /** the builtin type that this sygus type encodes */
-  Type d_sygus_type;
-  /** the variable list for the sygus function to synthesize */
-  Expr d_sygus_bvl;
-  /** whether all constants are allowed as solutions */
-  bool d_sygus_allow_const;
-  /** whether all terms are allowed as solutions */
-  bool d_sygus_allow_all;
-
-  /** the cardinality of this datatype
-  * "mutable" because computing the cardinality can be expensive,
-  * and so it's computed just once, on demand---this is the cache
-  */
-  mutable Cardinality d_card;
-
-  /** is this type a recursive singleton type?
-   * The range of this map stores
-   * 0 if the field has not been computed,
-   * 1 if this datatype is a recursive singleton type,
-   * -1 if this datatype is not a recursive singleton type.
-   * For definition of (co)recursive singleton, see
-   * Section 2 of Reynolds et al. CADE 2015.
-   */
-  mutable std::map<Type, int> d_card_rec_singleton;
-  /** if d_card_rec_singleton is true,
-  * This datatype has infinite cardinality if at least one of the
-  * following uninterpreted sorts having cardinality > 1.
-  */
-  mutable std::map<Type, std::vector<Type> > d_card_u_assume;
-  /** cache of whether this datatype is well-founded */
-  mutable int d_well_founded;
-  /** cache of ground term for this datatype */
-  mutable std::map<Type, Expr> d_ground_term;
-  /** cache of ground values for this datatype */
-  mutable std::map<Type, Expr> d_ground_value;
-  /** cache of shared selectors for this datatype */
-  mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > >
-      d_shared_sel;
-
   /**
    * Datatypes refer to themselves, recursively, and we have a
    * chicken-and-egg problem.  The DatatypeType around the Datatype
@@ -1061,7 +915,6 @@ class CVC4_PUBLIC Datatype {
    * they are two maps).  placeholders->replacements give type variables
    * that should be resolved in the case of parametric datatypes.
    *
-   * @param em the ExprManager at play
    * @param resolutions a map of strings to DatatypeTypes currently under
    * resolution
    * @param placeholders the types in these Datatypes under resolution that must
@@ -1071,52 +924,11 @@ class CVC4_PUBLIC Datatype {
    * that must be replaced
    * @param paramReplacements the corresponding (parametric) DatatypeTypes
    */
-  void resolve(ExprManager* em,
-               const std::map<std::string, DatatypeType>& resolutions,
+  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);
-  friend class ExprManager;  // for access to resolve()
-
-  /** compute the cardinality of this datatype */
-  Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
-  /** compute whether this datatype is a recursive singleton */
-  bool computeCardinalityRecSingleton(Type t,
-                                      std::vector<Type>& processing,
-                                      std::vector<Type>& u_assume) const;
-  /** compute whether this datatype is well-founded */
-  bool computeWellFounded(std::vector<Type>& processing) const;
-  /** compute ground term
-   *
-   * This method checks if there is a term of this datatype whose type is t
-   * that is finitely constructable. As needed, it traverses its subfield types.
-   *
-   * The argument processing is the set of datatype types we are currently
-   * traversing.
-   *
-   * The argument isValue is whether we are constructing a constant value. If
-   * this flag is false, we are constructing a canonical ground term that is
-   * not necessarily constant.
-   */
-  Expr computeGroundTerm(Type t,
-                         std::vector<Type>& processing,
-                         bool isValue) const;
-  /** Get the shared selector
-   *
-   * This returns the index^th (constructor-agnostic)
-   * selector for type t. The type dtt is the datatype
-   * type whose datatype is this class, where this may
-   * be an instantiated parametric datatype.
-   *
-   * In the terminology of "Datatypes with Shared Selectors",
-   * this returns the term sel_{dtt}^{t,index}.
-   */
-  Expr getSharedSelector(Type dtt, Type t, unsigned index) const;
-  /**
-   * Helper for mkGroundTerm and mkGroundValue above.
-   */
-  Expr mkGroundTermInternal(Type t, bool isValue) const;
 };/* class Datatype */
 
 /**
@@ -1202,116 +1014,6 @@ inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
 
 inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
 
-inline std::string Datatype::getName() const { return d_name; }
-inline size_t Datatype::getNumConstructors() const
-{
-  return d_constructors.size();
-}
-
-inline bool Datatype::isParametric() const { return d_params.size() > 0; }
-inline size_t Datatype::getNumParameters() const { return d_params.size(); }
-inline Type Datatype::getParameter( unsigned int i ) const {
-  CheckArgument(isParametric(), this,
-                "Cannot get type parameter of a non-parametric datatype.");
-  CheckArgument(i < d_params.size(), i,
-                "Type parameter index out of range for datatype.");
-  return d_params[i];
-}
-
-inline std::vector<Type> Datatype::getParameters() const {
-  CheckArgument(isParametric(), this,
-                "Cannot get type parameters of a non-parametric datatype.");
-  return d_params;
-}
-
-inline bool Datatype::isCodatatype() const {
-  return d_isCo;
-}
-
-inline bool Datatype::isSygus() const {
-  return !d_sygus_type.isNull();
-}
-
-inline bool Datatype::isTuple() const {
-  return d_isTuple;
-}
-
-inline bool Datatype::isRecord() const {
-  return d_isRecord;
-}
-
-inline Record * Datatype::getRecord() const {
-  return d_record;
-}
-inline bool Datatype::operator!=(const Datatype& other) const
-{
-  return !(*this == other);
-}
-
-inline bool Datatype::isResolved() const { return d_resolved; }
-inline Datatype::iterator Datatype::begin()
-{
-  return iterator(d_constructors, true);
-}
-
-inline Datatype::iterator Datatype::end()
-{
-  return iterator(d_constructors, false);
-}
-
-inline Datatype::const_iterator Datatype::begin() const
-{
-  return const_iterator(d_constructors, true);
-}
-
-inline Datatype::const_iterator Datatype::end() const
-{
-  return const_iterator(d_constructors, false);
-}
-
-inline bool DatatypeConstructor::isResolved() const
-{
-  return !d_tester.isNull();
-}
-
-inline size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
-inline 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_resolved;
-}
-
-inline DatatypeConstructor::iterator DatatypeConstructor::begin()
-{
-  return iterator(d_args, true);
-}
-
-inline DatatypeConstructor::iterator DatatypeConstructor::end()
-{
-  return iterator(d_args, false);
-}
-
-inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
-{
-  return const_iterator(d_args, true);
-}
-
-inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const
-{
-  return const_iterator(d_args, false);
-}
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 09555da1b..411d64a1b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -766,9 +766,11 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
       ++i) {
     const Datatype& dt = (*i).getDatatype();
     if(!dt.isResolved()) {
-      const_cast<Datatype&>(dt).resolve(this, nameResolutions,
-                                        placeholders, replacements,
-                                        paramTypes, paramReplacements);
+      const_cast<Datatype&>(dt).resolve(nameResolutions,
+                                        placeholders,
+                                        replacements,
+                                        paramTypes,
+                                        paramReplacements);
     }
 
     // Now run some checks, including a check to make sure that no
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1142da429..0c3f1b4cb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -262,12 +262,8 @@ const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
 
 const DType& NodeManager::getDTypeForIndex(unsigned index) const
 {
-  // when the Node-level API is in place, this function will be replaced by a
-  // direct lookup into a d_ownedDTypes vector, similar to d_ownedDatatypes
-  // above.
-  Unreachable() << "NodeManager::getDTypeForIndex: DType is not available in "
-                   "the current implementation.";
   const Datatype& d = getDatatypeForIndex(index);
+  // return its internal representation
   return *d.d_internal;
 }