Introduce the Node-level Datatypes API (#3462)

This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.

Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.

13 files changed, 2622 insertions, 41 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 0c1044e74..f6b48048f 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -46,6 +46,12 @@ libcvc4_add_sources(
   variable_type_map.h
   datatype.h
   datatype.cpp
+  dtype.h
+  dtype.cpp
+  dtype_cons.h
+  dtype_cons.cpp
+  dtype_selector.h
+  dtype_selector.cpp
   record.cpp
   record.h
   sygus_datatype.cpp
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index d52023b4c..f3f4c10d3 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -21,6 +21,7 @@
 
 #include "base/check.h"
 #include "expr/attribute.h"
+#include "expr/dtype.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/node.h"
@@ -54,6 +55,48 @@ typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFin
 typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
 
+Datatype::Datatype(std::string name, bool isCo)
+    : d_internal(nullptr),  // until the Node-level datatype API is activated
+      d_name(name),
+      d_params(),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_isRecord(false),
+      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)
+{
+}
+
+Datatype::Datatype(std::string name,
+                   const std::vector<Type>& params,
+                   bool isCo)
+    : d_internal(nullptr),  // until the Node-level datatype API is activated
+      d_name(name),
+      d_params(params),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_isRecord(false),
+      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)
+{
+}
+
 Datatype::~Datatype(){
   delete d_record;
 }
@@ -837,6 +880,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name)
        // 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(),
@@ -853,6 +897,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name,
        // 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(),
@@ -1233,10 +1278,12 @@ bool DatatypeConstructor::involvesUninterpretedType() const{
   return false;
 }
 
-DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
-  d_name(name),
-  d_selector(selector),
-  d_resolved(false) {
+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)
+{
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 }
 
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index b32001a89..c78fbc436 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -101,6 +101,8 @@ class CVC4_PUBLIC DatatypeResolutionException : public Exception {
 class CVC4_PUBLIC DatatypeSelfType {
 };/* class DatatypeSelfType */
 
+class DTypeSelector;
+
 /**
  * An unresolved type (used in calls to
  * DatatypeConstructor::addArg()) to allow a Datatype to refer to
@@ -159,6 +161,8 @@ class CVC4_PUBLIC DatatypeConstructorArg {
   void toStream(std::ostream& out) const;
 
  private:
+  /** The internal representation */
+  std::shared_ptr<DTypeSelector> d_internal;
   /** the name of this selector */
   std::string d_name;
   /** the selector expression */
@@ -199,6 +203,8 @@ class CVC4_PUBLIC SygusPrintCallback
                              Expr e) const = 0;
 };
 
+class DTypeConstructor;
+
 /**
  * A constructor for a Datatype.
  */
