4 files changed, 27 insertions, 18 deletions
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 537b8b124..156733c5b 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 noinst_LTLIBRARIES = libuf.la
 
 libuf_la_SOURCES = \
+	theory_def.h \
 	ecdata.h \
 	ecdata.cpp \
 	theory_uf.h \
diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h
new file mode 100644
index 000000000..8e3f5e9f1
--- /dev/null
+++ b/src/theory/uf/theory_def.h
@@ -0,0 +1,7 @@
+namespace CVC4 {
+  namespace theory {
+    namespace uf {
+      class TheoryUF;
+    }
+  }
+}
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1efe13b9b..47bda5bc4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -19,9 +19,10 @@
 #include "expr/kind.h"
 
 using namespace CVC4;
-using namespace context;
-using namespace theory;
-using namespace uf;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
 
 
 
@@ -30,8 +31,8 @@ Node getOperator(Node x) { return Node::null(); }
 
 
 
-TheoryUF::TheoryUF(Context* c) :
-  Theory(c),
+TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
+  TheoryImpl<TheoryUF>(c, out),
   d_pending(c),
   d_currentPendingIdx(c,0),
   d_disequality(c),
@@ -40,13 +41,16 @@ TheoryUF::TheoryUF(Context* c) :
 
 TheoryUF::~TheoryUF(){}
 
+void TheoryUF::preRegisterTerm(TNode n){
+}
+
 void TheoryUF::registerTerm(TNode n){
 
   d_registered.push_back(n);
 
   ECData* ecN;
 
-  if(n.hasAttribute(ECAttr(),&ecN)){
+  if(n.hasAttribute(ECAttr(), ecN)){
     /* registerTerm(n) is only called when a node has not been seen in the
      * current context.  ECAttr() is not a context-dependent attribute.
      * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
@@ -222,9 +226,9 @@ void TheoryUF::merge(){
   }
 }
 
-void TheoryUF::check(OutputChannel& out, Effort level){
+void TheoryUF::check(Effort level){
   while(!done()){
-    Node assertion = get();
+    Node assertion;// = get();
 
     switch(assertion.getKind()){
     case EQUAL:
@@ -252,7 +256,7 @@ void TheoryUF::check(OutputChannel& out, Effort level){
       TNode left  = (*diseqIter)[0];
       TNode right = (*diseqIter)[1];
       if(sameCongruenceClass(left, right)){
-        out.conflict(*diseqIter, true);
+        d_out->conflict(*diseqIter, true);
       }
     }
   }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index b68a96e65..4bb18bd43 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -21,7 +21,6 @@
 #include "expr/attribute.h"
 
 #include "theory/theory.h"
-#include "theory/output_channel.h"
 
 #include "context/context.h"
 #include "theory/uf/ecdata.h"
@@ -30,9 +29,8 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+class TheoryUF : public TheoryImpl<TheoryUF> {
 
-
-class TheoryUF : public Theory {
 private:
 
 
@@ -72,7 +70,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c);
+  TheoryUF(context::Context* c, OutputChannel& out);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUF();
@@ -82,14 +80,13 @@ public:
   //has pending changes to the contracts
 
   void registerTerm(TNode n);
+  void preRegisterTerm(TNode n);
 
-  void check(OutputChannel& out, Effort level= FULL_EFFORT);
+  void check(Effort level);
 
-  void propagate(OutputChannel& out, Effort level= FULL_EFFORT){}
+  void propagate(Effort level) {}
 
-  void explain(OutputChannel& out,
-               const Node& n,
-               Effort level = FULL_EFFORT){}
+  void explain(TNode n, Effort level) {}
 
 private:
   /**