Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

46 files changed, 603 insertions, 309 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index f98f434c1..608d6335b 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -3,9 +3,7 @@ UNIT_TESTS = \
 	theory/shared_term_manager_black \
 	theory/theory_engine_white \
 	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 \
@@ -30,9 +28,12 @@ UNIT_TESTS = \
 	context/cdo_black \
 	context/cdlist_black \
 	context/cdlist_context_memory_black \
+	context/cdcirclist_white \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
+	context/stacking_map_black \
+	context/stacking_vector_black \
 	util/assert_white \
 	util/bitvector_black \
 	util/datatype_black \
diff --git a/test/unit/context/cdcirclist_white.h b/test/unit/context/cdcirclist_white.h
new file mode 100644
index 000000000..b03a850a8
--- /dev/null
+++ b/test/unit/context/cdcirclist_white.h
@@ -0,0 +1,223 @@
+/*********************                                                        */
+/*! \file cdcirclist_white.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, 2011  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 White box testing of CVC4::context::CDCircList<>.
+ **
+ ** White box testing of CVC4::context::CDCircList<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+
+#include <limits.h>
+
+#include "context/context.h"
+#include "context/cdcirclist.h"
+
+#include "util/output.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4;
+
+class CDCircListWhite : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context();
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testSimple() {
+    //Debug.on("cdcirclist");
+    CDCircList<int> l(d_context, ContextMemoryAllocator<int>(d_context->getCMM()));
+
+    TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+
+    d_context->push();
+    {
+      TS_ASSERT(l.empty());
+      l.push_back(1);
+      TS_ASSERT(!l.empty());
+      TS_ASSERT_EQUALS(l.front(), 1);
+      TS_ASSERT_EQUALS(l.back(), 1);
+      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+
+      l.push_back(2);
+      TS_ASSERT(!l.empty());
+      TS_ASSERT_EQUALS(l.front(), 1);
+      TS_ASSERT_EQUALS(l.back(), 2);
+      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+
+      l.push_back(3);
+      TS_ASSERT(!l.empty());
+      TS_ASSERT_EQUALS(l.front(), 1);
+      TS_ASSERT_EQUALS(l.back(), 3);
+      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+
+#ifdef CVC4_ASSERTIONS
+      TS_ASSERT_THROWS( l.concat(l), AssertionException );
+#endif /* CVC4_ASSERTIONS */
+
+      CDCircList<int> l2(d_context, ContextMemoryAllocator<int>(d_context->getCMM()));
+      l2.push_back(4);
+      l2.push_back(5);
+      l2.push_back(6);
+      TS_ASSERT_EQUALS(l2.front(), 4);
+      TS_ASSERT_EQUALS(l2.back(), 6);
+      TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
+
+      d_context->push();
+      {
+        l.concat(l2);
+
+        TS_ASSERT_EQUALS(l.front(), 1);
+        TS_ASSERT_EQUALS(l.back(), 6);
+        TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+
+        TS_ASSERT_EQUALS(l2.front(), 4);
+        TS_ASSERT_EQUALS(l2.back(), 3);
+        TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
+
+        d_context->push();
+        {
+          CDCircList<int>::iterator i = l.begin();
+          CDCircList<int>::iterator j = l.begin();
+          TS_ASSERT_EQUALS(i, j);
+          TS_ASSERT_EQUALS(i++, j);
+          TS_ASSERT_EQUALS(i, ++j);
+          TS_ASSERT_EQUALS(l.erase(l.begin()), i);
+
+          i = l.begin();
+          TS_ASSERT_EQUALS(i, j); TS_ASSERT_DIFFERS(i, l.end());
+          TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
+          TS_ASSERT_EQUALS(*i, 2); TS_ASSERT_DIFFERS(i, l.end());
+          TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j);
+          TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
+          TS_ASSERT_EQUALS(i, l.begin()); TS_ASSERT_EQUALS(i, j);
+
+          TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+          TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
+        }
+        d_context->pop();
+
+        CDCircList<int>::iterator i = l.begin();
+        TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end());
+        TS_ASSERT_EQUALS(i, l.begin());
+
+        i = l2.begin();
+        TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end());
+        TS_ASSERT_EQUALS(i, l2.begin());
+
+        TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+        TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
+      }
+      d_context->pop();
+
+      TS_ASSERT(! l.empty());
+      TS_ASSERT(! l2.empty());
+
+      CDCircList<int>::iterator i = l.begin();
+      TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l.end());
+      TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end());
+      TS_ASSERT_EQUALS(i, l.begin());
+
+      i = l2.begin();
+      TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l2.end());
+      TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end());
+      TS_ASSERT_EQUALS(i, l2.begin());
+
+      TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+      TS_ASSERT_THROWS_NOTHING( l2.debugCheck() );
+    }
+    d_context->pop();
+
+    TS_ASSERT(l.empty());
+    TS_ASSERT_THROWS_NOTHING( l.debugCheck() );
+  }
+
+  void testCDPtr() {
+    int* x = (int*)0x12345678;
+    int* y = (int*)0x87654321;
+    CDPtr<int> p(d_context, NULL);
+    TS_ASSERT(p == NULL);
+    d_context->push();
+    TS_ASSERT(p == NULL);
+    d_context->push();
+    TS_ASSERT(p == NULL);
+    p = x;
+    TS_ASSERT(p == x);
+    d_context->push();
+    TS_ASSERT(p == x);
+    p = y;
+    TS_ASSERT(p == y);
+    d_context->pop();
+    TS_ASSERT(p == x);
+    d_context->pop();
+    TS_ASSERT(p == NULL);
+    d_context->pop();
+    TS_ASSERT(p == NULL);
+  }
+
+};/* class CDCircListWhite */
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 6541973bf..fcc6a7e55 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h
index 2f3c27ddb..a57fd131d 100644
--- a/test/unit/context/cdlist_context_memory_black.h
+++ b/test/unit/context/cdlist_context_memory_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 37beb5054..eb2caa98f 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
index a3abd6f25..42f9b8563 100644
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
index f844c2ef5..6d40a0fb1 100644
--- a/test/unit/context/cdo_black.h
+++ b/test/unit/context/cdo_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h
index 37a285abe..b49186dd0 100644
--- a/test/unit/context/cdvector_black.h
+++ b/test/unit/context/cdvector_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index e5aee4baa..33863e848 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index 126245af7..0e5de3198 100644
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 38649ef5b..9fb94097d 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
new file mode 100644
index 000000000..f0feb1293
--- /dev/null
+++ b/test/unit/context/stacking_map_black.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \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, 2011  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::context::StackingMap
+ **
+ ** Black box testing of CVC4::context::StackingMap.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "context/stacking_map.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the StackingMap.
+ */
+class StackingMapBlack : public CxxTest::TestSuite {
+  Context* d_ctxt;
+  StackingMap<TNode, TNode, TNodeHashFunction>* d_mapPtr;
+  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, NULL);
+    d_scope = new NodeManagerScope(d_nm);
+    d_mapPtr = new StackingMap<TNode, 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_mapPtr;
+    delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
+  }
+
+  void testSimpleContextual() {
+    StackingMap<TNode, TNode, TNodeHashFunction>& d_map = *d_mapPtr;
+
+    TS_ASSERT(d_map[a].isNull());
+    TS_ASSERT(d_map[b].isNull());
+    TS_ASSERT(d_map[c].isNull());
+    TS_ASSERT(d_map[d].isNull());
+    TS_ASSERT(d_map[e].isNull());
+    TS_ASSERT(d_map[f].isNull());
+    TS_ASSERT(d_map[g].isNull());
+
+    d_map.set(a, b);
+
+    TS_ASSERT(d_map[a] == b);
+    TS_ASSERT(d_map[b].isNull());
+    TS_ASSERT(d_map[c].isNull());
+    TS_ASSERT(d_map[d].isNull());
+    TS_ASSERT(d_map[e].isNull());
+    TS_ASSERT(d_map[f].isNull());
+    TS_ASSERT(d_map[g].isNull());
+
+    d_ctxt->push();
+    {
+      TS_ASSERT(d_map[a] == b);
+      TS_ASSERT(d_map[b].isNull());
+      TS_ASSERT(d_map[c].isNull());
+      TS_ASSERT(d_map[d].isNull());
+      TS_ASSERT(d_map[e].isNull());
+      TS_ASSERT(d_map[f].isNull());
+      TS_ASSERT(d_map[g].isNull());
+
+      d_map.set(c, d);
+      d_map.set(f, e);
+
+      TS_ASSERT(d_map[a] == b);
+      TS_ASSERT(d_map[b].isNull());
+      TS_ASSERT(d_map[c] == d);
+      TS_ASSERT(d_map[d].isNull());
+      TS_ASSERT(d_map[e].isNull());
+      TS_ASSERT(d_map[f] == e);
+      TS_ASSERT(d_map[g].isNull());
+
+      d_ctxt->push();
+      {
+
+        TS_ASSERT(d_map[a] == b);
+        TS_ASSERT(d_map[b].isNull());
+        TS_ASSERT(d_map[c] == d);
+        TS_ASSERT(d_map[d].isNull());
+        TS_ASSERT(d_map[e].isNull());
+        TS_ASSERT(d_map[f] == e);
+        TS_ASSERT(d_map[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[a] == c);
+        TS_ASSERT(d_map[b].isNull());
+        TS_ASSERT(d_map[c].isNull());
+        TS_ASSERT(d_map[d].isNull());
+        TS_ASSERT(d_map[e] == d);
+        TS_ASSERT(d_map[f] == f);
+        TS_ASSERT(d_map[g] == a);
+
+      }
+      d_ctxt->pop();
+
+      TS_ASSERT(d_map[a] == b);
+      TS_ASSERT(d_map[b].isNull());
+      TS_ASSERT(d_map[c] == d);
+      TS_ASSERT(d_map[d].isNull());
+      TS_ASSERT(d_map[e].isNull());
+      TS_ASSERT(d_map[f] == e);
+      TS_ASSERT(d_map[g].isNull());
+    }
+    d_ctxt->pop();
+
+    TS_ASSERT(d_map[a] == b);
+    TS_ASSERT(d_map[b].isNull());
+    TS_ASSERT(d_map[c].isNull());
+    TS_ASSERT(d_map[d].isNull());
+    TS_ASSERT(d_map[e].isNull());
+    TS_ASSERT(d_map[f].isNull());
+    TS_ASSERT(d_map[g].isNull());
+  }
+};
diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
new file mode 100644
index 000000000..5f410881b
--- /dev/null
+++ b/test/unit/context/stacking_vector_black.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file stacking_vector_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, 2011  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::context::StackingVector
+ **
+ ** Black box testing of CVC4::context::StackingVector.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "context/stacking_vector.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+
+using namespace std;
+
+/**
+ * Test the StackingVector.
+ */
+class StackingVectorBlack : public CxxTest::TestSuite {
+  Context* d_ctxt;
+  StackingVector<TNode>* d_vectorPtr;
+  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, NULL);
+    d_scope = new NodeManagerScope(d_nm);
+    d_vectorPtr = new StackingVector<TNode>(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_vectorPtr;
+    delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
+  }
+
+  void testSimpleContextual() {
+    StackingVector<TNode>& d_vector = *d_vectorPtr;
+
+    TS_ASSERT(d_vector[1].isNull());
+    TS_ASSERT(d_vector[2].isNull());
+    TS_ASSERT(d_vector[3].isNull());
+    TS_ASSERT(d_vector[4].isNull());
+    TS_ASSERT(d_vector[5].isNull());
+    TS_ASSERT(d_vector[6].isNull());
+    TS_ASSERT(d_vector[7].isNull());
+
+    d_vector.set(1, b);
+
+    TS_ASSERT(d_vector[1] == b);
+    TS_ASSERT(d_vector[2].isNull());
+    TS_ASSERT(d_vector[3].isNull());
+    TS_ASSERT(d_vector[4].isNull());
+    TS_ASSERT(d_vector[5].isNull());
+    TS_ASSERT(d_vector[6].isNull());
+    TS_ASSERT(d_vector[7].isNull());
+
+    d_ctxt->push();
+    {
+      TS_ASSERT(d_vector[1] == b);
+      TS_ASSERT(d_vector[2].isNull());
+      TS_ASSERT(d_vector[3].isNull());
+      TS_ASSERT(d_vector[4].isNull());
+      TS_ASSERT(d_vector[5].isNull());
+      TS_ASSERT(d_vector[6].isNull());
+      TS_ASSERT(d_vector[7].isNull());
+
+      d_vector.set(3, d);
+      d_vector.set(6, e);
+
+      TS_ASSERT(d_vector[1] == b);
+      TS_ASSERT(d_vector[2].isNull());
+      TS_ASSERT(d_vector[3] == d);
+      TS_ASSERT(d_vector[4].isNull());
+      TS_ASSERT(d_vector[5].isNull());
+      TS_ASSERT(d_vector[6] == e);
+      TS_ASSERT(d_vector[7].isNull());
+
+      d_ctxt->push();
+      {
+
+        TS_ASSERT(d_vector[1] == b);
+        TS_ASSERT(d_vector[2].isNull());
+        TS_ASSERT(d_vector[3] == d);
+        TS_ASSERT(d_vector[4].isNull());
+        TS_ASSERT(d_vector[5].isNull());
+        TS_ASSERT(d_vector[6] == e);
+        TS_ASSERT(d_vector[7].isNull());
+
+        d_vector.set(1, c);
+        d_vector.set(6, f);
+        d_vector.set(5, d);
+        d_vector.set(3, Node::null());
+        d_vector.set(7, a);
+
+        TS_ASSERT(d_vector[1] == c);
+        TS_ASSERT(d_vector[2].isNull());
+        TS_ASSERT(d_vector[3].isNull());
+        TS_ASSERT(d_vector[4].isNull());
+        TS_ASSERT(d_vector[5] == d);
+        TS_ASSERT(d_vector[6] == f);
+        TS_ASSERT(d_vector[7] == a);
+
+      }
+      d_ctxt->pop();
+
+      TS_ASSERT(d_vector[1] == b);
+      TS_ASSERT(d_vector[2].isNull());
+      TS_ASSERT(d_vector[3] == d);
+      TS_ASSERT(d_vector[4].isNull());
+      TS_ASSERT(d_vector[5].isNull());
+      TS_ASSERT(d_vector[6] == e);
+      TS_ASSERT(d_vector[7].isNull());
+    }
+    d_ctxt->pop();
+
+    TS_ASSERT(d_vector[1] == b);
+    TS_ASSERT(d_vector[2].isNull());
+    TS_ASSERT(d_vector[3].isNull());
+    TS_ASSERT(d_vector[4].isNull());
+    TS_ASSERT(d_vector[5].isNull());
+    TS_ASSERT(d_vector[6].isNull());
+    TS_ASSERT(d_vector[7].isNull());
+  }
+};
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index a324bbbf1..8e7f89795 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: taking
  ** Minor contributors (to current version): cconway, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h
