Removing dead code. StackingMap only appeared in unit tests.

3 files changed, 0 insertions, 318 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 98bedefbf..36203725f 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -37,7 +37,6 @@ UNIT_TESTS += \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
-	context/stacking_map_black \
 	context/stacking_vector_black \
 	util/array_store_all_black \
 	util/assert_white \
diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
deleted file mode 100644
index 4daab5cce..000000000
--- a/test/unit/context/stacking_map_black.h
+++ /dev/null
@@ -1,159 +0,0 @@
-/*********************                                                        */
-/*! \file stacking_map_black.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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(NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(d_ctxt);
-
-    a = d_nm->mkSkolem("a", d_nm->realType());
-    b = d_nm->mkSkolem("b", d_nm->realType());
-    c = d_nm->mkSkolem("c", d_nm->realType());
-    d = d_nm->mkSkolem("d", d_nm->realType());
-    e = d_nm->mkSkolem("e", d_nm->realType());
-    f = d_nm->mkSkolem("f", d_nm->realType());
-    g = d_nm->mkSkolem("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/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
deleted file mode 100644
index 8097220ad..000000000
--- a/test/unit/theory/stacking_map_black.h
+++ /dev/null
@@ -1,158 +0,0 @@
-/*********************                                                        */
-/*! \file stacking_map_black.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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, NULL);
-    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());
-  }
-};