Merge from ufprop branch, including:

* Theory::staticLearning() for statically adding new T-stuff before
  normal preprocessing.  UF's staticLearning() does transitivity of
  equality/iff, solving the diamonds.

* more aggressive T-propagation for UF

* new KEEP_STATISTIC macro to hide Theories from having to
  register/deregister statistics (and also has the advantage of
  keeping the statistic type, field name, and the 'tag' used to output
  the statistic in the same place---instead of scattered in the theory
  definition and constructor initializer list.  See documentation for
  KEEP_STATISTIC in src/util/stats.h for more of an explanation).

* more statistics for UF

* restart notifications from SAT (through TheoryEngine) via
  Theory::notifyRestart()

* StackingMap and UnionFind unit tests

* build fixes/adjustments

* code cleanup; minor other improvements

4 files changed, 352 insertions, 0 deletions

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 1471d8814..2e05386e0 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -19,6 +19,7 @@ TESTS =	\
 	eq_diamond1.smt \
 	eq_diamond14.reduced.smt \
 	eq_diamond14.reduced2.smt \
+	eq_diamond23.smt \
 	NEQ016_size5_reduced2a.smt \
 	NEQ016_size5_reduced2b.smt \
 	dead_dnd002.smt \
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 3583770b6..725d4a4bb 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -5,6 +5,8 @@ UNIT_TESTS = \
 	theory/theory_black \
 	theory/theory_uf_tim_white \
 	theory/theory_arith_white \
