The "UF engineering issues" release, after much profiling.

* swap in backtracking data structures (that use and maintain their own
  undo stack) in some places instead of the usual Context-aware
  paradigm (MUCH faster).

* cosmetic changes to UF, CC modules.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f27e615443c0430eba648ca5dff5f25a830dff06..48f983b3f2d7bc8678cd50e49781622f1821484b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -618,18 +618,18 @@ Node TheoryEngine::getValue(TNode node) {
 }/* TheoryEngine::getValue(TNode node) */
 
 
-bool TheoryEngine::presolve(){
+bool TheoryEngine::presolve() {
   d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
   try {
-    //d_uf->presolve();
+    d_uf->presolve();
     d_arith->presolve();
     //d_arrays->presolve();
     //d_bv->presolve();
   } catch(const theory::Interrupted&) {
     Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl;
   }
-  // Return wheather we have a conflict
+  // Return whether we have a conflict
   return d_theoryOut.d_conflictNode.get().isNull();
 }
 

diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am
index e9faa88df1cf10d7e1c3d6f2416a629f649a0b8f..886178a6f60e1a2419a475b9437ca23a615c489e 100644 (file)
--- a/src/theory/uf/morgan/Makefile.am
+++ b/src/theory/uf/morgan/Makefile.am
@@ -7,6 +7,10 @@ noinst_LTLIBRARIES = libufmorgan.la
 
 libufmorgan_la_SOURCES = \
        theory_uf_morgan.h \
-       theory_uf_morgan.cpp
+       theory_uf_morgan.cpp \
+       union_find.h \
+       union_find.cpp \
+       stacking_map.h \
+       stacking_map.cpp
 
 EXTRA_DIST =

diff --git a/src/theory/uf/morgan/stacking_map.cpp b/src/theory/uf/morgan/stacking_map.cpp
new file mode 100644 (file)
index 0000000..16a85e7
--- /dev/null
+++ b/src/theory/uf/morgan/stacking_map.cpp
@@ -0,0 +1,83 @@
+/*********************                                                        */
+/*! \file stacking_map.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 Backtrackable map using an undo stack
+ **
+ ** Backtrackable map using an undo stack rather than storing items in
+ ** a CDMap<>.
+ **/
+
+#include <iostream>
+
+#include "theory/uf/morgan/stacking_map.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace morgan {
+
+template <class NodeType, class NodeHash>
+TNode StackingMap<NodeType, NodeHash>::find(TNode n) const {
+  typename MapType::const_iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    return TNode();
+  } else {
+    return (*i).second;
+  }
+}
+
+template <class NodeType, class NodeHash>
+void StackingMap<NodeType, NodeHash>::set(TNode n, TNode newValue) {
+  Trace("ufsm") << "UFSM setting " << n << " : " << newValue << " @ " << d_trace.size() << endl;
+  NodeType& ref = d_map[n];
+  d_trace.push_back(make_pair(n, TNode(ref)));
+  d_offset = d_trace.size();
+  ref = newValue;
+}
+
+template <class NodeType, class NodeHash>
+void StackingMap<NodeType, NodeHash>::notify() {
+  Trace("ufsm") << "UFSM 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("ufsm") << "UFSM   " << d_trace.size() << " erasing " << p.first << endl;
+    } else {
+      d_map[p.first] = p.second;
+      Trace("ufsm") << "UFSM   " << d_trace.size() << " replacing " << p << endl;
+    }
+    d_trace.pop_back();
+  }
+  Trace("ufufsm") << "UFSM 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 TNode StackingMap<Node, NodeHashFunction>::find(TNode n) const;
+template void StackingMap<Node, NodeHashFunction>::set(TNode n, TNode newValue);
+template void StackingMap<Node, NodeHashFunction>::notify();
+
+template TNode StackingMap<TNode, TNodeHashFunction>::find(TNode n) const;
+template void StackingMap<TNode, TNodeHashFunction>::set(TNode n, TNode newValue);
+template void StackingMap<TNode, TNodeHashFunction>::notify();
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */

