Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

40 files changed, 3890 insertions, 188 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7c08293be..bcc96637f 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -2,10 +2,10 @@
 /*! \file command.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -498,6 +498,35 @@ void GetOptionCommand::toStream(std::ostream& out) const {
   out << "GetOption(" << d_flag << ")";
 }
 
+/* class DatatypeDeclarationCommand */
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
+  d_datatypes() {
+  d_datatypes.push_back(datatype);
+  Debug("datatypes") << "Create datatype command." << endl;
+}
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
+  d_datatypes(datatypes) {
+  Debug("datatypes") << "Create datatype command." << endl;
+}
+
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+  Debug("datatypes") << "Invoke datatype command." << endl;
+  //smtEngine->addDatatypeDefinitions(d_datatype);
+}
+
+void DatatypeDeclarationCommand::toStream(std::ostream& out) const {
+  out << "DatatypeDeclarationCommand([";
+  for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(),
+        i_end = d_datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i << ";" << endl;
+  }
+  out << "])";
+}
+
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) {
diff --git a/src/expr/command.h b/src/expr/command.h
index fbb48b6b0..585e60eb4 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -2,10 +2,10 @@
 /*! \file command.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -28,11 +28,13 @@
 #include <sstream>
 #include <string>
 #include <vector>
+#include <map>
 
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "util/result.h"
 #include "util/sexpr.h"
+#include "util/datatype.h"
 
 namespace CVC4 {
 
@@ -264,6 +266,16 @@ public:
   void printResult(std::ostream& out) const;
 };/* class GetOptionCommand */
 
+class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
+private:
+  std::vector<DatatypeType> d_datatypes;
+public:
+  DatatypeDeclarationCommand(const DatatypeType& datatype);
+  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+};/* class DatatypeDeclarationCommand */
+
 class CVC4_PUBLIC CommandSequence : public Command {
 private:
   /** All the commands to be executed (in sequence) */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6e8b6c63c..21fc0a4a1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -2,10 +2,10 @@
 /*! \file expr_manager_template.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -22,13 +22,15 @@
 #include "util/options.h"
 #include "util/stats.h"
 
+#include <map>
+
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 34 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
+DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+  NodeManagerScope nms(d_nodeManager);
+  TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype));
+  Type type(d_nodeManager, typeNode);
+  DatatypeType dtt(type);
+  const Datatype& dt = typeNode->getConst<Datatype>();
+  if(!dt.isResolved()) {
+    std::map<std::string, DatatypeType> resolutions;
+    resolutions.insert(std::make_pair(datatype.getName(), dtt));
+    const_cast<Datatype&>(dt).resolve(this, resolutions);
+  }
+  return dtt;
+}
+
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+  NodeManagerScope nms(d_nodeManager);
+  std::map<std::string, DatatypeType> resolutions;
+  std::vector<DatatypeType> dtts;
+  for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+    Type type(d_nodeManager, typeNode);
+    DatatypeType dtt(type);
+    CheckArgument(resolutions.find((*i).getName()) == resolutions.end(),
+                  datatypes,
+                  "cannot construct two datatypes at the same time with the same name `%s'",
+                  (*i).getName().c_str());
+    resolutions.insert(std::make_pair((*i).getName(), dtt));
+    dtts.push_back(dtt);
+  }
+  for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end();
+      i != i_end;
+      ++i) {
+    const Datatype& dt = (*i).getDatatype();
+    if(!dt.isResolved()) {
+      const_cast<Datatype&>(dt).resolve(this, resolutions);
+    }
+  }
+  return dtts;
+}
+
+ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
+}
+
+SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
+}
+
+TesterType ExprManager::mkTesterType(Type domain) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
+}
+
 SortType ExprManager::mkSort(const std::string& name) const {
   NodeManagerScope nms(d_nodeManager);
   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f51d6fa28..415d05878 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -241,20 +241,40 @@ public:
    */
   TupleType mkTupleType(const std::vector<Type>& types);
 
-  /** Make a type representing a bit-vector of the given size */
+  /** Make a type representing a bit-vector of the given size. */
   BitVectorType mkBitVectorType(unsigned size) const;
 
-  /** Make the type of arrays with the given parameterization */
+  /** Make the type of arrays with the given parameterization. */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
+  /** Make a type representing the given datatype. */
+  DatatypeType mkDatatypeType(const Datatype& datatype);
+
+  /**
+   * Make a set of types representing the given datatypes, which may be
+   * mutually recursive.
+   */
+  std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+
+  /**
+   * Make a type representing a constructor with the given parameterization.
+   */
+  ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+
+  /** Make a type representing a selector with the given parameterization. */
+  SelectorType mkSelectorType(Type domain, Type range) const;
+
+  /** Make a type representing a tester with the given parameterization. */
+  TesterType mkTesterType(Type domain) const;
+
   /** Make a new sort with the given name. */
   SortType mkSort(const std::string& name) const;
 
-  /** Make a new sort from a constructor */
+  /** Make a new sort from a constructor. */
   SortType mkSort(SortConstructorType constructor,
                   const std::vector<TypeNode>& children) const;
 
-  /** Make a sort constructor from a name and arity */
+  /** Make a sort constructor from a name and arity. */
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 1a9722939..489564d5f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -18,6 +18,13 @@
 
 #include "cvc4_public.h"
 
+// putting the constant-payload #includes up here allows circularity
+// (some of them may require a completely-defined Expr type).  This
+// way, those #includes can forward-declare some stuff to get Expr's
+// getConst<> template instantiations correct, and then #include
+// "expr.h" safely, then go on to completely declare their own stuff.
+${includes}
+
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
@@ -28,13 +35,11 @@
 #include "util/exception.h"
 #include "util/language.h"
 
-${includes}
-
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 38 "${template}"
+#line 43 "${template}"
 
 namespace CVC4 {
 
@@ -576,6 +581,31 @@ public:
   static inline void setDepth(std::ostream& out, long depth) {
     out.iword(s_iosIndex) = depth;
   }
+
+  /**
+   * Set the expression depth on the output stream for the current
+   * stack scope.  This makes sure the old depth is reset on the stream
+   * after normal OR exceptional exit from the scope, using the RAII
+   * C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    long d_oldDepth;
+
+  public:
+
+    inline Scope(std::ostream& out, long depth) :
+      d_out(out),
+      d_oldDepth(ExprSetDepth::getDepth(out)) {
+      ExprSetDepth::setDepth(out, depth);
+    }
+
+    inline ~Scope() {
+      ExprSetDepth::setDepth(d_out, d_oldDepth);
+    }
+
+  };/* class ExprSetDepth::Scope */
+
 };/* class ExprSetDepth */
 
 /**
@@ -621,6 +651,31 @@ public:
   static inline void setPrintTypes(std::ostream& out, bool printTypes) {
     out.iword(s_iosIndex) = printTypes;
   }
+
+  /**
+   * Set the print-types state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrintTypes;
+
+  public:
+
+    inline Scope(std::ostream& out, bool printTypes) :
+      d_out(out),
+      d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
+      ExprPrintTypes::setPrintTypes(out, printTypes);
+    }
+
+    inline ~Scope() {
+      ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
+    }
+
+  };/* class ExprPrintTypes::Scope */
+
 };/* class ExprPrintTypes */
 
 /**
@@ -668,13 +723,38 @@ public:
     // (offset by one to detect whether default has been set yet)
     out.iword(s_iosIndex) = int(l) + 1;
   }
+
+  /**
+   * Set a language on the output stream for the current stack scope.
+   * This makes sure the old language is reset on the stream after
+   * normal OR exceptional exit from the scope, using the RAII C++
+   * idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    OutputLanguage d_oldLanguage;
+
+  public:
+
+    inline Scope(std::ostream& out, OutputLanguage language) :
+      d_out(out),
+      d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
+      ExprSetLanguage::setLanguage(out, language);
+    }
+
+    inline ~Scope() {
+      ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
+    }
+
+  };/* class ExprSetLanguage::Scope */
+
 };/* class ExprSetLanguage */
 
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 676 "${template}"
+#line 682 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 40bf9992c..da2847d84 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -138,25 +138,26 @@ function constant {
   includes="${includes}
 #include \"$4\""
   mkConst_instantiations="${mkConst_instantiations}
-template <>
-Expr ExprManager::mkConst($2 const& val);
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val);
 "
   mkConst_implementations="${mkConst_implementations}
-template <>
-Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
   return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
 }
 "
   getConst_instantiations="${getConst_instantiations}
-template <>
-$2 const & Expr::getConst< $2 >() const;
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst< $2 >() const;
 "
   getConst_implementations="${getConst_implementations}
-template <>
-$2 const & Expr::getConst() const {
-  // check even for production builds
-  CheckArgument(getKind() == ::CVC4::kind::$1, *this,
-                \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst() const {
+#line $lineno \"$kf\"
+  CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
   return d_node->getConst< $2 >();
 }
 "
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 631f73a89..f7f6ba836 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -74,7 +74,7 @@ function theory {
 
   theory_id="$1"
   theory_enum="$1,
-    ${theory_enum}"
+  ${theory_enum}"
   theory_descriptions="${theory_descriptions}    case ${theory_id}: out << \"${theory_id}\"; break;
 "
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index 2509640e0..d3775cb3f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -813,7 +813,7 @@ namespace CVC4 {
 
 // for hash_maps, hash_sets..
 struct NodeHashFunction {
-  size_t operator()(const CVC4::Node& node) const {
+  size_t operator()(CVC4::Node node) const {
     return (size_t) node.getId();
   }
 };/* struct NodeHashFunction */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 793b701f8..9449594e3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -2,10 +2,10 @@
 /*! \file node_manager.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): acsys, taking
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): acsys, taking, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -26,6 +26,7 @@
 #include "theory/arith/theory_arith_type_rules.h"
 #include "theory/arrays/theory_arrays_type_rules.h"
 #include "theory/bv/theory_bv_type_rules.h"
+#include "theory/datatypes/theory_datatypes_type_rules.h"
 
 #include "util/Assert.h"
 #include "util/options.h"
@@ -434,6 +435,15 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   case kind::BITVECTOR_SIGN_EXTEND:
     typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
     break;
+  case kind::APPLY_CONSTRUCTOR:
+    typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check);
+    break;
+  case kind::APPLY_SELECTOR:
+    typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check);
+    break;
+  case kind::APPLY_TESTER:
+    typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
+    break;
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled(n.getKind());
@@ -509,4 +519,20 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
+TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) {
+  std::vector<TypeNode> sorts;
+  Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
+  for(Datatype::Constructor::const_iterator i = constructor.begin();
+      i != constructor.end();
+      ++i) {
+    Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl;
+    TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1];
+    Debug("datatypes") << "ctor sort: " << sort << std::endl;
+    sorts.push_back(sort);
+  }
+  Debug("datatypes") << "ctor range: " << range << std::endl;
+  sorts.push_back(range);
+  return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1760f48c7..7f7d37a52 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway, dejan
  ** Minor contributors (to current version): acsys, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -55,8 +55,8 @@ namespace attr {
   struct SortArityTag {};
 }/* CVC4::expr::attr namespace */
 
-typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
-typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 
 }/* CVC4::expr namespace */
 
@@ -542,6 +542,15 @@ public:
   /** Make the type of arrays with the given parameterization */
   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);
+
+  /** Make a type representing a selector with the given parameterization */
+  inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
+
+  /** Make a type representing a tester with given parameterization */
+  inline TypeNode mkTesterType(TypeNode domain);
+
   /** Make a new (anonymous) sort of arity 0. */
   inline TypeNode mkSort();
 
@@ -796,6 +805,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
+inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
+  return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
+}
+
+inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
+  return mkTypeNode(kind::TESTER_TYPE, domain );
+}
+
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
   if(find == d_nodeValuePool.end()) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 78554f61f..6dd9c5cec 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -2,10 +2,10 @@
 /*! \file type.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, dejan
+ ** Major contributors: dejan, mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -186,6 +186,58 @@ Type::operator BitVectorType() const throw(AssertionException) {
   return BitVectorType(*this);
 }
 
+/** Cast to a Constructor type */
+Type::operator DatatypeType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isDatatype());
+  return DatatypeType(*this);
+}
+
+/** Is this the Datatype type? */
+bool Type::isDatatype() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isDatatype();
+}
+
+/** Cast to a Constructor type */
+Type::operator ConstructorType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isConstructor());
+  return ConstructorType(*this);
+}
+
+/** Is this the Constructor type? */
+bool Type::isConstructor() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isConstructor();
+}
+
+/** Cast to a Selector type */
+Type::operator SelectorType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isSelector());
+  return SelectorType(*this);
+}
+
+/** Is this the Selector type? */
+bool Type::isSelector() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSelector();
+}
+
+/** Cast to a Tester type */
+Type::operator TesterType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isTester());
+  return TesterType(*this);
+}
+
+/** Is this the Tester type? */
+bool Type::isTester() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isTester();
+}
+
 /** Is this a function type? */
 bool Type::isFunction() const {
   NodeManagerScope nms(d_nodeManager);
@@ -349,6 +401,26 @@ BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
   Assert(isBitVector());
 }
 
+DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isDatatype());
+}
+
+ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isConstructor());
+}
+
+SelectorType::SelectorType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isSelector());
+}
+
+TesterType::TesterType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isTester());
+}
+
 FunctionType::FunctionType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isFunction());
@@ -392,8 +464,32 @@ Type ArrayType::getConstituentType() const {
   return makeType(d_typeNode->getArrayConstituentType());
 }
 
-size_t TypeHashStrategy::hash(const Type& t) {
-  return TypeNodeHashStrategy::hash(*t.d_typeNode);
+Type ConstructorType::getReturnType() const {
+  return makeType(d_typeNode->getConstructorReturnType());
+}
+
+const Datatype& DatatypeType::getDatatype() const {
+  return d_typeNode->getConst<Datatype>();
+}
+
+DatatypeType SelectorType::getDomain() const {
+  return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+Type SelectorType::getRangeType() const {
+  return makeType((*d_typeNode)[1]);
+}
+
+DatatypeType TesterType::getDomain() const {
+  return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+BooleanType TesterType::getRangeType() const {
+  return BooleanType(makeType(d_nodeManager->booleanType()));
+}
+
+size_t TypeHashFunction::operator()(const Type& t) {
+  return TypeNodeHashFunction()(NodeManager::fromType(t));
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index 130aa3122..3b476ddf5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters, dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -36,6 +36,8 @@ class TypeNode;
 
 class SmtEngine;
 
+class Datatype;
+
 template <bool ref_count>
 class NodeTemplate;
 
@@ -44,6 +46,10 @@ class IntegerType;
 class RealType;
 class BitVectorType;
 class ArrayType;
+class DatatypeType;
+class ConstructorType;
+class SelectorType;
+class TesterType;
 class FunctionType;
 class TupleType;
 class KindType;
@@ -52,10 +58,10 @@ class SortConstructorType;
 class Type;
 
 /** Strategy for hashing Types */
-struct CVC4_PUBLIC TypeHashStrategy {
+struct CVC4_PUBLIC TypeHashFunction {
   /** Return a hash code for type t */
-  static size_t hash(const CVC4::Type& t);
-};/* struct TypeHashStrategy */
+  size_t operator()(const CVC4::Type& t);
+};/* struct TypeHashFunction */
 
 /**
  * Output operator for types
@@ -259,6 +265,54 @@ public:
   operator ArrayType() const throw(AssertionException);
 
   /**
+   * Is this a datatype type?
+   * @return true if the type is a datatype type
+   */
+  bool isDatatype() const;
+
+  /**
+   * Cast this type to a datatype type
+   * @return the DatatypeType
+   */
+  operator DatatypeType() const throw(AssertionException);
+
+  /**
+   * Is this a constructor type?
+   * @return true if the type is a constructor type
+   */
+  bool isConstructor() const;
+
+  /**
+   * Cast this type to a constructor type
+   * @return the ConstructorType
+   */
+  operator ConstructorType() const throw(AssertionException);
+
+  /**
+   * Is this a selector type?
+   * @return true if the type is a selector type
+   */
+  bool isSelector() const;
+
+  /**
+   * Cast this type to a selector type
+   * @return the SelectorType
+   */
+  operator SelectorType() const throw(AssertionException);
+
+  /**
+   * Is this a tester type?
+   * @return true if the type is a tester type
+   */
+  bool isTester() const;
+
+  /**
+   * Cast this type to a tester type
+   * @return the TesterType
+   */
+  operator TesterType() const throw(AssertionException);
+
+  /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
@@ -449,6 +503,78 @@ public:
   unsigned getSize() const;
 };/* class BitVectorType */
 
+
+/**
+ * Class encapsulating the datatype type
+ */
+class CVC4_PUBLIC DatatypeType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  DatatypeType(const Type& type) throw(AssertionException);
+
+  /** Get the underlying datatype */
+  const Datatype& getDatatype() const;
+
+};/* class DatatypeType */
+
+
+/**
+ * Class encapsulating the constructor type
+ */
+class CVC4_PUBLIC ConstructorType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  ConstructorType(const Type& type) throw(AssertionException);
+
+  /** Get the return type */
+  Type getReturnType() const;
+
+};/* class ConstructorType */
+
+
+/**
+ * Class encapsulating the Selector type
+ */
+class CVC4_PUBLIC SelectorType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SelectorType(const Type& type) throw(AssertionException);
+
+  /** Get the domain type for this selector (the datatype type) */
+  DatatypeType getDomain() const;
+
+  /** Get the range type for this selector (the field type) */
+  Type getRangeType() const;
+
+};/* class SelectorType */
+
+/**
+ * Class encapsulating the Tester type
+ */
+class CVC4_PUBLIC TesterType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  TesterType(const Type& type) throw(AssertionException);
+
+  /** Get the type that this tester tests (the datatype type) */
+  DatatypeType getDomain() const;
+
+  /**
+   * Get the range type for this tester (included for sake of
+   * interface completeness), but doesn't give useful information).
+   */
+  BooleanType getRangeType() const;
+
+};/* class TesterType */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__TYPE_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index badc3b72f..7549af895 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -76,28 +76,38 @@ TypeNode TypeNode::getArrayConstituentType() const {
   return (*this)[1];
 }
 
