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.

8 files changed, 405 insertions, 29 deletions

diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am
index e9faa88df..886178a6f 100644
--- 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
index 000000000..16a85e71b
--- /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
index 000000000..c54acc363
--- /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 4ee698721..cc0296d0a 100644
--- 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 569f9bb49..d26e6ff8f 100644
--- 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
index 000000000..135320707
--- /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
index 000000000..b848be526
--- /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 44f061c12..73033f387 100644
--- 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
   }
 
   /**