@@ -454,6 +460,8 @@ class CVC4_PUBLIC DatatypeConstructor {
   void toStream(std::ostream& out) const;
 
  private:
+  /** The internal representation */
+  std::shared_ptr<DTypeConstructor> d_internal;
   /** the name of the constructor */
   std::string d_name;
   /** the constructor expression */
@@ -552,6 +560,8 @@ class CVC4_PUBLIC DatatypeConstructor {
   void computeSharedSelectors(Type domainType) const;
 };/* class DatatypeConstructor */
 
+class DType;
+
 /**
  * The representation of an inductive datatype.
  *
@@ -613,7 +623,8 @@ class CVC4_PUBLIC DatatypeConstructor {
  */
 class CVC4_PUBLIC Datatype {
   friend class DatatypeConstructor;
-public:
+  friend class NodeManager;  // temporary, for access to d_internal
+ public:
   /**
    * Get the datatype of a constructor, selector, or tester operator.
    */
@@ -645,13 +656,15 @@ public:
   typedef DatatypeConstructorIterator const_iterator;
 
   /** Create a new Datatype of the given name. */
-  inline explicit Datatype(std::string name, bool isCo = false);
+  explicit Datatype(std::string name, bool isCo = false);
 
   /**
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
+  Datatype(std::string name,
+           const std::vector<Type>& params,
+           bool isCo = false);
 
   ~Datatype();
 
@@ -963,6 +976,8 @@ public:
   void toStream(std::ostream& out) const;
 
  private:
+  /** 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)
@@ -1183,40 +1198,6 @@ inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
 }
 
 inline std::string DatatypeUnresolvedType::getName() const { return d_name; }
-inline Datatype::Datatype(std::string name, bool isCo)
-    : d_name(name),
-      d_params(),
-      d_isCo(isCo),
-      d_isTuple(false),
-      d_isRecord(false),
-      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) {}
-
-inline Datatype::Datatype(std::string name, const std::vector<Type>& params,
-                          bool isCo)
-    : d_name(name),
-      d_params(params),
-      d_isCo(isCo),
-      d_isTuple(false),
-      d_isRecord(false),
-      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) {}
 
 inline std::string Datatype::getName() const { return d_name; }
 inline size_t Datatype::getNumConstructors() const
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
new file mode 100644
index 000000000..f16b193ce
--- /dev/null
+++ b/src/expr/dtype.cpp
@@ -0,0 +1,739 @@
+/*********************                                                        */
+/*! \file dtype.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **/
+#include "expr/dtype.h"
+
+#include "expr/node_algorithm.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+DType::DType(std::string name, bool isCo)
+    : d_name(name),
+      d_params(),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_constructors(),
+      d_resolved(false),
+      d_self(),
+      d_involvesExt(false),
+      d_involvesUt(false),
+      d_sygusAllowConst(false),
+      d_sygusAllowAll(false),
+      d_card(CardinalityUnknown()),
+      d_wellFounded(0)
+{
+}
+
+DType::DType(std::string name, const std::vector<TypeNode>& params, bool isCo)
+    : d_name(name),
+      d_params(params),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_constructors(),
+      d_resolved(false),
+      d_self(),
+      d_involvesExt(false),
+      d_involvesUt(false),
+      d_sygusAllowConst(false),
+      d_sygusAllowAll(false),
+      d_card(CardinalityUnknown()),
+      d_wellFounded(0)
+{
+}
+
+DType::~DType() {}
+
+std::string DType::getName() const { return d_name; }
+size_t DType::getNumConstructors() const { return d_constructors.size(); }
+
+bool DType::isParametric() const { return d_params.size() > 0; }
+size_t DType::getNumParameters() const { return d_params.size(); }
+TypeNode DType::getParameter(size_t i) const
+{
+  Assert(isParametric());
+  Assert(i < d_params.size());
+  return d_params[i];
+}
+
+std::vector<TypeNode> DType::getParameters() const
+{
+  Assert(isParametric());
+  return d_params;
+}
+
+bool DType::isCodatatype() const { return d_isCo; }
+
+bool DType::isSygus() const { return !d_sygusType.isNull(); }
+
+bool DType::isTuple() const { return d_isTuple; }
+
+bool DType::isResolved() const { return d_resolved; }
+
+const DType& DType::datatypeOf(Node item)
+{
+  TypeNode t = item.getType();
+  switch (t.getKind())
+  {
+    case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
+    case SELECTOR_TYPE:
+    case TESTER_TYPE: return t[0].getDType();
+    default:
+      Unhandled() << "arg must be a datatype constructor, selector, or tester";
+  }
+}
+
+size_t DType::indexOf(Node item)
+{
+  Assert(item.getType().isConstructor() || item.getType().isTester()
+         || item.getType().isSelector());
+  return indexOfInternal(item);
+}
+
+size_t DType::indexOfInternal(Node item)
+{
+  if (item.getKind() == APPLY_TYPE_ASCRIPTION)
+  {
+    return indexOf(item[0]);
+  }
+  Assert(item.hasAttribute(DTypeIndexAttr()));
+  return item.getAttribute(DTypeIndexAttr());
+}
+
+size_t DType::cindexOf(Node item)
+{
+  Assert(item.getType().isSelector());
+  return cindexOfInternal(item);
+}
+size_t DType::cindexOfInternal(Node item)
+{
+  if (item.getKind() == APPLY_TYPE_ASCRIPTION)
+  {
+    return cindexOf(item[0]);
+  }
+  Assert(item.hasAttribute(DTypeConsIndexAttr()));
+  return item.getAttribute(DTypeConsIndexAttr());
+}
+
+bool DType::resolve(const std::map<std::string, TypeNode>& resolutions,
+                    const std::vector<TypeNode>& placeholders,
+                    const std::vector<TypeNode>& replacements,
+                    const std::vector<TypeNode>& paramTypes,
+                    const std::vector<TypeNode>& paramReplacements)
+{
+  Trace("datatypes-init") << "DType::resolve: " << std::endl;
+  Assert(!d_resolved);
+  Assert(resolutions.find(d_name) != resolutions.end());
+  Assert(placeholders.size() == replacements.size());
+  Assert(paramTypes.size() == paramReplacements.size());
+  Assert(getNumConstructors() > 0);
+  TypeNode self = (*resolutions.find(d_name)).second;
+  Assert(&self.getDType() == this);
+  d_resolved = true;
+  size_t index = 0;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    Trace("datatypes-init") << "DType::resolve ctor " << std::endl;
+    if (!ctor->resolve(self,
+                       resolutions,
+                       placeholders,
+                       replacements,
+                       paramTypes,
+                       paramReplacements,
+                       index))
+    {
+      return false;
+    }
+    ctor->d_constructor.setAttribute(DTypeIndexAttr(), index);
+    ctor->d_tester.setAttribute(DTypeIndexAttr(), index++);
+    Assert(ctor->isResolved());
+    Trace("datatypes-init") << "DType::resolve ctor finished" << std::endl;
+  }
+  d_self = self;
+
+  d_involvesExt = false;
+  d_involvesUt = false;
+  for (const std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    if (ctor->involvesExternalType())
+    {
+      d_involvesExt = true;
+    }
+    if (ctor->involvesUninterpretedType())
+    {
+      d_involvesUt = true;
+    }
+  }
+
+  if (isSygus())
+  {
+    // all datatype constructors should be sygus and have sygus operators whose
+    // free variables are subsets of sygus bound var list.
+    std::unordered_set<Node, NodeHashFunction> svs;
+    for (const Node& sv : d_sygusBvl)
+    {
+      svs.insert(sv);
+    }
+    for (size_t i = 0, ncons = d_constructors.size(); i < ncons; i++)
+    {
+      Node sop = d_constructors[i]->getSygusOp();
+      Assert(!sop.isNull())
+          << "Sygus datatype contains a non-sygus constructor";
+      std::unordered_set<Node, NodeHashFunction> fvs;
+      expr::getFreeVariables(sop, fvs);
+      for (const Node& v : fvs)
+      {
+        if (svs.find(v) == svs.end())
+        {
+          // return false, indicating we should abort, since this datatype is
+          // not well formed.
+          return false;
+        }
+      }
+    }
+  }
+  Trace("datatypes-init") << "DType::resolve: finished" << std::endl;
+  return true;
+}
+
+void DType::addConstructor(std::shared_ptr<DTypeConstructor> c)
+{
+  Assert(!d_resolved);
+  d_constructors.push_back(c);
+}
+
+void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll)
+{
+  Assert(!d_resolved);
+  d_sygusType = st;
+  d_sygusBvl = bvl;
+  d_sygusAllowConst = allowConst || allowAll;
+  d_sygusAllowAll = allowAll;
+}
+
+void DType::setTuple()
+{
+  Assert(!d_resolved);
+  d_isTuple = true;
+}
+
+Cardinality DType::getCardinality(TypeNode t) const
+{
+  Trace("datatypes-init") << "DType::getCardinality " << std::endl;
+  Assert(isResolved());
+  Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
+  std::vector<TypeNode> processing;
+  computeCardinality(t, processing);
+  return d_card;
+}
+
+Cardinality DType::getCardinality() const
+{
+  Assert(!isParametric());
+  return getCardinality(d_self);
+}
+
+Cardinality DType::computeCardinality(TypeNode t,
+                                      std::vector<TypeNode>& processing) const
+{
+  Trace("datatypes-init") << "DType::computeCardinality " << std::endl;
+  Assert(isResolved());
+  if (std::find(processing.begin(), processing.end(), d_self)
+      != processing.end())
+  {
+    d_card = Cardinality::INTEGERS;
+    return d_card;
+  }
+  processing.push_back(d_self);
+  Cardinality c = 0;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    c += ctor->computeCardinality(t, processing);
+  }
+  d_card = c;
+  processing.pop_back();
+  return d_card;
+}
+
+bool DType::isRecursiveSingleton(TypeNode t) const
+{
+  Trace("datatypes-init") << "DType::isRecursiveSingleton " << std::endl;
+  Assert(isResolved());
+  Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
+  if (d_cardRecSingleton.find(t) != d_cardRecSingleton.end())
+  {
+    return d_cardRecSingleton[t] == 1;
+  }
+  if (isCodatatype())
+  {
+    Assert(d_cardUAssume[t].empty());
+    std::vector<TypeNode> processing;
+    if (computeCardinalityRecSingleton(t, processing, d_cardUAssume[t]))
+    {
+      d_cardRecSingleton[t] = 1;
+      if (Trace.isOn("dt-card"))
+      {
+        Trace("dt-card") << "DType " << getName()
+                         << " is recursive singleton, dependent upon "
+                         << d_cardUAssume[t].size()
+                         << " uninterpreted sorts: " << std::endl;
+        for (size_t i = 0; i < d_cardUAssume[t].size(); i++)
+        {
+          Trace("dt-card") << "  " << d_cardUAssume[t][i] << std::endl;
+        }
+        Trace("dt-card") << std::endl;
+      }
+    }
+    else
+    {
+      d_cardRecSingleton[t] = -1;
+    }
+  }
+  else
+  {
+    d_cardRecSingleton[t] = -1;
+  }
+  return d_cardRecSingleton[t] == 1;
+}
+
+bool DType::isRecursiveSingleton() const
+{
+  Assert(!isParametric());
+  return isRecursiveSingleton(d_self);
+}
+
+unsigned DType::getNumRecursiveSingletonArgTypes(TypeNode t) const
+{
+  Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end());
+  Assert(isRecursiveSingleton(t));
+  return d_cardUAssume[t].size();
+}
+
+unsigned DType::getNumRecursiveSingletonArgTypes() const
+{
+  Assert(!isParametric());
+  return getNumRecursiveSingletonArgTypes(d_self);
+}
+
+TypeNode DType::getRecursiveSingletonArgType(TypeNode t, size_t i) const
+{
+  Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end());
+  Assert(isRecursiveSingleton(t));
+  return d_cardUAssume[t][i];
+}
+
+TypeNode DType::getRecursiveSingletonArgType(size_t i) const
+{
+  Assert(!isParametric());
+  return getRecursiveSingletonArgType(d_self, i);
+}
+
+bool DType::computeCardinalityRecSingleton(
+    TypeNode t,
+    std::vector<TypeNode>& processing,
+    std::vector<TypeNode>& u_assume) const
+{
+  Trace("datatypes-init") << "DType::computeCardinalityRecSingleton "
+                          << std::endl;
+  if (std::find(processing.begin(), processing.end(), d_self)
+      != processing.end())
+  {
+    return true;
+  }
+  if (d_cardRecSingleton[t] == 0)
+  {
+    // if not yet computed
+    if (d_constructors.size() != 1)
+    {
+      return false;
+    }
+    bool success = false;
+    processing.push_back(d_self);
+    for (size_t i = 0, nargs = d_constructors[0]->getNumArgs(); i < nargs; i++)
+    {
+      TypeNode tc = d_constructors[0]->getArgType(i);
+      // 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 DType& dt = tc.getDType();
+        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 if (d_cardRecSingleton[t] == -1)
+  {
+    return false;
+  }
+  for (size_t i = 0, csize = d_cardUAssume[t].size(); i < csize; i++)
+  {
+    if (std::find(u_assume.begin(), u_assume.end(), d_cardUAssume[t][i])
+        == u_assume.end())
+    {
+      u_assume.push_back(d_cardUAssume[t][i]);
+    }
+  }
+  return true;
+}
+
+bool DType::isFinite(TypeNode t) const
+{
+  Trace("datatypes-init") << "DType::isFinite " << std::endl;
+  Assert(isResolved());
+  Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
+
+  // is this already in the cache ?
+  if (d_self.getAttribute(DTypeFiniteComputedAttr()))
+  {
+    return d_self.getAttribute(DTypeFiniteAttr());
+  }
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    if (!ctor->isFinite(t))
+    {
+      d_self.setAttribute(DTypeFiniteComputedAttr(), true);
+      d_self.setAttribute(DTypeFiniteAttr(), false);
+      return false;
+    }
+  }
+  d_self.setAttribute(DTypeFiniteComputedAttr(), true);
+  d_self.setAttribute(DTypeFiniteAttr(), true);
+  return true;
+}
+bool DType::isFinite() const
+{
+  Assert(isResolved() && !isParametric());
+  return isFinite(d_self);
+}
+
+bool DType::isInterpretedFinite(TypeNode t) const
+{
+  Trace("datatypes-init") << "DType::isInterpretedFinite " << std::endl;
+  Assert(isResolved());
+  Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
+  // is this already in the cache ?
+  if (d_self.getAttribute(DTypeUFiniteComputedAttr()))
+  {
+    return d_self.getAttribute(DTypeUFiniteAttr());
+  }
+  // start by assuming it is not
+  d_self.setAttribute(DTypeUFiniteComputedAttr(), true);
+  d_self.setAttribute(DTypeUFiniteAttr(), false);
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    if (!ctor->isInterpretedFinite(t))
+    {
+      return false;
+    }
+  }
+  d_self.setAttribute(DTypeUFiniteComputedAttr(), true);
+  d_self.setAttribute(DTypeUFiniteAttr(), true);
+  return true;
+}
+bool DType::isInterpretedFinite() const
+{
+  Assert(isResolved() && !isParametric());
+  return isInterpretedFinite(d_self);
+}
+
+bool DType::isWellFounded() const
+{
+  Trace("datatypes-init") << "DType::isWellFounded " << std::endl;
+  Assert(isResolved());
+  if (d_wellFounded == 0)
+  {
+    std::vector<TypeNode> processing;
+    if (computeWellFounded(processing))
+    {
+      d_wellFounded = 1;
+    }
+    else
+    {
+      d_wellFounded = -1;
+    }
+  }
+  return d_wellFounded == 1;
+}
+
+bool DType::computeWellFounded(std::vector<TypeNode>& processing) const
+{
+  Trace("datatypes-init") << "DType::computeWellFounded " << std::endl;
+  Assert(isResolved());
+  if (std::find(processing.begin(), processing.end(), d_self)
+      != processing.end())
+  {
+    return d_isCo;
+  }
+  processing.push_back(d_self);
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    if (ctor->computeWellFounded(processing))
+    {
+      processing.pop_back();
+      return true;
+    }
+    else
+    {
+      Trace("dt-wf") << "Constructor " << ctor->getName()
+                     << " is not well-founded." << std::endl;
+    }
+  }
+  processing.pop_back();
+  Trace("dt-wf") << "DType " << getName() << " is not well-founded."
+                 << std::endl;
+  return false;
+}
+
+Node DType::mkGroundTerm(TypeNode t) const
+{
+  Assert(isResolved());
+  return mkGroundTermInternal(t, false);
+}
+
+Node DType::mkGroundValue(TypeNode t) const
+{
+  Assert(isResolved());
+  return mkGroundTermInternal(t, true);
+}
+
+Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const
+{
+  Trace("datatypes-init") << "DType::mkGroundTerm of type " << t
+                          << ", isValue = " << isValue << std::endl;
+  // is this already in the cache ?
+  std::map<TypeNode, Node>& cache = isValue ? d_groundValue : d_groundTerm;
+  std::map<TypeNode, Node>::iterator it = cache.find(t);
+  if (it != cache.end())
+  {
+    Trace("datatypes-init")
+        << "\nin cache: " << d_self << " => " << it->second << std::endl;
+    return it->second;
+  }
+  std::vector<TypeNode> processing;
+  Node groundTerm = computeGroundTerm(t, processing, isValue);
+  if (!groundTerm.isNull())
+  {
+    // we found a ground-term-constructing constructor!
+    cache[t] = groundTerm;
+    Trace("datatypes-init")
+        << "constructed: " << getName() << " => " << groundTerm << std::endl;
+  }
+  // if ground term is null, we are not well-founded
+  Trace("datatypes-init") << "DType::mkGroundTerm for " << t << " returns "
+                          << groundTerm << std::endl;
+  return groundTerm;
+}
+
+Node getSubtermWithType(Node e, TypeNode t, bool isTop)
+{
+  if (!isTop && e.getType() == t)
+  {
+    return e;
+  }
+  for (const Node& ei : e)
+  {
+    Node se = getSubtermWithType(ei, t, false);
+    if (!se.isNull())
+    {
+      return se;
+    }
+  }
+  return Node();
+}
+
+Node DType::computeGroundTerm(TypeNode t,
+                              std::vector<TypeNode>& processing,
+                              bool isValue) const
+{
+  if (std::find(processing.begin(), processing.end(), t) != processing.end())
+  {
+    Debug("datatypes-gt") << "...already processing " << t << " " << d_self
+                          << std::endl;
+    return Node();
+  }
+  processing.push_back(t);
+  for (unsigned r = 0; r < 2; r++)
+  {
+    for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+    {
+      // do nullary constructors first
+      if ((ctor->getNumArgs() == 0) != (r == 0))
+      {
+        continue;
+      }
+      Trace("datatypes-init")
+          << "Try constructing for " << ctor->getName()
+          << ", processing = " << processing.size() << std::endl;
+      Node e = ctor->computeGroundTerm(t, processing, d_groundTerm, isValue);
+      if (!e.isNull())
+      {
+        // must check subterms for the same type to avoid infinite loops in
+        // type enumeration
+        Node se = getSubtermWithType(e, t, true);
+        if (!se.isNull())
+        {
+          Trace("datatypes-init") << "Take subterm " << se << std::endl;
+          e = se;
+        }
+        processing.pop_back();
+        return e;
+      }
+      else
+      {
+        Trace("datatypes-init") << "...failed." << std::endl;
+      }
+    }
+  }
+  processing.pop_back();
+  return Node();
+}
+
+TypeNode DType::getTypeNode() const
+{
+  Assert(isResolved());
+  Assert(!d_self.isNull());
+  return d_self;
+}
+
+TypeNode DType::getTypeNode(const std::vector<TypeNode>& params) const
+{
+  Assert(isResolved());
+  Assert(!d_self.isNull() && d_self.isParametricDatatype());
+  return d_self.instantiateParametricDatatype(params);
+}
+
+const DTypeConstructor& DType::operator[](size_t index) const
+{
+  Assert(index < getNumConstructors());
+  return *d_constructors[index];
+}
+
+Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
+{
+  Assert(isResolved());
+  std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >::iterator
+      itd = d_sharedSel.find(dtt);
+  if (itd != d_sharedSel.end())
+  {
+    std::map<TypeNode, std::map<unsigned, Node> >::iterator its =
+        itd->second.find(t);
+    if (its != itd->second.end())
+    {
+      std::map<unsigned, Node>::iterator it = its->second.find(index);
+      if (it != its->second.end())
+      {
+        return it->second;
+      }
+    }
+  }
+  // make the shared selector
+  Node s;
+  NodeManager* nm = NodeManager::currentNM();
+  std::stringstream ss;
+  ss << "sel_" << index;
+  s = nm->mkSkolem(ss.str(),
+                   nm->mkSelectorType(dtt, t),
+                   "is a shared selector",
+                   NodeManager::SKOLEM_NO_NOTIFY);
+  d_sharedSel[dtt][t][index] = s;
+  Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
+                         << std::endl;
+  return s;
+}
+
+TypeNode DType::getSygusType() const { return d_sygusType; }
+
+Node DType::getSygusVarList() const { return d_sygusBvl; }
+
+bool DType::getSygusAllowConst() const { return d_sygusAllowConst; }
+
+bool DType::getSygusAllowAll() const { return d_sygusAllowAll; }
+
+bool DType::involvesExternalType() const { return d_involvesExt; }
+
+bool DType::involvesUninterpretedType() const { return d_involvesUt; }
+
+const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
+    const
+{
+  return d_constructors;
+}
+
+std::ostream& operator<<(std::ostream& os, const DType& 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 DType::toStream(std::ostream& out) const
+{
+  out << "DATATYPE " << getName();
+  if (isParametric())
+  {
+    out << '[';
+    for (size_t i = 0, nparams = getNumParameters(); i < nparams; ++i)
+    {
+      if (i > 0)
+      {
+        out << ',';
+      }
+      out << getParameter(i);
+    }
+    out << ']';
+  }
+  out << " = " << std::endl;
+  bool firstTime = true;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    if (!firstTime)
+    {
+      out << " | ";
+    }
+    firstTime = false;
+    out << *ctor;
+  }
+  out << " END;" << std::endl;
+}
+
+DTypeIndexConstant::DTypeIndexConstant(size_t index) : d_index(index) {}
+std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic)
+{
+  return out << "index_" << dic.getIndex();
+}
+
+}  // namespace CVC4
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
new file mode 100644
index 000000000..b2399472a
--- /dev/null
+++ b/src/expr/dtype.h
@@ -0,0 +1,615 @@
+/*********************                                                        */
+/*! \file dtype.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__DTYPE_H
+#define CVC4__EXPR__DTYPE_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/dtype_cons.h"
+#include "expr/dtype_selector.h"
+#include "expr/node.h"
+#include "expr/node_manager_attributes.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+// ----------------------- datatype attributes
+/**
+ * Attribute for the index of an expression within a datatype, which is either:
+ * (1) If the expression is a constructor, then its index refers to its
+ * placement in the constructor list of the datatype that owns it, (2) If the
+ * expression is a selector, then its index refers to its placement in the
+ * argument list of the constructor that owns it.
+ */
+struct DTypeIndexTag
+{
+};
+typedef expr::Attribute<DTypeIndexTag, size_t> DTypeIndexAttr;
+/**
+ * Attribute for the constructor index of a selector. This indicates the index
+ * (DTypeIndexAttr) of the constructor that owns this selector.
+ */
+struct DTypeConsIndexTag
+{
+};
+typedef expr::Attribute<DTypeConsIndexTag, size_t> DTypeConsIndexAttr;
+/** Attribute true for datatype types that are finite. */
+struct DTypeFiniteTag
+{
+};
+typedef expr::Attribute<DTypeFiniteTag, bool> DTypeFiniteAttr;
+/** Attribute true when we have computed whether a datatype type is finite */
+struct DTypeFiniteComputedTag
+{
+};
+typedef expr::Attribute<DTypeFiniteComputedTag, bool> DTypeFiniteComputedAttr;
+/**
+ * Attribute true for datatype types that are interpreted as finite (see
+ * TypeNode::isInterpretedFinite).
+ */
+struct DTypeUFiniteTag
+{
+};
+typedef expr::Attribute<DTypeUFiniteTag, bool> DTypeUFiniteAttr;
+/**
+ * Attribute true when we have computed whether a datatype type is interpreted
+ * as finite.
+ */
+struct DTypeUFiniteComputedTag
+{
+};
+typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
+// ----------------------- end datatype attributes
+
+class NodeManager;
+
+class Datatype;
+
+/**
+ * The Node-level representation of an inductive datatype, which currently
+ * resides within the Expr-level Datatype class (expr/datatype.h).
+ *
+ * Notice that this class is a specification for a datatype, and is not
+ * itself a type. The type that this specification corresponds to can be
+ * retrieved (after resolution as described in the following) via getTypeNode.
+ *
+ * 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;
+ *
+ * We build DType 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 TypeNode through ExprManager::mkMutualDatatypeTypes().
+ * The ExprManager creates a Type for each, but before "releasing" this type
+ * into the wild, it does a round of in-place "resolution" on each DType by
+ * calling DType::resolve() with a map of string -> TypeNode 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 DType with the
+ * NodeManager, the parser needs to go through the (now-resolved)
+ * DType 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.
+ *
+ * DTypes 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.  DTypes can be parameterized over multiple type variables
+ * using the syntax sym[ T1, ..., Tn ] = ...,
+ *
+ */
+class DType
+{
+  friend class Datatype;
+  friend class DTypeConstructor;
+  friend class NodeManager;  // for access to resolve()
+
+ public:
+  /**
+   * Get the datatype of a constructor, selector, or tester operator.
+   */
+  static const DType& datatypeOf(Node item);
+
+  /**
+   * 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(Node item);
+
+  /**
+   * Get the index of constructor corresponding to selector.  (Zero is
+   * always the first index.)
+   */
+  static size_t cindexOf(Node item);
+
+  /**
+   * Same as above, but without checks. These methods should be used by
+   * internal (Node-level) code.
+   */
+  static size_t indexOfInternal(Node item);
+  static size_t cindexOfInternal(Node item);
+
+  /** Create a new DType of the given name. */
+  DType(std::string name, bool isCo = false);
+
+  /**
+   * Create a new DType of the given name, with the given
+   * parameterization.
+   */
+  DType(std::string name,
+        const std::vector<TypeNode>& params,
+        bool isCo = false);
+
+  ~DType();
+
+  /** Add a constructor to this DType.
+   *
+   * Notice that constructor names need not
+   * be unique; they are for convenience and pretty-printing only.
+   */
+  void addConstructor(std::shared_ptr<DTypeConstructor> 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(TypeNode st, Node bvl, bool allowConst, bool allowAll);
+
+  /** set that this datatype is a tuple */
+  void setTuple();
+
+  /** Get the name of this DType. */
+  std::string getName() const;
+
+  /** Get the number of constructors (so far) for this DType. */
+  size_t getNumConstructors() const;
+
+  /** Is this datatype parametric? */
+  bool isParametric() const;
+
+  /** Get the number of type parameters */
+  size_t getNumParameters() const;
+
+  /** Get parameter */
+  TypeNode getParameter(size_t i) const;
+
+  /** Get parameters */
+  std::vector<TypeNode> 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;
+
+  /** get the record representation for this datatype */
+  Record* getRecord() const;
+
+  /**
+   * Return the cardinality of this datatype.
+   * The DType 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(TypeNode t) const;
+  Cardinality getCardinality() const;
+
+  /**
+   * Return true iff this DType has finite cardinality. If the
+   * datatype is not well-founded, this method returns false. The
+   * DType must be resolved or an assertion is violated.
+   *
+   * 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(TypeNode t) const;
+  bool isFinite() const;
+
+  /**
+   * Return true iff this  DType is finite (all constructors are
+   * finite, i.e., there  are finitely  many ground terms) under the
+   * assumption that unintepreted sorts are finite. If the
+   * datatype is  not well-founded, this method returns false.  The
+   * DType must be resolved or an assertion is violated.
+   *
+   * 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(TypeNode 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 assertion is
+   * violated.
+   */
+  bool isWellFounded() 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(TypeNode 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(TypeNode t) const;
+  TypeNode getRecursiveSingletonArgType(TypeNode t, size_t i) const;
+  unsigned getNumRecursiveSingletonArgTypes() const;
+  TypeNode getRecursiveSingletonArgType(size_t i) const;
+
+  /**
+   * Construct and return a ground term of this DType.  The
+   * DType 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.
+   */
+  Node mkGroundTerm(TypeNode 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.
+   */
+  Node mkGroundValue(TypeNode t) const;
+
+  /**
+   * Get the TypeNode associated to this DType.  Can only be
+   * called post-resolution.
+   */
+  TypeNode getTypeNode() const;
+
+  /**
+   * Get the TypeNode associated to this (parameterized) DType.  Can only be
+   * called post-resolution.
+   */
+  TypeNode getTypeNode(const std::vector<TypeNode>& params) const;
+
+  /** Return true iff this DType has already been resolved. */
+  bool isResolved() const;
+
+  /** Get the ith DTypeConstructor. */
+  const DTypeConstructor& operator[](size_t index) 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.
+   */
+  TypeNode 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.
+   */
+  Node 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<std::shared_ptr<DTypeConstructor> >& getConstructors()
+      const;
+
+  /** prints this datatype to stream */
+  void toStream(std::ostream& out) const;
+
+ private:
+  /**
+   * DTypes refer to themselves, recursively, and we have a
+   * chicken-and-egg problem.  The TypeNode around the DType
+   * cannot exist until the DType is finalized, and the DType
+   * cannot refer to the TypeNode representing itself until it
+   * exists.  resolve() is called by the NodeManager when a type is
+   * ultimately requested of the DType specification (that is, when
+   * NodeManager::mkTypeNode() or NodeManager::mkMutualTypeNodes()
+   * 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 em the NodeManager at play
+   * @param resolutions a map of strings to TypeNodes currently under
+   * resolution
+   * @param placeholders the types in these DTypes under resolution that must
+   * be replaced
+   * @param replacements the corresponding replacements
+   * @param paramTypes the sort constructors in these DTypes under resolution
+   * that must be replaced
+   * @param paramReplacements the corresponding (parametric) TypeNodes
+   */
+  bool resolve(const std::map<std::string, TypeNode>& resolutions,
+               const std::vector<TypeNode>& placeholders,
+               const std::vector<TypeNode>& replacements,
+               const std::vector<TypeNode>& paramTypes,
+               const std::vector<TypeNode>& paramReplacements);
+
+  /** compute the cardinality of this datatype */
+  Cardinality computeCardinality(TypeNode t,
+                                 std::vector<TypeNode>& processing) const;
+  /** compute whether this datatype is a recursive singleton */
+  bool computeCardinalityRecSingleton(TypeNode t,
+                                      std::vector<TypeNode>& processing,
+                                      std::vector<TypeNode>& u_assume) const;
+  /** compute whether this datatype is well-founded */
+  bool computeWellFounded(std::vector<TypeNode>& 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.
+   */
+  Node computeGroundTerm(TypeNode t,
+                         std::vector<TypeNode>& 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 "DTypes with Shared Selectors",
+   * this returns the term sel_{dtt}^{t,index}.
+   */
+  Node getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const;
+  /**
+   * Helper for mkGroundTerm and mkGroundValue above.
+   */
+  Node mkGroundTermInternal(TypeNode t, bool isValue) const;
+  /** name of this datatype */
+  std::string d_name;
+  /** the type parameters of this datatype (if this is a parametric datatype)
+   */
+  std::vector<TypeNode> d_params;
+  /** whether the datatype is a codatatype. */
+  bool d_isCo;
+  /** whether the datatype is a tuple */
+  bool d_isTuple;
+  /** the constructors of this datatype */
+  std::vector<std::shared_ptr<DTypeConstructor> > d_constructors;
+  /** whether this datatype has been resolved */
+  bool d_resolved;
+  /** self type */
+  mutable TypeNode 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 */
+  TypeNode d_sygusType;
+  /** the variable list for the sygus function to synthesize */
+  Node d_sygusBvl;
+  /** whether all constants are allowed as solutions */
+  bool d_sygusAllowConst;
+  /** whether all terms are allowed as solutions */
+  bool d_sygusAllowAll;
+
+  /** 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<TypeNode, int> d_cardRecSingleton;
+  /** if d_cardRecSingleton is true,
+   * This datatype has infinite cardinality if at least one of the
+   * following uninterpreted sorts having cardinality > 1.
+   */
+  mutable std::map<TypeNode, std::vector<TypeNode> > d_cardUAssume;
+  /**
+   * Cache of whether this datatype is well-founded, where 0 means we have
+   * not computed this information, 1 means it is well-founded, -1 means it is
+   * not.
+   */
+  mutable int d_wellFounded;
+  /** cache of ground term for this datatype */
+  mutable std::map<TypeNode, Node> d_groundTerm;
+  /** cache of ground values for this datatype */
+  mutable std::map<TypeNode, Node> d_groundValue;
+  /** cache of shared selectors for this datatype */
+  mutable std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >
+      d_sharedSel;
+}; /* class DType */
+
+/**
+ * A hash function for DTypes.  Needed to store them in hash sets
+ * and hash maps.
+ */
+struct DTypeHashFunction
+{
+  size_t operator()(const DType& dt) const
+  {
+    return std::hash<std::string>()(dt.getName());
+  }
+  size_t operator()(const DType* dt) const
+  {
+    return std::hash<std::string>()(dt->getName());
+  }
+}; /* struct DTypeHashFunction */
+
+/* stores an index to DType residing in NodeManager */
+class DTypeIndexConstant
+{
+ public:
+  DTypeIndexConstant(size_t index);
+
+  size_t getIndex() const { return d_index; }
+  bool operator==(const DTypeIndexConstant& uc) const
+  {
+    return d_index == uc.d_index;
+  }
+  bool operator!=(const DTypeIndexConstant& uc) const { return !(*this == uc); }
+  bool operator<(const DTypeIndexConstant& uc) const
+  {
+    return d_index < uc.d_index;
+  }
+  bool operator<=(const DTypeIndexConstant& uc) const
+  {
+    return d_index <= uc.d_index;
+  }
+  bool operator>(const DTypeIndexConstant& uc) const { return !(*this <= uc); }
+  bool operator>=(const DTypeIndexConstant& uc) const { return !(*this < uc); }
+
+ private:
+  const size_t d_index;
+}; /* class DTypeIndexConstant */
+
+std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic);
+
+struct DTypeIndexConstantHashFunction
+{
+  size_t operator()(const DTypeIndexConstant& dic) const
+  {
+    return IntegerHashFunction()(dic.getIndex());
+  }
+}; /* struct DTypeIndexConstantHashFunction */
+
+std::ostream& operator<<(std::ostream& os, const DType& dt);
+
+}  // namespace CVC4
+
+#endif
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
new file mode 100644
index 000000000..428097d54
--- /dev/null
+++ b/src/expr/dtype_cons.cpp
@@ -0,0 +1,649 @@
+/*********************                                                        */
+/*! \file dtype_cons.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **/
+#include "expr/dtype_cons.h"
+
+#include "expr/dtype.h"
+#include "expr/node_manager.h"
+#include "expr/type_matcher.h"
+#include "options/datatypes_options.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+
+DTypeConstructor::DTypeConstructor(std::string name,
+                                   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_name(name),
+      d_tester(),
+      d_args(),
+      d_weight(weight)
+{
+  Assert(name != "");
+}
+
+void DTypeConstructor::addArg(std::string selectorName, TypeNode 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)
+  Assert(!isResolved());
+  Assert(!selectorType.isNull());
+
+  Node type = NodeManager::currentNM()->mkSkolem(
+      "unresolved_" + selectorName,
+      selectorType,
+      "is an unresolved selector type placeholder",
+      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+  Trace("datatypes") << type << std::endl;
+  std::shared_ptr<DTypeSelector> a =
+      std::make_shared<DTypeSelector>(selectorName, type);
+  addArg(a);
+}
+
+void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
+{
+  d_args.push_back(a);
+}
+
+std::string DTypeConstructor::getName() const { return d_name; }
+
+Node DTypeConstructor::getConstructor() const
+{
+  Assert(isResolved());
+  return d_constructor;
+}
+
+Node DTypeConstructor::getTester() const
+{
+  Assert(isResolved());
+  return d_tester;
+}
+
+void DTypeConstructor::setSygus(Node op)
+{
+  Assert(!isResolved());
+  d_sygusOp = op;
+}
+
+Node DTypeConstructor::getSygusOp() const
+{
+  Assert(isResolved());
+  return d_sygusOp;
+}
+
+bool DTypeConstructor::isSygusIdFunc() const
+{
+  Assert(isResolved());
+  return (d_sygusOp.getKind() == LAMBDA && d_sygusOp[0].getNumChildren() == 1
+          && d_sygusOp[0][0] == d_sygusOp[1]);
+}
+
+unsigned DTypeConstructor::getWeight() const
+{
+  Assert(isResolved());
+  return d_weight;
+}
+
+size_t DTypeConstructor::getNumArgs() const { return d_args.size(); }
+
+TypeNode DTypeConstructor::getSpecializedConstructorType(
+    TypeNode returnType) const
+{
+  Assert(isResolved());
+  Assert(returnType.isDatatype());
+  const DType& dt = DType::datatypeOf(d_constructor);
+  Assert(dt.isParametric());
+  TypeNode dtt = dt.getTypeNode();
+  TypeMatcher m(dtt);
+  m.doMatching(dtt, returnType);
+  std::vector<TypeNode> subst;
+  m.getMatches(subst);
+  std::vector<TypeNode> params = dt.getParameters();
+  return d_constructor.getType().substitute(
+      params.begin(), params.end(), subst.begin(), subst.end());
+}
+
+const std::vector<std::shared_ptr<DTypeSelector> >& DTypeConstructor::getArgs()
+    const
+{
+  return d_args;
+}
+
+Cardinality DTypeConstructor::getCardinality(TypeNode t) const
+{
+  Assert(isResolved());
+
+  Cardinality c = 1;
+
+  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
+  {
+    c *= getArgType(i).getCardinality();
+  }
+
+  return c;
+}
+
+bool DTypeConstructor::isFinite(TypeNode t) const
+{
+  Assert(isResolved());
+
+  TNode self = d_constructor;
+  // is this already in the cache ?
+  if (self.getAttribute(DTypeFiniteComputedAttr()))
+  {
+    return self.getAttribute(DTypeFiniteAttr());
+  }
+  std::vector<TypeNode> instTypes;
+  std::vector<TypeNode> paramTypes;
+  bool isParam = t.isParametricDatatype();
+  if (isParam)
+  {
+    paramTypes = t.getDType().getParameters();
+    instTypes = TypeNode(t).getParamTypes();
+  }
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    TypeNode tc = getArgType(i);
+    if (isParam)
+    {
+      tc = tc.substitute(paramTypes.begin(),
+                         paramTypes.end(),
+                         instTypes.begin(),
+                         instTypes.end());
+    }
+    if (!tc.isFinite())
+    {
+      self.setAttribute(DTypeFiniteComputedAttr(), true);
+      self.setAttribute(DTypeFiniteAttr(), false);
+      return false;
+    }
+  }
+  self.setAttribute(DTypeFiniteComputedAttr(), true);
+  self.setAttribute(DTypeFiniteAttr(), true);
+  return true;
+}
+
+bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
+{
+  Assert(isResolved());
+  TNode self = d_constructor;
+  // is this already in the cache ?
+  if (self.getAttribute(DTypeUFiniteComputedAttr()))
+  {
+    return self.getAttribute(DTypeUFiniteAttr());
+  }
+  std::vector<TypeNode> instTypes;
+  std::vector<TypeNode> paramTypes;
+  bool isParam = t.isParametricDatatype();
+  if (isParam)
+  {
+    paramTypes = t.getDType().getParameters();
+    instTypes = TypeNode(t).getParamTypes();
+  }
+  for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    TypeNode tc = getArgType(i);
+    if (isParam)
+    {
+      tc = tc.substitute(paramTypes.begin(),
+                         paramTypes.end(),
+                         instTypes.begin(),
+                         instTypes.end());
+    }
+    if (!tc.isInterpretedFinite())
+    {
+      self.setAttribute(DTypeUFiniteComputedAttr(), true);
+      self.setAttribute(DTypeUFiniteAttr(), false);
+      return false;
+    }
+  }
+  self.setAttribute(DTypeUFiniteComputedAttr(), true);
+  self.setAttribute(DTypeUFiniteAttr(), true);
+  return true;
+}
+
+bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }
+
+const DTypeSelector& DTypeConstructor::operator[](size_t index) const
+{
+  Assert(index < getNumArgs());
+  return *d_args[index];
+}
+
+TypeNode DTypeConstructor::getArgType(size_t index) const
+{
+  Assert(index < getNumArgs());
+  return (*this)[index].getType().getSelectorRangeType();
+}
+
+Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
+                                           size_t index) const
+{
+  Assert(isResolved());
+  Assert(index < getNumArgs());
+  if (options::dtSharedSelectors())
+  {
+    computeSharedSelectors(domainType);
+    Assert(d_sharedSelectors[domainType].size() == getNumArgs());
+    return d_sharedSelectors[domainType][index];
+  }
+  else
+  {
+    return d_args[index]->getSelector();
+  }
+}
+
+int DTypeConstructor::getSelectorIndexInternal(Node sel) const
+{
+  Assert(isResolved());
+  if (options::dtSharedSelectors())
+  {
+    Assert(sel.getType().isSelector());
+    TypeNode domainType = sel.getType().getSelectorDomainType();
+    computeSharedSelectors(domainType);
+    std::map<Node, unsigned>::iterator its =
+        d_sharedSelectorIndex[domainType].find(sel);
+    if (its != d_sharedSelectorIndex[domainType].end())
+    {
+      return (int)its->second;
+    }
+  }
+  else
+  {
+    unsigned sindex = DType::indexOf(sel);
+    if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
+    {
+      return static_cast<int>(sindex);
+    }
+  }
+  return -1;
+}
+
+bool DTypeConstructor::involvesExternalType() const
+{
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    if (!getArgType(i).isDatatype())
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+bool DTypeConstructor::involvesUninterpretedType() const
+{
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    if (!getArgType(i).isSort())
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+Cardinality DTypeConstructor::computeCardinality(
+    TypeNode t, std::vector<TypeNode>& processing) const
+{
+  Cardinality c = 1;
+  std::vector<TypeNode> instTypes;
+  std::vector<TypeNode> paramTypes;
+  bool isParam = t.isParametricDatatype();
+  if (isParam)
+  {
+    paramTypes = t.getDType().getParameters();
+    instTypes = t.getParamTypes();
+  }
+  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
+  {
+    TypeNode tc = getArgType(i);
+    if (isParam)
+    {
+      tc = tc.substitute(paramTypes.begin(),
+                         paramTypes.end(),
+                         instTypes.begin(),
+                         instTypes.end());
+    }
+    if (tc.isDatatype())
+    {
+      const DType& dt = tc.getDType();
+      c *= dt.computeCardinality(t, processing);
+    }
+    else
+    {
+      c *= tc.getCardinality();
+    }
+  }
+  return c;
+}
+
+bool DTypeConstructor::computeWellFounded(
+    std::vector<TypeNode>& processing) const
+{
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    TypeNode t = getArgType(i);
+    if (t.isDatatype())
+    {
+      const DType& dt = t.getDType();
+      if (!dt.computeWellFounded(processing))
+      {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+Node DTypeConstructor::computeGroundTerm(TypeNode t,
+                                         std::vector<TypeNode>& processing,
+                                         std::map<TypeNode, Node>& gt,
+                                         bool isValue) const
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> groundTerms;
+  groundTerms.push_back(getConstructor());
+
+  // for each selector, get a ground term
+  std::vector<TypeNode> instTypes;
+  std::vector<TypeNode> paramTypes;
+  bool isParam = t.isParametricDatatype();
+  if (isParam)
+  {
+    paramTypes = t.getDType().getParameters();
+    instTypes = TypeNode(t).getParamTypes();
+  }
+  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
+  {
+    TypeNode selType = getArgType(i);
+    if (isParam)
+    {
+      selType = selType.substitute(paramTypes.begin(),
+                                   paramTypes.end(),
+                                   instTypes.begin(),
+                                   instTypes.end());
+    }
+    Node arg;
+    if (selType.isDatatype())
+    {
+      std::map<TypeNode, Node>::iterator itgt = gt.find(selType);
+      if (itgt != gt.end())
+      {
+        arg = itgt->second;
+      }
+      else
+      {
+        const DType& dt = selType.getDType();
+        arg = dt.computeGroundTerm(selType, processing, isValue);
+      }
+    }
+    else
+    {
+      // call mkGroundValue or mkGroundTerm based on isValue
+      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
+    }
+    if (arg.isNull())
+    {
+      Trace("datatypes") << "...unable to construct arg of "
+                         << d_args[i]->getName() << std::endl;
+      return Node();
+    }
+    else
+    {
+      Trace("datatypes") << "...constructed arg " << arg.getType() << std::endl;
+      groundTerms.push_back(arg);
+    }
+  }
+
+  Node groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
+  if (isParam)
+  {
+    Assert(DType::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] = nm->mkNode(
+        APPLY_TYPE_ASCRIPTION,
+        nm->mkConst(AscriptionType(getSpecializedConstructorType(t).toType())),
+        groundTerms[0]);
+    groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
+  }
+  return groundTerm;
+}
+
+void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const
+{
+  if (d_sharedSelectors[domainType].size() < getNumArgs())
+  {
+    TypeNode ctype;
+    if (domainType.isParametricDatatype())
+    {
+      ctype = getSpecializedConstructorType(domainType);
+    }
+    else
+    {
+      ctype = d_constructor.getType();
+    }
+    Assert(ctype.isConstructor());
+    Assert(ctype.getNumChildren() - 1 == getNumArgs());
+    // compute the shared selectors
+    const DType& dt = DType::datatypeOf(d_constructor);
+    std::map<TypeNode, unsigned> counter;
+    for (size_t j = 0, jend = ctype.getNumChildren() - 1; j < jend; j++)
+    {
+      TypeNode t = ctype[j];
+      Node ss = dt.getSharedSelector(domainType, t, counter[t]);
+      d_sharedSelectors[domainType].push_back(ss);
+      Assert(d_sharedSelectorIndex[domainType].find(ss)
+             == d_sharedSelectorIndex[domainType].end());
+      d_sharedSelectorIndex[domainType][ss] = j;
+      counter[t]++;
+    }
+  }
+}
+
+bool DTypeConstructor::resolve(
+    TypeNode self,
+    const std::map<std::string, TypeNode>& resolutions,
+    const std::vector<TypeNode>& placeholders,
+    const std::vector<TypeNode>& replacements,
+    const std::vector<TypeNode>& paramTypes,
+    const std::vector<TypeNode>& paramReplacements,
+    size_t cindex)
+{
+  if (isResolved())
+  {
+    // already resolved, fail
+    return false;
+  }
+  Trace("datatypes") << "DTypeConstructor::resolve, self type is " << self
+                     << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+  size_t index = 0;
+  std::vector<TypeNode> argTypes;
+  for (std::shared_ptr<DTypeSelector> arg : d_args)
+  {
+    std::string argName = arg->d_name;
+    TypeNode range;
+    if (arg->d_selector.isNull())
+    {
+      // the unresolved type wasn't created here; do name resolution
+      std::string typeName = argName.substr(argName.find('\0') + 1);
+      argName.resize(argName.find('\0'));
+      if (typeName == "")
+      {
+        range = self;
+        arg->d_selector = nm->mkSkolem(
+            argName,
+            nm->mkSelectorType(self, self),
+            "is a selector",
+            NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+      }
+      else
+      {
+        std::map<std::string, TypeNode>::const_iterator j =
+            resolutions.find(typeName);
+        if (j == resolutions.end())
+        {
+          // failed to resolve selector
+          return false;
+        }
+        else
+        {
+          range = (*j).second;
+          arg->d_selector = nm->mkSkolem(
+              argName,
+              nm->mkSelectorType(self, range),
+              "is a selector",
+              NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+        }
+      }
+    }
+    else
+    {
+      // the type for the selector already exists; may need
+      // complex-type substitution
+      range = arg->d_selector.getType();
+      if (!placeholders.empty())
+      {
+        range = range.substitute(placeholders.begin(),
+                                 placeholders.end(),
+                                 replacements.begin(),
+                                 replacements.end());
+      }
+      if (!paramTypes.empty())
+      {
+        range = doParametricSubstitution(range, paramTypes, paramReplacements);
+      }
+      arg->d_selector = nm->mkSkolem(
+          argName,
+          nm->mkSelectorType(self, range),
+          "is a selector",
+          NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+    }
+    arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
+    arg->d_selector.setAttribute(DTypeIndexAttr(), index++);
+    arg->d_resolved = true;
+    argTypes.push_back(range);
+  }
+
+  Assert(index == getNumArgs());
+
+  // Set constructor/tester last, since DTypeConstructor::isResolved()
+  // returns true when d_tester is not the null Node.  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.
+  // The name of the tester variable does not matter, it is only used
+  // internally.
+  std::string testerName("is_" + d_name);
+  d_tester = nm->mkSkolem(
+      testerName,
+      nm->mkTesterType(self),
+      "is a tester",
+      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+  d_constructor = nm->mkSkolem(
+      getName(),
+      nm->mkConstructorType(argTypes, self),
+      "is a constructor",
+      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+  Assert(d_constructor.getType().isConstructor());
+  // associate constructor with all selectors
+  for (std::shared_ptr<DTypeSelector> sel : d_args)
+  {
+    sel->d_constructor = d_constructor;
+  }
+  Assert(isResolved());
+  return true;
+}
+
+TypeNode DTypeConstructor::doParametricSubstitution(
+    TypeNode range,
+    const std::vector<TypeNode>& paramTypes,
+    const std::vector<TypeNode>& paramReplacements)
+{
+  if (range.getNumChildren() == 0)
+  {
+    return range;
+  }
+  std::vector<TypeNode> origChildren;
+  std::vector<TypeNode> children;
+  for (TypeNode::const_iterator i = range.begin(), iend = range.end();
+       i != iend;
+       ++i)
+  {
+    origChildren.push_back((*i));
+    children.push_back(
+        doParametricSubstitution((*i), paramTypes, paramReplacements));
+  }
+  for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
+  {
+    if (paramTypes[i].getNumChildren() + 1 == origChildren.size())
+    {
+      TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
+      if (range == tn)
+      {
+        TypeNode tret =
+            paramReplacements[i].instantiateParametricDatatype(children);
+        return tret;
+      }
+    }
+  }
+  NodeBuilder<> nb(range.getKind());
+  for (size_t i = 0, csize = children.size(); i < csize; ++i)
+  {
+    nb << children[i];
+  }
+  TypeNode tn = nb.constructTypeNode();
+  return tn;
+}
+
+void DTypeConstructor::toStream(std::ostream& out) const
+{
+  out << getName();
+
+  unsigned nargs = getNumArgs();
+  if (nargs == 0)
+  {
+    return;
+  }
+  out << "(";
+  for (unsigned i = 0; i < nargs; i++)
+  {
+    out << *d_args[i];
+    if (i + 1 < nargs)
+    {
+      out << ", ";
+    }
+  }
+  out << ")";
+}
+
+std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
+{
+  // can only output datatypes in the CVC4 native language
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+  ctor.toStream(os);
+  return os;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
new file mode 100644
index 000000000..d5d0013de
--- /dev/null
+++ b/src/expr/dtype_cons.h
@@ -0,0 +1,335 @@
+/*********************                                                        */
+/*! \file dtype_cons.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__DTYPE_CONS_H
+#define CVC4__EXPR__DTYPE_CONS_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/dtype_selector.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class DatatypeConstructor;
+
+/**
+ * The Node-level representation of a constructor for a datatype, which
+ * currently resides in the Expr-level DatatypeConstructor class
+ * (expr/datatype.h).
+ */
+class DTypeConstructor
+{
+  friend class DatatypeConstructor;
+  friend class DType;
+
+ public:
+  /**
+   * Create a new datatype constructor with the given name for the
+   * constructor and the same name (prefixed with "is_") for the
+   * tester.  The actual constructor and tester (meaning, the Nodes
+   * representing operators for these entities) aren't created until
+   * resolution time.
+   *
+   * weight is the value that this constructor carries when computing size
+   * for SyGuS. For example, if A, B, C have weights 0, 1, and 3 respectively,
+   * then C( B( A() ), B( A() ) ) has size 5.
+   */
+  DTypeConstructor(std::string name, unsigned weight = 1);
+
+  ~DTypeConstructor() {}
+  /**
+   * Add an argument (i.e., a data field) of the given name and type
+   * to this constructor.  Selector names need not be unique;
+   * they are for convenience and pretty-printing only.
+   */
+  void addArg(std::string selectorName, TypeNode selectorType);
+  /**
+   * Add an argument, given a pointer to a selector object.
+   */
+  void addArg(std::shared_ptr<DTypeSelector> a);
+
+  /** Get the name of this constructor. */
+  std::string getName() const;
+
+  /**
+   * Get the constructor operator of this constructor.  The
+   * DType must be resolved.
+   */
+  Node getConstructor() const;
+
+  /**
+   * Get the tester operator of this constructor.  The
+   * DType must be resolved.
+   */
+  Node getTester() const;
+  //-------------------------------------- sygus
+  /** set sygus
+   *
+   * Set that this constructor is a sygus datatype constructor that encodes
+   * operator op.
+   */
+  void setSygus(Node op);
+  /** 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.
+   */
+  Node 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;
+  //-------------------------------------- end sygus
+
+  /**
+   * Get the number of arguments (so far) of this DType constructor.
+   */
+  size_t getNumArgs() const;
+  /**
+   * Get the list of arguments to this constructor.
+   */
+  const std::vector<std::shared_ptr<DTypeSelector> >& getArgs() 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]".
+   */
+  TypeNode getSpecializedConstructorType(TypeNode returnType) const;
+
+  /**
+   * Return the cardinality of this constructor (the product of the
+   * cardinalities of its arguments).
+   */
+  Cardinality getCardinality(TypeNode 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(TypeNode 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(TypeNode t) const;
+
+  /**
+   * Returns true iff this constructor has already been
+   * resolved.
+   */
+  bool isResolved() const;
+
+  /** Get the ith DTypeConstructor arg. */
+  const DTypeSelector& operator[](size_t index) const;
+
+  /**
+   * Get argument type. Returns the return type of the i^th selector of this
+   * constructor.
+   */
+  TypeNode getArgType(size_t i) const;
+
+  /** get selector internal
+   *
+   * This gets the 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 "DTypes 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.
+   */
+  Node getSelectorInternal(TypeNode 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 "DTypes 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(Node 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 uninterpreted type
+   *
+   * Get whether this constructor has a subfield
+   * in any constructor that is an uninterpreted type.
+   */
+  bool involvesUninterpretedType() const;
+  /** prints this datatype constructor to stream */
+  void toStream(std::ostream& out) const;
+
+ private:
+  /** resolve
+   *
+   * This resolves (initializes) the constructor. For details
+   * on how datatypes and their constructors are resolved, see
+   * documentation for DType::resolve.
+   */
+  bool resolve(TypeNode self,
+               const std::map<std::string, TypeNode>& resolutions,
+               const std::vector<TypeNode>& placeholders,
+               const std::vector<TypeNode>& replacements,
+               const std::vector<TypeNode>& paramTypes,
+               const std::vector<TypeNode>& paramReplacements,
+               size_t cindex);
+
+  /** Helper function for resolving parametric datatypes.
+   *
+   * This replaces instances of the TypeNode produced for unresolved
+   * parametric datatypes, with the corresponding resolved TypeNode.  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;
+   */
+  TypeNode doParametricSubstitution(
+      TypeNode range,
+      const std::vector<TypeNode>& paramTypes,
+      const std::vector<TypeNode>& paramReplacements);
+
+  /** compute the cardinality of this datatype */
+  Cardinality computeCardinality(TypeNode t,
+                                 std::vector<TypeNode>& processing) const;
+  /** compute whether this datatype is well-founded */
+  bool computeWellFounded(std::vector<TypeNode>& 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.
+   */
+  Node computeGroundTerm(TypeNode t,
+                         std::vector<TypeNode>& processing,
+                         std::map<TypeNode, Node>& gt,
+                         bool isValue) const;
+  /** compute shared selectors
+   * This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
+   */
+  void computeSharedSelectors(TypeNode domainType) const;
+  /** the name of the constructor */
+  std::string d_name;
+  /** the name of the tester */
+  std::string d_testerName;
+  /** the constructor expression */
+  Node d_constructor;
+  /** the tester for this constructor */
+  Node d_tester;
+  /** the arguments of this constructor */
+  std::vector<std::shared_ptr<DTypeSelector> > d_args;
+  /** sygus operator */
+  Node d_sygusOp;
+  /** 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 "DTypes 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<TypeNode, std::vector<Node> > d_sharedSelectors;
+  /** for each type, a cache mapping from shared selectors to
+   * its argument index for this constructor.
+   */
+  mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
+}; /* class DTypeConstructor */
+
+/**
+ * A hash function for DTypeConstructors.  Needed to store them in hash sets
+ * and hash maps.
+ */
+struct DTypeConstructorHashFunction
+{
+  size_t operator()(const DTypeConstructor& dtc) const
+  {
+    return std::hash<std::string>()(dtc.getName());
+  }
+  size_t operator()(const DTypeConstructor* dtc) const
+  {
+    return std::hash<std::string>()(dtc->getName());
+  }
+}; /* struct DTypeConstructorHashFunction */
+
+std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor);
+
+}  // namespace CVC4
+
+#endif
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
new file mode 100644
index 000000000..960bbeb4d
--- /dev/null
+++ b/src/expr/dtype_selector.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file dtype_selector.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 selector.
+ **/
+
+#include "expr/dtype_selector.h"
+
+#include "options/set_language.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+DTypeSelector::DTypeSelector(std::string name, Node selector)
+    : d_name(name), d_selector(selector), d_resolved(false)
+{
+  Assert(name != "");
+}
+
+std::string DTypeSelector::getName() const { return d_name; }
+
+Node DTypeSelector::getSelector() const
+{
+  Assert(d_resolved);
+  return d_selector;
+}
+
+Node DTypeSelector::getConstructor() const
+{
+  Assert(d_resolved);
+  return d_constructor;
+}
+
+TypeNode DTypeSelector::getType() const { return d_selector.getType(); }
+
+TypeNode DTypeSelector::getRangeType() const
+{
+  return getType().getRangeType();
+}
+
+bool DTypeSelector::isResolved() const { return d_resolved; }
+
+void DTypeSelector::toStream(std::ostream& out) const
+{
+  out << getName() << ": ";
+  TypeNode t;
+  if (d_resolved)
+  {
+    t = getRangeType();
+  }
+  else if (d_selector.isNull())
+  {
+    std::string typeName = d_name.substr(d_name.find('\0') + 1);
+    out << ((typeName == "") ? "[self]" : typeName);
+    return;
+  }
+  else
+  {
+    out << "unresolved";
+    return;
+  }
+  out << t;
+}
+
+std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg)
+{
+  // can only output datatypes in the CVC4 native language
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+  arg.toStream(os);
+  return os;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
new file mode 100644
index 000000000..71b035d8c
--- /dev/null
+++ b/src/expr/dtype_selector.h
@@ -0,0 +1,95 @@
+/*********************                                                        */
+/*! \file dtype_selector.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 selector.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__DTYPE_SELECTOR_H
+#define CVC4__EXPR__DTYPE_SELECTOR_H
+
+#include <string>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class DatatypeConstructorArg;
+class DType;
+class DTypeConstructor;
+
+/**
+ * A datatype selector for a constructor argument (i.e., a datatype field).
+ */
+class DTypeSelector
+{
+  friend class DatatypeConstructorArg;
+  friend class DTypeConstructor;
+  friend class DType;
+
+ public:
+  /** constructor */
+  DTypeSelector(std::string name, Node selector);
+
+  /** 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.
+   */
+  Node getSelector() const;
+
+  /**
+   * Get the associated constructor for this constructor argument;
+   * this call is only permitted after resolution.
+   */
+  Node getConstructor() const;
+
+  /**
+   * Get the type of the selector for this constructor argument.
+   */
+  TypeNode getType() const;
+
+  /**
+   * Get the range type of this argument.
+   */
+  TypeNode 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 name of this selector */
+  std::string d_name;
+  /** the selector expression */
+  Node d_selector;
+  /**
+   * The constructor associated with this selector. This field is initialized
+   * by the constructor of this selector during a call to
+   * DTypeConstructor::resolve.
+   */
+  Node d_constructor;
+  /** whether this class has been resolved */
+  bool d_resolved;
+};
+
+std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg);
+
+}  // namespace CVC4
+
+#endif
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5223fd02c..201e428de 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -24,6 +24,7 @@
 #include "base/check.h"
 #include "base/listener.h"
 #include "expr/attribute.h"
+#include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_manager_listeners.h"
 #include "expr/type_checker.h"
@@ -186,6 +187,7 @@ NodeManager::~NodeManager() {
   d_rt_cache.d_children.clear();
   d_rt_cache.d_data = dummy;
 
+  // TODO: switch to DType
   for (std::vector<Datatype*>::iterator
            datatype_iter = d_ownedDatatypes.begin(),
            datatype_end = d_ownedDatatypes.end();
@@ -253,10 +255,22 @@ unsigned NodeManager::registerDatatype(Datatype* dt) {
 }
 
 const Datatype & NodeManager::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];
 }
 
+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 *d.d_internal;
+}
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
   Assert(!d_attrManager->inGarbageCollection());
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f47795c15..61ef1d39d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -43,6 +43,8 @@ namespace CVC4 {
 class StatisticsRegistry;
 class ResourceManager;
 
+class DType;
+
 namespace expr {
   namespace attr {
     class AttributeUniqueId;
@@ -429,6 +431,7 @@ public:
   unsigned registerDatatype(Datatype* dt);
   /** get datatype for index */
   const Datatype & getDatatypeForIndex( unsigned index ) const;
+  const DType& getDTypeForIndex(unsigned index) const;
 
   /** Get a Kind from an operator expression */
   static inline Kind operatorToKind(TNode n);
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 1ef5030ce..8cc10b5b2 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -647,4 +647,15 @@ std::string TypeNode::toString() const {
   return ss.str();
 }
 
+const DType& TypeNode::getDType() const
+{
+  if (getKind() == kind::DATATYPE_TYPE)
+  {
+    DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+    return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex());
+  }
+  Assert(getKind() == kind::PARAMETRIC_DATATYPE);
+  return (*this)[0].getDType();
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 472d29f5f..b1c4da026 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -37,6 +37,7 @@
 namespace CVC4 {
 
 class NodeManager;
+class DType;
 
 namespace expr {
   class NodeValue;
@@ -661,6 +662,9 @@ public:
   /** Get the Datatype specification from a datatype type */
   const Datatype& getDatatype() const;
 
+  /** Get the internal Datatype specification from a datatype type */
+  const DType& getDType() const;
+
   /** Get the exponent size of this floating-point type */
   unsigned getFloatingPointExponentSize() const;