-/** Is this a function type? */
+TypeNode TypeNode::getConstructorReturnType() const {
+  Assert(isConstructor());
+  return (*this)[getNumChildren()-1];
+}
+
 bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
 }
 
-/** Is this a predicate type? NOTE: all predicate types are also
-    function types. */
 bool TypeNode::isPredicate() const {
   return isFunction() && getRangeType().isBoolean();
 }
 
-vector<TypeNode> TypeNode::getArgTypes() const {
-  Assert(isFunction());
+std::vector<TypeNode> TypeNode::getArgTypes() const {
   vector<TypeNode> args;
-  for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
-    args.push_back((*this)[i]);
+  if(isTester()) {
+    Assert(getNumChildren() == 1);
+    args.push_back((*this)[0]);
+  } else {
+    Assert(isFunction() || isConstructor() || isSelector());
+    for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
+      args.push_back((*this)[i]);
+    }
   }
   return args;
 }
 
 TypeNode TypeNode::getRangeType() const {
-  Assert(isFunction());
+  if(isTester()) {
+    return NodeManager::currentNM()->booleanType();
+  }
+  Assert(isFunction() || isConstructor() || isSelector());
   return (*this)[getNumChildren()-1];
 }
 
@@ -137,6 +147,26 @@ bool TypeNode::isBitVector() const {
   return getKind() == kind::BITVECTOR_TYPE;
 }
 
+/** Is this a datatype type */
+bool TypeNode::isDatatype() const {
+  return getKind() == kind::DATATYPE_TYPE;
+}
+
+/** Is this a constructor type */
+bool TypeNode::isConstructor() const {
+  return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+/** Is this a selector type */
+bool TypeNode::isSelector() const {
+  return getKind() == kind::SELECTOR_TYPE;
+}
+
+/** Is this a tester type */
+bool TypeNode::isTester() const {
+  return getKind() == kind::TESTER_TYPE;
+}
+
 /** Is this a bit-vector type of size <code>size</code> */
 bool TypeNode::isBitVector(unsigned size) const {
   return getKind() == kind::BITVECTOR_TYPE &&
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index ead85cd19..049173867 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -360,18 +360,32 @@ public:
   /** Get the element type (for array types) */
   TypeNode getArrayConstituentType() const;
 
-  /** Is this a function type? */
+  /** Get the return type (for constructor types) */
+  TypeNode getConstructorReturnType() const;
+
+  /**
+   * Is this a function type?  Function-like things (e.g. datatype
+   * selectors) that aren't actually functions are NOT considered
+   * functions, here.
+   */
   bool isFunction() const;
 
-  /** Get the argument types */
+  /**
+   * Get the argument types of a function, datatype constructor,
+   * datatype selector, or datatype tester.
+   */
   std::vector<TypeNode> getArgTypes() const;
 
-  /** Get the range type (i.e., the type of the result). */
+  /**
+   * Get the range type (i.e., the type of the result) of a function,
+   * datatype constructor, datatype selector, or datatype tester.
+   */
   TypeNode getRangeType() const;
 
   /**
    * Is this a predicate type?
-   * NOTE: all predicate types are also function types.
+   * NOTE: all predicate types are also function types (so datatype
+   * testers are not considered "predicates" for the purpose of this function).
    */
   bool isPredicate() const;
 
@@ -387,6 +401,18 @@ public:
   /** Is this a bit-vector type of size <code>size</code> */
   bool isBitVector(unsigned size) const;
 
+  /** Is this a datatype type */
+  bool isDatatype() const;
+
+  /** Is this a constructor type */
+  bool isConstructor() const;
+
+  /** Is this a selector type */
+  bool isSelector() const;
+
+  /** Is this a tester type */
+  bool isTester() const;
+
   /** Get the size of this bit-vector type */
   unsigned getBitVectorSize() const;
 
@@ -430,11 +456,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 }
 
 // for hash_maps, hash_sets..
-struct TypeNodeHashStrategy {
-  static inline size_t hash(const TypeNode& node) {
+struct TypeNodeHashFunction {
+  size_t operator()(TypeNode node) const {
     return (size_t) node.getId();
   }
-};/* struct TypeNodeHashStrategy */
+};/* struct TypeNodeHashFunction */
 
 }/* CVC4 namespace */
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0a05271e2..33e576a32 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2,10 +2,10 @@
 /*! \file Cvc.g
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -37,7 +37,7 @@ options {
 
 @lexer::includes {
 /** This suppresses warnings about the redefinition of token symbols between different
-  * parsers. The redefinitions should be harmless as long as no client: (a) #include's 
+  * parsers. The redefinitions should be harmless as long as no client: (a) #include's
   * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
 #pragma GCC system_header
 
@@ -56,6 +56,26 @@ options {
 namespace CVC4 {
   class Expr;
 }/* CVC4 namespace */
+
+namespace CVC4 {
+  namespace parser {
+    namespace cvc {
+      /**
+       * This class is just here to get around an unfortunate bit of Antlr.
+       * We use strings below as return values from rules, which require
+       * them to be constructible by a uintptr_t.  So we derive the string
+       * class to provide just such a conversion.
+       */
+      class mystring : public std::string {
+      public:
+        mystring(const std::string& s) : std::string(s) {}
+        mystring(uintptr_t) : std::string() {}
+        mystring() : std::string() {}
+      };/* class mystring */
+    }/* CVC4::parser::cvc namespace */
+  }/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
 }
 
 @parser::postinclude {
@@ -72,7 +92,7 @@ using namespace CVC4::parser;
 
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef PARSER_STATE 
+#undef PARSER_STATE
 #define PARSER_STATE ((Parser*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
@@ -109,6 +129,8 @@ command returns [CVC4::Command* cmd = 0]
   Expr f;
   SExpr sexpr;
   std::string s;
+  Type t;
+  std::vector<CVC4::Datatype> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
@@ -119,6 +141,13 @@ command returns [CVC4::Command* cmd = 0]
     { cmd = new SetOptionCommand(AntlrInput::tokenText($STRING_LITERAL), sexpr); }
   | PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
   | POP_TOK SEMICOLON { cmd = new PopCommand(); }
+    // Datatypes can be mututally-recursive if they're in the same
+    // definition block, separated by a comma.  So we parse everything
+    // and then ask the ExprManager to resolve everything in one go.
+  | DATATYPE_TOK datatypeDef[dts]
+    ( COMMA datatypeDef[dts] )*
+    END_TOK SEMICOLON
+    { cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   | declaration[cmd]
   | EOF
   ;
@@ -159,8 +188,8 @@ declType[CVC4::Type& t, std::vector<std::string>& idList]
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
-    TYPE_TOK 
-    { PARSER_STATE->mkSorts(idList); 
+    TYPE_TOK
+    { PARSER_STATE->mkSorts(idList);
       t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
     type[t] { PARSER_STATE->mkVars(idList,t); }
@@ -179,7 +208,7 @@ type[CVC4::Type& t]
   : /* Simple type */
     baseType[t]
   | /* Single-parameter function type */
-    baseType[t] ARROW_TOK baseType[t2] 
+    baseType[t] ARROW_TOK baseType[t2]
     { t = EXPR_MANAGER->mkFunctionType(t,t2); }
   | /* Multi-parameter function type */
     LPAREN baseType[t]
@@ -218,34 +247,62 @@ identifier[std::string& id,
   ;
 
 /**
- * Matches a type.
- * TODO: parse more types
+ * Matches a type (which MUST be already declared).
+ *
+ * @return the type identifier
  */
 baseType[CVC4::Type& t]
+  : maybeUndefinedBaseType[t,CHECK_DECLARED]
+  ;
+
+/**
+ * Matches a type (which may not be declared yet).  Returns the
+ * identifier.  If the type is declared, returns the Type in the 't'
+ * parameter; otherwise a null Type is returned in 't'.  If 'check' is
+ * CHECK_DECLARED and the type is not declared, an exception is
+ * thrown.
+ *
+ * @return the type identifier
+ *
+ * @TODO parse more types
+ */
+maybeUndefinedBaseType[CVC4::Type& t,
+                       CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id]
 @init {
-  std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  AssertArgument(check == CHECK_DECLARED || check == CHECK_NONE,
+                 check, "CVC parser: can't use CHECK_UNDECLARED with maybeUndefinedBaseType[]");
 }
-  : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
-  | INT_TOK { t = EXPR_MANAGER->integerType(); }
-  | REAL_TOK { t = EXPR_MANAGER->realType(); }
-  | typeSymbol[t]
+  : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); id = AntlrInput::tokenText($BOOLEAN_TOK); }
+  | INT_TOK { t = EXPR_MANAGER->integerType(); id = AntlrInput::tokenText($INT_TOK); }
+  | REAL_TOK { t = EXPR_MANAGER->realType(); id = AntlrInput::tokenText($REAL_TOK); }
+  | typeSymbol[t,check]
+    { id = $typeSymbol.id; }
   ;
 
 /**
- * Matches a type identifier
+ * Matches a type identifier.  Returns the identifier.  If the type is
+ * declared, returns the Type in the 't' parameter; otherwise a null
+ * Type is returned in 't'.  If 'check' is CHECK_DECLARED and the type
+ * is not declared, an exception is thrown.
+ *
+ * @return the type identifier
  */
-typeSymbol[CVC4::Type& t]
+typeSymbol[CVC4::Type& t,
+           CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id]
 @init {
-  std::string id;
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : identifier[id,CHECK_DECLARED,SYM_SORT]
-    { t = PARSER_STATE->getSort(id); }
+  : identifier[id,check,SYM_SORT]
+    { bool isNew = (check == CHECK_UNDECLARED || check == CHECK_NONE) &&
+                   !PARSER_STATE->isDeclared(id, SYM_SORT);
+      t = isNew ? Type() : PARSER_STATE->getSort(id);
+    }
   ;
 
 /**
  * Matches a CVC4 formula.
+ *
  * @return the expression representing the formula
  */
 formula[CVC4::Expr& formula]
@@ -311,7 +368,7 @@ iffFormula[CVC4::Expr& f]
   Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : impliesFormula[f]
-    ( IFF_TOK 
+    ( IFF_TOK
     	iffFormula[e]
         { f = MK_EXPR(CVC4::kind::IFF, f, e); }
     )?
@@ -371,7 +428,7 @@ andFormula[CVC4::Expr& f]
   std::vector<Expr> exprs;
   Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : notFormula[f] 
+  : notFormula[f]
     ( AND_TOK { exprs.push_back(f); }
       notFormula[f] { exprs.push_back(f); } )*
     {
@@ -412,9 +469,9 @@ comparisonFormula[CVC4::Expr& f]
     ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; }
       | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; }
       | GT_TOK { op = CVC4::kind::GT; negate = false; }
-      | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } 
+      | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; }
       | LT_TOK { op = CVC4::kind::LT; negate = false; }
-      | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) 
+      | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; })
       plusTerm[e]
       { f = MK_EXPR(op, f, e);
         if(negate) {
@@ -424,7 +481,7 @@ comparisonFormula[CVC4::Expr& f]
     )?
   ;
 
-/** Parses a plus/minus term (left-associative). 
+/** Parses a plus/minus term (left-associative).
     TODO: This won't take advantage of n-ary PLUS's. */
 plusTerm[CVC4::Expr& f]
 @init {
@@ -435,13 +492,13 @@ plusTerm[CVC4::Expr& f]
 }
   : multTerm[f]
     ( ( PLUS_TOK { op = CVC4::kind::PLUS; }
-      | MINUS_TOK { op = CVC4::kind::MINUS; } ) 
+      | MINUS_TOK { op = CVC4::kind::MINUS; } )
       multTerm[e]
       { f = MK_EXPR(op, f, e); }
     )*
   ;
 
-/** Parses a multiply/divide term (left-associative). 
+/** Parses a multiply/divide term (left-associative).
     TODO: This won't take advantage of n-ary MULT's. */
 multTerm[CVC4::Expr& f]
 @init {
@@ -451,7 +508,7 @@ multTerm[CVC4::Expr& f]
 }
   : expTerm[f]
     ( ( STAR_TOK { op = CVC4::kind::MULT; }
-      | DIV_TOK { op = CVC4::kind::DIVISION; } ) 
+      | DIV_TOK { op = CVC4::kind::DIVISION; } )
       expTerm[e]
       { f = MK_EXPR(op, f, e); }
     )*
@@ -494,18 +551,29 @@ unaryTerm[CVC4::Expr& f]
   std::vector<Expr> args;
   Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : /* function application */
-    // { isFunction(AntlrInput::tokenText(LT(1))) }?
+  : /* function/constructor application */
     functionSymbol[f]
     { args.push_back( f ); }
     LPAREN formulaList[args] RPAREN
     // TODO: check arity
-    { f = MK_EXPR(CVC4::kind::APPLY_UF, args); }
+    { Type t = f.getType();
+      if( t.isFunction() ) {
+        f = MK_EXPR(CVC4::kind::APPLY_UF, args);
+      } else if( t.isConstructor() ) {
+        Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl;
+        f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+      } else if( t.isSelector() ) {
+        Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl;
+        f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
+      } else if( t.isTester() ) {
+        Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl;
+        f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
+      }
+    }
 
   | /* if-then-else */
     iteTerm[f]
 
-    
   | /* Unary minus */
     MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); }
 
@@ -517,10 +585,17 @@ unaryTerm[CVC4::Expr& f]
   | FALSE_TOK { f = MK_CONST(false); }
 
   | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
+  | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 
   | /* variable */
     identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { f = PARSER_STATE->getVariable(name); }
+    { f = PARSER_STATE->getVariable(name);
+      // datatypes: 0-ary constructors
+      if( PARSER_STATE->getType(name).isConstructor() ){
+        args.push_back( f );
+        f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+      }
+    }
   ;
 
 /**
@@ -546,7 +621,7 @@ iteElseTerm[CVC4::Expr& f]
   std::vector<Expr> args;
   Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : ELSE_TOK formula[f] 
+  : ELSE_TOK formula[f]
   | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
     THEN_TOK iteThen = formula[f] { args.push_back(f); }
     iteElse = iteElseTerm[f] { args.push_back(f); }
@@ -564,10 +639,65 @@ functionSymbol[CVC4::Expr& f]
   std::string name;
 }
   : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-    { PARSER_STATE->checkFunction(name);
+    { PARSER_STATE->checkFunctionLike(name);
       f = PARSER_STATE->getVariable(name); }
   ;
 
+/**
+ * Parses a datatype definition
+ */
+datatypeDef[std::vector<CVC4::Datatype>& datatypes]
+@init {
+  std::string id;
+}
+  : identifier[id,CHECK_UNDECLARED,SYM_SORT]
+    { datatypes.push_back(Datatype(id)); }
+    EQUAL_TOK constructorDef[datatypes.back()]
+    ( BAR_TOK constructorDef[datatypes.back()] )*
+  ;
+
+/**
+ * Parses a constructor defintion for type
+ */
+constructorDef[CVC4::Datatype& type]
+@init {
+  std::string id;
+  CVC4::Datatype::Constructor* ctor;
+}
+  : 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);
+    }
+    ( LPAREN
+      selector[*ctor]
+      ( COMMA selector[*ctor] )*
+      RPAREN
+    )?
+    { // make the constructor
+      type.addConstructor(*ctor);
+      Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
+      delete ctor;
+    }
+  ;
+
+selector[CVC4::Datatype::Constructor& ctor]
+@init {
+  std::string id;
+  Type type;
+}
+  : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE]
+    { if(type.isNull()) {
+        ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id));
+      } else {
+        ctor.addArg(id, type);
+      }
+      Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
+    }
+  ;
 
 // Keywords
 
@@ -598,6 +728,16 @@ TRUE_TOK : 'TRUE';
 TYPE_TOK : 'TYPE';
 XOR_TOK : 'XOR';
 
+DATATYPE_TOK : 'DATATYPE';
+END_TOK : 'END';
+BAR_TOK : '|';
+
+ARRAY_TOK : 'ARRAY';
+OF_TOK : 'OF';
+WITH_TOK : 'WITH';
+
+BITVECTOR_TOK : 'BITVECTOR';
+
 // Symbols
 
 COLON : ':';