index b1e77c614..bde04157c 100644
--- a/test/unit/expr/declaration_scope_black.h
+++ b/test/unit/expr/declaration_scope_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index e37c197ab..e709648c9 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 32e8da287..853d0086b 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway, dejan
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
index 314108a5b..5cf4ba30a 100644
--- a/test/unit/expr/kind_black.h
+++ b/test/unit/expr/kind_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6bd5aa1fd..40545e5e8 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: taking
  ** Minor contributors (to current version): cconway, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index c084c4ecb..c6d6d815e 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e6ebc6724..c30e4badb 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 95d3271f2..735fe2ac8 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index e97407dfc..9cc09f884 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 9d6311acb..ce67004c6 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index e56e8de8a..7773644da 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -2,10 +2,10 @@
 /*! \file interactive_shell_black.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 6da3c08b5..19b45c05d 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 06b09f2ce..0f0dc5fbd 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index c45740da9..8fb96c74a 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -2,10 +2,10 @@
 /*! \file cnf_stream_black.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index 0e8f5addb..1be116517 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: barrett
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): cconway, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
index c60da2922..d70aa8c22 100644
--- a/test/unit/theory/stacking_map_black.h
+++ b/test/unit/theory/stacking_map_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index fb82a7ac9..ded7cee97 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): barrett, mdeters
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 2d39af956..ff6b352d0 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: barrett, mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index f1a83cd49..a1b058eeb 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -2,10 +2,10 @@
 /*! \file theory_engine_white.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): barrett, cconway
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h
deleted file mode 100644
index ae3eee369..000000000
--- a/test/unit/theory/theory_uf_tim_white.h
+++ /dev/null
@@ -1,252 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_tim_white.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: barrett
- ** Minor contributors (to current version): cconway, dejan, mdeters
- ** 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 White box testing of CVC4::theory::uf::tim::TheoryUFTim.
- **
- ** White box testing of CVC4::theory::uf::tim::TheoryUFTim.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "theory/theory.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/tim/theory_uf_tim.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
-#include "theory/theory_test_utils.h"
-
-#include <vector>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-using namespace CVC4::theory::uf::tim;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-
-using namespace std;
-
-
-class TheoryUFTimWhite : public CxxTest::TestSuite {
-
-  Context* d_ctxt;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-
-  TestOutputChannel d_outputChannel;
-  Theory::Effort d_level;
-
-  TheoryUFTim* d_euf;
-
-  TypeNode* d_booleanType;
-
-public:
-
-  TheoryUFTimWhite() : d_level(Theory::FULL_EFFORT) {}
-
-  void setUp() {
-    d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_outputChannel.clear();
-    d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL));
-
-    d_booleanType = new TypeNode(d_nm->booleanType());
-  }
-
-  void tearDown() {
-    delete d_booleanType;
-    delete d_euf;
-    d_outputChannel.clear();
-    delete d_scope;
-    delete d_nm;
-    delete d_ctxt;
-  }
-
-  void testPushPopSimple() {
-    TypeNode t = d_nm->mkSort();
-    Node x = d_nm->mkVar(t);
-    Node x_eq_x = x.eqNode(x);
-
-    d_ctxt->push();
-    d_ctxt->pop();
-  }
-
-// FIXME: This is broken because of moving registration into theory_engine @CB
-// //   void testPushPopChain() {
-// //     Node x = d_nm->mkVar(*d_booleanType);
-// //     Node f = d_nm->mkVar(*d_booleanType);
-// //     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// //     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-// //     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-// //     Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
-// //     Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x);
-
-// //     Node f3_x_eq_x = f_f_f_x.eqNode(x);
-// //     Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x);
-// //     Node f1_x_neq_x = f_x.eqNode(x).notNode();
-
-// //     Node expectedConflict = d_nm->mkNode(kind::AND,
-// //                                          f1_x_neq_x,
-// //                                          f3_x_eq_x,
-// //                                          f5_x_eq_x
-// //                                          );
-
-// //     d_euf->assertFact( f3_x_eq_x );
-// //     d_euf->assertFact( f1_x_neq_x );
-// //     d_euf->check(d_level);
-// //     d_ctxt->push();
-
-// //     d_euf->assertFact( f5_x_eq_x );
-// //     d_euf->check(d_level);
-
-// //     TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-// //     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-// //     Node realConflict = d_outputChannel.getIthNode(0);
-// //     TS_ASSERT_EQUALS(expectedConflict, realConflict);
-
-// //     d_ctxt->pop();
-// //     d_euf->check(d_level);
-
-// //     //Test that no additional calls to the output channel occurred.
-// //     TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-
-// //     d_euf->assertFact( f5_x_eq_x );
-
-// //     d_euf->check(d_level);
-
-// //     TS_ASSERT_EQUALS(2u, d_outputChannel.getNumCalls());
-// //     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-// //     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1));
-// //     Node  firstConflict = d_outputChannel.getIthNode(0);
-// //     Node secondConflict = d_outputChannel.getIthNode(1);
-// //     TS_ASSERT_EQUALS(expectedConflict,  firstConflict);
-// //     TS_ASSERT_EQUALS(expectedConflict, secondConflict);
-
-// //   }
-
-
-
-//   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
-//   void testSimpleChain() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node f = d_nm->mkVar(*d_booleanType);
-//     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-//     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-//     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-
-//     Node f_f_x_eq_x = f_f_x.eqNode(x);
-//     Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode();
-
-//     Node expectedConflict = f_f_f_x_neq_f_x.andNode(f_f_x_eq_x);
-
-//     d_euf->assertFact(f_f_x_eq_x);
-//     d_euf->assertFact(f_f_f_x_neq_f_x);
-//     d_euf->check(d_level);
-
-//     TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-//     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-
-//     Node realConflict = d_outputChannel.getIthNode(0);
-//     TS_ASSERT_EQUALS(expectedConflict, realConflict);
-
-//   }
-
-  /* test that !(x == x) is inconsistent */
-//   void testSelfInconsistent() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node x_neq_x = (x.eqNode(x)).notNode();
-
-//     d_euf->assertFact(x_neq_x);
-//     d_euf->check(d_level);
-
-//     TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-//     TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0));
-//     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-//   }
-
-//   /* test that (x == x) is consistent */
-//   void testSelfConsistent() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node x_eq_x = x.eqNode(x);
-
-//     d_euf->assertFact(x_eq_x);
-//     d_euf->check(d_level);
-
-//     TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls());
-//   }
-
-
-//   /* test that
-//      {f(f(f(x))) == x,
-//       f(f(f(f(f(x))))) = x,
-//       f(x) != x
-//      } is inconsistent */
-//   void testChain() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node f = d_nm->mkVar(*d_booleanType);
-//     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-//     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-//     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-//     Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
-//     Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x);
-
-//     Node f3_x_eq_x = f_f_f_x.eqNode(x);
-//     Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x);
-//     Node f1_x_neq_x = f_x.eqNode(x).notNode();
-
-//     Node expectedConflict = d_nm->mkNode(kind::AND,
-//                                          f1_x_neq_x,
-//                                          f3_x_eq_x,
-//                                          f5_x_eq_x
-//                                          );
-
-//     d_euf->assertFact( f3_x_eq_x );
-//     d_euf->assertFact( f5_x_eq_x );
-//     d_euf->assertFact( f1_x_neq_x );
-//     d_euf->check(d_level);
-
-//     TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-//     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-//     Node realConflict = d_outputChannel.getIthNode(0);
-//     TS_ASSERT_EQUALS(expectedConflict, realConflict);
-//   }
-
-
-//   void testPushPopA() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node x_eq_x = x.eqNode(x);
-
-//     d_ctxt->push();
-//     d_euf->assertFact( x_eq_x );
-//     d_euf->check(d_level);
-//     d_ctxt->pop();
-//     d_euf->check(d_level);
-//   }
-
-//   void testPushPopB() {
-//     Node x = d_nm->mkVar(*d_booleanType);
-//     Node f = d_nm->mkVar(*d_booleanType);
-//     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-//     Node f_x_eq_x = f_x.eqNode(x);
-
-//     d_euf->assertFact( f_x_eq_x );
-//     d_ctxt->push();
-//     d_euf->check(d_level);
-//     d_ctxt->pop();
-//     d_euf->check(d_level);
-//   }
-
-};
diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
index 6ba653946..fead619d2 100644
--- a/test/unit/theory/union_find_black.h
+++ b/test/unit/theory/union_find_black.h
@@ -5,25 +5,25 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
+ ** \brief Black box testing of CVC4::datatypes::UnionFind
  **
