Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris!

14 files changed, 413 insertions, 593 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index fa5919e6a..a5d85821d 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1079,11 +1079,11 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
     AlwaysAssert(constructors[i].size() == selectors[i].size());
     AlwaysAssert(constructors[i].size() == types[i].size());
     for(unsigned j = 0; j < constructors[i].size(); ++j) {
-      CVC4::Datatype::Constructor ctor(constructors[i][j]);
+      CVC4::DatatypeConstructor ctor(constructors[i][j]);
       AlwaysAssert(selectors[i][j].size() == types[i][j].size());
       for(unsigned k = 0; k < selectors[i][j].size(); ++k) {
         if(types[i][j][k].getType().isString()) {
-          ctor.addArg(selectors[i][j][k], CVC4::Datatype::UnresolvedType(types[i][j][k].getConst<string>()));
+          ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<string>()));
         } else {
           ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k]));
         }
@@ -1106,7 +1106,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
       // For each constructor, register its name and its selectors names.
       AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker");
       d_constructors[(*j).getName()] = &dt;
-      for(CVC4::Datatype::Constructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) {
+      for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) {
         AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker");
         d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName());
       }
@@ -1769,7 +1769,7 @@ Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std
   ConstructorMap::const_iterator i = d_constructors.find(constructor);
   AlwaysAssert(i != d_constructors.end(), "no such constructor");
   const CVC4::Datatype& dt = *(*i).second;
-  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  const CVC4::DatatypeConstructor& ctor = dt[constructor];
   AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application");
   return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end()));
 }
@@ -1779,7 +1779,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a
   AlwaysAssert(i != d_selectors.end(), "no such selector");
   const CVC4::Datatype& dt = *(*i).second.first;
   string constructor = (*i).second.second;
-  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  const CVC4::DatatypeConstructor& ctor = dt[constructor];
   return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelector(selector), arg);
 }
 
@@ -1787,7 +1787,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp
   ConstructorMap::const_iterator i = d_constructors.find(constructor);
   AlwaysAssert(i != d_constructors.end(), "no such constructor");
   const CVC4::Datatype& dt = *(*i).second;
-  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  const CVC4::DatatypeConstructor& ctor = dt[constructor];
   return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg);
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 12a60021e..576d0324d 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -638,7 +638,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
   for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
       i != i_end;
       ++i) {
-    const Datatype::Constructor& c = *i;
+    const DatatypeConstructor& c = *i;
     Type testerType CVC4_UNUSED = c.getTester().getType();
     Assert(c.isResolved() &&
            testerType.isTester() &&
@@ -651,10 +651,10 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
            ConstructorType(ctorType).getRangeType() == dtt,
            "malformed constructor in datatype post-resolution");
     // for all selectors...
-    for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end();
+    for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
         j != j_end;
         ++j) {
-      const Datatype::Constructor::Arg& a = *j;
+      const DatatypeConstructorArg& a = *j;
       Type selectorType = a.getSelector().getType();
       Assert(a.isResolved() &&
              selectorType.isSelector() &&
@@ -669,7 +669,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
   }
 }
 
-ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
   NodeManagerScope nms(d_nodeManager);
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
 }
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index ade9a334d..81d30fd1e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -381,7 +381,7 @@ public:
   /**
    * Make a type representing a constructor with the given parameterization.
    */
-  ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
 
   /** Make a type representing a selector with the given parameterization. */
   SelectorType mkSelectorType(Type domain, Type range) const;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3b4d8ac66..2bf0a864a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -298,11 +298,11 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor,
+TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
                                         TypeNode range) {
   std::vector<TypeNode> sorts;
   Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
-  for(Datatype::Constructor::const_iterator i = constructor.begin();
+  for(DatatypeConstructor::const_iterator i = constructor.begin();
       i != constructor.end();
       ++i) {
     TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index adba8087c..3646e91c5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -580,7 +580,7 @@ public:
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
   /** Make a type representing a constructor with the given parameterization */
-  TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range);
+  TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
 
   /** Make a type representing a selector with the given parameterization */
   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 22cf368eb..2d659cfe3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1486,7 +1486,7 @@ postfixTerm[CVC4::Expr& f]
       { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
           std::vector<CVC4::Expr> v;
           Expr e = f.getOperator();
-          const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+          const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
           v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
                                MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
           v.insert(v.end(), f.begin(), f.end());
@@ -1783,14 +1783,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 constructorDef[CVC4::Datatype& type]
 @init {
   std::string id;
-  CVC4::Datatype::Constructor* ctor = NULL;
+  CVC4::DatatypeConstructor* ctor = NULL;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
       std::string testerId("is_");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
-      ctor = new CVC4::Datatype::Constructor(id, testerId);
+      ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN
       selector[*ctor]
@@ -1804,7 +1804,7 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
 @init {
   std::string id;
   Type t, t2;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f1ad4b330..4418ea18f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -286,7 +286,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
           j_end = dt.end();
         j != j_end;
         ++j) {
-      const Datatype::Constructor& ctor = *j;
+      const DatatypeConstructor& ctor = *j;
       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
       Expr constructor = ctor.getConstructor();
       Debug("parser-idt") << "+ define " << constructor << std::endl;
@@ -302,7 +302,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
         throw ParserException(testerName + " already declared");
       }
       defineVar(testerName, tester);
-      for(Datatype::Constructor::const_iterator k = ctor.begin(),
+      for(DatatypeConstructor::const_iterator k = ctor.begin(),
             k_end = ctor.end();
           k != k_end;
           ++k) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 974de29b2..a093aa1ef 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -824,14 +824,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 constructorDef[CVC4::Datatype& type]
 @init {
   std::string id;
-  CVC4::Datatype::Constructor* ctor = NULL;
+  CVC4::DatatypeConstructor* ctor = NULL;
 }
   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
       std::string testerId("is_");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
-      ctor = new CVC4::Datatype::Constructor(id, testerId);
+      ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
@@ -841,7 +841,7 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
 @init {
   std::string id;
   Type t, t2;
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7a45c98aa..23768545d 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -67,7 +67,7 @@ public:
       size_t selectorIndex = Datatype::indexOf(selectorExpr);
       size_t constructorIndex = Datatype::indexOf(constructorExpr);
       const Datatype& dt = Datatype::datatypeOf(constructorExpr);
-      const Datatype::Constructor& c = dt[constructorIndex];
+      const DatatypeConstructor& c = dt[constructorIndex];
       if(c.getNumArgs() > selectorIndex &&
          c[selectorIndex].getSelector() == selectorExpr) {
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6b067c681..75980993b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -32,7 +32,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons )
+const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons )
 {
   Expr consExpr = cons.toExpr();
   return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ];
@@ -272,7 +272,7 @@ void TheoryDatatypes::check(Effort e) {
             }
           }
           if( !cons.isNull() ) {
-            const Datatype::Constructor& cn = getConstructor( cons );
+            const DatatypeConstructor& cn = getConstructor( cons );
             Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
             Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
             NodeBuilder<> nb(kind::OR);
@@ -464,7 +464,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
     vector< Node > selectorVals;
     selectorVals.push_back( cons );
     bool foundSel = false;
-    const Datatype::Constructor& cn = getConstructor( cons );
+    const DatatypeConstructor& cn = getConstructor( cons );
     for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
       Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
       if( d_selectors.find( s ) != d_selectors.end() ) {
@@ -480,7 +480,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
       if( val.getType()!=te.getType() ){ //IDT-param
         Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() );
         Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl;
-        const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
+        const DatatypeConstructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
         Debug("datatypes-gt") << "constructor is " << dtc << std::endl;
         Type tspec = dtc.getSpecializedConstructorType(te.getType().toType());
         Debug("datatypes-gt") << "tpec is " << tspec << std::endl;
@@ -537,7 +537,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
     Node cons = getConstructorForSelector( sel );
-    const Datatype::Constructor& cn = getConstructor( cons );
+    const DatatypeConstructor& cn = getConstructor( cons );
     Node tmp = find( t[0] );
     Node retNode = t;
     if( tmp.getKind() == APPLY_CONSTRUCTOR ) {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 433af38c3..4d429bc54 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -65,7 +65,7 @@ private:
   /** has seen cycle */
   context::CDO< bool > d_hasSeenCycle;
   /** get the constructor for the node */
-  const Datatype::Constructor& getConstructor( Node cons );
+  const DatatypeConstructor& getConstructor( Node cons );
   /** get the constructor for the selector */
   Node getConstructorForSelector( Node sel );
 
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 19415769e..f009bbbbe 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -95,6 +95,8 @@ void Datatype::resolve(ExprManager* em,
                 "Datatype::resolve(): resolutions doesn't contain me!");
   AssertArgument(placeholders.size() == replacements.size(), placeholders,
                 "placeholders and replacements must be the same size");
+  AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+                "paramTypes and paramReplacements must be the same size");
   CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
   DatatypeType self = (*resolutions.find(d_name)).second;
   AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
@@ -110,7 +112,7 @@ void Datatype::resolve(ExprManager* em,
   Assert(index == getNumConstructors());
 }
 
-void Datatype::addConstructor(const Constructor& c) {
+void Datatype::addConstructor(const DatatypeConstructor& c) {
   CheckArgument(!d_resolved, this,
                 "cannot add a constructor to a finalized Datatype");
   d_constructors.push_back(c);
@@ -233,7 +235,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
         i != i_end;
         ++i) {
       if( groundTerm.isNull() ){
-        Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
+        DatatypeConstructor::const_iterator j = (*i).begin(), j_end = (*i).end();
         for(; j != j_end; ++j) {
           SelectorType stype((*j).getSelector().getType());
           if(stype.getDomain() == stype.getRangeType()) {
@@ -245,7 +247,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
 
         if(j == j_end && (*i).isWellFounded()) {
           groundTerm = (*i).mkGroundTerm( t );
-          // Constructor::mkGroundTerm() doesn't ever return null when
+          // DatatypeConstructor::mkGroundTerm() doesn't ever return null when
           // called from the outside.  But in recursive invocations, it
           // can: say you have dt = a(one:dt) | b(two:INT), and you ask
           // the "a" constructor for a ground term.  It asks "dt" for a
@@ -253,7 +255,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
           // ground term!  Thus, even though "a" is a well-founded
           // constructor, it cannot construct a ground-term by itself.  We
           // have to skip past it, and we do that with a
-          // RecursionBreaker<> in Constructor::mkGroundTerm().  In the
+          // RecursionBreaker<> in DatatypeConstructor::mkGroundTerm().  In the
           // case of recursion, it returns null.
           if(!groundTerm.isNull()) {
             // we found a ground-term-constructing constructor!
@@ -323,7 +325,7 @@ bool Datatype::operator==(const Datatype& other) const throw() {
     if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
       return false;
     }
-    for(Constructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
+    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;
@@ -359,12 +361,12 @@ bool Datatype::operator==(const Datatype& other) const throw() {
   return true;
 }
 
-const Datatype::Constructor& Datatype::operator[](size_t index) const {
+const DatatypeConstructor& Datatype::operator[](size_t index) const {
   CheckArgument(index < getNumConstructors(), index, "index out of bounds");
   return d_constructors[index];
 }
 
-const Datatype::Constructor& Datatype::operator[](std::string name) const {
+const DatatypeConstructor& Datatype::operator[](std::string name) const {
   for(const_iterator i = begin(); i != end(); ++i) {
     if((*i).getName() == name) {
       return *i;
@@ -377,12 +379,12 @@ Expr Datatype::getConstructor(std::string name) const {
   return (*this)[name].getConstructor();
 }
 
-void Datatype::Constructor::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)
+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)
   throw(AssertionException, DatatypeResolutionException) {
 
   AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
@@ -428,7 +430,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
 
   Assert(index == getNumArgs());
 
-  // Set constructor/tester last, since Constructor::isResolved()
+  // 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
@@ -442,7 +444,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
   }
 }
 
-Type Datatype::Constructor::doParametricSubstitution( Type range,
+Type DatatypeConstructor::doParametricSubstitution( Type range,
                                   const std::vector< SortConstructorType >& paramTypes,
                                   const std::vector< DatatypeType >& paramReplacements ) {
   TypeNode typn = TypeNode::fromType( range );
@@ -455,23 +457,23 @@ Type Datatype::Constructor::doParametricSubstitution( Type range,
       origChildren.push_back( (*i).toType() );
       children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
     }
-    for( int i=0; i<(int)paramTypes.size(); i++ ) {
-      if( paramTypes[i].getArity()==origChildren.size() ) {
+    for( unsigned i = 0; i < paramTypes.size(); ++i ) {
+      if( paramTypes[i].getArity() == origChildren.size() ) {
         Type tn = paramTypes[i].instantiate( origChildren );
-        if( range==tn ) {
+        if( range == tn ) {
           return paramReplacements[i].instantiate( children );
         }
       }
     }
     NodeBuilder<> nb(typn.getKind());
-    for( int i=0; i<(int)children.size(); i++ ) {
+    for( unsigned i = 0; i < children.size(); ++i ) {
       nb << TypeNode::fromType( children[i] );
     }
     return nb.constructTypeNode().toType();
   }
 }
 
-Datatype::Constructor::Constructor(std::string name) :
+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
@@ -482,7 +484,7 @@ Datatype::Constructor::Constructor(std::string name) :
   CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
-Datatype::Constructor::Constructor(std::string name, std::string tester) :
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   // 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
@@ -494,7 +496,7 @@ Datatype::Constructor::Constructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
-void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) {
+void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
   // the selector type away inside a var until resolution (when we can
@@ -503,30 +505,30 @@ void Datatype::Constructor::addArg(std::string selectorName, Type selectorType)
   CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
   Expr type = selectorType.getExprManager()->mkVar(selectorType);
   Debug("datatypes") << type << endl;
-  d_args.push_back(Arg(selectorName, type));
+  d_args.push_back(DatatypeConstructorArg(selectorName, type));
 }
 
-void Datatype::Constructor::addArg(std::string selectorName, Datatype::UnresolvedType selectorType) {
+void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
   // the selector type away after a NUL in the name string until
   // resolution (when we can create the proper selector type)
   CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
   CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
-  d_args.push_back(Arg(selectorName + '\0' + selectorType.getName(), Expr()));
+  d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
 }
 
-void Datatype::Constructor::addArg(std::string selectorName, Datatype::SelfType) {
+void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we mark
   // the name string with a NUL to indicate that we have a
   // self-selecting selector until resolution (when we can create the
   // proper selector type)
   CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  d_args.push_back(Arg(selectorName + '\0', Expr()));
+  d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
 }
 
-std::string Datatype::Constructor::getName() const throw() {
+std::string DatatypeConstructor::getName() const throw() {
   string name = d_name;
   if(!isResolved()) {
     name.resize(name.find('\0'));
@@ -534,16 +536,16 @@ std::string Datatype::Constructor::getName() const throw() {
   return name;
 }
 
-Expr Datatype::Constructor::getConstructor() const {
+Expr DatatypeConstructor::getConstructor() const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_constructor;
 }
 
-Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const {
+Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
   CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved");
-  DatatypeType dtt = DatatypeType(dt.d_self);
+  DatatypeType dtt = dt.getDatatypeType();
   Matcher m(dtt);
   m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
   vector<Type> subst;
@@ -552,12 +554,12 @@ Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const
   return d_constructor.getType().substitute(params, subst);
 }
 
-Expr Datatype::Constructor::getTester() const {
+Expr DatatypeConstructor::getTester() const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_tester;
 }
 
-Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) {
+Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   Cardinality c = 1;
@@ -569,7 +571,7 @@ Cardinality Datatype::Constructor::getCardinality() const throw(AssertionExcepti
   return c;
 }
 
-bool Datatype::Constructor::isFinite() const throw(AssertionException) {
+bool DatatypeConstructor::isFinite() const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -595,7 +597,7 @@ bool Datatype::Constructor::isFinite() const throw(AssertionException) {
   return true;
 }
 
-bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
+bool DatatypeConstructor::isWellFounded() const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -608,7 +610,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
     return self.getAttribute(DatatypeWellFoundedAttr());
   }
 
-  RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     // This *path* is cyclic, sso may not be well-founded.  The
     // constructor itself might still be well-founded, though (we'll
@@ -639,7 +641,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
   return true;
 }
 
-Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -653,7 +655,7 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio
     return groundTerm;
   }
 
-  RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     // Recursive path, we should skip and go to the next constructor;
     // see lengthy comments in Datatype::mkGroundTerm().
@@ -693,12 +695,12 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio
   return groundTerm;
 }
 
-const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const {
+const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
   CheckArgument(index < getNumArgs(), index, "index out of bounds");
   return d_args[index];
 }
 
-const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string name) const {
+const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
   for(const_iterator i = begin(); i != end(); ++i) {
     if((*i).getName() == name) {
       return *i;
@@ -707,18 +709,18 @@ const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string
   CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
 }
 
-Expr Datatype::Constructor::getSelector(std::string name) const {
+Expr DatatypeConstructor::getSelector(std::string name) const {
   return (*this)[name].getSelector();
 }
 
-Datatype::Constructor::Arg::Arg(std::string name, Expr selector) :
+DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
   d_name(name),
   d_selector(selector),
   d_resolved(false) {
   CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 }
 
-std::string Datatype::Constructor::Arg::getName() const throw() {
+std::string DatatypeConstructorArg::getName() const throw() {
   string name = d_name;
   const size_t nul = name.find('\0');
   if(nul != string::npos) {
@@ -727,28 +729,28 @@ std::string Datatype::Constructor::Arg::getName() const throw() {
   return name;
 }
 
-Expr Datatype::Constructor::Arg::getSelector() const {
+Expr DatatypeConstructorArg::getSelector() const {
   CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
   return d_selector;
 }
 
-Expr Datatype::Constructor::Arg::getConstructor() const {
+Expr DatatypeConstructorArg::getConstructor() const {
   CheckArgument(isResolved(), this,
                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
   return d_constructor;
 }
 
-Type Datatype::Constructor::Arg::getSelectorType() const {
+Type DatatypeConstructorArg::getType() const {
   return getSelector().getType();
 }
 
-bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() {
+bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
   return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
 }
 
 static const int s_printDatatypeNamesOnly = std::ios_base::xalloc();
 
-std::string Datatype::Constructor::Arg::getSelectorTypeName() const {
+std::string DatatypeConstructorArg::getTypeName() const {
   Type t;
   if(isResolved()) {
     t = SelectorType(d_selector.getType()).getRangeType();
@@ -809,13 +811,13 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   return os;
 }
 
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) {
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
 
   os << ctor.getName();
 
-  Datatype::Constructor::const_iterator i = ctor.begin(), i_end = ctor.end();
+  DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end();
   if(i != i_end) {
     os << "(";
     do {
@@ -830,11 +832,11 @@ std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) {
   return os;
 }
 
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) {
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
 
-  os << arg.getName() << ": " << arg.getSelectorTypeName();
+  os << arg.getName() << ": " << arg.getTypeName();
 
   return os;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 24a625bd1..5a1d9b931 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -53,6 +53,259 @@ public:
 };/* class DatatypeResolutionException */
 
 /**
+ * A holder type (used in calls to DatatypeConstructor::addArg())
+ * to allow a Datatype to refer to itself.  Self-typed fields of
+ * Datatypes will be properly typed when a Type is created for the
+ * Datatype by the ExprManager (which calls Datatype::resolve()).
+ */
+class CVC4_PUBLIC DatatypeSelfType {
+};/* class DatatypeSelfType */
+
+/**
+ * An unresolved type (used in calls to
+ * DatatypeConstructor::addArg()) to allow a Datatype to refer to
+ * itself or to other mutually-recursive Datatypes.  Unresolved-type
+ * fields of Datatypes will be properly typed when a Type is created
+ * for the Datatype by the ExprManager (which calls
+ * Datatype::resolve()).
+ */
+class CVC4_PUBLIC DatatypeUnresolvedType {
+  std::string d_name;
+public:
+  inline DatatypeUnresolvedType(std::string name);
+  inline std::string getName() const throw();
+};/* class DatatypeUnresolvedType */
+
+/**
+ * A Datatype constructor argument (i.e., a Datatype field).
+ */
+class CVC4_PUBLIC DatatypeConstructorArg {
+
+  std::string d_name;
+  Expr d_selector;
+  /** the constructor associated with this selector */
+  Expr d_constructor;
+  bool d_resolved;
+
+  DatatypeConstructorArg(std::string name, Expr selector);
+  friend class DatatypeConstructor;
+  friend class Datatype;
+
+  bool isUnresolvedSelf() const throw();
+
+public:
+
+  /** Get the name of this constructor argument. */
+  std::string getName() const throw();
+
+  /**
+   * Get the selector for this constructor argument; this call is
+   * only permitted after resolution.
+   */
+  Expr getSelector() const;
+
+  /**
+   * Get the associated constructor for this constructor argument;
+   * this call is only permitted after resolution.
+   */
+  Expr getConstructor() const;
+
+  /**
+   * Get the type of the selector for this constructor argument;
+   * this call is only permitted after resolution.
+   */
+  Type getType() const;
+
+  /**
+   * Get the name of the type of this constructor argument
+   * (Datatype field).  Can be used for not-yet-resolved Datatypes
+   * (in which case the name of the unresolved type, or "[self]"
+   * for a self-referential type is returned).
+   */
+  std::string getTypeName() const;
+
+  /**
+   * Returns true iff this constructor argument has been resolved.
+   */
+  bool isResolved() const throw();
+
+};/* class DatatypeConstructorArg */
+
+/**
+ * A constructor for a Datatype.
+ */
+class CVC4_PUBLIC DatatypeConstructor {
+public:
+
+  /** The type for iterators over constructor arguments. */
+  typedef std::vector<DatatypeConstructorArg>::iterator iterator;
+  /** The (const) type for iterators over constructor arguments. */
+  typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator;
+
+private:
+
+  std::string d_name;
+  Expr d_constructor;
+  Expr d_tester;
+  std::vector<DatatypeConstructorArg> d_args;
+
+  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)
+    throw(AssertionException, DatatypeResolutionException);
+  friend class Datatype;
+
+  /** @FIXME document this! */
+  Type doParametricSubstitution(Type range,
+                                const std::vector< SortConstructorType >& paramTypes,
+                                const std::vector< DatatypeType >& paramReplacements);
+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 Exprs
+   * representing operators for these entities) aren't created until
+   * resolution time.
+   */
+  explicit DatatypeConstructor(std::string name);
+
+  /**
+   * Create a new Datatype constructor with the given name for the
+   * constructor and the given name for the tester.  The actual
+   * constructor and tester aren't created until resolution time.
+   */
+  DatatypeConstructor(std::string name, std::string tester);
+
+  /**
+   * Add an argument (i.e., a data field) of the given name and type
+   * to this Datatype constructor.  Selector names need not be unique;
+   * they are for convenience and pretty-printing only.
+   */
+  void addArg(std::string selectorName, Type selectorType);
+
+  /**
+   * Add an argument (i.e., a data field) of the given name to this
+   * Datatype constructor that refers to an as-yet-unresolved
+   * Datatype (which may be mutually-recursive).  Selector names need
+   * not be unique; they are for convenience and pretty-printing only.
+   */
+  void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
+
+  /**
+   * Add a self-referential (i.e., a data field) of the given name
+   * to this Datatype constructor that refers to the enclosing
+   * Datatype.  For example, using the familiar "nat" Datatype, to
+   * create the "pred" field for "succ" constructor, one uses
+   * succ::addArg("pred", DatatypeSelfType())---the actual Type
+   * cannot be passed because the Datatype is still under
+   * construction.  Selector names need not be unique; they are for
+   * convenience and pretty-printing only.
+   *
+   * This is a special case of
+   * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType).
+   */
+  void addArg(std::string selectorName, DatatypeSelfType);
+
+  /** Get the name of this Datatype constructor. */
+  std::string getName() const throw();
+
+  /**
+   * Get the constructor operator of this Datatype constructor.  The
+   * Datatype must be resolved.
+   */
+  Expr getConstructor() const;
+
+  /**
+   * Get the tester operator of this Datatype constructor.  The
+   * Datatype must be resolved.
+   */
+  Expr getTester() const;
+
+  /**
+   * Get the number of arguments (so far) of this Datatype constructor.
+   */
+  inline size_t getNumArgs() const throw();
+
+  /**
+   * Get the specialized constructor type for a parametric
+   * constructor; this call is only permitted after resolution.
+   * Given a (concrete) returnType, the constructor's concrete
+   * type in this parametric datatype is returned.
+   *
+   * For instance, if the datatype is list[T], with constructor
+   * "cons[T]" of type "T -> list[T] -> list[T]", then calling
+   * this function with "list[int]" will return the concrete
+   * "cons" constructor type for lists of int---namely,
+   * "int -> list[int] -> list[int]".
+   */
+  Type getSpecializedConstructorType(Type returnType) const;
+
+  /**
+   * Return the cardinality of this constructor (the product of the
+   * cardinalities of its arguments).
+   */
+  Cardinality getCardinality() const throw(AssertionException);
+
+  /**
+   * 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() const throw(AssertionException);
+
+  /**
+   * Return true iff this constructor is well-founded (there exist
+   * ground terms).  The constructor must be resolved or an
+   * exception is thrown.
+   */
+  bool isWellFounded() const throw(AssertionException);
+
+  /**
+   * Construct and return a ground term of this constructor.  The
+   * constructor must be both resolved and well-founded, or else an
+   * exception is thrown.
+   */
+  Expr mkGroundTerm( Type t ) const throw(AssertionException);
+
+  /**
+   * Returns true iff this Datatype constructor has already been
+   * resolved.
+   */
+  inline bool isResolved() const throw();
+
+  /** Get the beginning iterator over DatatypeConstructor args. */
+  inline iterator begin() throw();
+  /** Get the ending iterator over DatatypeConstructor args. */
+  inline iterator end() throw();
+  /** Get the beginning const_iterator over DatatypeConstructor args. */
+  inline const_iterator begin() const throw();
+  /** Get the ending const_iterator over DatatypeConstructor args. */
+  inline const_iterator end() const throw();
+
+  /** Get the ith DatatypeConstructor arg. */
+  const DatatypeConstructorArg& operator[](size_t index) const;
+
+  /**
+   * Get the DatatypeConstructor arg named.  This is a linear search
+   * through the arguments, so in the case of multiple,
+   * similarly-named arguments, the first is returned.
+   */
+  const DatatypeConstructorArg& operator[](std::string name) const;
+
+  /**
+   * Get the selector named.  This is a linear search
+   * through the arguments, so in the case of multiple,
+   * similarly-named arguments, the selector for the first
+   * is returned.
+   */
+  Expr getSelector(std::string name) const;
+
+};/* class DatatypeConstructor */
+
+/**
  * The representation of an inductive datatype.
  *
  * This is far more complicated than it first seems.  Consider this
@@ -66,7 +319,7 @@ public:
  * 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 recusion
+ * 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):
@@ -94,8 +347,9 @@ public:
  * on the task of generating its own selectors and testers, for
  * instance.  That means that, after reifying the Datatype with the
  * ExprManager, the parser needs to go through the (now-resolved)
- * Datatype and request ; see src/parser/parser.cpp for how this is
- * done.  For API usage ideas, see test/unit/util/datatype_black.h.
+ * Datatype and request the constructor, selector, and tester terms.
+ * See src/parser/parser.cpp for how this is done.  For API usage
+ * ideas, see test/unit/util/datatype_black.h.
  */
 class CVC4_PUBLIC Datatype {
 public:
@@ -111,255 +365,15 @@ public:
    */
   static size_t indexOf(Expr item) CVC4_PUBLIC;
 
-  /**
-   * A holder type (used in calls to Datatype::Constructor::addArg())
-   * to allow a Datatype to refer to itself.  Self-typed fields of
-   * Datatypes will be properly typed when a Type is created for the
-   * Datatype by the ExprManager (which calls Datatype::resolve()).
-   */
-  class CVC4_PUBLIC SelfType {
-  };/* class Datatype::SelfType */
-
-  /**
-   * An unresolved type (used in calls to
-   * Datatype::Constructor::addArg()) to allow a Datatype to refer to
-   * itself or to other mutually-recursive Datatypes.  Unresolved-type
-   * fields of Datatypes will be properly typed when a Type is created
-   * for the Datatype by the ExprManager (which calls
-   * Datatype::resolve()).
-   */
-  class CVC4_PUBLIC UnresolvedType {
-    std::string d_name;
-  public:
-    inline UnresolvedType(std::string name);
-    inline std::string getName() const throw();
-  };/* class Datatype::UnresolvedType */
-
-  /**
-   * A constructor for a Datatype.
-   */
-  class CVC4_PUBLIC Constructor {
-  public:
-    /**
-     * A Datatype constructor argument (i.e., a Datatype field).
-     */
-    class CVC4_PUBLIC Arg {
-
-      std::string d_name;
-      Expr d_selector;
-      /** the constructor associated with this selector */
-      Expr d_constructor;
-      bool d_resolved;
-
-      explicit Arg(std::string name, Expr selector);
-      friend class Constructor;
-      friend class Datatype;
-
-      bool isUnresolvedSelf() const throw();
-
-    public:
-
-      /** Get the name of this constructor argument. */
-      std::string getName() const throw();
-
-      /**
-       * Get the selector for this constructor argument; this call is
-       * only permitted after resolution.
-       */
-      Expr getSelector() const;
-
-      /**
-       * Get the associated constructor for this constructor argument;
-       * this call is only permitted after resolution.
-       */
-      Expr getConstructor() const;
-
-      /**
-       * Get the selector for this constructor argument; this call is
-       * only permitted after resolution.
-       */
-      Type getSelectorType() const;
-
-      /**
-       * Get the name of the type of this constructor argument
-       * (Datatype field).  Can be used for not-yet-resolved Datatypes
-       * (in which case the name of the unresolved type, or "[self]"
-       * for a self-referential type is returned).
-       */
-      std::string getSelectorTypeName() const;
-
-      /**
-       * Returns true iff this constructor argument has been resolved.
-       */
-      bool isResolved() const throw();
-
-    };/* class Datatype::Constructor::Arg */
-
-    /** The type for iterators over constructor arguments. */
-    typedef std::vector<Arg>::iterator iterator;
-    /** The (const) type for iterators over constructor arguments. */
-    typedef std::vector<Arg>::const_iterator const_iterator;
-
-  private:
-
-    std::string d_name;
-    Expr d_constructor;
-    Expr d_tester;
-    std::vector<Arg> d_args;
-
-    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)
-      throw(AssertionException, DatatypeResolutionException);
-    friend class Datatype;
-
-    /** @FIXME document this! */
-    Type doParametricSubstitution(Type range,
-                                  const std::vector< SortConstructorType >& paramTypes,
-                                  const std::vector< DatatypeType >& paramReplacements);
-  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 aren't created until
-     * resolution time.
-     */
-    explicit Constructor(std::string name);
-
-    /**
-     * Create a new Datatype constructor with the given name for the
-     * constructor and the given name for the tester.  The actual
-     * constructor and tester aren't created until resolution time.
-     */
-    explicit Constructor(std::string name, std::string tester);
-
-    /**
-     * Add an argument (i.e., a data field) of the given name and type
-     * to this Datatype constructor.
-     */
-    void addArg(std::string selectorName, Type selectorType);
-
-    /**
-     * Add an argument (i.e., a data field) of the given name to this
-     * Datatype constructor that refers to an as-yet-unresolved
-     * Datatype (which may be mutually-recursive).
-     */
-    void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
-
-    /**
-     * Add a self-referential (i.e., a data field) of the given name
-     * to this Datatype constructor that refers to the enclosing
-     * Datatype.  For example, using the familiar "nat" Datatype, to
-     * create the "pred" field for "succ" constructor, one uses
-     * succ::addArg("pred", Datatype::SelfType())---the actual Type
-     * cannot be passed because the Datatype is still under
-     * construction.
-     *
-     * This is a special case of
-     * Constructor::addArg(std::string, Datatype::UnresolvedType).
-     */
-    void addArg(std::string selectorName, Datatype::SelfType);
-
-    /** Get the name of this Datatype constructor. */
-    std::string getName() const throw();
-
-    /**
-     * Get the constructor operator of this Datatype constructor.  The
-     * Datatype must be resolved.
-     */
-    Expr getConstructor() const;
-
-    /**
-     * Get the tester operator of this Datatype constructor.  The
-     * Datatype must be resolved.
-     */
-    Expr getTester() const;
-
-    /**
-     * Get the number of arguments (so far) of this Datatype constructor.
-     */
-    inline size_t getNumArgs() const throw();
-
-    /**
-     * Get the specialized constructor type for a parametric
-     * constructor; this call is only permitted after resolution.
-     */
-    Type getSpecializedConstructorType(Type returnType) const;
-
-    /**
-     * Return the cardinality of this constructor (the product of the
-     * cardinalities of its arguments).
-     */
-    Cardinality getCardinality() const throw(AssertionException);
-
-    /**
-     * 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() const throw(AssertionException);
-
-    /**
-     * Return true iff this constructor is well-founded (there exist
-     * ground terms).  The constructor must be resolved or an
-     * exception is thrown.
-     */
-    bool isWellFounded() const throw(AssertionException);
-
-    /**
-     * Construct and return a ground term of this constructor.  The
-     * constructor must be both resolved and well-founded, or else an
-     * exception is thrown.
-     */
-    Expr mkGroundTerm( Type t ) const throw(AssertionException);
-
-    /**
-     * Returns true iff this Datatype constructor has already been
-     * resolved.
-     */
-    inline bool isResolved() const throw();
-
-    /** Get the beginning iterator over Constructor args. */
-    inline iterator begin() throw();
-    /** Get the ending iterator over Constructor args. */
-    inline iterator end() throw();
-    /** Get the beginning const_iterator over Constructor args. */
-    inline const_iterator begin() const throw();
-    /** Get the ending const_iterator over Constructor args. */
-    inline const_iterator end() const throw();
-
-    /** Get the ith Constructor arg. */
-    const Arg& operator[](size_t index) const;
-
-    /**
-     * Get the Constructor arg named.  This is a linear search
-     * through the arguments, so in the case of multiple,
-     * similarly-named arguments, the first is returned.
-     */
-    const Arg& operator[](std::string name) const;
-
-    /**
-     * Get the selector named.  This is a linear search
-     * through the arguments, so in the case of multiple,
-     * similarly-named arguments, the selector for the first
-     * is returned.
-     */
-    Expr getSelector(std::string name) const;
-
-  };/* class Datatype::Constructor */
-
   /** The type for iterators over constructors. */
-  typedef std::vector<Constructor>::iterator iterator;
+  typedef std::vector<DatatypeConstructor>::iterator iterator;
   /** The (const) type for iterators over constructors. */
-  typedef std::vector<Constructor>::const_iterator const_iterator;
+  typedef std::vector<DatatypeConstructor>::const_iterator const_iterator;
 
 private:
   std::string d_name;
   std::vector<Type> d_params;
-  std::vector<Constructor> d_constructors;
+  std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
 
@@ -368,9 +382,26 @@ private:
    * chicken-and-egg problem.  The DatatypeType around the Datatype
    * cannot exist until the Datatype is finalized, and the Datatype
    * cannot refer to the DatatypeType representing itself until it
-   * exists.  resolve() is called by the ExprManager when a Type.  Has
-   * the effect of freezing the object, too; that is, addConstructor()
-   * will fail after a call to resolve().
+   * exists.  resolve() is called by the ExprManager when a Type is
+   * ultimately requested of the Datatype specification (that is, when
+   * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes()
+   * is called).  Has the effect of freezing the object, too; that is,
+   * addConstructor() will fail after a call to resolve().
+   *
+   * The basic goal of resolution is to assign constructors, selectors,
+   * and testers.  To do this, any UnresolvedType/SelfType references
+   * must be cleared up.  This is the purpose of the "resolutions" map;
+   * it includes any mutually-recursive datatypes that are currently
+   * under resolution.  The four vectors come in two pairs (so, really
+   * they are two maps).  placeholders->replacements give type variables
+   * that should be resolved in the case of parametric datatypes.
+   *
+   * @param 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 be replaced
+   * @param replacements the corresponding replacements
+   * @param paramTypes the sort constructors in these Datatypes under resolution that must be replaced
+   * @param paramReplacements the corresponding (parametric) DatatypeTypes
    */
   void resolve(ExprManager* em,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -390,10 +421,13 @@ public:
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline explicit Datatype(std::string name, std::vector<Type>& params);
+  inline Datatype(std::string name, std::vector<Type>& params);
 
-  /** Add a constructor to this Datatype. */
-  void addConstructor(const Constructor& c);
+  /**
+   * Add a constructor to this Datatype.  Constructor names need not
+   * be unique; they are for convenience and pretty-printing only.
+   */
+  void addConstructor(const DatatypeConstructor& c);
 
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
@@ -473,34 +507,37 @@ public:
   /** Return true iff this Datatype has already been resolved. */
   inline bool isResolved() const throw();
 
-  /** Get the beginning iterator over Constructors. */
-  inline std::vector<Constructor>::iterator begin() throw();
-  /** Get the ending iterator over Constructors. */
-  inline std::vector<Constructor>::iterator end() throw();
-  /** Get the beginning const_iterator over Constructors. */
-  inline std::vector<Constructor>::const_iterator begin() const throw();
-  /** Get the ending const_iterator over Constructors. */
-  inline std::vector<Constructor>::const_iterator end() const throw();
+  /** Get the beginning iterator over DatatypeConstructors. */
+  inline std::vector<DatatypeConstructor>::iterator begin() throw();
+  /** Get the ending iterator over DatatypeConstructors. */
+  inline std::vector<DatatypeConstructor>::iterator end() throw();
+  /** Get the beginning const_iterator over DatatypeConstructors. */
+  inline std::vector<DatatypeConstructor>::const_iterator begin() const throw();
+  /** Get the ending const_iterator over DatatypeConstructors. */
+  inline std::vector<DatatypeConstructor>::const_iterator end() const throw();
 
-  /** Get the ith Constructor. */
-  const Constructor& operator[](size_t index) const;
+  /** Get the ith DatatypeConstructor. */
+  const DatatypeConstructor& operator[](size_t index) const;
 
   /**
-   * Get the Constructor named.  This is a linear search
+   * Get the DatatypeConstructor named.  This is a linear search
    * through the constructors, so in the case of multiple,
    * similarly-named constructors, the first is returned.
    */
-  const Constructor& operator[](std::string name) const;
+  const DatatypeConstructor& operator[](std::string name) const;
 
   /**
    * Get the constructor operator for the named constructor.
+   * This is a linear search through the constructors, so in
+   * the case of multiple, similarly-named constructors, the
+   * first is returned.
+   *
    * This Datatype must be resolved.
    */
   Expr getConstructor(std::string name) const;
 
 };/* class Datatype */
 
-
 /**
  * A hash strategy for Datatypes.  Needed because Datatypes are used
  * as the constant payload in CONSTANT-kinded TypeNodes (for
@@ -523,10 +560,10 @@ struct CVC4_PUBLIC DatatypeHashFunction {
   inline size_t operator()(const Datatype* dt) const {
     return StringHashFunction()(dt->getName());
   }
-  inline size_t operator()(const Datatype::Constructor& dtc) const {
+  inline size_t operator()(const DatatypeConstructor& dtc) const {
     return StringHashFunction()(dtc.getName());
   }
-  inline size_t operator()(const Datatype::Constructor* dtc) const {
+  inline size_t operator()(const DatatypeConstructor* dtc) const {
     return StringHashFunction()(dtc->getName());
   }
 };/* struct DatatypeHashFunction */
@@ -534,8 +571,8 @@ struct CVC4_PUBLIC DatatypeHashFunction {
 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
 
 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
 
 // INLINE FUNCTIONS
 
@@ -543,11 +580,11 @@ inline DatatypeResolutionException::DatatypeResolutionException(std::string msg)
   Exception(msg) {
 }
 
-inline Datatype::UnresolvedType::UnresolvedType(std::string name) :
+inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
   d_name(name) {
 }
 
-inline std::string Datatype::UnresolvedType::getName() const throw() {
+inline std::string DatatypeUnresolvedType::getName() const throw() {
   return d_name;
 }
 
@@ -618,15 +655,15 @@ inline Datatype::const_iterator Datatype::end() const throw() {
   return d_constructors.end();
 }
 
-inline bool Datatype::Constructor::isResolved() const throw() {
+inline bool DatatypeConstructor::isResolved() const throw() {
   return !d_tester.isNull();
 }
 
-inline size_t Datatype::Constructor::getNumArgs() const throw() {
+inline size_t DatatypeConstructor::getNumArgs() const throw() {
   return d_args.size();
 }
 
-inline bool Datatype::Constructor::Arg::isResolved() const throw() {
+inline bool DatatypeConstructorArg::isResolved() const throw() {
   // We could just write:
   //
   //   return !d_selector.isNull() && d_selector.getType().isSelector();
@@ -643,19 +680,19 @@ inline bool Datatype::Constructor::Arg::isResolved() const throw() {
   return d_resolved;
 }
 
-inline Datatype::Constructor::iterator Datatype::Constructor::begin() throw() {
+inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() {
   return d_args.begin();
 }
 
-inline Datatype::Constructor::iterator Datatype::Constructor::end() throw() {
+inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() {
   return d_args.end();
 }
 
-inline Datatype::Constructor::const_iterator Datatype::Constructor::begin() const throw() {
+inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() {
   return d_args.begin();
 }
 
-inline Datatype::Constructor::const_iterator Datatype::Constructor::end() const throw() {
+inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() {
   return d_args.end();
 }
 
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 34e890214..056c15004 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -2,15 +2,10 @@
 #include "util/datatype.h"
 %}
 
-namespace CVC4 {
-%rename(DatatypeConstructor) CVC4::Datatype::Constructor;
-%rename(DatatypeConstructor) CVC4::Constructor;
-}
-
 %extend std::vector< CVC4::Datatype > {
   /* These member functions have slightly different signatures in
    * different swig language packages.  The underlying issue is that
-   * Datatype::Constructor doesn't have a default constructor */
+   * DatatypeConstructor doesn't have a default constructor */
   %ignore vector(unsigned int size = 0);// ocaml
   %ignore set( int i, const CVC4::Datatype &x );// ocaml
   %ignore to_array();// ocaml
@@ -19,17 +14,17 @@ namespace CVC4 {
 };
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
-%extend std::vector< CVC4::Datatype::Constructor > {
+%extend std::vector< CVC4::DatatypeConstructor > {
   /* These member functions have slightly different signatures in
    * different swig language packages.  The underlying issue is that
-   * Datatype::Constructor doesn't have a default constructor */
+   * DatatypeConstructor doesn't have a default constructor */
   %ignore vector(unsigned int size = 0);// ocaml
-  %ignore set( int i, const CVC4::Datatype::Constructor &x );// ocaml
+  %ignore set( int i, const CVC4::DatatypeConstructor &x );// ocaml
   %ignore to_array();// ocaml
   %ignore vector(size_type);// java/python
   %ignore resize(size_type);// java/python
 };
-%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
+%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
 
 %rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
@@ -41,234 +36,20 @@ namespace CVC4 {
 
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
-%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
-%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
+%rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const;
+%ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const;
 
-%rename(beginConst) CVC4::Constructor::begin() const;
-%rename(endConst) CVC4::Constructor::end() const;
+%rename(beginConst) CVC4::DatatypeConstructor::begin() const;
+%rename(endConst) CVC4::DatatypeConstructor::end() const;
 
-%rename(getArg) CVC4::Constructor::operator[](size_t) const;
+%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
-%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
-%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
+%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
+%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&);
 
-%feature("valuewrapper") CVC4::Datatype::UnresolvedType;
-%feature("valuewrapper") CVC4::Datatype::Constructor;
+%feature("valuewrapper") CVC4::DatatypeUnresolvedType;
+%feature("valuewrapper") CVC4::DatatypeConstructor;
 
 %include "util/datatype.h"
 
-namespace CVC4 {
-    class CVC4_PUBLIC Arg {
-
-      std::string d_name;
-      Expr d_selector;
-      /** the constructor associated with this selector */
-      Expr d_constructor;
-      bool d_resolved;
-
-      explicit Arg(std::string name, Expr selector);
-      friend class Constructor;
-      friend class Datatype;
-
-      bool isUnresolvedSelf() const throw();
-
-    public:
-
-      /** Get the name of this constructor argument. */
-      std::string getName() const throw();
-
-      /**
-       * Get the selector for this constructor argument; this call is
-       * only permitted after resolution.
-       */
-      Expr getSelector() const;
-
-      /**
-       * Get the associated constructor for this constructor argument;
-       * this call is only permitted after resolution.
-       */
-      Expr getConstructor() const;
-
-      /**
-       * Get the selector for this constructor argument; this call is
-       * only permitted after resolution.
-       */
-      Type getSelectorType() const;
-
-      /**
-       * Get the name of the type of this constructor argument
-       * (Datatype field).  Can be used for not-yet-resolved Datatypes
-       * (in which case the name of the unresolved type, or "[self]"
-       * for a self-referential type is returned).
-       */
-      std::string getSelectorTypeName() const;
-
-      /**
-       * Returns true iff this constructor argument has been resolved.
-       */
-      bool isResolved() const throw();
-
-    };/* class Datatype::Constructor::Arg */
-
-  class Constructor {
-  public:
-
-    /** The type for iterators over constructor arguments. */
-    typedef std::vector<Arg>::iterator iterator;
-    /** The (const) type for iterators over constructor arguments. */
-    typedef std::vector<Arg>::const_iterator const_iterator;
-
-  private:
-
-    std::string d_name;
-    Expr d_constructor;
-    Expr d_tester;
-    std::vector<Arg> d_args;
-
-    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)
-      throw(AssertionException, DatatypeResolutionException);
-    friend class Datatype;
-
-    /** @FIXME document this! */
-    Type doParametricSubstitution(Type range,
-                                  const std::vector< SortConstructorType >& paramTypes,
-                                  const std::vector< DatatypeType >& paramReplacements);
-  public:
-    /**
-     * Create a new Datatype constructor with the given name for the
-     * constructor and the given name for the tester.  The actual
-     * constructor and tester aren't created until resolution time.
-     */
-    explicit Constructor(std::string name, std::string tester);
-
-    /**
-     * Add an argument (i.e., a data field) of the given name and type
-     * to this Datatype constructor.
-     */
-    void addArg(std::string selectorName, Type selectorType);
-
-    /**
-     * Add an argument (i.e., a data field) of the given name to this
-     * Datatype constructor that refers to an as-yet-unresolved
-     * Datatype (which may be mutually-recursive).
-     */
-    void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
-
-    /**
-     * Add a self-referential (i.e., a data field) of the given name
-     * to this Datatype constructor that refers to the enclosing
-     * Datatype.  For example, using the familiar "nat" Datatype, to
-     * create the "pred" field for "succ" constructor, one uses
-     * succ::addArg("pred", Datatype::SelfType())---the actual Type
-     * cannot be passed because the Datatype is still under
-     * construction.
-     *
-     * This is a special case of
-     * Constructor::addArg(std::string, Datatype::UnresolvedType).
-     */
-    void addArg(std::string selectorName, Datatype::SelfType);
-
-    /** Get the name of this Datatype constructor. */
-    std::string getName() const throw();
-    /**
-     * Get the constructor operator of this Datatype constructor.  The
-     * Datatype must be resolved.
-     */
-    Expr getConstructor() const;
-    /**
-     * Get the tester operator of this Datatype constructor.  The
-     * Datatype must be resolved.
-     */
-    Expr getTester() const;
-    /**
-     * Get the number of arguments (so far) of this Datatype constructor.
-     */
-    inline size_t getNumArgs() const throw();
-
-    /**
-     * Get the specialized constructor type for a parametric
-     * constructor; this call is only permitted after resolution.
-     */
-    Type getSpecializedConstructorType(Type returnType) const;
-
-    /**
-     * Return the cardinality of this constructor (the product of the
-     * cardinalities of its arguments).
-     */
-    Cardinality getCardinality() const throw(AssertionException);
-
-    /**
-     * 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() const throw(AssertionException);
-
-    /**
-     * Return true iff this constructor is well-founded (there exist
-     * ground terms).  The constructor must be resolved or an
-     * exception is thrown.
-     */
-    bool isWellFounded() const throw(AssertionException);
-
-    /**
-     * Construct and return a ground term of this constructor.  The
-     * constructor must be both resolved and well-founded, or else an
-     * exception is thrown.
-     */
-    Expr mkGroundTerm( Type t ) const throw(AssertionException);
-
-    /**
-     * Returns true iff this Datatype constructor has already been
-     * resolved.
-     */
-    inline bool isResolved() const throw();
-
-    /** Get the beginning iterator over Constructor args. */
-    inline iterator begin() throw();
-    /** Get the ending iterator over Constructor args. */
-    inline iterator end() throw();
-    /** Get the beginning const_iterator over Constructor args. */
-    inline const_iterator begin() const throw();
-    /** Get the ending const_iterator over Constructor args. */
-    inline const_iterator end() const throw();
-
-    /** Get the ith Constructor arg. */
-    const Arg& operator[](size_t index) const;
-
-  };/* class Datatype::Constructor */
-
-  class SelfType {
-  };/* class Datatype::SelfType */
-
-  /**
-   * An unresolved type (used in calls to
-   * Datatype::Constructor::addArg()) to allow a Datatype to refer to
-   * itself or to other mutually-recursive Datatypes.  Unresolved-type
-   * fields of Datatypes will be properly typed when a Type is created
-   * for the Datatype by the ExprManager (which calls
-   * Datatype::resolve()).
-   */
-  class UnresolvedType {
-    std::string d_name;
-  public:
-    inline UnresolvedType(std::string name);
-    inline std::string getName() const throw();
-  };/* class Datatype::UnresolvedType */
-}
-
-%{
-namespace CVC4 {
-typedef Datatype::Constructor Constructor;
-typedef Datatype::Constructor::Arg Arg;
-typedef Datatype::SelfType SelfType;
-typedef Datatype::UnresolvedType UnresolvedType;
-}
-%}
-