diff --git a/src/parser/input.h b/src/parser/input.h
index b9123fc45..71b2faeae 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -2,10 +2,10 @@
 /*! \file input.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -179,7 +179,7 @@ protected:
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
-};
+};/* class Input */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 0ebccf720..c8a9876d5 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -72,8 +72,7 @@ Expr Parser::getFunction(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Type
-Parser::getType(const std::string& var_name,
+Type Parser::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
   Type t = getSymbol(var_name, type).getType();
@@ -98,9 +97,15 @@ bool Parser::isBoolean(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 }
 
-/* Returns true if name is bound to a function. */
-bool Parser::isFunction(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
+/* Returns true if name is bound to a function-like thing (function,
+ * constructor, tester, or selector). */
+bool Parser::isFunctionLike(const std::string& name) {
+  if(!isDeclared(name, SYM_VARIABLE)) {
+    return false;
+  }
+  Type type = getType(name);
+  return type.isFunction() || type.isConstructor() ||
+    type.isTester() || type.isSelector();
 }
 
 /* Returns true if name is bound to a defined function. */
@@ -200,7 +205,7 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) {
   return type;
 }
 
-const std::vector<Type>
+std::vector<Type>
 Parser::mkSorts(const std::vector<std::string>& names) {
   std::vector<Type> types;
   for(unsigned i = 0; i < names.size(); ++i) {
@@ -209,6 +214,53 @@ Parser::mkSorts(const std::vector<std::string>& names) {
   return types;
 }
 
+std::vector<DatatypeType>
+Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+  std::vector<DatatypeType> types =
+    d_exprManager->mkMutualDatatypeTypes(datatypes);
+  Assert(datatypes.size() == types.size());
+  for(unsigned i = 0; i < datatypes.size(); ++i) {
+    DatatypeType t = types[i];
+    const Datatype& dt = t.getDatatype();
+    Debug("parser-idt") << "define " << dt.getName() << " as " << t << std::endl;
+    defineType(dt.getName(), t);
+    for(Datatype::const_iterator j = dt.begin(),
+          j_end = dt.end();
+        j != j_end;
+        ++j) {
+      const Datatype::Constructor& ctor = *j;
+      Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+      Expr constructor = ctor.getConstructor();
+      Debug("parser-idt") << "+ define " << constructor << std::endl;
+      string constructorName = constructor.toString();
+      if(isDeclared(constructorName, SYM_VARIABLE)) {
+        throw ParserException(constructorName + " already declared");
+      }
+      defineVar(constructorName, constructor);
+      Expr tester = ctor.getTester();
+      Debug("parser-idt") << "+ define " << tester << std::endl;
+      string testerName = tester.toString();
+      if(isDeclared(testerName, SYM_VARIABLE)) {
+        throw ParserException(testerName + " already declared");
+      }
+      defineVar(testerName, tester);
+      for(Datatype::Constructor::const_iterator k = ctor.begin(),
+            k_end = ctor.end();
+          k != k_end;
+          ++k) {
+        Expr selector = (*k).getSelector();
+        Debug("parser-idt") << "+++ define " << selector << std::endl;
+        string selectorName = selector.toString();
+        if(isDeclared(selectorName, SYM_VARIABLE)) {
+          throw ParserException(selectorName + " already declared");
+        }
+        defineVar(selectorName, selector);
+      }
+    }
+  }
+  return types;
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
@@ -249,10 +301,10 @@ void Parser::checkDeclaration(const std::string& varName,
   }
 }
 
-void Parser::checkFunction(const std::string& name)
+void Parser::checkFunctionLike(const std::string& name)
   throw (ParserException) {
-  if( d_checksEnabled && !isFunction(name) ) {
-    parseError("Expecting function symbol, found '" + name + "'");
+  if( d_checksEnabled && !isFunctionLike(name) ) {
+    parseError("Expecting function-like symbol, found '" + name + "'");
   }
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 15fe5126c..718b862ab 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -263,7 +263,7 @@ public:
    * @throws ParserException if checks are enabled and name is not
    * bound to a function
    */
-  void checkFunction(const std::string& name) throw (ParserException);
+  void checkFunctionLike(const std::string& name) throw (ParserException);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
@@ -337,8 +337,13 @@ public:
   /**
    * Creates new sorts with the given names (all of arity 0).
    */
-  const std::vector<Type>
-  mkSorts(const std::vector<std::string>& names);
+  std::vector<Type> mkSorts(const std::vector<std::string>& names);
+
+  /**
+   * Create sorts of mutually-recursive datatypes.
+   */
+  std::vector<DatatypeType>
+  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
 
   /**
    * Add an operator to the current legal set.
@@ -357,8 +362,8 @@ public:
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
-  /** Is the symbol bound to a function? */
-  bool isFunction(const std::string& name);
+  /** Is the symbol bound to a function (or function-like thing)? */
+  bool isFunctionLike(const std::string& name);
 
   /** Is the symbol bound to a defined function? */
   bool isDefinedFunction(const std::string& name);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 39d834891..96ac46bf1 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -2,10 +2,10 @@
 /*! \file Smt.g
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters, taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -365,7 +365,7 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { PARSER_STATE->checkFunction(name);
+    { PARSER_STATE->checkFunctionLike(name);
       fun = PARSER_STATE->getVariable(name); }
   ;
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f34279149..a5a633e48 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2,8 +2,8 @@
 /*! \file Smt2.g
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -357,7 +357,7 @@ term[CVC4::Expr& expr]
   | /* A non-built-in function application */
     LPAREN_TOK
     functionName[name,CHECK_DECLARED]
-    { PARSER_STATE->checkFunction(name);
+    { PARSER_STATE->checkFunctionLike(name);
       const bool isDefinedFunction =
         PARSER_STATE->isDefinedFunction(name);
       if(isDefinedFunction) {
@@ -578,7 +578,7 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { PARSER_STATE->checkFunction(name);
+    { PARSER_STATE->checkFunctionLike(name);
       fun = PARSER_STATE->getVariable(name); }
   ;
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d2cf3f8b1..a048bc3b2 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -20,6 +20,8 @@
 #include "util/language.h"
 
 #include <iostream>
+#include <algorithm>
+#include <iterator>
 
 using namespace std;
 
@@ -29,7 +31,157 @@ namespace cvc {
 
 void CvcPrinter::toStream(std::ostream& out, TNode n,
                           int toDepth, bool types) const {
-  n.toStream(out, toDepth, types, language::output::LANG_AST);
+  // null
+  if(n.getKind() == kind::NULL_EXPR) {
+    out << "NULL";
+    return;
+  }
+
+  // variable
+  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    string s;
+    if(n.getAttribute(expr::VarNameAttr(), s)) {
+      out << s;
+    } else {
+      if(n.getKind() == kind::VARIABLE) {
+        out << "var_";
+      } else {
+        out << n.getKind() << '_';
+      }
+      out << n.getId();
+    }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, -1, false, language::output::LANG_CVC4);
+    }
+
+    return;
+  }
+
+  // constant
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    switch(n.getKind()) {
+    case kind::BITVECTOR_TYPE:
+      out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";
+      break;
+    case kind::CONST_BITVECTOR: {
+      const BitVector& bv = n.getConst<BitVector>();
+      const Integer& x = bv.getValue();
+      out << "0bin";
+      unsigned n = bv.getSize();
+      while(n-- > 0) {
+        out << (x.testBit(n) ? '1' : '0');
+      }
+      break;
+    }
+    case kind::CONST_BOOLEAN:
+      // the default would print "1" or "0" for bool, that's not correct
+      // for our purposes
+      out << (n.getConst<bool>() ? "TRUE" : "FALSE");
+      break;
+    case kind::CONST_RATIONAL: {
+      const Rational& rat = n.getConst<Rational>();
+      out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      break;
+    }
+    case kind::BUILTIN:
+      switch(Kind k = n.getConst<Kind>()) {
+      case kind::EQUAL: out << '='; break;
+      case kind::PLUS: out << '+'; break;
+      case kind::MULT: out << '*'; break;
+      case kind::MINUS:
+      case kind::UMINUS: out << '-'; break;
+      case kind::DIVISION: out << '/'; break;
+      case kind::LT: out << '<'; break;
+      case kind::LEQ: out << "<="; break;
+      case kind::GT: out << '>'; break;
+      case kind::GEQ: out << ">="; break;
+      case kind::IMPLIES: out << "=>"; break;
+      case kind::IFF: out << "<=>"; break;
+      default:
+        out << k;
+      }
+      break;
+    default:
+      // fall back on whatever operator<< does on underlying type; we
+      // might luck out and be SMT-LIB v2 compliant
+      kind::metakind::NodeValueConstPrinter::toStream(out, n);
+    }
+
+    return;
+  } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    out << n.getOperator();
+    if(n.getNumChildren() > 0) {
+      out << '(';
+      if(n.getNumChildren() > 1) {
+        copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+      }
+      out << n[n.getNumChildren() - 1] << ')';
+    }
+    return;
+  } else if(n.getMetaKind() == kind::metakind::OPERATOR) {
+    switch(Kind k = n.getKind()) {
+    case kind::FUNCTION_TYPE:
+    case kind::CONSTRUCTOR_TYPE:
+    case kind::SELECTOR_TYPE:
+    case kind::TESTER_TYPE:
+      if(n.getNumChildren() > 0) {
+        copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " -> "));
+        out << n[n.getNumChildren() - 1];
+      }
+      break;
+
+    case kind::ARRAY_TYPE:
+      out << "ARRAY " << n[0] << " OF " << n[1];
+      break;
+    case kind::SELECT:
+      out << n[0] << '[' << n[1] << ']';
+      break;
+    case kind::STORE:
+      out << n[0] << " WITH [" << n[1] << "] = " << n[2];
+      break;
+
+    case kind::TUPLE_TYPE:
+      out << '[';
+      copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ","));
+      out << n[n.getNumChildren() - 1];
+      out << ']';
+      break;
+    case kind::TUPLE:
+      out << "( ";
+      copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", "));
+      out << n[n.getNumChildren() - 1];
+      out << " )";
+      break;
+
+    case kind::ITE:
+      out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2];
+      break;
+
+    default:
+      if(k == kind::NOT && n[0].getKind() == kind::EQUAL) {
+        // collapse NOT-over-EQUAL
+        out << n[0][0] << " /= " << n[0][1];
+      } else if(n.getNumChildren() == 2) {
+        // infix operator
+        out << n[0] << ' ' << n.getOperator() << ' ' << n[1];
+      } else {
+        // prefix operator
+        out << n.getOperator() << ' ';
+        if(n.getNumChildren() > 0) {
+          if(n.getNumChildren() > 1) {
+            copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " "));
+          }
+          out << n[n.getNumChildren() - 1];
+        }
+      }
+    }
+    return;
+  }
+
+  Unhandled();
+
 }/* CvcPrinter::toStream() */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d821b7f4a..2467db3bb 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -46,6 +46,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/datatypes/theory_datatypes.h"
 
 
 using namespace std;