- ** Black box testing of CVC4::theory::uf::morgan::UnionFind.
+ ** Black box testing of CVC4::theory::datatypes::UnionFind.
  **/
 
 #include <cxxtest/TestSuite.h>
 
 #include "context/context.h"
 #include "expr/node.h"
-#include "theory/uf/morgan/union_find.h"
+#include "theory/datatypes/union_find.h"
 
 using namespace CVC4;
-using namespace CVC4::theory::uf::morgan;
+using namespace CVC4::theory::datatypes;
 using namespace CVC4::context;
 
 using namespace std;
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 6a8438136..6d88f89bd 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h
index e06fe9636..faafb28f7 100644
--- a/test/unit/util/configuration_black.h
+++ b/test/unit/util/configuration_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h
index f5e299377..187b7dc08 100644
--- a/test/unit/util/congruence_closure_white.h
+++ b/test/unit/util/congruence_closure_white.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 485820a61..ea8d8a900 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): ajreynol
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
index 2bbd727fb..f92b6af93 100644
--- a/test/unit/util/exception_black.h
+++ b/test/unit/util/exception_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 5b8397f66..92846bdf1 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -2,10 +2,10 @@
 /*! \file integer_black.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h
index 1c6b03cdf..284c94670 100644
--- a/test/unit/util/integer_white.h
+++ b/test/unit/util/integer_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h
index dcae800d1..66d119567 100644
--- a/test/unit/util/rational_black.h
+++ b/test/unit/util/rational_black.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h
index 2fcb33642..b5d120c52 100644
--- a/test/unit/util/rational_white.h
+++ b/test/unit/util/rational_white.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index d32ef828c..7ba88edc6 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h
index dfa066194..251e47a17 100644
--- a/test/unit/util/trans_closure_black.h
+++ b/test/unit/util/trans_closure_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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