Merge from "cc" branch:

CongruenceClosure implementation; CongruenceClosure white-box test.

New UF theory implementation based on new CC module.  This one
supports predicates.  The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").

Added type infrastructure for TUPLE.

Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).

Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)

Other minor changes.

13 files changed, 895 insertions, 228 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index dfa94a66d..d3b9d12fb 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -127,3 +127,4 @@ constant TYPE_CONSTANT \
     "expr/type_constant.h" \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
+operator TUPLE_TYPE 2: "tuple type"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 354bf02bd..42c9902e5 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -44,7 +44,7 @@ class EqualityTypeRule {
         std::stringstream ss;
         ss << "Types do not match in equation ";
         ss << "[" << lhsType << "<>" << rhsType << "]";
-        
+
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
@@ -54,7 +54,8 @@ class EqualityTypeRule {
     }
     return booleanType;
   }
-};
+};/* class EqualityTypeRule */
+
 
 class DistinctTypeRule {
 public:
@@ -71,7 +72,22 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class DistinctTypeRule */
+
+
+class TupleTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    std::vector<TypeNode> types;
+    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+        child_it != child_it_end;
+        ++child_it) {
+      types.push_back((*child_it).getType(check));
+    }
+    return nodeManager->mkTupleType(types);
+  }
+};/* class TupleTypeRule */
+
 
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 54204ae3f..cc0e663fa 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -30,10 +30,13 @@
 #include "theory/builtin/theory_builtin.h"
 #include "theory/booleans/theory_bool.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/uf/morgan/theory_uf_morgan.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
 