diff --git a/src/theory/uf/morgan/stacking_map.h b/src/theory/uf/morgan/stacking_map.h
new file mode 100644 (file)
index 0000000..c54acc3
--- /dev/null
+++ b/src/theory/uf/morgan/stacking_map.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file stacking_map.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 Backtrackable map using an undo stack
+ **
+ ** Backtrackable map using an undo stack rather than storing items in
+ ** a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H
+#define __CVC4__THEORY__UF__MORGAN__STACKING_MAP_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 uf {
+namespace morgan {
+
+// NodeType \in { Node, TNode }
+template <class NodeType, class NodeHash>
+class StackingMap : context::ContextNotifyObj {
+  /** Our underlying map type. */
+  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+
+  /**
+   * Our map of Nodes to their values.
+   */
+  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:
+  StackingMap(context::Context* ctxt) :
+    context::ContextNotifyObj(ctxt),
+    d_offset(ctxt, 0) {
+  }
+
+  ~StackingMap() throw() { }
+
+  /**
+   * Return a Node's value in the key-value map.  If n is not a key in
+   * the map, this function returns TNode::null().
+   */
+  TNode find(TNode n) const;
+
+  /**
+   * Set the value in the key-value map for Node n to newValue.
+   */
+  void set(TNode n, TNode newValue);
+
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::notify().
+   */
+  void notify();
+
+};/* class StackingMap<> */
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__UF__MORGAN__STACKING_MAP_H */

diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index 4ee6987219558755ea60f68bd1d42f328cbe56f6..cc0296d0ad3f0a944fbdea24a35715208509fcb4 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -131,25 +131,6 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) {
   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::notifyCongruent(TNode a, TNode b) {
   Debug("uf") << "uf: notified of merge " << a << std::endl
               << "                  and " << b << std::endl;
@@ -188,7 +169,7 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
   // should have already found such a conflict
   Assert(find(d_trueNode) != find(d_falseNode));
 
-  d_unionFind[a] = b;
+  d_unionFind.setCanon(a, b);
 
   DiseqLists::iterator deq_i = d_disequalities.find(a);
   if(deq_i != d_disequalities.end()) {

diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 569f9bb4958b84cd77b37d5230e96e14d369bda3..d26e6ff8fcd428ec985d11976b749d36fcf88efa 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -30,6 +30,7 @@
 
 #include "theory/theory.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/morgan/union_find.h"
 
 #include "context/context.h"
 #include "context/context_mm.h"
@@ -75,8 +76,10 @@ private:
    */
   CongruenceClosure<CongruenceChannel> d_cc;
 
-  typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind;
-  UnionFind d_unionFind;
+  /**
+   * Our union find for equalities.
+   */
+  UnionFind<TNode, TNodeHashFunction> d_unionFind;
 
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList;
   typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
@@ -130,8 +133,8 @@ public:
    */
   void check(Effort level);
 
-  void presolve(){
-    Unimplemented();
+  void presolve() {
+    // do nothing for now
   }
 
   /**
@@ -172,8 +175,8 @@ private:
   /** Constructs a conflict from an inconsistent disequality. */
   Node constructConflict(TNode diseq);
 
-  TNode find(TNode a);
-  TNode debugFind(TNode a) const;
+  inline TNode find(TNode a);
+  inline TNode debugFind(TNode a) const;
 
   void appendToDiseqList(TNode of, TNode eq);
   void addDisequality(TNode eq);
@@ -195,6 +198,14 @@ private:
 
 };/* class TheoryUFMorgan */
 
+inline TNode TheoryUFMorgan::find(TNode a) {
+  return d_unionFind.find(a);
+}
+
+inline TNode TheoryUFMorgan::debugFind(TNode a) const {
+  return d_unionFind.debugFind(a);
+}
+
 }/* CVC4::theory::uf::morgan namespace */
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */

diff --git a/src/theory/uf/morgan/union_find.cpp b/src/theory/uf/morgan/union_find.cpp
new file mode 100644 (file)
index 0000000..1353207
--- /dev/null
+++ b/src/theory/uf/morgan/union_find.cpp
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/*! \file union_find.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include <iostream>
+
+#include "theory/uf/morgan/union_find.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace morgan {
+
+template <class NodeType, class NodeHash>
+void UnionFind<NodeType, NodeHash>::notify() {
+  Trace("ufuf") << "UFUF 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("ufuf") << "UFUF   " << d_trace.size() << " erasing " << p.first << endl;
+    } else {
+      d_map[p.first] = p.second;
+      Trace("ufuf") << "UFUF   " << d_trace.size() << " replacing " << p << endl;
+    }
+    d_trace.pop_back();
+  }
+  Trace("ufuf") << "UFUF 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::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */

diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h
new file mode 100644 (file)
index 0000000..b848be5
--- /dev/null
+++ b/src/theory/uf/morgan/union_find.h
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file union_find.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__MORGAN__UNION_FIND_H
+#define __CVC4__THEORY__UF__MORGAN__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 uf {
+namespace morgan {
+
+// 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);
+
+  /**
+   * 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("ufuf") << "UFUF find of " << n << endl;
+  typename MapType::iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    Trace("ufuf") << "UFUF   it is rep" << endl;
+    return n;
+  } else {
+    Trace("ufuf") << "UFUF   not rep: par is " << (*i).second << endl;
+    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(make_pair(n, pr.second));
+    d_offset = d_trace.size();
+    Trace("ufuf") << "UFUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << 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());
+  Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl;
+  d_map[n] = newParent;
+  d_trace.push_back(make_pair(n, TNode::null()));
+  d_offset = d_trace.size();
+}
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__UF__MORGAN__UNION_FIND_H */

diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 44f061c1210fc48083e428732508cf885b09ec46..73033f387853eb299087a1568da27be58ae05b6a 100644 (file)
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -125,9 +125,8 @@ public:
    */
   void check(Effort level);
 
-
   void presolve() {
-    Unimplemented();
+    // do nothing
   }
 
   /**

diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index db9d5bc65ae4d7f0d2a5b5954db7f116065c5ccc..90ab11f9ff9da2605ab418639e1b91dc7c7bf4bf 100644 (file)
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -34,6 +34,7 @@
 #include "context/cdset.h"
 #include "context/cdlist_context_memory.h"
 #include "util/exception.h"
+#include "theory/uf/morgan/stacking_map.h"
 
 namespace CVC4 {
 
@@ -103,7 +104,7 @@ class CongruenceClosure {
   OutputChannel* d_out;
 
   // typedef all of these so that iterators are easy to define
-  typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap;
+  typedef theory::uf::morgan::StackingMap <Node, NodeHashFunction> RepresentativeMap;
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
   typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
@@ -115,6 +116,13 @@ class CongruenceClosure {
   typedef context::CDMap<Node, Node, NodeHashFunction> ProofMap;
   typedef context::CDMap<Node, Node, NodeHashFunction> ProofLabel;
 
+  // Simple, NON-context-dependent pending list, union find and "seen
+  // set" types for constructing explanations and
+  // nearestCommonAncestor(); see explain().
+  typedef std::list<std::pair<Node, Node> > PendingProofList_t;
+  typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> UnionFind_t;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> SeenSet_t;
+
   RepresentativeMap d_representative;
   ClassLists d_classList;
   UseLists d_useList;
@@ -210,7 +218,7 @@ public:
     }
   }
 
-  TNode proofRewrite(TNode pfStep) {
+  TNode proofRewrite(TNode pfStep) const {
     ProofMap::const_iterator i = d_proofRewrite.find(pfStep);
     if(i == d_proofRewrite.end()) {
       return pfStep;
@@ -254,18 +262,17 @@ public:
    * Find the EC representative for a term t in the current context.
    */
   inline TNode find(TNode t) const throw(AssertionException) {
-    context::CDMap<Node, Node, NodeHashFunction>::iterator i =
-      d_representative.find(t);
-    return (i == d_representative.end()) ? t : TNode((*i).second);
+    TNode rep1 = d_representative.find(t);
+    return rep1.isNull() ? t : rep1;
   }
 
-  void explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+  void explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list<Node>& pf)
     throw(AssertionException);
 
-  Node highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+  Node highestNode(TNode a, UnionFind_t& unionFind) const
     throw(AssertionException);
 
-  Node nearestCommonAncestor(TNode a, TNode b)
+  Node nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind)
     throw(AssertionException);
 
   /**
@@ -311,7 +318,7 @@ private:
    * Internal lookup mapping from tuples to equalities.
    */
   inline TNode lookup(TNode a) const {
-    context::CDMap<Node, Node, NodeHashFunction>::iterator i = d_lookup.find(a);
+    LookupMap::iterator i = d_lookup.find(a);
     if(i == d_lookup.end()) {
       return TNode::null();
     } else {
@@ -343,7 +350,7 @@ private:
    * Append equality "eq" to uselist of "of".
    */
   inline void appendToUseList(TNode of, TNode eq) {
-    Debug("cc") << "adding " << eq << " to use list of " << of << std::endl;
+    Trace("cc") << "adding " << eq << " to use list of " << of << std::endl;
     Assert(eq.getKind() == kind::EQUAL ||
            eq.getKind() == kind::IFF);
     Assert(of == find(of));
@@ -406,14 +413,14 @@ template <class OutputChannel>
 void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
   d_proofRewrite[eq] = inputEq;
 
-  if(Debug.isOn("cc")) {
-    Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
+  if(Trace.isOn("cc")) {
+    Trace("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
   }
   Assert(eq.getKind() == kind::EQUAL ||
          eq.getKind() == kind::IFF);
   Assert(eq[1].getKind() != kind::APPLY_UF);
   if(areCongruent(eq[0], eq[1])) {
-    Debug("cc") << "CC -- redundant, ignoring...\n";
+    Trace("cc") << "CC -- redundant, ignoring...\n";
     return;
   }
 
@@ -421,10 +428,10 @@ void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
 
   Assert(s != t);
 
-  Debug("cc:detail") << "CC        " << s << " == " << t << std::endl;
+  Trace("cc:detail") << "CC        " << s << " == " << t << std::endl;
 
   // change from paper: do this whether or not s, t are applications
-  Debug("cc:detail") << "CC        propagating the eq" << std::endl;
+  Trace("cc:detail") << "CC        propagating the eq" << std::endl;
 
   if(s.getKind() != kind::APPLY_UF) {
     // s, t are constants
@@ -433,26 +440,24 @@ void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
     // s is an apply, t is a constant
     Node ap = buildRepresentativesOfApply(s);
 
-    Debug("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl;
-    Debug("cc") << "CC ap is   " << ap << std::endl;
+    Trace("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl;
+    Trace("cc") << "CC ap is   " << ap << std::endl;
 
     TNode l = lookup(ap);
-    Debug("cc:detail") << "CC lookup(ap): " << l << std::endl;
+    Trace("cc:detail") << "CC lookup(ap): " << l << std::endl;
     if(!l.isNull()) {
       // ensure a hard Node link exists to this during the call
       Node pending = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, l);
-      Debug("cc:detail") << "pending1 " << pending << std::endl;
+      Trace("cc:detail") << "pending1 " << pending << std::endl;
       propagate(pending);
     } else {
-      Debug("cc") << "CC lookup(ap) setting to " << eq << std::endl;
+      Trace("cc") << "CC lookup(ap) setting to " << eq << std::endl;
       setLookup(ap, eq);
       for(Node::iterator i = ap.begin(); i != ap.end(); ++i) {
         appendToUseList(*i, eq);
       }
     }
   }
-
-  Debug("cc") << *this;
 }/* addEq() */
 
 
@@ -462,6 +467,7 @@ Node CongruenceClosure<OutputChannel>::buildRepresentativesOfApply(TNode apply,
   throw(AssertionException) {
   Assert(apply.getKind() == kind::APPLY_UF);
   NodeBuilder<> argspb(kindToBuild);
+  // FIXME probably don't have to do find() of operator
   argspb << find(apply.getOperator());
   for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) {
     argspb << find(*i);
@@ -472,18 +478,18 @@ Node CongruenceClosure<OutputChannel>::buildRepresentativesOfApply(TNode apply,
 
 template <class OutputChannel>
 void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
-  Debug("cc:detail") << "=== doing a round of propagation ===" << std::endl
+  Trace("cc:detail") << "=== doing a round of propagation ===" << std::endl
                      << "the \"seed\" propagation is: " << seed << std::endl;
 
   std::list<Node> pending;
 
-  Debug("cc") << "seed propagation with: " << seed << std::endl;
+  Trace("cc") << "seed propagation with: " << seed << std::endl;
   pending.push_back(seed);
   do { // while(!pending.empty())
     Node e = pending.front();
     pending.pop_front();
 
-    Debug("cc") << "=== top of propagate loop ===" << std::endl
+    Trace("cc") << "=== top of propagate loop ===" << std::endl
                 << "=== e is " << e << " ===" << std::endl;
 
     TNode a, b;
@@ -494,11 +500,11 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
       a = e[0];
       b = e[1];
 
-      Debug("cc:detail") << "propagate equality: " << a << " == " << b << std::endl;
+      Trace("cc:detail") << "propagate equality: " << a << " == " << b << std::endl;
     } else {
       // e is a tuple ( apply f A... = a , apply f B... = b )
 
-      Debug("cc") << "propagate tuple: " << e << "\n";
+      Trace("cc") << "propagate tuple: " << e << "\n";
 
       Assert(e.getKind() == kind::TUPLE);
 
@@ -515,11 +521,11 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
       Assert(a.getKind() != kind::APPLY_UF);
       Assert(b.getKind() != kind::APPLY_UF);
 
-      Debug("cc") << "                 ( " << a << " , " << b << " )" << std::endl;
+      Trace("cc") << "                 ( " << a << " , " << b << " )" << std::endl;
     }
 
     if(Debug.isOn("cc")) {
-      Debug("cc:detail") << "=====at start=====" << std::endl
+      Trace("cc:detail") << "=====at start=====" << std::endl
                          << "a          :" << a << std::endl
                          << "NORMALIZE a:" << normalize(a) << std::endl
                          << "b          :" << b << std::endl
@@ -532,7 +538,7 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
     Node ap = find(a), bp = find(b);
     if(ap != bp) {
 
-      Debug("cc:detail") << "EC[a] == " << ap << std::endl
+      Trace("cc:detail") << "EC[a] == " << ap << std::endl
                          << "EC[b] == " << bp << std::endl;
 
       { // w.l.o.g., |classList ap| <= |classList bp|
@@ -540,9 +546,9 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
         ClassLists::iterator cl_bpi = d_classList.find(bp);
         unsigned sizeA = (cl_api == d_classList.end() ? 0 : (*cl_api).second->size());
         unsigned sizeB = (cl_bpi == d_classList.end() ? 0 : (*cl_bpi).second->size());
-        Debug("cc") << "sizeA == " << sizeA << "  sizeB == " << sizeB << std::endl;
+        Trace("cc") << "sizeA == " << sizeA << "  sizeB == " << sizeB << std::endl;
         if(sizeA > sizeB) {
-          Debug("cc") << "swapping..\n";
+          Trace("cc") << "swapping..\n";
           TNode tmp = ap; ap = bp; bp = tmp;
           tmp = a; a = b; b = tmp;
         }
@@ -555,17 +561,17 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
           cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false,
                                                      context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
           d_classList.insertDataFromContextMemory(bp, cl_bp);
-          Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
+          Trace("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
         } else {
           cl_bp = (*cl_bpi).second;
         }
         // we don't store 'ap' in its own class list; so process it here
-        Debug("cc:detail") << "calling mergeproof/merge1 " << ap
+        Trace("cc:detail") << "calling mergeproof/merge1 " << ap
                            << "   AND   " << bp << std::endl;
         mergeProof(a, b, e);
         merge(ap, bp);
 
-        Debug("cc") << " adding ap == " << ap << std::endl
+        Trace("cc") << " adding ap == " << ap << std::endl
                     << "   to class list of " << bp << std::endl;
         cl_bp->push_back(ap);
         ClassLists::const_iterator cli = d_classList.find(ap);
@@ -581,15 +587,15 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
               Debug("cc") << " it's find ptr is: " << find(c) << std::endl;
             }
             Assert(find(c) == ap);
-            Debug("cc:detail") << "calling merge2 " << c << bp << std::endl;
+            Trace("cc:detail") << "calling merge2 " << c << bp << std::endl;
             merge(c, bp);
             // move c from classList(ap) to classlist(bp);
             //i = cl.erase(i);// FIXME do we need to?
-            Debug("cc") << " adding c to class list of " << bp << std::endl;
+            Trace("cc") << " adding c to class list of " << bp << std::endl;
             cl_bp->push_back(c);
           }
         }
-        Debug("cc:detail") << "bottom\n";
+        Trace("cc:detail") << "bottom\n";
       }
 
       { // use list handling
@@ -606,7 +612,7 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
               i != ul->end();
               ++i) {
             TNode eq = *i;
-            Debug("cc") << "CC  -- useList: " << eq << std::endl;
+            Trace("cc") << "CC  -- useList: " << eq << std::endl;
             Assert(eq.getKind() == kind::EQUAL ||
                    eq.getKind() == kind::IFF);
             // change from paper
@@ -623,21 +629,21 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
               // if lookup(c1',c2') is some f(d1,d2)=d then
               TNode n = lookup(cp);
 
-              Debug("cc:detail") << "CC     -- c' is " << cp << std::endl;
+              Trace("cc:detail") << "CC     -- c' is " << cp << std::endl;
 
               if(!n.isNull()) {
-                Debug("cc:detail") << "CC     -- lookup(c') is " << n << std::endl;
+                Trace("cc:detail") << "CC     -- lookup(c') is " << n << std::endl;
                 // add (f(c1,c2)=c,f(d1,d2)=d) to pending
                 Node tuple = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, n);
-                Debug("cc") << "CC add tuple to pending: " << tuple << std::endl;
+                Trace("cc") << "CC add tuple to pending: " << tuple << std::endl;
                 pending.push_back(tuple);
                 // remove f(c1,c2)=c from UseList(ap)
-                Debug("cc:detail") << "supposed to remove " << eq << std::endl
+                Trace("cc:detail") << "supposed to remove " << eq << std::endl
                                    << "  from UseList of " << ap << std::endl;
                 //i = ul.erase(i);// FIXME do we need to?
               } else {
-                Debug("cc") << "CC     -- lookup(c') is null" << std::endl;
-                Debug("cc") << "CC     -- setlookup(c') to " << eq << std::endl;
+                Trace("cc") << "CC     -- lookup(c') is null" << std::endl;
+                Trace("cc") << "CC     -- setlookup(c') to " << eq << std::endl;
                 // set lookup(c1',c2') to f(c1,c2)=c
                 setLookup(cp, eq);
                 // move f(c1,c2)=c from UseList(ap) to UseList(b')
@@ -648,9 +654,9 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
           }
         }
       }/* use lists */
-      Debug("cc:detail") << "CC in prop done with useList of " << ap << std::endl;
+      Trace("cc:detail") << "CC in prop done with useList of " << ap << std::endl;
     } else {
-      Debug("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl;
+      Trace("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl;
     }
 
     if(Debug.isOn("cc")) {
@@ -679,8 +685,8 @@ void CongruenceClosure<OutputChannel>::merge(TNode ec1, TNode ec2) {
   }
   */
 
-  Debug("cc") << "CC setting rep of " << ec1 << std::endl;
-  Debug("cc") << "CC             to " << ec2 << std::endl;
+  Trace("cc") << "CC setting rep of " << ec1 << std::endl;
+  Trace("cc") << "CC             to " << ec2 << std::endl;
 
   /* can now be applications
   Assert(ec1.getKind() != kind::APPLY_UF);
@@ -691,7 +697,7 @@ void CongruenceClosure<OutputChannel>::merge(TNode ec1, TNode ec2) {
   //Assert(find(ec1) == ec1);
   Assert(find(ec2) == ec2);
 
-  d_representative[ec1] = ec2;
+  d_representative.set(ec1, ec2);
 
   if(d_careSet.find(ec1) != d_careSet.end()) {
     d_careSet.insert(ec2);
@@ -702,18 +708,18 @@ void CongruenceClosure<OutputChannel>::merge(TNode ec1, TNode ec2) {
 
 template <class OutputChannel>
 void CongruenceClosure<OutputChannel>::mergeProof(TNode a, TNode b, TNode e) {
-  Debug("cc") << "  -- merge-proofing " << a << "\n"
+  Trace("cc") << "  -- merge-proofing " << a << "\n"
               << "                and " << b << "\n"
               << "               with " << e << "\n";
 
   // proof forest gets a -> b labeled with e
 
   // first reverse all the edges in proof forest to root of this proof tree
-  Debug("cc") << "CC PROOF reversing proof tree\n";
+  Trace("cc") << "CC PROOF reversing proof tree\n";
   // c and p are child and parent in (old) proof tree
   Node c = a, p = d_proof[a], edgePf = d_proofLabel[a];
   // when we hit null p, we're at the (former) root
-  Debug("cc") << "CC PROOF start at c == " << c << std::endl
+  Trace("cc") << "CC PROOF start at c == " << c << std::endl
               << "                  p == " << p << std::endl
               << "             edgePf == " << edgePf << std::endl;
   while(!p.isNull()) {
@@ -728,7 +734,7 @@ void CongruenceClosure<OutputChannel>::mergeProof(TNode a, TNode b, TNode e) {
     c = p;
     p = pParSave;
     edgePf = pLabelSave;
-    Debug("cc") << "CC PROOF now   at c == " << c << std::endl
+    Trace("cc") << "CC PROOF now   at c == " << c << std::endl
                 << "                  p == " << p << std::endl
                 << "             edgePf == " << edgePf << std::endl;
   }
@@ -742,10 +748,10 @@ void CongruenceClosure<OutputChannel>::mergeProof(TNode a, TNode b, TNode e) {
 template <class OutputChannel>
 Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
   throw(AssertionException) {
-  Debug("cc:detail") << "normalize " << t << std::endl;
+  Trace("cc:detail") << "normalize " << t << std::endl;
   if(t.getKind() != kind::APPLY_UF) {// t is a constant
     t = find(t);
-    Debug("cc:detail") << "  find " << t << std::endl;
+    Trace("cc:detail") << "  find " << t << std::endl;
     return t;
   } else {// t is an apply
     NodeBuilder<> apb(kind::TUPLE);
@@ -761,7 +767,7 @@ Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
     }
 
     Node ap = apb;
-    Debug("cc:detail") << "  got ap " << ap << std::endl;
+    Trace("cc:detail") << "  got ap " << ap << std::endl;
 
     Node theLookup = lookup(ap);
     if(allConstants && !theLookup.isNull()) {
@@ -783,10 +789,13 @@ Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
 }/* normalize() */
 
 
+// This is the find() operation for the auxiliary union-find.  This
+// union-find is not context-dependent, as it's used only during
+// explain().  It does path compression.
 template <class OutputChannel>
-Node CongruenceClosure<OutputChannel>::highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+Node CongruenceClosure<OutputChannel>::highestNode(TNode a, UnionFind_t& unionFind) const
   throw(AssertionException) {
-  __gnu_cxx::hash_map<Node, Node, NodeHashFunction>::iterator i = unionFind.find(a);
+  UnionFind_t::iterator i = unionFind.find(a);
   if(i == unionFind.end()) {
     return a;
   } else {
@@ -796,7 +805,7 @@ Node CongruenceClosure<OutputChannel>::highestNode(TNode a, __gnu_cxx::hash_map<
 
 
 template <class OutputChannel>
-void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list<Node>& pf)
   throw(AssertionException) {
 
   a = highestNode(a, unionFind);
@@ -829,10 +838,27 @@ void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::l
 
 
 template <class OutputChannel>
-Node CongruenceClosure<OutputChannel>::nearestCommonAncestor(TNode a, TNode b)
+Node CongruenceClosure<OutputChannel>::nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind)
   throw(AssertionException) {
+  SeenSet_t seen;
+
   Assert(find(a) == find(b));
-  return find(a); // FIXME
+
+  do {
+    a = highestNode(a, unionFind);
+    seen.insert(a);
+    a = d_proof[a];
+  } while(!a.isNull());
+
+  for(;;) {
+    b = highestNode(b, unionFind);
+    if(seen.find(b) != seen.end()) {
+      return b;
+    }
+    b = d_proof[b];
+
+    Assert(!b.isNull());
+  }
 }/* nearestCommonAncestor() */
 
 
@@ -854,13 +880,13 @@ Node CongruenceClosure<OutputChannel>::explain(Node a, Node b)
     b = replace(flatten(b));
   }
 
-  std::list<std::pair<Node, Node> > pending;
-  __gnu_cxx::hash_map<Node, Node, NodeHashFunction> unionFind;
+  PendingProofList_t pending;
+  UnionFind_t unionFind;
   std::list<Node> terms;
 
   pending.push_back(std::make_pair(a, b));
 
-  Debug("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
+  Trace("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
 
   do {// while(!pending.empty())
     std::pair<Node, Node> eq = pending.front();
@@ -869,29 +895,29 @@ Node CongruenceClosure<OutputChannel>::explain(Node a, Node b)
     a = eq.first;
     b = eq.second;
 
-    Node c = nearestCommonAncestor(a, b);
+    Node c = nearestCommonAncestor(a, b, unionFind);
 
     explainAlongPath(a, c, pending, unionFind, terms);
     explainAlongPath(b, c, pending, unionFind, terms);
   } while(!pending.empty());
 
-  if(Debug.isOn("cc")) {
-    Debug("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl;
+  if(Trace.isOn("cc")) {
+    Trace("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl;
   }
 
   NodeBuilder<> pf(kind::AND);
   while(!terms.empty()) {
     Node p = terms.front();
     terms.pop_front();
-    Debug("cc") << "CC EXPLAIN " << p << std::endl;
+    Trace("cc") << "CC EXPLAIN " << p << std::endl;
     p = proofRewrite(p);
-    Debug("cc") << "   rewrite " << p << std::endl;
+    Trace("cc") << "   rewrite " << p << std::endl;
     if(!p.isNull()) {
       pf << p;
     }
   }
 
-  Debug("cc") << "CC EXPLAIN done" << std::endl;
+  Trace("cc") << "CC EXPLAIN done" << std::endl;
 
   Assert(pf.getNumChildren() > 0);
 
@@ -908,10 +934,10 @@ std::ostream& operator<<(std::ostream& out,
                          const CongruenceClosure<OutputChannel>& cc) {
   out << "==============================================" << std::endl;
 
-  out << "Representatives:" << std::endl;
+  /*out << "Representatives:" << std::endl;
   for(typename CongruenceClosure<OutputChannel>::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) {
     out << "  " << (*i).first << " => " << (*i).second << std::endl;
-  }
+  }*/
 
   out << "ClassLists:" << std::endl;
   for(typename CongruenceClosure<OutputChannel>::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) {