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.

13 files changed, 1971 insertions, 9 deletions

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;