+#include "util/options.h"
 #include "util/stats.h"
 
 namespace CVC4 {
@@ -134,6 +137,12 @@ class TheoryEngine {
   theory::bv::TheoryBV* d_bv;
 
   /**
+   * Debugging flag to ensure that shutdown() is called before the
+   * destructor.
+   */
+  bool d_hasShutDown;
+
+  /**
    * Check whether a node is in the pre-rewrite cache or not.
    */
   static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
@@ -193,16 +202,26 @@ public:
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(context::Context* ctxt) :
+  TheoryEngine(context::Context* ctxt, const Options* opts) :
     d_propEngine(NULL),
     d_theoryOut(this, ctxt),
+    d_hasShutDown(false),
     d_statistics() {
 
     d_sharedTermManager = new SharedTermManager(this, ctxt);
 
     d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
     d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
-    d_uf = new theory::uf::TheoryUF(2, ctxt, d_theoryOut);
+    switch(opts->uf_implementation) {
+    case Options::TIM:
+      d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
+      break;
+    case Options::MORGAN:
+      d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
+      break;
+    default:
+      Unhandled(opts->uf_implementation);
+    }
     d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
     d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
     d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
@@ -222,12 +241,24 @@ public:
     d_theoryOfTable.registerTheory(d_bv);
   }
 
+  ~TheoryEngine() {
+    Assert(d_hasShutDown);
+
+    delete d_bv;
+    delete d_arrays;
+    delete d_arith;
+    delete d_uf;
+    delete d_bool;
+    delete d_builtin;
+
+    delete d_sharedTermManager;
+  }
+
   SharedTermManager* getSharedTermManager() {
     return d_sharedTermManager;
   }
 
-  void setPropEngine(prop::PropEngine* propEngine)
-  {
+  void setPropEngine(prop::PropEngine* propEngine) {
     Assert(d_propEngine == NULL);
     d_propEngine = propEngine;
   }
@@ -238,21 +269,17 @@ public:
    * ordering issues between PropEngine and Theory.
    */
   void shutdown() {
+    // Set this first; if a Theory shutdown() throws an exception,
+    // at least the destruction of the TheoryEngine won't confound
+    // matters.
+    d_hasShutDown = true;
+
     d_builtin->shutdown();
     d_bool->shutdown();
     d_uf->shutdown();
     d_arith->shutdown();
     d_arrays->shutdown();
     d_bv->shutdown();
-
-    delete d_bv;
-    delete d_arrays;
-    delete d_arith;
-    delete d_uf;
-    delete d_bool;
-    delete d_builtin;
-
-    delete d_sharedTermManager;
   }
 
   /**
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 4e399aeb7..85b41bdbe 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -6,10 +6,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libuf.la
 
 libuf_la_SOURCES = \
-	ecdata.h \
-	ecdata.cpp \
 	theory_uf.h \
-	theory_uf.cpp \
 	theory_uf_type_rules.h 
 
+libuf_la_LIBADD = \
+	@builddir@/tim/libuftim.la \
+	@builddir@/morgan/libufmorgan.la
+
+SUBDIRS = tim morgan
+
 EXTRA_DIST = kinds
diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am
new file mode 100644
index 000000000..e9faa88df
--- /dev/null
+++ b/src/theory/uf/morgan/Makefile.am
@@ -0,0 +1,12 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libufmorgan.la
+
+libufmorgan_la_SOURCES = \
+	theory_uf_morgan.h \
+	theory_uf_morgan.cpp
+
+EXTRA_DIST =
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
new file mode 100644
index 000000000..a480a4d21
--- /dev/null
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -0,0 +1,348 @@
+/*********************                                                        */
+/*! \file theory_uf_morgan.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** 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)
+ ** 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 uninterpreted functions.
+ **
+ ** Implementation of the theory of uninterpreted functions.
+ **/
+
+#include "theory/uf/morgan/theory_uf_morgan.h"
+#include "expr/kind.h"
+#include "util/congruence_closure.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::morgan;
+
+TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
+  TheoryUF(id, ctxt, out),
+  d_assertions(ctxt),
+  d_ccChannel(this),
+  d_cc(ctxt, &d_ccChannel),
+  d_unionFind(ctxt),
+  d_disequalities(ctxt),
+  d_disequality(ctxt),
+  d_conflict(),
+  d_trueNode(),
+  d_falseNode() {
+  TypeNode boolType = NodeManager::currentNM()->booleanType();
+  d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType);
+  d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType);
+  d_cc.addTerm(d_trueNode);
+  d_cc.addTerm(d_falseNode);
+}
+
+TheoryUFMorgan::~TheoryUFMorgan() {
+}
+
+RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
+  if(topLevel) {
+    Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+    Node ret(n);
+    if(n.getKind() == EQUAL) {
+      if(n[0] == n[1]) {
+        ret = NodeManager::currentNM()->mkConst(true);
+      }
+    }
+    Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+    return RewriteComplete(ret);
+  } else {
+    return RewriteComplete(n);
+  }
+}
+
+void TheoryUFMorgan::preRegisterTerm(TNode n) {
+  Debug("uf") << "uf: preRegisterTerm(" << n << ")" << std::endl;
+}
+
+void TheoryUFMorgan::registerTerm(TNode n) {
+  Debug("uf") << "uf: registerTerm(" << n << ")" << std::endl;
+}
+
+Node TheoryUFMorgan::constructConflict(TNode diseq) {
+  Debug("uf") << "uf: begin constructConflict()" << std::endl;
+  Debug("uf") << "uf:   using diseq == " << diseq << std::endl;
+
+  Node explanation = d_cc.explain(diseq[0], diseq[1]);
+
+  NodeBuilder<> nb(kind::AND);
+  if(explanation.getKind() == kind::AND) {
+    for(Node::iterator i = explanation.begin();
+        i != explanation.end();
+        ++i) {
+      nb << *i;
+    }
+  } else {
+    Assert(explanation.getKind() == kind::EQUAL);
+    nb << explanation;
+  }
+  nb << diseq.notNode();
+
+  // by construction this should be true
+  Assert(nb.getNumChildren() > 1);
+
+  Node conflict = nb;
+  Debug("uf") << "conflict constructed : " << conflict << std::endl;
+
+  Debug("uf") << "uf: ending constructConflict()" << std::endl;
+
+  return conflict;
+}
+
+TNode TheoryUFMorgan::find(TNode a) {
+  UnionFind::iterator i = d_unionFind.find(a);
+  if(i == d_unionFind.end()) {
+    return a;
+  } else {
+    return d_unionFind[a] = find((*i).second);
+  }
+}
+
+// no path compression
+TNode TheoryUFMorgan::debugFind(TNode a) const {
+  UnionFind::iterator i = d_unionFind.find(a);
+  if(i == d_unionFind.end()) {
+    return a;
+  } else {
+    return debugFind((*i).second);
+  }
+}
+
+void TheoryUFMorgan::unionClasses(TNode a, TNode b) {
+  if(a == b) {
+    return;
+  }
+  Assert(d_unionFind.find(a) == d_unionFind.end());
+  Assert(d_unionFind.find(b) == d_unionFind.end());
+  d_unionFind[a] = b;
+}
+
+void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
+  Debug("uf") << "uf: notified of merge " << a << std::endl
+              << "                  and " << b << std::endl;
+  if(!d_conflict.isNull()) {
+    // if already a conflict, we don't care
+    return;
+  }
+
+  // make "a" the one with shorter diseqList
+  DiseqLists::iterator deq_ia = d_disequalities.find(a);
+  DiseqLists::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;
+      Debug("uf") << "    swapping to make a shorter diseqList" << std::endl;
+    }
+  }
+  a = find(a);
+  b = find(b);
+  Debug("uf") << "uf: uf reps are " << a << std::endl
+              << "            and " << b << std::endl;
+  unionClasses(a, b);
+
+  DiseqLists::iterator deq_i = d_disequalities.find(a);
+  if(deq_i != d_disequalities.end()) {
+    // a set of other trees we are already disequal to
+    // (for the optimization below)
+    std::set<TNode> alreadyDiseqs;
+    DiseqLists::iterator deq_ib = d_disequalities.find(b);
+    if(deq_ib != d_disequalities.end()) {
+      DiseqList* deq = (*deq_i).second;
+      for(DiseqList::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);
+        if(sp == b) {
+          alreadyDiseqs.insert(tp);
+        } else {
+          alreadyDiseqs.insert(sp);
+        }
+      }
+    }
+
+    DiseqList* deq = (*deq_i).second;
+    Debug("uf") << "a == " << a << std::endl;
+    Debug("uf") << "size of deq(a) is " << deq->size() << std::endl;
+    for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
+      Debug("uf") << "  deq(a) ==> " << *j << std::endl;
+      TNode deqn = *j;
+      Assert(deqn.getKind() == kind::EQUAL);
+      TNode s = deqn[0];
+      TNode t = deqn[1];
+      Debug("uf") << "       s  ==> " << s << std::endl
+                  << "       t  ==> " << t << std::endl
+                  << "  find(s) ==> " << debugFind(s) << std::endl
+                  << "  find(t) ==> " << debugFind(t) << std::endl;
+      TNode sp = find(s);
+      TNode tp = find(t);
+      if(sp == tp) {
+        d_conflict = deqn;
+        return;
+      }
+      Assert(sp == b || tp == b);
+      // optimization: don't put redundant diseq's in the list
+      if(sp == b) {
+        if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
+          appendToDiseqList(b, deqn);
+          alreadyDiseqs.insert(tp);
+        }
+      } else {
+        if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
+          appendToDiseqList(b, deqn);
+          alreadyDiseqs.insert(sp);
+        }
+      }
+    }
+    Debug("uf") << "end" << std::endl;
+  }
+}
+
+void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
+  Debug("uf") << "appending " << eq << std::endl
+              << "  to diseq list of " << of << std::endl;
+  Assert(eq.getKind() == kind::EQUAL);
+  Assert(of == debugFind(of));
+  DiseqLists::iterator deq_i = d_disequalities.find(of);
+  DiseqList* deq;
+  if(deq_i == d_disequalities.end()) {
+    deq = new(getContext()->getCMM()) DiseqList(true, getContext());
+    d_disequalities.insertDataFromContextMemory(of, deq);
+  } else {
+    deq = (*deq_i).second;
+  }
+  deq->push_back(eq);
+  Debug("uf") << "  size is now " << deq->size() << std::endl;
+}
+
+void TheoryUFMorgan::addDisequality(TNode eq) {
+  Assert(eq.getKind() == kind::EQUAL);
+
+  Node a = eq[0];
+  Node b = eq[1];
+
+  appendToDiseqList(find(a), eq);
+  appendToDiseqList(find(b), eq);
+}
+
+void TheoryUFMorgan::check(Effort level) {
+  Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
+
+  while(!done()) {
+    Node assertion = get();
+
+    Debug("uf") << "uf check(): " << assertion << std::endl;
+
+    switch(assertion.getKind()) {
+    case EQUAL:
+      d_cc.addEquality(assertion);
+      if(!d_conflict.isNull()) {
+        Node conflict = constructConflict(d_conflict);
+        d_conflict = Node::null();
+        d_out->conflict(conflict, false);
+        return;
+      }
+      break;
+    case APPLY_UF:
+      { // predicate
+        Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode);
+        d_cc.addTerm(assertion);
+        d_cc.addEquality(eq);
+        Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+        Assert(find(d_trueNode) != find(d_falseNode));
+      }
+      break;
+    case NOT:
+      if(assertion[0].getKind() == kind::EQUAL) {
+        Node a = assertion[0][0];
+        Node b = assertion[0][1];
+
+        addDisequality(assertion[0]);
+        d_disequality.push_back(assertion[0]);
+
+        d_cc.addTerm(a);
+        d_cc.addTerm(b);
+
+        Debug("uf") << "       a  ==> " << a << std::endl
+                    << "       b  ==> " << b << std::endl
+                    << "  find(a) ==> " << debugFind(a) << std::endl
+                    << "  find(b) ==> " << debugFind(b) << std::endl;
+
+        // There are two ways to get a conflict here.
+        if(!d_conflict.isNull()) {
+          // We get a conflict this way if we weren't watching a, b
+          // before and we were just now notified (via
+          // notifyCongruent()) when we called addTerm() above that
+          // they are congruent.  We make this a separate case (even
+          // though the check in the "else if.." below would also
+          // catch it, so that we can clear out d_conflict.
+          Node conflict = constructConflict(d_conflict);
+          d_conflict = Node::null();
+          d_out->conflict(conflict, false);
+          return;
+        } else 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.
+          Node conflict = constructConflict(assertion[0]);
+          d_out->conflict(conflict, false);
+          return;
+        }
+
+        // If we get this far, there should be nothing conflicting due
+        // to this disequality.
+        Assert(!d_cc.areCongruent(a, b));
+      } else {
+        Assert(assertion[0].getKind() == kind::APPLY_UF);
+        Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion[0], d_falseNode);
+        d_cc.addTerm(assertion[0]);
+        d_cc.addEquality(eq);
+        Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+        Assert(find(d_trueNode) != find(d_falseNode));
+      }
+      break;
+    default:
+      Unhandled(assertion.getKind());
+    }
+  }
+  Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl;
+
+  for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
+      diseqIter != d_disequality.end();
+      ++diseqIter) {
+
+    TNode left  = (*diseqIter)[0];
+    TNode right = (*diseqIter)[1];
+    Debug("uf") << "testing left: " << left << std::endl
+                << "       right: " << right << std::endl
+                << "     find(L): " << debugFind(left) << std::endl
+                << "     find(R): " << debugFind(right) << std::endl
+                << "     areCong: " << d_cc.areCongruent(left, right) << std::endl;
+    Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right));
+  }
+
+  Debug("uf") << "uf: end check(" << level << ")" << std::endl;
+}
+
+void TheoryUFMorgan::propagate(Effort level) {
+  Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl;
+  Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
+}
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
new file mode 100644
index 000000000..1a1ade250
--- /dev/null
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -0,0 +1,186 @@
+/*********************                                                        */
+/*! \file theory_uf_morgan.h
+ ** \verbatim
+ ** Original author: taking
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.
+ **
+ ** This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.  It is based on the Nelson-Oppen algorithm given in
+ ** "Fast Decision Procedures Based on Congruence Closure"
+ **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
+ ** This has been extended to work in a context-dependent way.
+ ** This interacts heavily with the data-structures given in ecdata.h .
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H
+#define __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "util/congruence_closure.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace morgan {
+
+class TheoryUFMorgan : public TheoryUF {
+
+private:
+
+  class CongruenceChannel {
+    TheoryUFMorgan* d_uf;
+
+  public:
+    CongruenceChannel(TheoryUFMorgan* uf) : d_uf(uf) {}
+    void notifyCongruent(TNode a, TNode b) {
+      d_uf->notifyCongruent(a, b);
+    }
+  };/* class CongruenceChannel */
+  friend class CongruenceChannel;
+
+  /**
+   * List of all of the non-negated literals from the assertion queue.
+   * This is used only for conflict generation.
+   * This differs from pending as the program generates new equalities that
+   * are not in this list.
+   * This will probably be phased out in future version.
+   */
+  context::CDList<Node> d_assertions;
+
+  /**
+   * Our channel connected to the congruence closure module.
+   */
+  CongruenceChannel d_ccChannel;
+
+  /**
+   * Instance of the congruence closure module.
+   */
+  CongruenceClosure<CongruenceChannel> d_cc;
+
+  typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind;
+  UnionFind d_unionFind;
+
+  typedef context::CDList<Node> DiseqList;
+  typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
+
+  /** List of all disequalities this theory has seen. */
+  DiseqLists d_disequalities;
+
+  context::CDList<Node> d_disequality;
+
+  Node d_conflict;
+
+  Node d_trueNode, d_falseNode;
+
+public:
+
+  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+  TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out);
+
+  /** Destructor for the TheoryUF object. */
+  ~TheoryUFMorgan();
+
+  /**
+   * Registers a previously unseen [in this context] node n.
+   * For TheoryUF, this sets up and maintains invaraints about
+   * equivalence class data-structures.
+   *
+   * Overloads a void registerTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void registerTerm(TNode n);
+
+  /**
+   * Currently this does nothing.
+   *
+   * Overloads a void preRegisterTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void preRegisterTerm(TNode n);
+
+  /**
+   * Checks whether the set of literals provided to the theory is consistent.
+   *
+   * If this is called at any effort level, it computes the congruence closure
+   * of all of the positive literals in the context.
+   *
+   * If this is called at full effort it checks if any of the negative literals
+   * are inconsistent with the congruence closure.
+   *
+   * Overloads  void check(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void check(Effort level);
+
+  /**
+   * Rewrites a node in the theory of uninterpreted functions.
+   * This is fairly basic and only ensures that atoms that are
+   * unsatisfiable or a valid are rewritten to false or true respectively.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel);
+
+  /**
+   * Propagates theory literals.
+   *
+   * Overloads void propagate(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void propagate(Effort level);
+
+  /**
+   * Explains a previously reported conflict. Currently does nothing.
+   *
+   * Overloads void explain(TNode n, Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void explain(TNode n, Effort level) {}
+
+  std::string identify() const { return std::string("TheoryUFMorgan"); }
+
+private:
+
+  /** Constructs a conflict from an inconsistent disequality. */
+  Node constructConflict(TNode diseq);
+
+  TNode find(TNode a);
+  TNode debugFind(TNode a) const;
+  void unionClasses(TNode a, TNode b);
+
+  void appendToDiseqList(TNode of, TNode eq);
+  void addDisequality(TNode eq);
+
+  /**
+   * Receives a notification from the congruence closure module that
+   * two nodes have been merged into the same congruence class.
+   */
+  void notifyCongruent(TNode a, TNode b);
+
+};/* class TheoryUFMorgan */
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f0be0668a..f745cf402 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file theory_uf.h
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: mdeters
+ ** 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)
@@ -11,16 +11,10 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.
- **
- ** This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.  It is based on the Nelson-Oppen algorithm given in
- ** "Fast Decision Procedures Based on Congruence Closure"
- **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
- ** This has been extended to work in a context-dependent way.
- ** This interacts heavily with the data-structures given in ecdata.h .
+ ** \brief This is the interface to TheoryUF implementations
  **