@@ -98,7 +99,7 @@ class SmtEnginePrivate {
 public:
 
   /**
-   * Pre-process an Node.  This is expected to be highly-variable,
+   * Pre-process a Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
    * passes over the Node.
    */
@@ -141,6 +142,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->addTheory<theory::arith::TheoryArith>();
   d_theoryEngine->addTheory<theory::arrays::TheoryArrays>();
   d_theoryEngine->addTheory<theory::bv::TheoryBV>();
+  d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>();
   switch(Options::current()->uf_implementation) {
   case Options::TIM:
     d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>();
@@ -442,29 +444,40 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n,
 Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
   throw(NoSuchFunctionException, AssertionException) {
 
-  Node n;
-  if(!Options::current()->lazyDefinitionExpansion) {
-    Debug("expand") << "have: " << n << endl;
-    hash_map<TNode, Node, TNodeHashFunction> cache;
-    n = expandDefinitions(smt, in, cache);
-    Debug("expand") << "made: " << n << endl;
-  } else {
-    n = in;
-  }
+  try {
+    Node n;
+    if(!Options::current()->lazyDefinitionExpansion) {
+      Debug("expand") << "have: " << n << endl;
+      hash_map<TNode, Node, TNodeHashFunction> cache;
+      n = expandDefinitions(smt, in, cache);
+      Debug("expand") << "made: " << n << endl;
+    } else {
+      n = in;
+    }
 
-  // For now, don't re-statically-learn from learned facts; this could
-  // be useful though (e.g., theory T1 could learn something further
-  // from something learned previously by T2).
-  NodeBuilder<> learned(kind::AND);
-  learned << n;
-  smt.d_theoryEngine->staticLearning(n, learned);
-  if(learned.getNumChildren() == 1) {
-    learned.clear();
-  } else {
-    n = learned;
-  }
+    // For now, don't re-statically-learn from learned facts; this could
+    // be useful though (e.g., theory T1 could learn something further
+    // from something learned previously by T2).
+    NodeBuilder<> learned(kind::AND);
+    learned << n;
+    smt.d_theoryEngine->staticLearning(n, learned);
+    if(learned.getNumChildren() == 1) {
+      learned.clear();
+    } else {
+      n = learned;
+    }
 
-  return smt.d_theoryEngine->preprocess(n);
+    return smt.d_theoryEngine->preprocess(n);
+  } catch(TypeCheckingExceptionPrivate& tcep) {
+    // Calls to this function should have already weeded out any
+    // typechecking exceptions via (e.g.) ensureBoolean().  But a
+    // theory could still create a new expression that isn't
+    // well-typed, and we don't want the C++ runtime to abort our
+    // process without any error notice.
+    InternalError("A bad expression was produced.  "
+                  "Original exception follows:\n%s",
+                  tcep.toString().c_str());
+  }
 }
 
 Result SmtEngine::check() {
@@ -479,10 +492,21 @@ Result SmtEngine::quickCheck() {
 
 void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
   throw(NoSuchFunctionException, AssertionException) {
-  Debug("smt") << "push_back assertion " << n << endl;
-  smt.d_haveAdditions = true;
-  Node node = SmtEnginePrivate::preprocess(smt, n);
-  smt.d_propEngine->assertFormula(node);
+  try {
+    Debug("smt") << "push_back assertion " << n << endl;
+    smt.d_haveAdditions = true;
+    Node node = SmtEnginePrivate::preprocess(smt, n);
+    smt.d_propEngine->assertFormula(node);
+  } catch(TypeCheckingExceptionPrivate& tcep) {
+    // Calls to this function should have already weeded out any
+    // typechecking exceptions via (e.g.) ensureBoolean().  But a
+    // theory could still create a new expression that isn't
+    // well-typed, and we don't want the C++ runtime to abort our
+    // process without any error notice.
+    InternalError("A bad expression was produced.  "
+                  "Original exception follows:\n%s",
+                  tcep.toString().c_str());
+  }
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index b72502eca..0d680f4c9 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -3,7 +3,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = builtin booleans uf arith arrays bv
+SUBDIRS = builtin booleans uf arith arrays bv datatypes
 
 noinst_LTLIBRARIES = libtheory.la
 
@@ -36,7 +36,8 @@ libtheory_la_LIBADD = \
 	@builddir@/uf/libuf.la \
 	@builddir@/arith/libarith.la \
 	@builddir@/arrays/libarrays.la \
-	@builddir@/bv/libbv.la
+	@builddir@/bv/libbv.la \
+	@builddir@/datatypes/libdatatypes.la
 
 EXTRA_DIST = \
 	rewriter_tables_template.h \
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index d50397598..716323b8a 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_builtin_rewriter.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -36,7 +36,7 @@ class TheoryBuiltinRewriter {
 public:
 
   static inline RewriteResponse postRewrite(TNode node) {
-    if (node.getKind() == kind::EQUAL) {
+    if(node.getKind() == kind::EQUAL) {
       return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node);
     }
     return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/datatypes/Makefile b/src/theory/datatypes/Makefile
new file mode 100644
index 000000000..cb3da4be3
--- /dev/null
+++ b/src/theory/datatypes/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/datatypes
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
new file mode 100644
index 000000000..69d83faf4
--- /dev/null
+++ b/src/theory/datatypes/Makefile.am
@@ -0,0 +1,16 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libdatatypes.la
+
+libdatatypes_la_SOURCES = \
+	theory_datatypes_type_rules.h \
+	theory_datatypes.h \
+	datatypes_rewriter.h \
+	theory_datatypes.cpp \
+	union_find.h \
+	union_find.cpp
+
+EXTRA_DIST = kinds
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
new file mode 100644
index 000000000..4fa684c6e
--- /dev/null
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file datatypes_rewriter.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewriter for the theory of inductive datatypes
+ **
+ ** Rewriter for the theory of inductive datatypes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
+#define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
+
+#include "theory/rewriter.h"
+#include "theory/datatypes/theory_datatypes.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+class DatatypesRewriter {
+
+public:
+
+  static RewriteResponse postRewrite(TNode in) {
+    Debug("datatypes-rewrite") << "post-rewriting " << in << std::endl;
+
+    /*
+    checkFiniteWellFounded();
+    */
+
+    if(in.getKind() == kind::APPLY_TESTER) {
+      if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
+        bool result = TheoryDatatypes::checkTrivialTester(in);
+        Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial tester " << in
+                                   << " " << result << std::endl;
+        return RewriteResponse(REWRITE_DONE,
+                               NodeManager::currentNM()->mkConst(result));
+      } else {
+        const Datatype& dt = in[0].getType().getConst<Datatype>();
+        if(dt.getNumConstructors() == 1) {
+          // only one constructor, so it must be
+          Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                     << "only one ctor for " << dt.getName()
+                                     << " and that is " << dt[0].getName()
+                                     << std::endl;
+          return RewriteResponse(REWRITE_DONE,
+                                 NodeManager::currentNM()->mkConst(true));
+        }
+      }
+    }
+    if(in.getKind() == kind::APPLY_SELECTOR &&
+       in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
+      // Have to be careful not to rewrite well-typed expressions
+      // where the selector doesn't match the constructor,
+      // e.g. "pred(zero)".
+      TNode selector = in.getOperator();
+      TNode constructor = in[0].getOperator();
+      Expr selectorExpr = selector.toExpr();
+      Expr constructorExpr = constructor.toExpr();
+      size_t selectorIndex = Datatype::indexOf(selectorExpr);
+      size_t constructorIndex = Datatype::indexOf(constructorExpr);
+      const Datatype& dt = Datatype::datatypeOf(constructorExpr);
+      const Datatype::Constructor& c = dt[constructorIndex];
+      if(c.getNumArgs() > selectorIndex &&
+         c[selectorIndex].getSelector() == selectorExpr) {
+        Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial selector " << in
+                                   << std::endl;
+        return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
+      } else {
+        Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Would rewrite trivial selector " << in
+                                   << " but ctor doesn't match stor"
+                                   << std::endl;
+      }
+    }
+
+    if(in.getKind() == kind::EQUAL && in[0] == in[1]) {
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(true));
+    }
+    if(in.getKind() == kind::EQUAL &&
+       TheoryDatatypes::checkClashSimple(in[0], in[1])) {
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(false));
+    }
+
+    return RewriteResponse(REWRITE_DONE, in);
+  }
+
+  static RewriteResponse preRewrite(TNode in) {
+    Debug("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
+    return RewriteResponse(REWRITE_DONE, in);
+  }
+
+  static inline void init() {}
+  static inline void shutdown() {}
+
+};/* class DatatypesRewriter */
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */
+
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
new file mode 100644
index 000000000..8cac2da62
--- /dev/null
+++ b/src/theory/datatypes/kinds
@@ -0,0 +1,34 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
+
+properties check presolve
+
+rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"
+
+# constructor type has a list of selector types followed by a return type
+operator CONSTRUCTOR_TYPE 1: "constructor"
+
+# selector type has domain type and a range type
+operator SELECTOR_TYPE 2 "selector"
+
+# tester type has a constructor type
+operator TESTER_TYPE 1 "tester"
+
+parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application"
+
+parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
+
+parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
+
+constant DATATYPE_TYPE \
+    ::CVC4::Datatype \
+    "::CVC4::DatatypeHashStrategy" \
+    "util/datatype.h" \
+    "datatype type"
+
+endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
new file mode 100644
index 000000000..f55003178
--- /dev/null
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -0,0 +1,1260 @@
+/*********************                                                        */
+/*! \file theory_datatypes.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the theory of datatypes
+ **
+ ** Implementation of the theory of datatypes.
+ **/
+
+
+#include "theory/datatypes/theory_datatypes.h"
+#include "theory/valuation.h"
+#include "expr/kind.h"
+#include "util/datatype.h"
+#include "util/Assert.h"
+
+#include <map>
+
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::datatypes;
+
+int TheoryDatatypes::getConstructorIndex( TypeNode t, Node c ) {
+  map<TypeNode, vector<Node> >::iterator it = d_cons.find( t );
+  if( it != d_cons.end() ) {
+    for( int i = 0; i<(int)it->second.size(); i++ ) {
+      if( it->second[i] == c ) {
+        return i;
+      }
+    }
+  }
+  return -1;
+}
+
+int TheoryDatatypes::getTesterIndex( TypeNode t, Node c ) {
+  map<TypeNode, vector<Node> >::iterator it = d_testers.find( t );
+  if( it != d_testers.end() ) {
+    for( int i = 0; i<(int)it->second.size(); i++ ) {
+      if( it->second[i] == c ) {
+        return i;
+      }
+    }
+  }
+  return -1;
+}
+
+void TheoryDatatypes::checkFiniteWellFounded() {
+  if( requiresCheckFiniteWellFounded ) {
+    Debug("datatypes-finite") << "Check finite, well-founded." << endl;
+
+    //check well-founded and finite, create distinguished ground terms
+    map<TypeNode, vector<Node> >::iterator it;
+    vector<Node>::iterator itc;
+    for( it = d_cons.begin(); it != d_cons.end(); ++it ) {
+      d_distinguishTerms[it->first] = Node::null();
+      d_finite[it->first] = false;
+      d_wellFounded[it->first] = false;
+      for( itc = it->second.begin(); itc != it->second.end(); ++itc ) {
+        d_cons_finite[*itc] = false;
+        d_cons_wellFounded[*itc] = false;
+      }
+    }
+    bool changed;
+    do{
+      changed = false;
+      for( it = d_cons.begin(); it != d_cons.end(); ++it ) {
+        TypeNode t = it->first;
+        Debug("datatypes-finite") << "check " << t << endl;
+        bool typeFinite = true;
+        for( itc = it->second.begin(); itc != it->second.end(); ++itc ) {
+          Node cn = *itc;
+          TypeNode ct = cn.getType();
+          Debug("datatypes-finite") << " check cons " << ct << endl;
+          if( !d_cons_finite[cn] ) {
+            int c;
+            for( c=0; c<(int)ct.getNumChildren()-1; c++ ) {
+              Debug("datatypes-finite") << "  check sel " << c << " of " << ct << ": " << endl << ct[c] << endl;
+              TypeNode ts = ct[c];
+              Debug("datatypes") << "  check : " << ts << endl;
+              if( !isDatatype( ts ) || !d_finite[ ts ] ) {
+                break;
+              }
+            }
+            if( c == (int)ct.getNumChildren()-1 ) {
+              changed = true;
+              d_cons_finite[cn] = true;
+              Debug("datatypes-finite") << ct << " is finite" << endl;
+            } else {
+              typeFinite = false;
+            }
+          }
+          if( !d_cons_wellFounded[cn] ) {
+            int c;
+            for( c=0; c<(int)ct.getNumChildren()-1; c++ ) {
+              Debug("datatypes") << "  check sel " << c << " of " << ct << endl;
+              Debug("datatypes") << ct[c] << endl;
+              TypeNode ts = ct[c];
+              Debug("datatypes") << "  check : " << ts << endl;
+              if( isDatatype( ts ) && !d_wellFounded[ ts ] ) {
+                break;
+              }
+            }
+            if( c == (int)ct.getNumChildren()-1 ) {
+              changed = true;
+              d_cons_wellFounded[cn] = true;
+              Debug("datatypes-finite") << ct << " is well founded" << endl;
+            }
+          }
+          if( d_cons_wellFounded[cn] ) {
+            if( !d_wellFounded[t] ) {
+              changed = true;
+              d_wellFounded[t] = true;
+              // also set distinguished ground term
+              Debug("datatypes") << "set distinguished ground term out of " << ct << endl;
+              Debug("datatypes-finite") << t << " is type wf" << endl;
+              NodeManager* nm = NodeManager::currentNM();
+              vector< NodeTemplate<true> > children;
+              children.push_back( cn );
+              for( int c=0; c<(int)ct.getNumChildren()-1; c++ ) {
+                TypeNode ts = ct[c];
+                if( isDatatype( ts ) ) {
+                  children.push_back( d_distinguishTerms[ts] );
+                } else {
+                  nm->mkVar( ts );
+                }
+              }
+              Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children );
+              Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl;
+              d_distinguishTerms[t] = dgt;
+            }
+          }
+        }
+        if( typeFinite && !d_finite[t] ) {
+          changed = true;
+          d_finite[t] = true;
+          Debug("datatypes-finite") << t << " now type finite" << endl;
+        }
+      }
+    } while( changed );
+    map<TypeNode, bool >::iterator itb;
+    for( itb=d_finite.begin(); itb != d_finite.end(); ++itb ) {
+      Debug("datatypes-finite") << itb->first << " is ";
+      Debug("datatypes-finite") << ( itb->second ? "" : "not ") << "finite." << endl;
+    }
+    for( itb=d_wellFounded.begin(); itb != d_wellFounded.end(); ++itb ) {
+      Debug("datatypes-finite") << itb->first << " is ";
+      Debug("datatypes-finite") << ( itb->second ? "" : "not ") << "well founded." << endl;
+      if( !itb->second && isDatatype( itb->first ) ) {
+        //throw exception?
+      }
+    }
+    requiresCheckFiniteWellFounded = false;
+  }
+}
+
+TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_DATATYPES, c, out, valuation),
+  d_currAsserts(c),
+  d_currEqualities(c),
+  d_drv_map(c),
+  d_axioms(c),
+  d_selectors(c),
+  d_reps(c),
+  d_selector_eq(c),
+  d_equivalence_class(c),
+  d_inst_map(c),
+  d_labels(c),
+  d_ccChannel(this),
+  d_cc(c, &d_ccChannel),
+  d_unionFind(c),
+  d_disequalities(c),
+  d_equalities(c),
+  d_conflict(),
+  d_noMerge(false) {
+  requiresCheckFiniteWellFounded = true;
+}
+
+
+TheoryDatatypes::~TheoryDatatypes() {
+}
+
+
+void TheoryDatatypes::addDatatypeDefinitions(TypeNode dttn) {
+  AssertArgument(dttn.getKind() == DATATYPE_TYPE, dttn, "expected a datatype");
+
+  Debug("datatypes") << "TheoryDatatypes::addDataTypeDefinitions(): "
+                     << dttn.getConst<Datatype>().getName() << endl;
+  if(d_addedDatatypes.find(dttn) != d_addedDatatypes.end()) {
+    // already have incorporated this datatype definition
+    Debug("datatypes") << "+ can skip" << endl;
+    return;
+  }
+
+  const Datatype& dt = dttn.getConst<Datatype>();
+  Debug("datatypes") << dt << endl;
+  for(Datatype::const_iterator it = dt.begin(); it != dt.end(); ++it) {
+    Node constructor = Node::fromExpr((*it).getConstructor());
+    d_cons[dttn].push_back(constructor);
+    d_testers[dttn].push_back(Node::fromExpr((*it).getTester()));
+    for(Datatype::Constructor::const_iterator itc = (*it).begin(); itc != (*it).end(); ++itc) {
+      Node selector = Node::fromExpr((*itc).getSelector());
+      d_sels[constructor].push_back(selector);
+      d_sel_cons[selector] = constructor;
+    }
+  }
+  requiresCheckFiniteWellFounded = true;
+  d_addedDatatypes.insert(dttn);
+}
+
+
+void TheoryDatatypes::addSharedTerm(TNode t) {
+  Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
+                     << t << endl;
+}
+
+
+void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) {
+  Debug("datatypes") << "TheoryDatatypes::notifyEq(): "
+                     << lhs << " = " << rhs << endl;
+  //if(!d_conflict.isNull()) {
+  //  return;
+  //}
+  //merge(lhs,rhs);
+  //FIXME
+  //Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
+  //addEquality(eq);
+  //d_drv_map[eq] = d_cc.explain( lhs, rhs );
+}
+
+void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
+  Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): "
+                     << lhs << " = " << rhs << endl;
+  if(d_conflict.isNull()) {
+    merge(lhs,rhs);
+  }
+  Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl;
+}
+
+
+void TheoryDatatypes::presolve() {
+  Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
+  checkFiniteWellFounded();
+}
+
+void TheoryDatatypes::check(Effort e) {
+  for( int i=0; i<(int)d_currAsserts.size(); i++ ) {
+    Debug("datatypes") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl;
+  }
+  for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
+    Debug("datatypes") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
+  }
+  for( BoolMap::iterator i = d_inst_map.begin(); i != d_inst_map.end(); i++ ) {
+    Debug("datatypes") << "inst_map = " << (*i).first << endl;
+  }
+  for( EqListsN::iterator i = d_selector_eq.begin(); i != d_selector_eq.end(); i++ ) {
+    EqListN* m = (*i).second;
+    Debug("datatypes") << "selector_eq " << (*i).first << ":" << endl;
+    for( EqListN::const_iterator j = m->begin(); j != m->end(); j++ ) {
+      Debug("datatypes") << "  : " << (*j) << endl;
+    }
+  }
+  while(!done()) {
+    Node assertion = get();
+    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
+      cout << "*** TheoryDatatypes::check(): " << assertion << endl;
+    }
+    d_currAsserts.push_back( assertion );
+
+    //clear from the derived map
+    if( !d_drv_map[assertion].get().isNull() ) {
+      Debug("datatypes") << "Assertion has already been derived" << endl;
+      d_drv_map[assertion] = Node::null();
+    } else {
+      collectTerms( assertion );
+      switch(assertion.getKind()) {
+      case kind::EQUAL:
+      case kind::IFF:
+        addEquality(assertion);
+        break;
+      case kind::APPLY_TESTER:
+        checkTester( assertion );
+        break;
+      case kind::NOT:
+        {
+          switch( assertion[0].getKind()) {
+          case kind::EQUAL:
+          case kind::IFF:
+            {
+              Node a = assertion[0][0];
+              Node b = assertion[0][1];
+              addDisequality(assertion[0]);
+              Debug("datatypes") << "hello." << endl;
+              d_cc.addTerm(a);
+              d_cc.addTerm(b);
+              if(Debug.isOn("datatypes")) {
+                Debug("datatypes") << "       a  == > " << a << endl
+                            << "       b  == > " << b << endl
+                            << "  find(a) == > " << debugFind(a) << endl
+                            << "  find(b) == > " << debugFind(b) << endl;
+              }
+              // There are two ways to get a conflict here.
+              if(d_conflict.isNull()) {
+                if(find(a) == find(b)) {
+                  // We get a conflict this way if we WERE previously watching
+                  // a, b and were notified previously (via notifyCongruent())
+                  // that they were congruent.
+                  NodeBuilder<> nb(kind::AND);
+                  nb << d_cc.explain( assertion[0][0], assertion[0][1] );
+                  nb << assertion;
+                  d_conflict = nb;
+                  Debug("datatypes") << "Disequality conflict " << d_conflict << endl;
+                } else {
+
+                  // If we get this far, there should be nothing conflicting due
+                  // to this disequality.
+                  Assert(!d_cc.areCongruent(a, b));
+                }
+              }
+            }
+            break;
+          case kind::APPLY_TESTER:
+            checkTester( assertion );
+            break;
+          default:
+            Unhandled(assertion[0].getKind());
+            break;
+          }
+        }
+        break;
+      default:
+        Unhandled(assertion.getKind());
+        break;
+      }
+      if(!d_conflict.isNull()) {
+        throwConflict();
+        return;
+      }
+    }
+  }
+
+  if( e == FULL_EFFORT ) {
+    Debug("datatypes-split") << "Check for splits " << e << endl;
+    //do splitting
+    for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
+      Node sf = find( (*i).first );
+      if( sf == (*i).first || sf.getKind() != APPLY_CONSTRUCTOR ) {
+        Debug("datatypes-split") << "Check for splitting " << (*i).first << ", ";
+        EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second;
+        if( lbl->empty() ) {
+          Debug("datatypes-split") << "empty label" << endl;
+        } else {
+          Debug("datatypes-split") << "label size = " << lbl->size() << endl;
+        }
+        Node cons = getPossibleCons( (*i).first, false );
+        if( !cons.isNull() ) {
+          Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
+          TypeNode typ = (*i).first.getType();
+          int cIndex = getConstructorIndex( typ, cons );
+          Assert( cIndex != -1 );
+          Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], (*i).first );
+          NodeBuilder<> nb(kind::OR);
+          nb << test << test.notNode();
+          Node lemma = nb;
+          Debug("datatypes-split") << "Lemma is " << lemma << endl;
+          d_out->lemma( lemma );
+          return;
+        }
+      } else {
+        Debug("datatypes-split") << (*i).first << " is " << sf << endl;
+      }
+    }
+  }
+  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
+    cout << "TheoryDatatypes::check(): done" << endl;
+  }
+}
+
+void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) {
+  Debug("datatypes") << "Check tester " << assertion << endl;
+
+  Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion;
+
+  //add the term into congruence closure consideration
+  d_cc.addTerm( tassertion[0] );
+
+  Node assertionRep = assertion;
+  Node tassertionRep = tassertion;
+  Node tRep = tassertion[0];
+  //tRep = collapseSelector( tRep, Node::null(), true );
+  tRep = find( tRep );
+  Debug("datatypes") << "tRep is " << tRep << " " << tassertion[0] << endl;
+  //add label instead for the representative (if it is different)
+  if( tRep != tassertion[0] ) {
+    tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep );
+    assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep;
+    //add explanation
+    if( doAdd ) {
+      Node explanation = d_cc.explain( tRep, tassertion[0] );
+      NodeBuilder<> nb(kind::AND);
+      nb << explanation << assertion;
+      explanation = nb;
+      Debug("datatypes-drv") << "Check derived tester " << assertionRep << endl;
+      Debug("datatypes-drv") << "  Justification is " << explanation << endl;
+      d_drv_map[assertionRep] = explanation;
+    }
+  }
+
+  //if tRep is a constructor, it is trivial
+  if( tRep.getKind() == APPLY_CONSTRUCTOR ) {
+    if( checkTrivialTester( tassertionRep ) == (assertionRep.getKind() == NOT) ) {
+      d_conflict = doAdd ? assertionRep : NodeManager::currentNM()->mkConst(true);
+      Debug("datatypes") << "Trivial conflict " << assertionRep << endl;
+    }
+    return;
+  }
+
+  addTermToLabels( tRep );
+  EqLists::iterator lbl_i = d_labels.find(tRep);
+  //Debug("datatypes") << "Found " << (lbl_i == d_labels.end()) << endl;
+  Assert( lbl_i != d_labels.end() );
+
+  EqList* lbl = (*lbl_i).second;
+  //Debug("datatypes") << "Check lbl = " << lbl << ", size = " << lbl->size() << endl;
+
+  //check if empty label (no possible constructors for term)
+  bool add = true;
+  int notCount = 0;
+  if( !lbl->empty() ) {
+    for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+      Node leqn = (*i);
+      if( leqn.getKind() == kind::NOT ) {
+        if( leqn[0].getOperator() == tassertionRep.getOperator() ) {
+          if( assertionRep.getKind() == NOT ) {
+            add = false;
+          } else {
+            NodeBuilder<> nb(kind::AND);
+            nb << leqn;
+            if( doAdd ) nb << assertionRep;
+            d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
+            Debug("datatypes") << "Contradictory labels " << d_conflict << endl;
+            return;
+          }
+          break;
+        }
+        notCount++;
+      } else {
+        if( (leqn.getOperator() == tassertionRep.getOperator()) == (assertionRep.getKind() == NOT) ) {
+          NodeBuilder<> nb(kind::AND);
+          nb << leqn;
+          if( doAdd ) nb << assertionRep;
+          d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
+          Debug("datatypes") << "Contradictory labels(2) " << d_conflict << endl;
+          return;
+        }
+        add = false;
+        break;
+      }
+    }
+  }
+  if( add ) {
+    if( assertionRep.getKind() == NOT && notCount == (int)d_cons[ tRep.getType() ].size()-1 ) {
+      NodeBuilder<> nb(kind::AND);
+      if( !lbl->empty() ) {
+        for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+          nb << (*i);
+        }
+      }
+      if( doAdd ) nb << assertionRep;
+      d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
+      Debug("datatypes") << "Exhausted possibilities for labels " << d_conflict << endl;
+      return;
+    }
+    if( doAdd ) {
+      lbl->push_back( assertionRep );
+      Debug("datatypes") << "Add to labels " << lbl->size() << endl;
+    }
+  }
+  if( doAdd ) {
+    checkInstantiate( tRep );
+    if( !d_conflict.isNull() ) {
+      return;
+    }
+    //inspect selectors
+    updateSelectors( tRep );
+  }
+  return;
+}
+
+bool TheoryDatatypes::checkTrivialTester(Node assertion) {
+  AssertArgument(assertion.getKind() == APPLY_TESTER &&
+                 assertion[0].getKind() == APPLY_CONSTRUCTOR,
+                 assertion, "argument must be a tester-over-constructor");
+  TNode tester = assertion.getOperator();
+  TNode ctor = assertion[0].getOperator();
+  // if they have the same index (and the node has passed
+  // typechecking) then this is a trivial tester
+  return Datatype::indexOf(tester.toExpr()) == Datatype::indexOf(ctor.toExpr());
+}
+
+void TheoryDatatypes::checkInstantiate( Node t ) {
+  Debug("datatypes") << "TheoryDatatypes::checkInstantiate() " << t << endl;
+  Assert( t == find( t ) );
+
+  //if labels were created for t, and t has not been instantiated
+  if( t.getKind() != APPLY_CONSTRUCTOR ) {
+    //for each term in equivalance class
+    initializeEqClass( t );
+    EqListN* eqc = (*d_equivalence_class.find( t )).second;
+    for( EqListN::const_iterator iter = eqc->begin(); iter != eqc->end(); iter++ ) {
+      Node te = *iter;
+      Assert( find( te ) == t );
+      if( d_inst_map.find( te ) == d_inst_map.end() ) {
+        Node cons = getPossibleCons( te, true );
+        EqLists::iterator lbl_i = d_labels.find( t );
+        //there is one remaining constructor
+        if( !cons.isNull() && lbl_i != d_labels.end() ) {
+          EqList* lbl = (*lbl_i).second;
+          //only one constructor possible for term (label is singleton), apply instantiation rule
+          bool consFinite = d_cons_finite[cons];
+          //find if selectors have been applied to t
+          vector< Node > selectorVals;
+          selectorVals.push_back( cons );
+          NodeBuilder<> justifyEq(kind::AND);
+          bool foundSel = false;
+          for( int i=0; i<(int)d_sels[cons].size(); i++ ) {
+            Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], te );
+            Debug("datatypes") << "Selector[" << i << "] = " << s << endl;
+            if( d_selectors.find( s ) != d_selectors.end() ) {
+              Node sf = find( s );
+              if( sf != s && sf.getKind() != SKOLEM ) {
+                justifyEq << d_cc.explain( sf, s );
+              }
+              foundSel = true;
+              s = sf;
+            }
+            selectorVals.push_back( s );
+          }
+          if( consFinite || foundSel ) {
+            d_inst_map[ te ] = true;
+            //instantiate, add equality
+            Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+            if( find( val ) != find( te ) ) {
+              Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te );
+              Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl;
+              if( lbl->size() == 1 || (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
+                justifyEq << (*lbl)[ lbl->size()-1 ];
+              } else {
+                if( !lbl->empty() ) {
+                  for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+                    justifyEq << (*i);
+                  }
+                }
+              }
+              Node jeq;
+              if( justifyEq.getNumChildren() == 1 ) {
+                jeq = justifyEq.getChild( 0 );
+              } else {
+                jeq = justifyEq;
+              }
+              Debug("datatypes-split") << "Instantiate " << newEq << endl;
+              addDerivedEquality( newEq, jeq );
+              return;
+            }
+          } else {
+            Debug("datatypes") << "infinite constructor, no selectors " << cons << endl;
+          }
+        }
+      }
+    }
+  }
+}
+
+//checkInst = true is for checkInstantiate, checkInst = false is for splitting
+Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) {
+  Node tf = find( t );
+  EqLists::iterator lbl_i = d_labels.find( tf );
+  if( lbl_i != d_labels.end() ) {
+    EqList* lbl = (*lbl_i).second;
+    TypeNode typ = t.getType();
+
+    //if ended by one positive tester
+    if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
+      if( checkInst ) {
+        Assert( getTesterIndex( typ, (*lbl)[ lbl->size()-1 ].getOperator() ) != -1 );
+        return d_cons[typ][ getTesterIndex( typ, (*lbl)[ lbl->size()-1 ].getOperator() ) ];
+      }
+    //if (n-1) negative testers
+    } else if( !checkInst || (int)lbl->size() == (int)d_cons[ t.getType() ].size()-1 ) {
+      vector< bool > possibleCons;
+      possibleCons.resize( (int)d_cons[ t.getType() ].size(), true );
+      if( !lbl->empty() ) {
+        for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+          TNode leqn = (*i);
+          Assert( getTesterIndex( typ, leqn[0].getOperator() ) != -1 );
+          possibleCons[ getTesterIndex( typ, leqn[0].getOperator() ) ] = false;
+        }
+      }
+      Node cons = Node::null();
+      for( int i=0; i<(int)possibleCons.size(); i++ ) {
+        if( possibleCons[i] ) {
+          cons = d_cons[typ][ i ];
+          if( !checkInst ) {
+            //if there is a selector, split
+            for( int i=0; i<(int)d_sels[cons].size(); i++ ) {
+              Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], tf );
+              if( d_selectors.find( s ) != d_selectors.end() ) {
+                Debug("datatypes") << "  getPosCons: found selector " << s << endl;
+                return cons;
+              }
+            }
+          }
+        }
+      }
+      if( !checkInst ) {
+        for( int i=0; i<(int)possibleCons.size(); i++ ) {
+          if( possibleCons[i] && !d_cons_finite[ d_cons[typ][ i ] ] ) {
+            Debug("datatypes") << "Did not find selector for " << tf;
+            Debug("datatypes") << " and " << d_cons[typ][ i ] << " is not finite." << endl;
+            return Node::null();
+          }
+        }
+      } else {
+        Assert( !cons.isNull() );
+      }
+      return cons;
+    }
+  }
+  return Node::null();
+}
+
+Node TheoryDatatypes::getValue(TNode n) {
+  NodeManager* nodeManager = NodeManager::currentNM();
+
+  switch(n.getKind()) {
+
+  case kind::VARIABLE:
+    Unhandled(kind::VARIABLE);
+
+  case kind::EQUAL: // 2 args
+    return nodeManager->
+      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
+
+  default:
+    Unhandled(n.getKind());
+  }
+}
+
+void TheoryDatatypes::merge(TNode a, TNode b) {
+  if( d_noMerge ) {
+    Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl;
+    d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) );
+    return;
+  }
+  Assert(d_conflict.isNull());
+  Debug("datatypes") << "Merge "<< a << " " << b << endl;
+
+  // make "a" the one with shorter diseqList
+  EqLists::iterator deq_ia = d_disequalities.find(a);
+  EqLists::iterator deq_ib = d_disequalities.find(b);
+
+  if(deq_ia != d_disequalities.end()) {
+    if(deq_ib == d_disequalities.end() ||
+       (*deq_ia).second->size() > (*deq_ib).second->size()) {
+      TNode tmp = a;
+      a = b;
+      b = tmp;
+    }
+  }
+
+  a = find(a);
+  b = find(b);
+
+  //Debug("datatypes") << "After find: "<< a << " " << b << endl;
+
+  if( a == b) {
+    return;
+  }
+  //if b is a selector, swap a and b
+  if( b.getKind() == APPLY_SELECTOR && a.getKind() != APPLY_SELECTOR ) {
+    TNode tmp = a;
+    a = b;
+    b = tmp;
+  }
+  //make constructors the representatives
+  if( a.getKind() == APPLY_CONSTRUCTOR ) {
+    TNode tmp = a;
+    a = b;
+    b = tmp;
+  }
+  //make sure skolem variable is not representative
+  if( b.getKind() == SKOLEM ) {
+    TNode tmp = a;
+    a = b;
+    b = tmp;
+  }
+
+
+  NodeBuilder<> explanation(kind::AND);
+  if( checkClash( a, b, explanation ) ) {
+    explanation << d_cc.explain( a, b );
+    d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
+    Debug("datatypes") << "Clash " << a << " " << b << endl;
+    Debug("datatypes") << "Conflict is " << d_conflict << endl;
+    return;
+  }
+  Debug("datatypes-debug") << "Done clash" << endl;
+
+  Debug("datatypes") << "Set canon: "<< a << " " << b << endl;
+
+  // b becomes the canon of a
+  d_unionFind.setCanon(a, b);
+  d_reps[a] = false;
+  d_reps[b] = true;
+  //merge equivalence classes
+  initializeEqClass( a );
+  initializeEqClass( b );
+  EqListN* eqc_a = (*d_equivalence_class.find( a )).second;
+  EqListN* eqc_b = (*d_equivalence_class.find( b )).second;
+  for( EqListN::const_iterator i = eqc_a->begin(); i != eqc_a->end(); i++ ) {
+    eqc_b->push_back( *i );
+  }
+
+ //Debug("datatypes") << "After check 1" << endl;
+
+  deq_ia = d_disequalities.find(a);
+  map<TNode, TNode> alreadyDiseqs;
+  if(deq_ia != d_disequalities.end()) {
+    /*
+     * Collecting the disequalities of b, no need to check for conflicts
+     * since the representative of b does not change and we check all the things
+     * in a's class when we look at the diseq list of find(a)
+     */
+
+    EqLists::iterator deq_ib = d_disequalities.find(b);
+    if(deq_ib != d_disequalities.end()) {
+      EqList* deq = (*deq_ib).second;
+      for(EqList::const_iterator j = deq->begin(); j != deq->end(); j++) {
+        TNode deqn = *j;
+        TNode s = deqn[0];
+        TNode t = deqn[1];
+        TNode sp = find(s);
+        TNode tp = find(t);
+        Assert(sp == b || tp == b, "test1");
+        if(sp == b) {
+          alreadyDiseqs[tp] = deqn;
+        } else {
+          alreadyDiseqs[sp] = deqn;
+        }
+      }
+    }
+
+    /*
+     * Looking for conflicts in the a disequality list. Note
+     * that at this point a and b are already merged. Also has
+     * the side effect that it adds them to the list of b (which
+     * became the canonical representative)
+     */
+
+    EqList* deqa = (*deq_ia).second;
+    for(EqList::const_iterator i = deqa->begin(); i != deqa->end(); i++) {
+      TNode deqn = (*i);
+      Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
+      TNode s = deqn[0];
+      TNode t = deqn[1];
+
+      TNode sp = find(s);
+      TNode tp = find(t);
+      if(sp == tp) {
+        Debug("datatypes") << "Construct standard conflict " << deqn << " " << sp << endl;
+        Node explanation = d_cc.explain(deqn[0], deqn[1]);
+        d_conflict = NodeManager::currentNM()->mkNode( kind::AND, explanation, deqn.notNode() );
+        Debug("datatypes") << "Conflict is " << d_conflict << endl;
+        return;
+      }
+      Assert( sp == b || tp == b, "test2");
+
+      // make sure not to add duplicates
+
+      if(sp == b) {
+        if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
+          appendToDiseqList(b, deqn);
+          alreadyDiseqs[tp] = deqn;
+        }
+      } else {
+        if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
+          appendToDiseqList(b, deqn);
+          alreadyDiseqs[sp] = deqn;
+        }
+      }
+
+    }
+  }
+
+  //Debug("datatypes-debug") << "Done clash" << endl;
+  checkCycles();
+  if( !d_conflict.isNull() ) {
+    return;
+  }
+  Debug("datatypes-debug") << "Done cycles" << endl;
+
+  //merge selector lists
+  updateSelectors( a );
+  Debug("datatypes-debug") << "Done collapse" << endl;
+
+  //merge labels
+  EqLists::iterator lbl_i = d_labels.find( a );
+  if(lbl_i != d_labels.end()) {
+    EqList* lbl = (*lbl_i).second;
+    if( !lbl->empty() ) {
+      for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+        checkTester( *i );
+        if( !d_conflict.isNull() ) {
+          return;
+        }
+      }
+    }
+  }
+  Debug("datatypes-debug") << "Done merge labels" << endl;
+
+  //do unification
+  if( d_conflict.isNull() ) {
+    if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR &&
+        a.getOperator() == b.getOperator() ) {
+      Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl;
+      for( int i=0; i<(int)a.getNumChildren(); i++ ) {
+        if( find( a[i] ) != find( b[i] ) ) {
+          Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] );
+          Node jEq = d_cc.explain(a, b);
+          Debug("datatypes-drv") << "UEqual: " << newEq << ", justification: " << jEq << " from " << a << " " << b << endl;
+          Debug("datatypes-drv") << "UEqual find: " << find( a[i] ) << " " << find( b[i] ) << endl;
+          addDerivedEquality( newEq, jEq );
+        }
+      }
+    }
+  }
+
+  Debug("datatypes-debug") << "merge(): Done" << endl;
+}
+
+Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
+  if( t.getKind() == APPLY_SELECTOR ) {
+    //collapse constructor
+    TypeNode typ = t[0].getType();
+    Node sel = t.getOperator();
+    TypeNode selType = sel.getType();
+    Node cons = d_sel_cons[sel];
+    Node tmp = find( t[0] );
+    Node retNode = t;
+    if( tmp.getKind() == APPLY_CONSTRUCTOR ) {
+      if( tmp.getOperator() == cons ) {
+        int selIndex = -1;
+        for(int i=0; i<(int)d_sels[cons].size(); i++ ) {
+          if( d_sels[cons][i] == sel ) {
+            selIndex = i;
+            break;
+          }
+        }
+        Assert( selIndex != -1 );
+        Debug("datatypes") << "Applied selector " << t << " to correct constructor, index = " << selIndex << endl;
+        Debug("datatypes") << "Return " << tmp[selIndex] << endl;
+        retNode = tmp[selIndex];
+      } else {
+        Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl;
+        Debug("datatypes") << "Return distinguished term ";
+        Debug("datatypes") << d_distinguishTerms[ selType[1] ] << " of type " << selType[1] << endl;
+        retNode = d_distinguishTerms[ selType[1] ];
+      }
+      if( useContext ) {
+        Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
+        d_axioms[neq] = true;
+        Debug("datatypes-split") << "Collapse selector " << neq << endl;
+        addEquality( neq );
+      }
+    } else {
+      if( useContext ) {
+        int cIndex = getConstructorIndex( typ, cons );
+        Assert( cIndex != -1 );
+        //check labels
+        Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], tmp );
+        checkTester( tester, false );
+        if( !d_conflict.isNull() ) {
+          Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
+          retNode = d_distinguishTerms[ selType[1] ];
+
+          Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
+          NodeBuilder<> nb(kind::AND);
+          Node trueNode = NodeManager::currentNM()->mkConst(true);
+          if( d_conflict != trueNode ) {
+            nb << d_conflict;
+          }
+          d_conflict = Node::null();
+          tmp = find( tmp );
+          if( tmp != t[0] ) {
+            nb << d_cc.explain( tmp, t[0] );
+          }
+          Assert( nb.getNumChildren()>0 );
+          Node jEq = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
+          Debug("datatypes-drv") << "Collapse selector " << neq << endl;
+          addDerivedEquality( neq, jEq );
+        }
+      }
+    }
+    return retNode;
+  }
+  return t;
+}
+
+void TheoryDatatypes::updateSelectors( Node a ) {
+  EqListsN::iterator sel_a_i = d_selector_eq.find( a );
+  if( sel_a_i != d_selector_eq.end() ) {
+    EqListN* sel_a = (*sel_a_i).second;
+    Debug("datatypes") << a << " has " << sel_a->size() << " selectors" << endl;
+    if( !sel_a->empty() ) {
+      EqListN* sel_b = NULL;
+      for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) {
+        Node s = (*i);
+        Node b = find( a );
+        if( b != a ) {
+          EqListsN::iterator sel_b_i = d_selector_eq.find( b );
+          if( sel_b_i == d_selector_eq.end() ) {
+            sel_b = new(getContext()->getCMM()) EqListN(true, getContext(), false,
+                                                  ContextMemoryAllocator<Node>(getContext()->getCMM()));
+            d_selector_eq.insertDataFromContextMemory(b, sel_b);
+          } else {
+            sel_b = (*sel_b_i).second;
+          }
+          a = b;
+        }
+        Debug("datatypes") << "Merge selector " << s << " into " << b << endl;
+        Debug("datatypes") << "Find is " << find( s[0] ) << endl;
+        Assert( s.getKind() == APPLY_SELECTOR &&
+                find( s[0] ) == b );
+        if( b != s[0] ) {
+          Node t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), b );
+          //add to labels
+          addTermToLabels( t );
+          merge( s, t );
+          s = t;
+          d_selectors[s] = true;
+          d_cc.addTerm( s );
+        }
+        s = collapseSelector( s, true );
+        if( !d_conflict.isNull() ) {
+          return;
+        }
+        if( sel_b && s.getKind() == APPLY_SELECTOR ) {
+          sel_b->push_back( s );
+        }
+      }
+    }
+  } else {
+    Debug("datatypes") << a << " has no selectors" << endl;
+  }
+}
+
+void TheoryDatatypes::collectTerms( TNode t ) {
+  for( int i=0; i<(int)t.getNumChildren(); i++ ) {
+    collectTerms( t[i] );
+  }
+  if( t.getKind() == APPLY_SELECTOR ) {
+    if( d_selectors.find( t ) == d_selectors.end() ) {
+      Debug("datatypes-split") << "  Found selector " << t << endl;
+      d_selectors[ t ] = true;
+      d_cc.addTerm( t );
+      Node tmp = find( t[0] );
+      checkInstantiate( tmp );
+
+      Node s = t;
+      if( tmp != t[0] ) {
+        s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
+      }
+      Debug("datatypes-split") << "  Before collapse: " << s << endl;
+      s = collapseSelector( s, true );
+      Debug("datatypes-split") << "  After collapse: " << s << endl;
+      if( s.getKind() == APPLY_SELECTOR ) {
+        //add selector to selector eq list
+        Debug("datatypes") << "  Add selector to list " << tmp << " " << t << endl;
+        EqListsN::iterator sel_i = d_selector_eq.find( tmp );
+        EqListN* sel;
+        if( sel_i == d_selector_eq.end() ) {
+          sel = new(getContext()->getCMM()) EqListN(true, getContext(), false,
+                                            ContextMemoryAllocator<Node>(getContext()->getCMM()));
+          d_selector_eq.insertDataFromContextMemory(tmp, sel);
+        } else {
+          sel = (*sel_i).second;
+        }
+        sel->push_back( s );
+      } else {
+        Debug("datatypes") << "  collapsed selector to " << s << endl;
+      }
+    }
+  }
+  addTermToLabels( t );
+}
+
+void TheoryDatatypes::addTermToLabels( Node t ) {
+  if( t.getKind() == APPLY_SELECTOR ) {
+
+  }
+  if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) {
+    Node tmp = find( t );
+    if( tmp == t ) {
+      //add to labels
+      EqLists::iterator lbl_i = d_labels.find(t);
+      if(lbl_i == d_labels.end()) {
+        EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false,
+                                                ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+        d_labels.insertDataFromContextMemory(tmp, lbl);
+      }
+    }
+  }
+}
+
+void TheoryDatatypes::initializeEqClass( Node t ) {
+  EqListsN::iterator eqc_i = d_equivalence_class.find( t );
+  if( eqc_i == d_equivalence_class.end() ) {
+    EqListN* eqc = new(getContext()->getCMM()) EqListN(true, getContext(), false,
+                                          ContextMemoryAllocator<Node>(getContext()->getCMM()));
+    eqc->push_back( t );
+    d_equivalence_class.insertDataFromContextMemory(t, eqc);
+  }
+}
+
+void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) {
+  Debug("datatypes") << "appending " << eq << endl
+              << "  to diseq list of " << of << endl;
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
+  Assert(of == debugFind(of));
+  EqLists::iterator deq_i = d_disequalities.find(of);
+  EqList* deq;
+  if(deq_i == d_disequalities.end()) {
+    deq = new(getContext()->getCMM()) EqList(true, getContext(), false,
+                                             ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+    d_disequalities.insertDataFromContextMemory(of, deq);
+  } else {
+    deq = (*deq_i).second;
+  }
+  deq->push_back(eq);
+  //if(Debug.isOn("uf")) {
+  //  Debug("uf") << "  size is now " << deq->size() << endl;
+  //}
+}
+
+void TheoryDatatypes::appendToEqList(TNode of, TNode eq) {
+  Debug("datatypes") << "appending " << eq << endl
+              << "  to eq list of " << of << endl;
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
+  Assert(of == debugFind(of));
+  EqLists::iterator eq_i = d_equalities.find(of);
+  EqList* eql;
+  if(eq_i == d_equalities.end()) {
+    eql = new(getContext()->getCMM()) EqList(true, getContext(), false,
+                                             ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+    d_equalities.insertDataFromContextMemory(of, eql);
+  } else {
+    eql = (*eq_i).second;
+  }
+  eql->push_back(eq);
+  //if(Debug.isOn("uf")) {
+  //  Debug("uf") << "  size is now " << eql->size() << endl;
+  //}
+}
+
+void TheoryDatatypes::addDerivedEquality(TNode eq, TNode jeq) {
+  Debug("datatypes-drv") << "Justification for " << eq << "is: " << jeq << "." << endl;
+  d_drv_map[eq] = jeq;
+  addEquality( eq );
+}
+
+void TheoryDatatypes::addEquality(TNode eq) {
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
+  if( eq[0] != eq[1] ) {
+    Debug("datatypes") << "Add equality " << eq << "." << endl;
+    d_merge_pending.push_back( vector< pair< Node, Node > >() );
+    bool prevNoMerge = d_noMerge;
+    d_noMerge = true;
+    d_cc.addTerm(eq[0]);
+    d_cc.addTerm(eq[1]);
+    d_cc.addEquality(eq);
+    d_currEqualities.push_back(eq);
+    d_noMerge = prevNoMerge;
+    unsigned int mpi = d_merge_pending.size()-1;
+    vector< pair< Node, Node > > mp;
+    mp.insert( mp.begin(), d_merge_pending[mpi].begin(), d_merge_pending[mpi].end() );
+    d_merge_pending.pop_back();
+    if( d_conflict.isNull() ) {
+      merge(eq[0], eq[1]);
+    }
+    for( int i=0; i<(int)mp.size(); i++ ) {
+      if( d_conflict.isNull() ) {
+        merge( mp[i].first, mp[i].second );
+      }
+    }
+  }
+}
+
+void TheoryDatatypes::addDisequality(TNode eq) {
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
+
+  TNode a = eq[0];
+  TNode b = eq[1];
+
+  appendToDiseqList(find(a), eq);
+  appendToDiseqList(find(b), eq);
+}
+
+void TheoryDatatypes::registerEqualityForPropagation(TNode eq) {
+  // should NOT be in search at this point, this must be called during
+  // preregistration
+
+  // FIXME with lemmas on demand, this could miss future propagations,
+  // since we are not necessarily at context level 0, but are updating
+  // context-sensitive structures.
+
+  Assert(eq.getKind() == kind::EQUAL ||
+         eq.getKind() == kind::IFF);
+
+  TNode a = eq[0];
+  TNode b = eq[1];
+
+  appendToEqList(find(a), eq);
+  appendToEqList(find(b), eq);
+}
+
+void TheoryDatatypes::throwConflict() {
+  Debug("datatypes") << "Convert conflict : " << d_conflict << endl;
+  NodeBuilder<> nb(kind::AND);
+  convertDerived( d_conflict, nb );
+  if( nb.getNumChildren() == 1 ) {
+    d_conflict = nb.getChild( 0 );
+  } else {
+    d_conflict = nb;
+  }
+  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
+    cout << "Conflict constructed : " << d_conflict << endl;
+  }
+  if( d_conflict.getKind() != kind::AND ) {
+    NodeBuilder<> nb(kind::AND);
+    nb << d_conflict << d_conflict;
+    d_conflict = nb;
+  }
+  d_out->conflict( d_conflict, false );
+  d_conflict = Node::null();
+}
+
+void TheoryDatatypes::convertDerived(Node n, NodeBuilder<>& nb) {
+  if( n.getKind() == kind::AND ) {
+    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+      convertDerived( n[i], nb );
+    }
+  } else if( !d_drv_map[ n ].get().isNull() ) {
+    //Debug("datatypes") << "Justification for " << n << " is " << d_drv_map[ n ].get() << endl;
+    convertDerived( d_drv_map[ n ].get(), nb );
+  } else if( d_axioms.find( n ) == d_axioms.end() ) {
+    nb << n;
+  }
+}
+
+void TheoryDatatypes::checkCycles() {
+  for( BoolMap::iterator i = d_reps.begin(); i != d_reps.end(); i++ ) {
+    if( (*i).second ) {
+      map< Node, bool > visited;
+      NodeBuilder<> explanation(kind::AND);
+      if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) {
+        Assert( explanation.getNumChildren()>0 );
+        d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
+        Debug("datatypes") << "Detected cycle for " << (*i).first << endl;
+        Debug("datatypes") << "Conflict is " << d_conflict << endl;
+        return;
+      }
+    }
+  }
+}
+
+//postcondition: if cycle detected, explanation is why n is a subterm of on
+bool TheoryDatatypes::searchForCycle( Node n, Node on,
+                                      map< Node, bool >& visited,
+                                      NodeBuilder<>& explanation ) {
+  //Debug("datatypes") << "Search for cycle " << n << " " << on << endl;
+  if( n.getKind() == APPLY_CONSTRUCTOR ) {
+    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+      Node nn = find( n[i] );
+      if( visited.find( nn ) == visited.end() ) {
+        visited[nn] = true;
+        if( nn == on || searchForCycle( nn, on, visited, explanation ) ) {
+          if( nn != n[i] ) {
+            explanation << d_cc.explain( nn, n[i] );
+          }
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
+//should be called initially with explanation of why n1 and n2 are equal
+bool TheoryDatatypes::checkClash( Node n1, Node n2, NodeBuilder<>& explanation ) {
+  //Debug("datatypes") << "Check clash " << n1 << " " << n2 << endl;
+  Node n1f = find( n1 );
+  Node n2f = find( n2 );
+  bool retVal = false;
+  if( n1f != n2f ) {
+    if( n1f.getKind() == kind::APPLY_CONSTRUCTOR && n2f.getKind() == kind::APPLY_CONSTRUCTOR ) {
+      if( n1f.getOperator() != n2f.getOperator() ) {
+        retVal =true;
+      } else {
+        Assert( n1f.getNumChildren() == n2f.getNumChildren() );
+        for( int i=0; i<(int)n1f.getNumChildren(); i++ ) {
+          if( checkClash( n1f[i], n2f[i], explanation ) ) {
+            retVal = true;
+            break;
+          }
+        }
+      }
+    }
+    if( retVal ) {
+      if( n1f != n1 ) {
+        explanation << d_cc.explain( n1f, n1 );
+      }
+      if( n2f != n2 ) {
+        explanation << d_cc.explain( n2f, n2 );
+      }
+    }
+  }
+  return retVal;
+}
+
+bool TheoryDatatypes::checkClashSimple( Node n1, Node n2 ) {
+  if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
+    if( n1.getOperator() != n2.getOperator() ) {
+      return true;
+    } else {
+      Assert( n1.getNumChildren() == n2.getNumChildren() );
+      for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
+        if( checkClashSimple( n1[i], n2[i] ) ) {
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
new file mode 100644
index 000000000..e3f045e06
--- /dev/null
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -0,0 +1,218 @@
+/*********************                                                        */
+/*! \file theory_datatypes.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of datatypes.
+ **
+ ** Theory of datatypes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
+#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
+
+#include "theory/theory.h"
+#include "util/congruence_closure.h"
+#include "util/datatype.h"
+#include "theory/datatypes/union_find.h"
+#include "util/hash.h"
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+class TheoryDatatypes : public Theory {
+private:
+  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList;
+  typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists;
+  typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN;
+  typedef context::CDMap<Node, EqListN*, NodeHashFunction> EqListsN;
+  typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap;
+
+  std::hash_set<TypeNode, TypeNodeHashFunction> d_addedDatatypes;
+
+  context::CDList<Node> d_currAsserts;
+  context::CDList<Node> d_currEqualities;
+  /** a list of types with the list of constructors for that type */
+  std::map<TypeNode, std::vector<Node> > d_cons;
+  /** a list of types with the list of constructors for that type */
+  std::map<TypeNode, std::vector<Node> > d_testers;
+  /** a list of constructors with the list of selectors */
+  std::map<Node, std::vector<Node> > d_sels;
+  /** map from selectors to the constructors they are for */
+  std::map<Node, Node > d_sel_cons;
+  /**  the distinguished ground term for each type */
+  std::map<TypeNode, Node > d_distinguishTerms;
+  /** finite datatypes/constructor */
+  std::map< TypeNode, bool > d_finite;
+  std::map< Node, bool > d_cons_finite;
+  /** well founded datatypes/constructor */
+  std::map< TypeNode, bool > d_wellFounded;
+  std::map< Node, bool > d_cons_wellFounded;
+  /** whether we need to check finite and well foundedness */
+  bool requiresCheckFiniteWellFounded;
+  /** map from equalties and the equalities they are derived from */
+  context::CDMap< Node, Node, NodeHashFunction > d_drv_map;
+  /** equalities that are axioms */
+  BoolMap d_axioms;
+  /** list of all selectors */
+  BoolMap d_selectors;
+  /** list of all representatives */
+  BoolMap d_reps;
+  /** map from nodes to a list of selectors whose arguments are in the equivalence class of that node */
+  EqListsN d_selector_eq;
+  /** map from node representatives to list of nodes in their eq class */
+  EqListsN d_equivalence_class;
+  /** map from terms to whether they have been instantiated */
+  BoolMap d_inst_map;
+  //Type getType( TypeNode t );
+  int getConstructorIndex( TypeNode t, Node c );
+  int getTesterIndex( TypeNode t, Node c );
+  bool isDatatype( TypeNode t ) { return d_cons.find( t )!=d_cons.end(); }
+  void checkFiniteWellFounded();
+
+  /**
+   * map from terms to testers asserted for that term
+   * for each t, this is either a list of equations of the form
+   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers,
+   * or a list of equations of the form
+   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t )  followed by
+   *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
+   */
+  EqLists d_labels;
+
+  class CongruenceChannel {
+    TheoryDatatypes* d_datatypes;
+
+  public:
+    CongruenceChannel(TheoryDatatypes* datatypes) : d_datatypes(datatypes) {}
+    void notifyCongruent(TNode a, TNode b) {
+      d_datatypes->notifyCongruent(a, b);
+    }
+  };/* class CongruenceChannel */
+  friend class CongruenceChannel;
+
+  /**
+   * Output channel connected to the congruence closure module.
+   */
+  CongruenceChannel d_ccChannel;
+
+  /**
+   * Instance of the congruence closure module.
+   */
+  CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cc;
+
+  /**
+   * Union find for storing the equalities.
+   */
+  UnionFind<Node, NodeHashFunction> d_unionFind;
+
+  /**
+   * Received a notification from the congruence closure algorithm that the two nodes
+   * a and b have been merged.
+   */
+  void notifyCongruent(TNode a, TNode b);
+
+  /**
+   * List of all disequalities this theory has seen.
+   * Maintaints the invariant that if a is in the
+   * disequality list of b, then b is in that of a.
+   * */
+  EqLists d_disequalities;
+
+  /** List of all (potential) equalities to be propagated. */
+  EqLists d_equalities;
+
+  /**
+   * stores the conflicting disequality (still need to call construct
+   * conflict to get the actual explanation)
+   */
+  Node d_conflict;
+  bool d_noMerge;
+  std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending;
+public:
+  TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation);
+  ~TheoryDatatypes();
+  void preRegisterTerm(TNode n) {
+    TypeNode type = n.getType();
+    if(type.getKind() == kind::DATATYPE_TYPE) {
+      addDatatypeDefinitions(type);
+    }
+  }
+  void registerTerm(TNode n) { }
+
+  void presolve();
+
+  void addSharedTerm(TNode t);
+  void notifyEq(TNode lhs, TNode rhs);
+  void check(Effort e);
+  void propagate(Effort e) { }
+  void explain(TNode n, Effort e) { }
+  Node getValue(TNode n);
+  void shutdown() { }
+  std::string identify() const { return std::string("TheoryDatatypes"); }
+
+  void addDatatypeDefinitions(TypeNode dttn);
+
+private:
+  /* Helper methods */
+  void checkTester( Node assertion, bool doAdd = true );
+  static bool checkTrivialTester(Node assertion);
+  void checkInstantiate( Node t );
+  Node getPossibleCons( Node t, bool checkInst = false );
+  Node collapseSelector( TNode t, bool useContext = false );
+  void updateSelectors( Node a );
+  void collectTerms( TNode t );
+  void addTermToLabels( Node t );
+  void initializeEqClass( Node t );
+
+  /* from uf_morgan */
+  void merge(TNode a, TNode b);
+  inline TNode find(TNode a);
+  inline TNode debugFind(TNode a) const;
+  void appendToDiseqList(TNode of, TNode eq);
+  void appendToEqList(TNode of, TNode eq);
+  void addDisequality(TNode eq);
+  void addDerivedEquality(TNode eq, TNode jeq);
+  void addEquality(TNode eq);
+  void registerEqualityForPropagation(TNode eq);
+  void convertDerived(Node n, NodeBuilder<>& nb);
+  void throwConflict();
+
+  void checkCycles();
+  bool searchForCycle( Node n, Node on,
+                       std::map< Node, bool >& visited,
+                       NodeBuilder<>& explanation );
+  bool checkClash( Node n1, Node n2, NodeBuilder<>& explanation );
+  static bool checkClashSimple( Node n1, Node n2 );
+  friend class DatatypesRewriter;// for access to checkClashSimple();
+};/* class TheoryDatatypes */
+
+inline TNode TheoryDatatypes::find(TNode a) {
+  return d_unionFind.find(a);
+}
+
+inline TNode TheoryDatatypes::debugFind(TNode a) const {
+  return d_unionFind.debugFind(a);
+}
+
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
new file mode 100644
index 000000000..1fd24cf53
--- /dev/null
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file theory_datatypes_type_rules.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of datatypes
+ **
+ ** Theory of datatypes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+struct DatatypeConstructorTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+    TypeNode consType = n.getOperator().getType(check);
+    if(check) {
+      Debug("typecheck-idt") << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl;
+      Debug("typecheck-idt") << "cons type: " << consType << " " << consType.getNumChildren() << std::endl;
+      if(n.getNumChildren() != consType.getNumChildren() - 1) {
+        throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the constructor type");
+      }
+      TNode::iterator child_it = n.begin();
+      TNode::iterator child_it_end = n.end();
+      TypeNode::iterator tchild_it = consType.begin();
+      for(; child_it != child_it_end; ++child_it, ++tchild_it) {
+        TypeNode childType = (*child_it).getType(check);
+        Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl;
+        if(childType != *tchild_it) {
+          throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument");
+        }
+      }
+    }
+    return consType.getConstructorReturnType();
+  }
+};/* struct DatatypeConstructorTypeRule */
+
+struct DatatypeSelectorTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::APPLY_SELECTOR);
+    TypeNode selType = n.getOperator().getType(check);
+    Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
+    Debug("typecheck-idt") << "sel type: " << selType << std::endl;
+    if(check) {
+      if(n.getNumChildren() != 1) {
+        throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the selector type");
+      }
+      TypeNode childType = n[0].getType(check);
+      if(selType[0] != childType) {
+        throw TypeCheckingExceptionPrivate(n, "bad type for selector argument");
+      }
+    }
+    return selType[1];
+  }
+};/* struct DatatypeSelectorTypeRule */
+
+struct DatatypeTesterTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::APPLY_TESTER);
+    if(check) {
+      if(n.getNumChildren() != 1) {
+        throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the tester type");
+      }
+      TypeNode testType = n.getOperator().getType(check);
+      TypeNode childType = n[0].getType(check);
+      Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
+      Debug("typecheck-idt") << "test type: " << testType << std::endl;
+      if(testType[0] != childType) {
+        throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct DatatypeSelectorTypeRule */
+
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */
diff --git a/src/theory/datatypes/union_find.cpp b/src/theory/datatypes/union_find.cpp
new file mode 100644
index 000000000..e56c9f282
--- /dev/null
+++ b/src/theory/datatypes/union_find.cpp
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file union_find.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Path-compressing, backtrackable union-find using an undo
+ ** stack. Refactored from the UF union-find.
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include <iostream>
+
+#include "theory/datatypes/union_find.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+template <class NodeType, class NodeHash>
+void UnionFind<NodeType, NodeHash>::notify() {
+  Trace("datatypesuf") << "datatypesUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
+  while(d_offset < d_trace.size()) {
+    pair<TNode, TNode> p = d_trace.back();
+    if(p.second.isNull()) {
+      d_map.erase(p.first);
+      Trace("datatypesuf") << "datatypesUF   " << d_trace.size() << " erasing " << p.first << endl;
+    } else {
+      d_map[p.first] = p.second;
+      Trace("datatypesuf") << "datatypesUF   " << d_trace.size() << " replacing " << p << endl;
+    }
+    d_trace.pop_back();
+  }
+  Trace("datatypesuf") << "datatypesUF cancelling finished." << endl;
+}
+
+// The following declarations allow us to put functions in the .cpp file
+// instead of the header, since we know which instantiations are needed.
+
+template void UnionFind<Node, NodeHashFunction>::notify();
+
+template void UnionFind<TNode, TNodeHashFunction>::notify();
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/datatypes/union_find.h b/src/theory/datatypes/union_find.h
new file mode 100644
index 000000000..31b18e7e9
--- /dev/null
+++ b/src/theory/datatypes/union_find.h
@@ -0,0 +1,148 @@
+/*********************                                                        */
+/*! \file union_find.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Path-compressing, backtrackable union-find using an undo
+ ** stack. Refactored from the UF union-find.
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__UNION_FIND_H
+#define __CVC4__THEORY__DATATYPES__UNION_FIND_H
+
+#include <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+
+namespace context {
+  class Context;
+}/* CVC4::context namespace */
+
+namespace theory {
+namespace datatypes {
+
+// NodeType \in { Node, TNode }
+template <class NodeType, class NodeHash>
+class UnionFind : context::ContextNotifyObj {
+  /** Our underlying map type. */
+  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+
+  /**
+   * Our map of Nodes to their canonical representatives.
+   * If a Node is not present in the map, it is its own
+   * representative.
+   */
+  MapType d_map;
+
+  /** Our undo stack for changes made to d_map. */
+  std::vector<std::pair<TNode, TNode> > d_trace;
+
+  /** Our current offset in the d_trace stack (context-dependent). */
+  context::CDO<size_t> d_offset;
+
+public:
+  UnionFind(context::Context* ctxt) :
+    context::ContextNotifyObj(ctxt),
+    d_offset(ctxt, 0) {
+  }
+
+  ~UnionFind() throw() { }
+
+  /**
+   * Return a Node's union-find representative, doing path compression.
+   */
+  inline TNode find(TNode n);
+
+  /**
+   * Return a Node's union-find representative, NOT doing path compression.
+   * This is useful for Assert() statements, debug checking, and similar
+   * things that you do NOT want to mutate the structure.
+   */
+  inline TNode debugFind(TNode n) const;
+
+  /**
+   * Set the canonical representative of n to newParent.  They should BOTH
+   * be their own canonical representatives on entry to this funciton.
+   */
+  inline void setCanon(TNode n, TNode newParent);
+
+
+public:
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::notify().
+   */
+  void notify();
+
+};/* class UnionFind<> */
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
+  typename MapType::const_iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    return n;
+  } else {
+    return debugFind((*i).second);
+  }
+}
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
+  Trace("datatypesuf") << "datatypesUF find of " << n << std::endl;
+  typename MapType::iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    Trace("datatypesuf") << "datatypesUF   it is rep" << std::endl;
+    return n;
+  } else {
+    Trace("datatypesuf") << "datatypesUF   not rep: par is " << (*i).second << std::endl;
+    std::pair<TNode, TNode> pr = *i;
+    // our iterator is invalidated by the recursive call to find(),
+    // since it mutates the map
+    TNode p = find(pr.second);
+    if(p == pr.second) {
+      return p;
+    }
+    d_trace.push_back(std::make_pair(n, pr.second));
+    d_offset = d_trace.size();
+    Trace("datatypesuf") << "datatypesUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
+    pr.second = p;
+    d_map.insert(pr);
+    return p;
+  }
+}
+
+template <class NodeType, class NodeHash>
+inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
+  Assert(d_map.find(n) == d_map.end());
+  Assert(d_map.find(newParent) == d_map.end());
+  if(n != newParent) {
+    Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
+    d_map[n] = newParent;
+    d_trace.push_back(std::make_pair(n, TNode::null()));
+    d_offset = d_trace.size();
+  }
+}
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__DATATYPES__UNION_FIND_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cb29bb98e..d37916515 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_engine.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: barrett
- ** Minor contributors (to current version): cconway, taking
+ ** Major contributors: taking, barrett, dejan
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -166,6 +166,11 @@ struct preprocess_stack_element {
 };
 
 Node TheoryEngine::preprocess(TNode node) {
+  // Make sure the node is type-checked first (some rewrites depend on
+  // typechecking having succeeded to be safe).
+  if(Options::current()->typeChecking) {
+    node.getType(true);
+  }
   // Remove ITEs and rewrite the node
   Node preprocessed = Rewriter::rewrite(removeITEs(node));
   return preprocessed;
@@ -300,7 +305,7 @@ Node TheoryEngine::removeITEs(TNode node) {
 
       Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])"
                    << "->"