+	theory/stacking_map_black \
+	theory/union_find_black \
 	expr/expr_public \
         expr/expr_manager_public \
 	expr/node_white \
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
new file mode 100644
index 000000000..39dad4732
--- /dev/null
+++ b/test/unit/theory/stacking_map_black.h
@@ -0,0 +1,160 @@
+/*********************                                                        */
+/*! \file stacking_map_black.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 Black box testing of CVC4::theory::uf::morgan::StackingMap
+ **
+ ** Black box testing of CVC4::theory::uf::morgan::StackingMap.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/uf/morgan/stacking_map.h"
+
+using namespace CVC4;
+using namespace CVC4::theory::uf::morgan;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the StackingMap.
+ */
+class StackingMapBlack : public CxxTest::TestSuite {
+  Context* d_ctxt;
+  StackingMap<TNode, TNodeHashFunction>* d_map;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+
+  Node a, b, c, d, e, f, g;
+
+public:
+
+  void setUp() {
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
+    d_scope = new NodeManagerScope(d_nm);
+    d_map = new StackingMap<TNode, TNodeHashFunction>(d_ctxt);
+
+    a = d_nm->mkVar("a", d_nm->realType());
+    b = d_nm->mkVar("b", d_nm->realType());
+    c = d_nm->mkVar("c", d_nm->realType());
+    d = d_nm->mkVar("d", d_nm->realType());
+    e = d_nm->mkVar("e", d_nm->realType());
+    f = d_nm->mkVar("f", d_nm->realType());
+    g = d_nm->mkVar("g", d_nm->realType());
+  }
+
+  void tearDown() {
+    g = Node::null();
+    f = Node::null();
+    e = Node::null();
+    d = Node::null();
+    c = Node::null();
+    b = Node::null();
+    a = Node::null();
+
+    delete d_map;
+    delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
+  }
+
+  void testSimpleContextual() {
+    TS_ASSERT(d_map->find(a).isNull());
+    TS_ASSERT(d_map->find(b).isNull());
+    TS_ASSERT(d_map->find(c).isNull());
+    TS_ASSERT(d_map->find(d).isNull());
+    TS_ASSERT(d_map->find(e).isNull());
+    TS_ASSERT(d_map->find(f).isNull());
+    TS_ASSERT(d_map->find(g).isNull());
+
+    d_map->set(a, b);
+
+    TS_ASSERT(d_map->find(a) == b);
+    TS_ASSERT(d_map->find(b).isNull());
+    TS_ASSERT(d_map->find(c).isNull());
+    TS_ASSERT(d_map->find(d).isNull());
+    TS_ASSERT(d_map->find(e).isNull());
+    TS_ASSERT(d_map->find(f).isNull());
+    TS_ASSERT(d_map->find(g).isNull());
+
+    d_ctxt->push();
+    {
+      TS_ASSERT(d_map->find(a) == b);
+      TS_ASSERT(d_map->find(b).isNull());
+      TS_ASSERT(d_map->find(c).isNull());
+      TS_ASSERT(d_map->find(d).isNull());
+      TS_ASSERT(d_map->find(e).isNull());
+      TS_ASSERT(d_map->find(f).isNull());
+      TS_ASSERT(d_map->find(g).isNull());
+
+      d_map->set(c, d);
+      d_map->set(f, e);
+
+      TS_ASSERT(d_map->find(a) == b);
+      TS_ASSERT(d_map->find(b).isNull());
+      TS_ASSERT(d_map->find(c) == d);
+      TS_ASSERT(d_map->find(d).isNull());
+      TS_ASSERT(d_map->find(e).isNull());
+      TS_ASSERT(d_map->find(f) == e);
+      TS_ASSERT(d_map->find(g).isNull());
+
+      d_ctxt->push();
+      {
+
+        TS_ASSERT(d_map->find(a) == b);
+        TS_ASSERT(d_map->find(b).isNull());
+        TS_ASSERT(d_map->find(c) == d);
+        TS_ASSERT(d_map->find(d).isNull());
+        TS_ASSERT(d_map->find(e).isNull());
+        TS_ASSERT(d_map->find(f) == e);
+        TS_ASSERT(d_map->find(g).isNull());
+
+        d_map->set(a, c);
+        d_map->set(f, f);
+        d_map->set(e, d);
+        d_map->set(c, Node::null());
+        d_map->set(g, a);
+
+        TS_ASSERT(d_map->find(a) == c);
+        TS_ASSERT(d_map->find(b).isNull());
+        TS_ASSERT(d_map->find(c).isNull());
+        TS_ASSERT(d_map->find(d).isNull());
+        TS_ASSERT(d_map->find(e) == d);
+        TS_ASSERT(d_map->find(f) == f);
+        TS_ASSERT(d_map->find(g) == a);
+
+      }
+      d_ctxt->pop();
+
+      TS_ASSERT(d_map->find(a) == b);
+      TS_ASSERT(d_map->find(b).isNull());
+      TS_ASSERT(d_map->find(c) == d);
+      TS_ASSERT(d_map->find(d).isNull());
+      TS_ASSERT(d_map->find(e).isNull());
+      TS_ASSERT(d_map->find(f) == e);
+      TS_ASSERT(d_map->find(g).isNull());
+    }
+    d_ctxt->pop();
+
+    TS_ASSERT(d_map->find(a) == b);
+    TS_ASSERT(d_map->find(b).isNull());
+    TS_ASSERT(d_map->find(c).isNull());
+    TS_ASSERT(d_map->find(d).isNull());
+    TS_ASSERT(d_map->find(e).isNull());
+    TS_ASSERT(d_map->find(f).isNull());
+    TS_ASSERT(d_map->find(g).isNull());
+  }
+};
diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
new file mode 100644
index 000000000..b9b4e58ce
--- /dev/null
+++ b/test/unit/theory/union_find_black.h
@@ -0,0 +1,189 @@
+/*********************                                                        */
+/*! \file union_find_black.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 Black box testing of CVC4::theory::uf::morgan::UnionFind
+ **
+ ** Black box testing of CVC4::theory::uf::morgan::UnionFind.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/uf/morgan/union_find.h"
+
+using namespace CVC4;
+using namespace CVC4::theory::uf::morgan;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the UnionFind.
+ */
+class UnionFindBlack : public CxxTest::TestSuite {
+  Context* d_ctxt;
+  UnionFind<TNode, TNodeHashFunction>* d_uf;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+
+  Node a, b, c, d, e, f, g;
+
+public:
+
+  void setUp() {
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
+    d_scope = new NodeManagerScope(d_nm);
+    d_uf = new UnionFind<TNode, TNodeHashFunction>(d_ctxt);
+
+    a = d_nm->mkVar("a", d_nm->realType());
+    b = d_nm->mkVar("b", d_nm->realType());
+    c = d_nm->mkVar("c", d_nm->realType());
+    d = d_nm->mkVar("d", d_nm->realType());
+    e = d_nm->mkVar("e", d_nm->realType());
+    f = d_nm->mkVar("f", d_nm->realType());
+    g = d_nm->mkVar("g", d_nm->realType());
+  }
+
+  void tearDown() {
+    g = Node::null();
+    f = Node::null();
+    e = Node::null();
+    d = Node::null();
+    c = Node::null();
+    b = Node::null();
+    a = Node::null();
+
+    delete d_uf;
+    delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
+  }
+
+  void testSimpleContextual() {
+    TS_ASSERT(d_uf->find(a) == a);
+    TS_ASSERT(d_uf->find(b) == b);
+    TS_ASSERT(d_uf->find(c) == c);
+    TS_ASSERT(d_uf->find(d) == d);
+    TS_ASSERT(d_uf->find(e) == e);
+    TS_ASSERT(d_uf->find(f) == f);
+    TS_ASSERT(d_uf->find(g) == g);
+
+    d_ctxt->push();
+
+    d_uf->setCanon(a, b);
+
+    TS_ASSERT(d_uf->find(a) == b);
+    TS_ASSERT(d_uf->find(b) == b);
+    TS_ASSERT(d_uf->find(c) == c);
+    TS_ASSERT(d_uf->find(d) == d);
+    TS_ASSERT(d_uf->find(e) == e);
+    TS_ASSERT(d_uf->find(f) == f);
+    TS_ASSERT(d_uf->find(g) == g);
+
+    d_ctxt->push();
+    {
+      TS_ASSERT(d_uf->find(a) == b);
+      TS_ASSERT(d_uf->find(b) == b);
+      TS_ASSERT(d_uf->find(c) == c);
+      TS_ASSERT(d_uf->find(d) == d);
+      TS_ASSERT(d_uf->find(e) == e);
+      TS_ASSERT(d_uf->find(f) == f);
+      TS_ASSERT(d_uf->find(g) == g);
+
+      d_uf->setCanon(c, d);
+      d_uf->setCanon(f, e);
+
+      TS_ASSERT(d_uf->find(a) == b);
+      TS_ASSERT(d_uf->find(b) == b);
+      TS_ASSERT(d_uf->find(c) == d);
+      TS_ASSERT(d_uf->find(d) == d);
+      TS_ASSERT(d_uf->find(e) == e);
+      TS_ASSERT(d_uf->find(f) == e);
+      TS_ASSERT(d_uf->find(g) == g);
+
+      d_ctxt->push();
+      {
+
+        TS_ASSERT(d_uf->find(a) == b);
+        TS_ASSERT(d_uf->find(b) == b);
+        TS_ASSERT(d_uf->find(c) == d);
+        TS_ASSERT(d_uf->find(d) == d);
+        TS_ASSERT(d_uf->find(e) == e);
+        TS_ASSERT(d_uf->find(f) == e);
+        TS_ASSERT(d_uf->find(g) == g);
+
+#ifdef CVC4_ASSERTIONS
+        TS_ASSERT_THROWS(d_uf->setCanon(a, c), AssertionException);
+        TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(a), c), AssertionException);
+        TS_ASSERT_THROWS(d_uf->setCanon(a, d_uf->find(c)), AssertionException);
+#endif /* CVC4_ASSERTIONS */
+        d_uf->setCanon(d_uf->find(a), d_uf->find(c));
+        d_uf->setCanon(d_uf->find(f), g);
+        d_uf->setCanon(d_uf->find(e), d);
+#ifdef CVC4_ASSERTIONS
+        TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(c), f), AssertionException);
+#endif /* CVC4_ASSERTIONS */
+        d_uf->setCanon(d_uf->find(c), d_uf->find(f));
+
+        TS_ASSERT(d_uf->find(a) == d);
+        TS_ASSERT(d_uf->find(b) == d);
+        TS_ASSERT(d_uf->find(c) == d);
+        TS_ASSERT(d_uf->find(d) == d);
+        TS_ASSERT(d_uf->find(e) == d);
+        TS_ASSERT(d_uf->find(f) == d);
+        TS_ASSERT(d_uf->find(g) == d);
+
+        d_uf->setCanon(d_uf->find(g), d_uf->find(a));
+
+        TS_ASSERT(d_uf->find(a) == d);
+        TS_ASSERT(d_uf->find(b) == d);
+        TS_ASSERT(d_uf->find(c) == d);
+        TS_ASSERT(d_uf->find(d) == d);
+        TS_ASSERT(d_uf->find(e) == d);
+        TS_ASSERT(d_uf->find(f) == d);
+        TS_ASSERT(d_uf->find(g) == d);
+
+      }
+      d_ctxt->pop();
+
+      TS_ASSERT(d_uf->find(a) == b);
+      TS_ASSERT(d_uf->find(b) == b);
+      TS_ASSERT(d_uf->find(c) == d);
+      TS_ASSERT(d_uf->find(d) == d);
+      TS_ASSERT(d_uf->find(e) == e);
+      TS_ASSERT(d_uf->find(f) == e);
+      TS_ASSERT(d_uf->find(g) == g);
+    }
+    d_ctxt->pop();
+
+    TS_ASSERT(d_uf->find(a) == b);
+    TS_ASSERT(d_uf->find(b) == b);
+    TS_ASSERT(d_uf->find(c) == c);
+    TS_ASSERT(d_uf->find(d) == d);
+    TS_ASSERT(d_uf->find(e) == e);
+    TS_ASSERT(d_uf->find(f) == f);
+    TS_ASSERT(d_uf->find(g) == g);
+
+    d_ctxt->pop();
+
+    TS_ASSERT(d_uf->find(a) == a);
+    TS_ASSERT(d_uf->find(b) == b);
+    TS_ASSERT(d_uf->find(c) == c);
+    TS_ASSERT(d_uf->find(d) == d);
+    TS_ASSERT(d_uf->find(e) == e);
+    TS_ASSERT(d_uf->find(f) == f);
+    TS_ASSERT(d_uf->find(g) == g);
+  }
+};