diff options
author | Tim King <taking@google.com> | 2016-01-05 17:35:12 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 17:35:12 -0800 |
commit | 774af8c91c94f74fec03bc60a4c29abf60f4a5de (patch) | |
tree | 42cd0f25fe56df45a1916677ea5da3e780d76922 /test | |
parent | b5f91dae58691468f6c8f2d7c6aebf639f1d017b (diff) |
Removing dead code. StackingMap only appeared in unit tests.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/context/stacking_map_black.h | 159 | ||||
-rw-r--r-- | test/unit/theory/stacking_map_black.h | 158 |
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()); - } -}; |