-                   << "["<<newAssertion.getId() << "," << newAssertion << "]"
+                   << "[" << newAssertion.getId() << "," << newAssertion << "]"
                    << endl;
 
       Node preprocessed = preprocess(newAssertion);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1cdae3810..6226406d7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -265,7 +265,7 @@ public:
     // Get the atom
     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 
-    // Again, eqaulity is a special case
+    // Again, equality is a special case
     if (atom.getKind() == kind::EQUAL) {
       theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]);
       Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl;
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 5bb2e830f..ec942e00b 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): acsys
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -200,6 +200,29 @@ public:
   }
 };/* class IllegalArgumentException */
 
+class CVC4_PUBLIC InternalErrorException : public AssertionException {
+protected:
+  InternalErrorException() : AssertionException() {}
+
+public:
+  InternalErrorException(const char* function, const char* file, unsigned line) :
+    AssertionException() {
+    construct("Internal error detected", "",
+              function, file, line);
+  }
+
+  InternalErrorException(const char* function, const char* file, unsigned line,
+                         const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Internal error detected", "",
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+};/* class InternalErrorException */
+
 #ifdef CVC4_DEBUG
 
 #ifdef CVC4_DEBUG
@@ -249,6 +272,8 @@ void debugAssertionFailed(const AssertionException& thisException,
   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unimplemented(msg...) \
   throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define InternalError(msg...) \
+  throw InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 24d82f01c..eb63885a2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -37,6 +37,8 @@ libutil_la_SOURCES = \
 	configuration_private.h \
 	configuration.cpp \
 	bitvector.h \
+	datatype.h \
+	datatype.cpp \
 	gmp_util.h \
 	sexpr.h \
 	stats.h \
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index ca69fb506..ade08164b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -2,10 +2,10 @@
 /*! \file bitvector.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: cconway
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters, cconway
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -28,7 +28,7 @@
 
 namespace CVC4 {
 
-class BitVector {
+class CVC4_PUBLIC BitVector {
 
 private:
 
@@ -157,24 +157,24 @@ inline BitVector::BitVector(const std::string& num, unsigned base) {
   }
 
   d_value = Integer(num,base);
-}
+}/* BitVector::BitVector() */
 
 
 /**
  * Hash function for the BitVector constants.
  */
-struct BitVectorHashStrategy {
+struct CVC4_PUBLIC BitVectorHashStrategy {
   static inline size_t hash(const BitVector& bv) {
     return bv.hash();
   }
-};
+};/* struct BitVectorHashStrategy */
 
 /**
  * The structure representing the extraction operation for bit-vectors. The
  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
  * by taking the bits at indices <code>high ... low</code>
  */
-struct BitVectorExtract  {
+struct CVC4_PUBLIC BitVectorExtract {
   /** The high bit of the range for this extract */
   unsigned high;
   /** The low bit of the range for this extract */
@@ -186,73 +186,75 @@ struct BitVectorExtract  {
   bool operator == (const BitVectorExtract& extract) const {
     return high == extract.high && low == extract.low;
   }
-};
+};/* struct BitVectorExtract */
 
 /**
  * Hash function for the BitVectorExtract objects.
  */
-class BitVectorExtractHashStrategy {
+class CVC4_PUBLIC BitVectorExtractHashStrategy {
 public:
   static size_t hash(const BitVectorExtract& extract) {
     size_t hash = extract.low;
     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     return hash;
   }
-};
+};/* class BitVectorExtractHashStrategy */
 
-struct BitVectorSize {
+struct CVC4_PUBLIC BitVectorSize {
   unsigned size;
   BitVectorSize(unsigned size)
   : size(size) {}
   operator unsigned () const { return size; }
-};
+};/* struct BitVectorSize */
 
-struct BitVectorRepeat {
+struct CVC4_PUBLIC BitVectorRepeat {
   unsigned repeatAmount;
   BitVectorRepeat(unsigned repeatAmount)
   : repeatAmount(repeatAmount) {}
   operator unsigned () const { return repeatAmount; }
-};
+};/* struct BitVectorRepeat */
 
-struct BitVectorZeroExtend {
+struct CVC4_PUBLIC BitVectorZeroExtend {
   unsigned zeroExtendAmount;
   BitVectorZeroExtend(unsigned zeroExtendAmount)
   : zeroExtendAmount(zeroExtendAmount) {}
   operator unsigned () const { return zeroExtendAmount; }
-};
+};/* struct BitVectorZeroExtend */
 
-struct BitVectorSignExtend {
+struct CVC4_PUBLIC BitVectorSignExtend {
   unsigned signExtendAmount;
   BitVectorSignExtend(unsigned signExtendAmount)
   : signExtendAmount(signExtendAmount) {}
   operator unsigned () const { return signExtendAmount; }
-};
+};/* struct BitVectorSignExtend */
 
-struct BitVectorRotateLeft {
+struct CVC4_PUBLIC BitVectorRotateLeft {
   unsigned rotateLeftAmount;
   BitVectorRotateLeft(unsigned rotateLeftAmount)
   : rotateLeftAmount(rotateLeftAmount) {}
   operator unsigned () const { return rotateLeftAmount; }
-};
+};/* struct BitVectorRotateLeft */
 
-struct BitVectorRotateRight {
+struct CVC4_PUBLIC BitVectorRotateRight {
   unsigned rotateRightAmount;
   BitVectorRotateRight(unsigned rotateRightAmount)
   : rotateRightAmount(rotateRightAmount) {}
   operator unsigned () const { return rotateRightAmount; }
-};
+};/* struct BitVectorRotateRight */
 
 template <typename T>
-struct UnsignedHashStrategy {
+struct CVC4_PUBLIC UnsignedHashStrategy {
   static inline size_t hash(const T& x) {
     return (size_t)x;
   }
-};
+};/* struct UnsignedHashStrategy */
 
+inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
   return os << bv.toString();
 }
 
+inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
   return os << "[" << bv.high << ":" << bv.low << "]";
 }
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
new file mode 100644
index 000000000..c795eaba6
--- /dev/null
+++ b/src/util/datatype.cpp
@@ -0,0 +1,371 @@
+/*********************                                                        */
+/*! \file datatype.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a Datatype definition
+ **
+ ** A class representing a Datatype definition for the theory of
+ ** inductive datatypes.
+ **/
+
+#include <string>
+#include <sstream>
+
+#include "util/datatype.h"
+#include "expr/type.h"
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+namespace expr {
+  namespace attr {
+    struct DatatypeIndexTag {};
+  }
+}
+
+typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
+
+const Datatype& Datatype::datatypeOf(Expr item) {
+  TypeNode t = Node::fromExpr(item).getType();
+  switch(t.getKind()) {
+  case kind::CONSTRUCTOR_TYPE:
+    return t[t.getNumChildren() - 1].getConst<Datatype>();
+  case kind::SELECTOR_TYPE:
+  case kind::TESTER_TYPE:
+    return t[0].getConst<Datatype>();
+  default:
+    Unhandled("arg must be a datatype constructor, selector, or tester");
+  }
+}
+
+size_t Datatype::indexOf(Expr item) {
+  AssertArgument(item.getType().isConstructor() ||
+                 item.getType().isTester() ||
+                 item.getType().isSelector(),
+                 item,
+                 "arg must be a datatype constructor, selector, or tester");
+  TNode n = Node::fromExpr(item);
+  Assert(n.hasAttribute(DatatypeIndexAttr()));
+  return n.getAttribute(DatatypeIndexAttr());
+}
+
+void Datatype::resolve(ExprManager* em,
+                       const std::map<std::string, DatatypeType>& resolutions)
+  throw(AssertionException, DatatypeResolutionException) {
+
+  CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
+  CheckArgument(!d_resolved, "cannot resolve a Datatype twice");
+  CheckArgument(resolutions.find(d_name) != resolutions.end(), "Datatype::resolve(): resolutions doesn't contain me!");
+  DatatypeType self = (*resolutions.find(d_name)).second;
+  CheckArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
+  d_resolved = true;
+  size_t index = 0;
+  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    (*i).resolve(em, self, resolutions);
+    Assert((*i).isResolved());
+    Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
+    Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
+  }
+  Assert(index == getNumConstructors());
+}
+
+void Datatype::addConstructor(const Constructor& c) {
+  CheckArgument(!d_resolved, this,
+                "cannot add a constructor to a finalized Datatype");
+  d_constructors.push_back(c);
+}
+
+bool Datatype::operator==(const Datatype& other) const throw() {
+  // two datatypes are == iff the name is the same and they have
+  // exactly matching constructors (in the same order)
+
+  if(this == &other) {
+    return true;
+  }
+
+  if(isResolved() != other.isResolved()) {
+    return false;
+  }
+
+  if(d_name != other.d_name ||
+     getNumConstructors() != other.getNumConstructors()) {
+    return false;
+  }
+  for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
+    Assert(j != other.end());
+    // two constructors are == iff they have the same name, their
+    // constructors and testers are equal and they have exactly
+    // matching args (in the same order)
+    if((*i).getName() != (*j).getName() ||
+       (*i).getNumArgs() != (*j).getNumArgs()) {
+      return false;
+    }
+    // testing equivalence of constructors and testers is harder b/c
+    // this constructor might not be resolved yet; only compare them
+    // if they are both resolved
+    Assert(isResolved() == !(*i).d_constructor.isNull() &&
+           isResolved() == !(*i).d_tester.isNull() &&
+           (*i).d_constructor.isNull() == (*j).d_constructor.isNull() &&
+           (*i).d_tester.isNull() == (*j).d_tester.isNull());
+    if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
+      return false;
+    }
+    if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
+      return false;
+    }
+    for(Constructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
+      Assert(l != (*j).end());
+      if((*k).getName() != (*l).getName()) {
+        return false;
+      }
+      // testing equivalence of selectors is harder b/c args might not
+      // be resolved yet
+      Assert(isResolved() == (*k).isResolved() &&
+             (*k).isResolved() == (*l).isResolved());
+      if((*k).isResolved()) {
+        // both are resolved, so simply compare the selectors directly
+        if((*k).d_selector != (*l).d_selector) {
+          return false;
+        }
+      } else {
+        // neither is resolved, so compare their (possibly unresolved)
+        // types; we don't know if they'll be resolved the same way,
+        // so we can't ever say unresolved types are equal
+        if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) {
+          if((*k).d_selector.getType() != (*l).d_selector.getType()) {
+            return false;
+          }
+        } else {
+          if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) {
+            // Fine, the selectors are equal if the rest of the
+            // enclosing datatypes are equal...
+          } else {
+            return false;
+          }
+        }
+      }
+    }
+  }
+  return true;
+}
+
+const Datatype::Constructor& Datatype::operator[](size_t index) const {
+  CheckArgument(index < getNumConstructors(), index, "index out of bounds");
+  return d_constructors[index];
+}
+
+void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
+                                    const std::map<std::string, DatatypeType>& resolutions)
+  throw(AssertionException, DatatypeResolutionException) {
+  CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
+  CheckArgument(!isResolved(),
+                "cannot resolve a Datatype constructor twice; "
+                "perhaps the same constructor was added twice, "
+                "or to two datatypes?");
+  size_t index = 0;
+  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    if((*i).d_selector.isNull()) {
+      string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
+      (*i).d_name.resize((*i).d_name.find('\0'));
+      if(typeName == "") {
+        (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, self));
+      } else {
+        map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
+        if(j == resolutions.end()) {
+          stringstream msg;
+          msg << "cannot resolve type \"" << typeName << "\" "
+              << "in selector \"" << (*i).d_name << "\" "
+              << "of constructor \"" << d_name << "\"";
+          throw DatatypeResolutionException(msg.str());
+        } else {
+          (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*j).second));
+        }
+      }
+    } else {
+      (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*i).d_selector.getType()));
+    }
+    Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
+    (*i).d_resolved = true;
+  }
+
+  Assert(index == getNumArgs());
+
+  // Set constructor/tester last, since Constructor::isResolved()
+  // returns true when d_tester is not the null Expr.  If something
+  // fails above, we want Constuctor::isResolved() to remain "false"
+  d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self));
+  d_name.resize(d_name.find('\0'));
+  d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self));
+}
+
+Datatype::Constructor::Constructor(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
+  // resolution.
+  d_name(name + '\0' + tester),
+  d_tester(),
+  d_args() {
+  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+}
+
+void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) {
+  // We don't want to introduce a new data member, because eventually
+  // we're going to be a constant stuffed inside a node.  So we stow
+  // the selector type away inside a var until resolution (when we can
+  // create the proper selector type)
+  CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+  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));
+}
+
+void Datatype::Constructor::addArg(std::string selectorName, Datatype::UnresolvedType 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()));
+}
+
+void Datatype::Constructor::addArg(std::string selectorName, Datatype::SelfType) {
+  // 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()));
+}
+
+std::string Datatype::Constructor::getName() const throw() {
+  string name = d_name;
+  if(!isResolved()) {
+    name.resize(name.find('\0'));
+  }
+  return name;
+}
+
+Expr Datatype::Constructor::getConstructor() const {
+  CheckArgument(isResolved(), this, "this datatype constructor not yet resolved");
+  return d_constructor;
+}
+
+Expr Datatype::Constructor::getTester() const {
+  CheckArgument(isResolved(), this, "this datatype constructor not yet resolved");
+  return d_tester;
+}
+
+const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const {
+  CheckArgument(index < getNumArgs(), index, "index out of bounds");
+  return d_args[index];
+}
+
+Datatype::Constructor::Arg::Arg(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() {
+  string name = d_name;
+  const size_t nul = name.find('\0');
+  if(nul != string::npos) {
+    name.resize(nul);
+  }
+  return name;
+}
+
+Expr Datatype::Constructor::Arg::getSelector() const {
+  CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
+  return d_selector;
+}
+
+bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() {
+  return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
+}
+
+std::string Datatype::Constructor::Arg::getSelectorTypeName() const {
+  Type t;
+  if(isResolved()) {
+    t = SelectorType(d_selector.getType()).getRangeType();
+  } else {
+    if(d_selector.isNull()) {
+      string typeName = d_name.substr(d_name.find('\0') + 1);
+      return (typeName == "") ? "[self]" : typeName;
+    } else {
+      t = d_selector.getType();
+    }
+  }
+
+  return t.isDatatype() ? DatatypeType(t).getDatatype().getName() : t.toString();
+}
+
+std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
+  // can only output datatypes in the CVC4 native language
+  Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+
+  os << "DATATYPE " << dt.getName() << " =" << endl;
+  Datatype::const_iterator i = dt.begin(), i_end = dt.end();
+  if(i != i_end) {
+    os << "  ";
+    do {
+      os << *i << endl;
+      if(++i != i_end) {
+        os << "| ";
+      }
+    } while(i != i_end);
+  }
+  os << "END;" << endl;
+
+  return os;
+}
+
+std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& 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();
+  if(i != i_end) {
+    os << "(";
+    do {
+      os << *i;
+      if(++i != i_end) {
+        os << ", ";
+      }
+    } while(i != i_end);
+    os << ")";
+  }
+
+  return os;
+}
+
+std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) {
+  // can only output datatypes in the CVC4 native language
+  Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+
+  os << arg.getName() << ": " << arg.getSelectorTypeName();
+
+  return os;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/datatype.h b/src/util/datatype.h
new file mode 100644
index 000000000..e3e7d669c
--- /dev/null
+++ b/src/util/datatype.h
@@ -0,0 +1,445 @@
+/*********************                                                        */
+/*! \file datatype.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a Datatype definition
+ **
+ ** A class representing a Datatype definition for the theory of
+ ** inductive datatypes.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__DATATYPE_H
+#define __CVC4__DATATYPE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+
+namespace CVC4 {
+  // messy; Expr needs Datatype (because it's the payload of a
+  // CONSTANT-kinded expression), and Datatype needs Expr.
+  class CVC4_PUBLIC Datatype;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "util/Assert.h"
+#include "util/output.h"
+#include "util/hash.h"
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC ExprManager;
+
+/**
+ * An exception that is thrown when a datatype resolution fails.
+ */
+class CVC4_PUBLIC DatatypeResolutionException : public Exception {
+public:
+  inline DatatypeResolutionException(std::string msg);
+};/* class DatatypeResolutionException */
+
+/**
+ * The representation of an inductive datatype.
+ *
+ * This is far more complicated than it first seems.  Consider this
+ * datatype definition:
+ *
+ *   DATATYPE nat =
+ *     succ(pred: nat)
+ *   | zero
+ *   END;
+ *
+ * You cannot define "nat" until you have a Type for it, but you
+ * cannot have a Type for it until you fill in the type of the "pred"
+ * selector, which needs the Type.  So we have a chicken-and-egg
+ * problem.  It's even more complicated when we have mutual recusion
+ * between datatypes, since the CVC presentation language does not
+ * require forward-declarations.  Here, we define trees of lists that
+ * contain trees of lists (etc):
+ *
+ *   DATATYPE
+ *     tree = node(left: tree, right: tree) | leaf(list),
+ *     list = cons(car: tree, cdr: list) | nil
+ *   END;
+ *
+ * Note that while parsing the "tree" definition, we have to take it
+ * on faith that "list" is a valid type.  We build Datatype objects to
+ * describe "tree" and "list", and their constructors and constructor
+ * arguments, but leave any unknown types (including self-references)
+ * in an "unresolved" state.  After parsing the whole DATATYPE block,
+ * we create a DatatypeType through
+ * ExprManager::mkMutualDatatypeTypes().  The ExprManager creates a
+ * DatatypeType for each, but before "releasing" this type into the
+ * wild, it does a round of in-place "resolution" on each Datatype by
+ * calling Datatype::resolve() with a map of string -> DatatypeType to
+ * allow the datatype to construct the necessary testers and
+ * selectors.
+ *
+ * An additional point to make is that we want to ease the burden on
+ * both the parser AND the users of the CVC4 API, so this class takes
+ * on the task of generating its own selectors and testers, for
+ * instance.  That means that, after reifying the Datatype with the
+ * ExprManager, the parser needs to go through the (now-resolved)
+ * Datatype and request ; 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:
+  static const Datatype& datatypeOf(Expr item);
+  static size_t indexOf(Expr item);
+
+  /**
+   * 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;
+      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 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)
+      throw(AssertionException, DatatypeResolutionException);
+    friend class Datatype;
+
+  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();
+
+    /**
+     * 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 */
+
+  /** The type for iterators over constructors. */
+  typedef std::vector<Constructor>::iterator iterator;
+  /** The (const) type for iterators over constructors. */
+  typedef std::vector<Constructor>::const_iterator const_iterator;
+
+private:
+  std::string d_name;
+  std::vector<Constructor> d_constructors;
+  bool d_resolved;
+
+  /**
+   * Datatypes refer to themselves, recursively, and we have a
+   * chicken-and-egg problem.  The DatatypeType around the Datatype
+   * cannot exist until the Datatype is finalized, and the Datatype
+   * cannot refer to the DatatypeType representing itself until it
+   * exists.  resolve() is called by the ExprManager when a Type.  Has
+   * the effect of freezing the object, too; that is, addConstructor()
+   * will fail after a call to resolve().
+   */
+  void resolve(ExprManager* em,
+               const std::map<std::string, DatatypeType>& resolutions)
+    throw(AssertionException, DatatypeResolutionException);
+  friend class ExprManager;// for access to resolve()
+
+public:
+
+  /** Create a new Datatype of the given name. */
+  inline explicit Datatype(std::string name);
+
+  /** Add a constructor to this Datatype. */
+  void addConstructor(const Constructor& c);
+
+  /** Get the name of this Datatype. */
+  inline std::string getName() const throw();
+  /** Get the number of constructors (so far) for this Datatype. */
+  inline size_t getNumConstructors() const throw();
+
+  /**
+   * Return true iff the two Datatypes are the same.
+   *
+   * We need == for mkConst(Datatype) to properly work---since if the
+   * Datatype Expr requested is the same as an already-existing one,
+   * we need to return that one.  For that, we have a hash and
+   * operator==.  We provide != for symmetry.  We don't provide
+   * operator<() etc. because given two Datatype Exprs, you could
+   * simply compare those rather than the (bare) Datatypes.  This
+   * means, though, that Datatype cannot be stored in a sorted list or
+   * RB tree directly, so maybe we can consider adding these
+   * comparison operators later on.
+   */
+  bool operator==(const Datatype& other) const throw();
+  /** Return true iff the two Datatypes are not the same. */
+  inline bool operator!=(const Datatype& other) const throw();
+
+  /** Return true iff this Datatype has already been resolved. */
+  inline bool isResolved() const throw();
+
+  /** Get the beginning iterator over Constructors. */
+  inline iterator begin() throw();
+  /** Get the ending iterator over Constructors. */
+  inline iterator end() throw();
+  /** Get the beginning const_iterator over Constructors. */
+  inline const_iterator begin() const throw();
+  /** Get the ending const_iterator over Constructors. */
+  inline const_iterator end() const throw();
+
+  /** Get the ith Constructor. */
+  const Constructor& operator[](size_t index) const;
+
+};/* class Datatype */
+
+
+/**
+ * A hash strategy for Datatypes.  Needed because Datatypes are used
+ * as the constant payload in CONSTANT-kinded TypeNodes (for
+ * DATATYPE_TYPE expressions).
+ */
+struct CVC4_PUBLIC DatatypeHashStrategy {
+  static inline size_t hash(const Datatype& dt) {
+    return StringHashFunction()(dt.getName());
+  }
+};/* struct DatatypeHashStrategy */
+
+
+// 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;
+
+// INLINE FUNCTIONS
+
+inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) :
+  Exception(msg) {
+}
+
+inline Datatype::UnresolvedType::UnresolvedType(std::string name) :
+  d_name(name) {
+}
+
+inline std::string Datatype::UnresolvedType::getName() const throw() {
+  return d_name;
+}
+
+inline Datatype::Datatype(std::string name) :
+  d_name(name),
+  d_constructors(),
+  d_resolved(false) {
+}
+
+inline std::string Datatype::getName() const throw() {
+  return d_name;
+}
+
+inline size_t Datatype::getNumConstructors() const throw() {
+  return d_constructors.size();
+}
+
+inline bool Datatype::operator!=(const Datatype& other) const throw() {
+  return !(*this == other);
+}
+
+inline bool Datatype::isResolved() const throw() {
+  return d_resolved;
+}
+
+inline Datatype::iterator Datatype::begin() throw() {
+  return d_constructors.begin();
+}
+
+inline Datatype::iterator Datatype::end() throw() {
+  return d_constructors.end();
+}
+
+inline Datatype::const_iterator Datatype::begin() const throw() {
+  return d_constructors.begin();
+}
+
+inline Datatype::const_iterator Datatype::end() const throw() {
+  return d_constructors.end();
+}
+
+inline bool Datatype::Constructor::isResolved() const throw() {
+  return !d_tester.isNull();
+}
+
+inline size_t Datatype::Constructor::getNumArgs() const throw() {
+  return d_args.size();
+}
+
+inline bool Datatype::Constructor::Arg::isResolved() const throw() {
+  // We could just write:
+  //
+  //   return !d_selector.isNull() && d_selector.getType().isSelector();
+  //
+  // HOWEVER, this causes problems in ExprManager tear-down, because
+  // the attributes are removed before the pool is purged.  When the
+  // pool is purged, this triggers an equality test between Datatypes,
+  // and this triggers a call to isResolved(), which breaks because
+  // d_selector has no type after attributes are stripped.
+  //
+  // This problem, coupled with the fact that this function is called
+  // _often_, means we should just use a boolean flag.
+  //
+  return d_resolved;
+}
+
+inline Datatype::Constructor::iterator Datatype::Constructor::begin() throw() {
+  return d_args.begin();
+}
+
+inline Datatype::Constructor::iterator Datatype::Constructor::end() throw() {
+  return d_args.end();
+}
+
+inline Datatype::Constructor::const_iterator Datatype::Constructor::begin() const throw() {
+  return d_args.begin();
+}
+
+inline Datatype::Constructor::const_iterator Datatype::Constructor::end() const throw() {
+  return d_args.end();
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DATATYPE_H */