+ ** This is the interface to TheoryUF implementations.  All
+ ** implementations of TheoryUF should inherit from this class.
  **/
 
 #include "cvc4_private.h"
@@ -34,191 +28,20 @@
 #include "theory/theory.h"
 
 #include "context/context.h"
-#include "context/cdo.h"
-#include "context/cdlist.h"
-#include "theory/uf/ecdata.h"
 
 namespace CVC4 {
 namespace theory {
 namespace uf {
 
 class TheoryUF : public Theory {
-
-private:
-
-  /**
-   * List of all of the non-negated literals from the assertion queue.
-   * This is used only for conflict generation.
-   * This differs from pending as the program generates new equalities that
-   * are not in this list.
-   * This will probably be phased out in future version.
-   */
-  context::CDList<Node> d_assertions;
-
-  /**
-   * List of pending equivalence class merges.
-   *
-   * Tricky part:
-   * Must keep a hard link because new equality terms are created and appended
-   * to this list.
-   */
-  context::CDList<Node> d_pending;
-
-  /** Index of the next pending equality to merge. */
-  context::CDO<unsigned> d_currentPendingIdx;
-
-  /** List of all disequalities this theory has seen. */
-  context::CDList<Node> d_disequality;
-
-  /**
-   * List of all of the terms that are registered in the current context.
-   * When registerTerm is called on a term we want to guarentee that there
-   * is a hard link to the term for the duration of the context in which
-   * register term is called.
-   * This invariant is enough for us to use soft links where we want is the
-   * current implementation as well as making ECAttr() not context dependent.
-   * Soft links used both in ECData, and Link.
-   */
-  context::CDList<Node> d_registered;
-
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(int id, context::Context* c, OutputChannel& out);
-
-  /** Destructor for the TheoryUF object. */
-  ~TheoryUF();
-
-
-
-  /**
-   * Registers a previously unseen [in this context] node n.
-   * For TheoryUF, this sets up and maintains invaraints about
-   * equivalence class data-structures.
-   *
-   * Overloads a void registerTerm(TNode n); from theory.h.
-   * See theory/theory.h for more information about this method.
-   */
-  void registerTerm(TNode n);
-
-  /**
-   * Currently this does nothing.
-   *
-   * Overloads a void preRegisterTerm(TNode n); from theory.h.
-   * See theory/theory.h for more information about this method.
-   */
-  void preRegisterTerm(TNode n);
-
-  /**
-   * Checks whether the set of literals provided to the theory is consistent.
-   *
-   * If this is called at any effort level, it computes the congruence closure
-   * of all of the positive literals in the context.
-   *
-   * If this is called at full effort it checks if any of the negative literals
-   * are inconsistent with the congruence closure.
-   *
-   * Overloads  void check(Effort level); from theory.h.
-   * See theory/theory.h for more information about this method.
-   */
-  void check(Effort level);
-
-
-  /**
-   * Rewrites a node in the theory of uninterpreted functions.
-   * This is fairly basic and only ensures that atoms that are
-   * unsatisfiable or a valid are rewritten to false or true respectively.
-   */
-  Node rewrite(TNode n);
-
-  /**
-   * Plug in old rewrite to the new (pre,post)rewrite interface.
-   */
-  RewriteResponse postRewrite(TNode n, bool topLevel) {
-    return RewriteComplete(topLevel ? rewrite(n) : Node(n));
-  }
-
-  /**
-   * Propagates theory literals. Currently does nothing.
-   *
-   * Overloads void propagate(Effort level); from theory.h.
-   * See theory/theory.h for more information about this method.
-   */
-  void propagate(Effort level) {}
-
-  /**
-   * Explains a previously reported conflict. Currently does nothing.
-   *
-   * Overloads void explain(TNode n, Effort level); from theory.h.
-   * See theory/theory.h for more information about this method.
-   */
-  void explain(TNode n, Effort level) {}
-
-  std::string identify() const { return std::string("TheoryUF"); }
-
-private:
-  /**
-   * Checks whether 2 nodes are already in the same equivalence class tree.
-   * This should only be used internally, and it should only be called when
-   * the only thing done with the equivalence classes is an equality check.
-   *
-   * @returns true iff ccFind(x) == ccFind(y);
-   */
-  bool sameCongruenceClass(TNode x, TNode y);
-
-  /**
-   * Checks whether Node x and Node y are currently congruent
-   * using the equivalence class data structures.
-   * @returns true iff
-   *    |x| = n = |y| and
-   *    x.getOperator() == y.getOperator() and
-   *    forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
-   */
-  bool equiv(TNode x, TNode y);
-
-  /**
-   * Merges 2 equivalence classes, checks wether any predecessors need to
-   * be set equal to complete congruence closure.
-   * The class with the smaller class size will be merged.
-   * @pre ecX->isClassRep()
-   * @pre ecY->isClassRep()
-   */
-  void ccUnion(ECData* ecX, ECData* ecY);
-
-  /**
-   * Returns the representative of the equivalence class.
-   * May modify the find pointers associated with equivalence classes.
-   */
-  ECData* ccFind(ECData* x);
-
-  /** Performs Congruence Closure to reflect the new additions to d_pending. */
-  void merge();
-
-  /** Constructs a conflict from an inconsistent disequality. */
-  Node constructConflict(TNode diseq);
+  TheoryUF(int id, context::Context* ctxt, OutputChannel& out)
+    : Theory(id, ctxt, out) {}
 
 };/* class TheoryUF */
 
-
-/**
- * Cleanup function for ECData. This will be used for called whenever
- * a ECAttr is being destructed.
- */
-struct ECCleanupStrategy {
-  static void cleanup(ECData* ec) {
-    Debug("ufgc") << "cleaning up ECData " << ec << "\n";
-    ec->deleteSelf();
-  }
-};/* struct ECCleanupStrategy */
-
-/** Unique name to use for constructing ECAttr. */
-struct ECAttrTag {};
-
-/**
- * ECAttr is the attribute that maps a node to an equivalence class.
- */
-typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
-
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am
new file mode 100644
index 000000000..647783885
--- /dev/null
+++ b/src/theory/uf/tim/Makefile.am
@@ -0,0 +1,14 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libuftim.la
+
+libuftim_la_SOURCES = \
+	ecdata.h \
+	ecdata.cpp \
+	theory_uf_tim.h \
+	theory_uf_tim.cpp
+
+EXTRA_DIST =
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp
index 822f3a95b..52a110ff2 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/tim/ecdata.cpp
@@ -17,12 +17,13 @@
  ** context-dependent object.
  **/
 
-#include "theory/uf/ecdata.h"
+#include "theory/uf/tim/ecdata.h"
 
 using namespace CVC4;
-using namespace context;
-using namespace theory;
-using namespace uf;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
 
 ECData::ECData(Context * context, TNode n) :
   ContextObj(context),
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/tim/ecdata.h
index bff0a67a2..5e72f0042 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/tim/ecdata.h
@@ -19,8 +19,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__UF__ECDATA_H
-#define __CVC4__THEORY__UF__ECDATA_H
+#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H
+#define __CVC4__THEORY__UF__TIM__ECDATA_H
 
 #include "expr/node.h"
 #include "context/context.h"
@@ -30,6 +30,7 @@
 namespace CVC4 {
 namespace theory {
 namespace uf {
+namespace tim {
 
 /**
  * Link is a context dependent linked list of nodes.
@@ -252,8 +253,9 @@ public:
 
 };/* class ECData */
 
+}/* CVC4::theory::uf::tim namespace */
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__UF__ECDATA_H */
+#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index 9060568b2..ccc37a24b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_uf.cpp
+/*! \file theory_uf_tim.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
@@ -16,8 +16,8 @@
  ** Implementation of the theory of uninterpreted functions.
  **/
 
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/ecdata.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/uf/tim/ecdata.h"
 #include "expr/kind.h"
 
 using namespace CVC4;
@@ -25,9 +25,10 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
 
-TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) :
-  Theory(id, c, out),
+TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
+  TheoryUF(id, c, out),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
@@ -35,10 +36,10 @@ TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) :
   d_registered(c) {
 }
 
-TheoryUF::~TheoryUF() {
+TheoryUFTim::~TheoryUFTim() {
 }
 
-Node TheoryUF::rewrite(TNode n){
+Node TheoryUFTim::rewrite(TNode n){
   Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
   Node ret(n);
   if(n.getKind() == EQUAL){
@@ -50,12 +51,12 @@ Node TheoryUF::rewrite(TNode n){
   Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
   return ret;
 }
-void TheoryUF::preRegisterTerm(TNode n) {
+void TheoryUFTim::preRegisterTerm(TNode n) {
   Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
   Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
 }
 
-void TheoryUF::registerTerm(TNode n) {
+void TheoryUFTim::registerTerm(TNode n) {
 
   Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
 
@@ -147,13 +148,13 @@ void TheoryUF::registerTerm(TNode n) {
 
 }
 
-bool TheoryUF::sameCongruenceClass(TNode x, TNode y) {
+bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) {
   return
     ccFind(x.getAttribute(ECAttr())) ==
     ccFind(y.getAttribute(ECAttr()));
 }
 
-bool TheoryUF::equiv(TNode x, TNode y) {
+bool TheoryUFTim::equiv(TNode x, TNode y) {
   Assert(x.getKind() == kind::APPLY_UF);
   Assert(y.getKind() == kind::APPLY_UF);
 
@@ -189,7 +190,7 @@ bool TheoryUF::equiv(TNode x, TNode y) {
  *    many better algorithms use eager path compression.
  * 2) Elminate recursion.
  */
-ECData* TheoryUF::ccFind(ECData * x) {
+ECData* TheoryUFTim::ccFind(ECData * x) {
   if(x->getFind() == x) {
     return x;
   } else {
@@ -208,7 +209,7 @@ ECData* TheoryUF::ccFind(ECData * x) {
   */
 }
 
-void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) {
+void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) {
   ECData* nslave;
   ECData* nmaster;
 
@@ -234,7 +235,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) {
   ECData::takeOverDescendantWatchList(nslave, nmaster);
 }
 
-void TheoryUF::merge() {
+void TheoryUFTim::merge() {
   while(d_currentPendingIdx < d_pending.size() ) {
     Node assertion = d_pending[d_currentPendingIdx];
     d_currentPendingIdx = d_currentPendingIdx + 1;
@@ -259,7 +260,7 @@ void TheoryUF::merge() {
   }
 }
 
-Node TheoryUF::constructConflict(TNode diseq) {
+Node TheoryUFTim::constructConflict(TNode diseq) {
   Debug("uf") << "uf: begin constructConflict()" << std::endl;
 
   NodeBuilder<> nb(kind::AND);
@@ -278,13 +279,13 @@ Node TheoryUF::constructConflict(TNode diseq) {
   return conflict;
 }
 
-void TheoryUF::check(Effort level) {
+void TheoryUFTim::check(Effort level) {
 
   Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
 
   while(!done()) {
     Node assertion = get();
-    Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
+    Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl;
 
     switch(assertion.getKind()) {
     case EQUAL:
@@ -293,13 +294,17 @@ void TheoryUF::check(Effort level) {
       merge();
       break;
     case NOT:
+      Assert(assertion[0].getKind() == EQUAL,
+             "predicates not supported in this UF implementation");
       d_disequality.push_back(assertion[0]);
       break;
+    case APPLY_UF:
+      Unhandled("predicates not supported in this UF implementation");
     default:
       Unhandled(assertion.getKind());
     }
 
-    Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl;
+    Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl;
   }
 
   //Make sure all outstanding merges are completed.
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
new file mode 100644
index 000000000..1591cc05c
--- /dev/null
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -0,0 +1,229 @@
+/*********************                                                        */
+/*! \file theory_uf.h
+ ** \verbatim
+ ** Original author: taking
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.
+ **
+ ** This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.  It is based on the Nelson-Oppen algorithm given in
+ ** "Fast Decision Procedures Based on Congruence Closure"
+ **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
+ ** This has been extended to work in a context-dependent way.
+ ** This interacts heavily with the data-structures given in ecdata.h .
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/theory.h"
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/ecdata.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+class TheoryUFTim : public TheoryUF {
+
+private:
+
+  /**
+   * List of all of the non-negated literals from the assertion queue.
+   * This is used only for conflict generation.
+   * This differs from pending as the program generates new equalities that
+   * are not in this list.
+   * This will probably be phased out in future version.
+   */
+  context::CDList<Node> d_assertions;
+
+  /**
+   * List of pending equivalence class merges.
+   *
+   * Tricky part:
+   * Must keep a hard link because new equality terms are created and appended
+   * to this list.
+   */
+  context::CDList<Node> d_pending;
+
+  /** Index of the next pending equality to merge. */
+  context::CDO<unsigned> d_currentPendingIdx;
+
+  /** List of all disequalities this theory has seen. */
+  context::CDList<Node> d_disequality;
+
+  /**
+   * List of all of the terms that are registered in the current context.
+   * When registerTerm is called on a term we want to guarentee that there
+   * is a hard link to the term for the duration of the context in which
+   * register term is called.
+   * This invariant is enough for us to use soft links where we want is the
+   * current implementation as well as making ECAttr() not context dependent.
+   * Soft links used both in ECData, and Link.
+   */
+  context::CDList<Node> d_registered;
+
+public:
+
+  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+  TheoryUFTim(int id, context::Context* c, OutputChannel& out);
+
+  /** Destructor for the TheoryUF object. */
+  ~TheoryUFTim();
+
+
+
+  /**
+   * Registers a previously unseen [in this context] node n.
+   * For TheoryUF, this sets up and maintains invaraints about
+   * equivalence class data-structures.
+   *
+   * Overloads a void registerTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void registerTerm(TNode n);
+
+  /**
+   * Currently this does nothing.
+   *
+   * Overloads a void preRegisterTerm(TNode n); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void preRegisterTerm(TNode n);
+
+  /**
+   * Checks whether the set of literals provided to the theory is consistent.
+   *
+   * If this is called at any effort level, it computes the congruence closure
+   * of all of the positive literals in the context.
+   *
+   * If this is called at full effort it checks if any of the negative literals
+   * are inconsistent with the congruence closure.
+   *
+   * Overloads  void check(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void check(Effort level);
+
+
+  /**
+   * Rewrites a node in the theory of uninterpreted functions.
+   * This is fairly basic and only ensures that atoms that are
+   * unsatisfiable or a valid are rewritten to false or true respectively.
+   */
+  Node rewrite(TNode n);
+
+  /**
+   * Plug in old rewrite to the new (pre,post)rewrite interface.
+   */
+  RewriteResponse postRewrite(TNode n, bool topLevel) {
+    return RewriteComplete(topLevel ? rewrite(n) : Node(n));
+  }
+
+  /**
+   * Propagates theory literals. Currently does nothing.
+   *
+   * Overloads void propagate(Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void propagate(Effort level) {}
+
+  /**
+   * Explains a previously reported conflict. Currently does nothing.
+   *
+   * Overloads void explain(TNode n, Effort level); from theory.h.
+   * See theory/theory.h for more information about this method.
+   */
+  void explain(TNode n, Effort level) {}
+
+  std::string identify() const { return std::string("TheoryUFTim"); }
+
+private:
+  /**
+   * Checks whether 2 nodes are already in the same equivalence class tree.
+   * This should only be used internally, and it should only be called when
+   * the only thing done with the equivalence classes is an equality check.
+   *
+   * @returns true iff ccFind(x) == ccFind(y);
+   */
+  bool sameCongruenceClass(TNode x, TNode y);
+
+  /**
+   * Checks whether Node x and Node y are currently congruent
+   * using the equivalence class data structures.
+   * @returns true iff
+   *    |x| = n = |y| and
+   *    x.getOperator() == y.getOperator() and
+   *    forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
+   */
+  bool equiv(TNode x, TNode y);
+
+  /**
+   * Merges 2 equivalence classes, checks wether any predecessors need to
+   * be set equal to complete congruence closure.
+   * The class with the smaller class size will be merged.
+   * @pre ecX->isClassRep()
+   * @pre ecY->isClassRep()
+   */
+  void ccUnion(ECData* ecX, ECData* ecY);
+
+  /**
+   * Returns the representative of the equivalence class.
+   * May modify the find pointers associated with equivalence classes.
+   */
+  ECData* ccFind(ECData* x);
+
+  /** Performs Congruence Closure to reflect the new additions to d_pending. */
+  void merge();
+
+  /** Constructs a conflict from an inconsistent disequality. */
+  Node constructConflict(TNode diseq);
+
+};/* class TheoryUFTim */
+
+
+/**
+ * Cleanup function for ECData. This will be used for called whenever
+ * a ECAttr is being destructed.
+ */
+struct ECCleanupStrategy {
+  static void cleanup(ECData* ec) {
+    Debug("ufgc") << "cleaning up ECData " << ec << "\n";
+    ec->deleteSelf();
+  }
+};/* struct ECCleanupStrategy */
+
+/** Unique name to use for constructing ECAttr. */
+struct ECAttrTag {};
+
+/**
+ * ECAttr is the attribute that maps a node to an equivalence class.
+ */
+typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */