* Node::isAtomic() now looks at an "atomic" attribute of arguments

  instead of assuming it's atomic based on kind.  Atomicity is
  determined at node building time.  Fixes bug #81.  If this is
  determined to make node building too slow, we can allocate another
  attribute "AtomicHasBeenComputed" to lazily compute atomicity.

* TheoryImpl<> has gone away.  Theory implementations now derive from
  Theory directly and share a single RegisteredAttr attribute for term
  registration (which shouldn't overlap: every term is "owned" by
  exactly one Theory).  Fixes bug #79.

* Additional atomicity tests in ExprBlack unit test.

* More appropriate whitebox testing for attribute ID assignment
  (AttributeWhite unit test).

* Better (and more correct) assertion checking in NodeBuilderBlack.

* run-regression script now checks exit status against what's provided
  in "% EXIT: " gesture in .cvc input files, and stderr against
  "% EXPECT-ERROR: ".  These can be used to support intended failures.
  Fixes bug #84.  Also add "% EXIT: " gestures to all .cvc regressions
  in repository.

* Solved some "control reaches end of non-void function" warnings in
  src/parser/bounded_token_buffer.cpp by replacing
  "AlwaysAssert(false)" with "Unreachable()" (which is known
  statically to never return normally).

* Regression tests now use the cvc4 binary under
  builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
  may not be properly installed yet at that point of the build.
  (Partially fixes bug #46.)

* -fvisibility=hidden is now included by configure.ac instead of each
   Makefile.am, which will make it easier to support platforms
   (e.g. cygwin) that do things a different way.

* TheoryUF code formatting.  (re: my code review bug #64)

* CDMap<> is leaking memory again, pending a fix for bug #85 in the
  context subsystem.  (To avoid serious errors, can't free context
  objects.)

* add ContextWhite unit test for bug #85 (though it's currently
  "defanged," awaiting the bugfix)

* Minor documentation, other cleanup.

14 files changed, 177 insertions, 224 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 2891e64cf..6b1854bfc 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libtheory.la
 
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 226d5af12..cb838f497 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarith.la
 
 libarith_la_SOURCES = \
-	theory_def.h \
 	theory_arith.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 973651f7a..d211cd37d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class TheoryArith : public TheoryImpl<TheoryArith> {
+class TheoryArith : public Theory {
 public:
   TheoryArith(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryArith>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index af3a28b3b..5d3514dda 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarrays.la
 
 libarrays_la_SOURCES = \
-	theory_def.h \
 	theory_arrays.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index ec3b88ccd..2f62aacd7 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace arrays {
 
-class TheoryArrays : public TheoryImpl<TheoryArrays> {
+class TheoryArrays : public Theory {
 public:
   TheoryArrays(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryArrays>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index cbdf13add..690299630 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbooleans.la
 
 libbooleans_la_SOURCES = \
-	theory_def.h \
 	theory_bool.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 5196bb018..eb6e84c39 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-class TheoryBool : public TheoryImpl<TheoryBool> {
+class TheoryBool : public Theory {
 public:
   TheoryBool(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryBool>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 54622bf9a..d90472fd3 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
-	theory_def.h \
 	theory_bv.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fbb62545d..a859291a7 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class TheoryBV : public TheoryImpl<TheoryBV> {
+class TheoryBV : public Theory {
 public:
   TheoryBV(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryBV>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 17a35f2ed..d4bd717be 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -23,5 +23,82 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+Node Theory::get() {
+  Assert( !d_facts.empty(),
+          "Theory::get() called with assertion queue empty!" );
+
+  Node fact = d_facts.front();
+  d_facts.pop_front();
+
+  Debug("theory") << "Theory::get() => " << fact
+                  << "(" << d_facts.size() << " left)" << std::endl;
+
+  if(! fact.getAttribute(RegisteredAttr())) {
+    std::list<TNode> toReg;
+    toReg.push_back(fact);
+
+    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+
+    /* Essentially this is doing a breadth-first numbering of
+     * non-registered subterms with children.  Any non-registered
+     * leaves are immediately registered. */
+    for(std::list<TNode>::iterator workp = toReg.begin();
+        workp != toReg.end();
+        ++workp) {
+
+      TNode n = *workp;
+
+      if(n.hasOperator()) {
+        TNode c = n.getOperator();
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+
+      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+        TNode c = *i;
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+    }
+
+    /* Now register the list of terms in reverse order.  Between this
+     * and the above registration of leaves, this should ensure that
+     * all subterms in the entire tree were registered in
+     * reverse-topological order. */
+    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+        i != toReg.rend();
+        ++i) {
+
+      TNode n = *i;
+
+      /* Note that a shared TNode in the DAG rooted at "fact" could
+       * appear twice on the list, so we have to avoid hitting it
+       * twice. */
+      // FIXME when ExprSets are online, use one of those to avoid
+      // duplicates in the above?
+      if(! n.getAttribute(RegisteredAttr())) {
+        n.setAttribute(RegisteredAttr(), true);
+        registerTerm(n);
+      }
+    }
+  }
+
+  return fact;
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4c3a43061..2fcac86b0 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -38,36 +38,22 @@ namespace theory {
 struct RewriteCacheTag {};
 typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
 
-template <class T>
-class TheoryImpl;
-
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
  *
  * This is essentially an interface class.  The TheoryEngine has
- * pointers to Theory.  But each individual theory implementation T
- * should inherit from TheoryImpl<T>, which specializes a few things
- * for that theory.
+ * pointers to Theory.  Note that only one specific Theory type (e.g.,
+ * TheoryUF) can exist per NodeManager, because of how the
+ * RegisteredAttr works.  (If you need multiple instances of the same
+ * theory, you'll have to write a multiplexed theory that dispatches
+ * all calls to them.)
  */
 class Theory {
 private:
 
-  template <class T>
-  friend class ::CVC4::theory::TheoryImpl;
-
   friend class ::CVC4::TheoryEngine;
 
   /**
-   * Construct a Theory.
-   */
-  Theory(context::Context* ctxt, OutputChannel& out) throw() :
-    d_context(ctxt),
-    d_facts(),
-    d_factsResetter(*this),
-    d_out(&out) {
-  }
-
-  /**
    * Disallow default construction.
    */
   Theory();
@@ -110,13 +96,23 @@ private:
 protected:
 
   /**
+   * Construct a Theory.
+   */
+  Theory(context::Context* ctxt, OutputChannel& out) throw() :
+    d_context(ctxt),
+    d_facts(),
+    d_factsResetter(*this),
+    d_out(&out) {
+  }
+
+  /**
    * This is called at shutdown time by the TheoryEngine, just before
    * destruction.  It is important because there are destruction
    * ordering issues between PropEngine and Theory (based on what
    * hard-links to Nodes are outstanding).  As the fact queue might be
    * nonempty, we ensure here that it's clear.  If you overload this,
-   * you must make an explicit call here to the Theory implementation
-   * of this function too.
+   * you must make an explicit call here to this->Theory::shutdown()
+   * too.
    */
   virtual void shutdown() {
     d_facts.clear();
@@ -158,6 +154,24 @@ protected:
     return n.getAttribute(RewriteCache());
   }
 
+  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+  struct Registered {};
+  /** The "registerTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
+  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
+  struct PreRegistered {};
+  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+
+  /**
+   * Returns the next atom in the assertFact() queue.  Guarantees that
+   * registerTerm() has been called on the theory specific subterms.
+   *
+   * @return the next atom in the assertFact() queue.
+   */
+  Node get();
+
 public:
 
   /**
@@ -308,133 +322,6 @@ protected:
 
 };/* class Theory */
 
-
-/**
- * Base class for T-solver implementations.  Each individual
- * implementation T of the Theory interface should inherit from
- * TheoryImpl<T>.  This class specializes some things for a particular
- * theory implementation.
- *
- * The problem with this is that Theory implementations cannot be
- * further subclassed without designing all non-children in the type
- * DAG to play the same trick as here (be template-polymorphic in their
- * most-derived child), linearizing the inheritance hierarchy (viewing
- * each instantiation separately).
- */
-template <class T>
-class TheoryImpl : public Theory {
-
-protected:
-
-  /**
-   * Construct a Theory.
-   */
-  TheoryImpl(context::Context* ctxt, OutputChannel& out) :
-    Theory(ctxt, out) {
-    /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
-     * for this NodeManager??  If it does, we're hosed because they'll
-     * share per-theory node attributes. */
-  }
-
-  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-  struct Registered {};
-  /** The "registerTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
-
-  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
-  struct PreRegistered {};
-  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
-
-  /**
-   * Returns the next atom in the assertFact() queue.  Guarantees that
-   * registerTerm() has been called on the theory specific subterms.
-   *
-   * @return the next atom in the assertFact() queue.
-   */
-  Node get();
-};/* class TheoryImpl<T> */
-
-template <class T>
-Node TheoryImpl<T>::get() {
-  Assert(typeid(*this) == typeid(T),
-         "Improper Theory inheritance chain detected.");
-
-  Assert( !d_facts.empty(),
-          "Theory::get() called with assertion queue empty!" );
-
-  Node fact = d_facts.front();
-  d_facts.pop_front();
-
-  Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
-
-  if(! fact.getAttribute(RegisteredAttr())) {
-    std::list<TNode> toReg;
-    toReg.push_back(fact);
-
-    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
-
-    /* Essentially this is doing a breadth-first numbering of
-     * non-registered subterms with children.  Any non-registered
-     * leaves are immediately registered. */
-    for(std::list<TNode>::iterator workp = toReg.begin();
-        workp != toReg.end();
-        ++workp) {
-
-      TNode n = *workp;
-
-      if(n.hasOperator()) {
-        TNode c = n.getOperator();
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-
-      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-        TNode c = *i;
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-    }
-
-    /* Now register the list of terms in reverse order.  Between this
-     * and the above registration of leaves, this should ensure that
-     * all subterms in the entire tree were registered in
-     * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
-        i != toReg.rend();
-        ++i) {
-
-      TNode n = *i;
-
-      /* Note that a shared TNode in the DAG rooted at "fact" could
-       * appear twice on the list, so we have to avoid hitting it
-       * twice. */
-      // FIXME when ExprSets are online, use one of those to avoid
-      // duplicates in the above?
-      if(! n.getAttribute(RegisteredAttr())) {
-        n.setAttribute(RegisteredAttr(), true);
-        registerTerm(n);
-      }
-    }
-  }
-
-  return fact;
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 156733c5b..e0aa3a1df 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_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_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3fe82b16c..f0d8b47e0 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -10,10 +10,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- **
+ ** Implementation of the theory of uninterpreted functions.
  **/
 
-
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/ecdata.h"
 #include "expr/kind.h"
@@ -24,37 +23,32 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
-
-
 TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
-  TheoryImpl<TheoryUF>(c, out),
+  Theory(c, out),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
   d_disequality(c),
-  d_registered(c)
-{}
+  d_registered(c) {
+}
 
-TheoryUF::~TheoryUF(){}
+TheoryUF::~TheoryUF() {
+}
 
-void TheoryUF::preRegisterTerm(TNode n){
+void TheoryUF::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 TheoryUF::registerTerm(TNode n) {
 
   Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
 
-
   d_registered.push_back(n);
 
-
-
-
   ECData* ecN;
 
-  if(n.getAttribute(ECAttr(), ecN)){
+  if(n.getAttribute(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,
@@ -101,7 +95,7 @@ void TheoryUF::registerTerm(TNode n){
            "Expected getWatchListSize() == 0.  "
            "This data is either already in use or was not properly maintained "
            "during backtracking");
-  }else{
+  } else {
     //The attribute does not exist, so it is created and set
     ecN = new (true) ECData(getContext(), n);
     n.setAttribute(ECAttr(), ecN);
@@ -110,10 +104,10 @@ void TheoryUF::registerTerm(TNode n){
   /* If the node is an APPLY_UF, we need to add it to the predecessor list
    * of its children.
    */
-  if(n.getKind() == APPLY_UF){
+  if(n.getKind() == APPLY_UF) {
     TNode::iterator cIter = n.begin();
 
-    for(; cIter != n.end(); ++cIter){
+    for(; cIter != n.end(); ++cIter) {
       TNode child = *cIter;
 
       /* Because this can be called after nodes have been merged, we need
@@ -124,8 +118,8 @@ void TheoryUF::registerTerm(TNode n){
       /* Because this can be called after nodes have been merged we may need
        * to be merged with other predecessors of the equivalence class.
        */
-      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){
-        if(equiv(n, Px->d_data)){
+      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) {
+        if(equiv(n, Px->d_data)) {
           Node pend = n.eqNode(Px->d_data);
           d_pending.push_back(pend);
         }
@@ -138,30 +132,32 @@ void TheoryUF::registerTerm(TNode n){
 
 }
 
-bool TheoryUF::sameCongruenceClass(TNode x, TNode y){
+bool TheoryUF::sameCongruenceClass(TNode x, TNode y) {
   return
     ccFind(x.getAttribute(ECAttr())) ==
     ccFind(y.getAttribute(ECAttr()));
 }
 
-bool TheoryUF::equiv(TNode x, TNode y){
+bool TheoryUF::equiv(TNode x, TNode y) {
   Assert(x.getKind() == kind::APPLY_UF);
   Assert(y.getKind() == kind::APPLY_UF);
 
-  if(x.getNumChildren() != y.getNumChildren())
+  if(x.getNumChildren() != y.getNumChildren()) {
     return false;
+  }
 
-  if(x.getOperator() != y.getOperator())
+  if(x.getOperator() != y.getOperator()) {
     return false;
+  }
 
   // intentionally don't look at operator
 
   TNode::iterator xIter = x.begin();
   TNode::iterator yIter = y.begin();
 
-  while(xIter != x.end()){
+  while(xIter != x.end()) {
 
-    if(!sameCongruenceClass(*xIter, *yIter)){
+    if(!sameCongruenceClass(*xIter, *yIter)) {
       return false;
     }
 
@@ -178,10 +174,10 @@ bool TheoryUF::equiv(TNode x, TNode y){
  *    many better algorithms use eager path compression.
  * 2) Elminate recursion.
  */
-ECData* TheoryUF::ccFind(ECData * x){
-  if( x->getFind() == x)
+ECData* TheoryUF::ccFind(ECData * x) {
+  if(x->getFind() == x) {
     return x;
-  else{
+  } else {
     return ccFind(x->getFind());
   }
   /* Slightly better Find w/ path compression and no recursion*/
@@ -189,7 +185,7 @@ ECData* TheoryUF::ccFind(ECData * x){
     ECData* start;
     ECData* next = x;
     while(x != x->getFind()) x=x->getRep();
-    while( (start = next) != x){
+    while( (start = next) != x) {
       next = start->getFind();
       start->setFind(x);
     }
@@ -197,23 +193,23 @@ ECData* TheoryUF::ccFind(ECData * x){
   */
 }
 
-void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
+void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) {
   ECData* nslave;
   ECData* nmaster;
 
-  if(ecX->getWatchListSize() <= ecY->getWatchListSize()){
+  if(ecX->getWatchListSize() <= ecY->getWatchListSize()) {
     nslave = ecX;
     nmaster = ecY;
-  }else{
+  } else {
     nslave = ecY;
     nmaster = ecX;
   }
 
   nslave->setFind(nmaster);
 
-  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){
-    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){
-      if(equiv(Px->d_data,Py->d_data)){
+  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ) {
+    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) {
+      if(equiv(Px->d_data,Py->d_data)) {
         Node pendingEq = (Px->d_data).eqNode(Py->d_data);
         d_pending.push_back(pendingEq);
       }
@@ -223,7 +219,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
   ECData::takeOverDescendantWatchList(nslave, nmaster);
 }
 
-void TheoryUF::merge(){
+void TheoryUF::merge() {
   while(d_currentPendingIdx < d_pending.size() ) {
     Node assertion = d_pending[d_currentPendingIdx];
     d_currentPendingIdx = d_currentPendingIdx + 1;
@@ -248,7 +244,7 @@ void TheoryUF::merge(){
   }
 }
 
-Node TheoryUF::constructConflict(TNode diseq){
+Node TheoryUF::constructConflict(TNode diseq) {
   Debug("uf") << "uf: begin constructConflict()" << std::endl;
 
   NodeBuilder<> nb(kind::AND);
@@ -267,15 +263,15 @@ Node TheoryUF::constructConflict(TNode diseq){
   return conflict;
 }
 
-void TheoryUF::check(Effort level){
+void TheoryUF::check(Effort level) {
 
   Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
 
-  while(!done()){
+  while(!done()) {
     Node assertion = get();
     Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
 
-    switch(assertion.getKind()){
+    switch(assertion.getKind()) {
     case EQUAL:
       d_assertions.push_back(assertion);
       d_pending.push_back(assertion);
@@ -292,18 +288,18 @@ void TheoryUF::check(Effort level){
   }
 
   //Make sure all outstanding merges are completed.
-  if(d_currentPendingIdx < d_pending.size()){
+  if(d_currentPendingIdx < d_pending.size()) {
     merge();
   }
 
-  if(fullEffort(level)){
+  if(fullEffort(level)) {
     for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
         diseqIter != d_disequality.end();
-        ++diseqIter){
+        ++diseqIter) {
 
       TNode left  = (*diseqIter)[0];
       TNode right = (*diseqIter)[1];
-      if(sameCongruenceClass(left, right)){
+      if(sameCongruenceClass(left, right)) {
         Node remakeNeq = (*diseqIter).notNode();
         Node conflict = constructConflict(remakeNeq);
         d_out->conflict(conflict, false);
@@ -313,5 +309,4 @@ void TheoryUF::check(Effort level){
   }
 
   Debug("uf") << "uf: end check(" << level << ")" << std::endl;
-
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8495e6c9c..5863a31fc 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -38,7 +38,7 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class TheoryUF : public TheoryImpl<TheoryUF> {
+class TheoryUF : public Theory {
 
 private:
 
@@ -176,31 +176,30 @@ private:
   /** Constructs a conflict from an inconsistent disequality. */
   Node constructConflict(TNode diseq);
 
-};
+};/* 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){
+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 EquivClass;
+struct ECAttrTag {};
 
 /**
  * ECAttr is the attribute that maps a node to an equivalence class.
  */
-typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr;
-
-} /* CVC4::theory::uf namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
 
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__UF__THEORY_UF_H */