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.

12 files changed, 554 insertions, 9 deletions

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());
+  }
+};