From 774af8c91c94f74fec03bc60a4c29abf60f4a5de Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 5 Jan 2016 17:35:12 -0800 Subject: [PATCH] Removing dead code. StackingMap only appeared in unit tests. --- src/Makefile.am | 1 - src/context/stacking_map.h | 162 ------------------------- test/unit/Makefile.am | 1 - test/unit/context/stacking_map_black.h | 159 ------------------------ test/unit/theory/stacking_map_black.h | 158 ------------------------ 5 files changed, 481 deletions(-) delete mode 100644 src/context/stacking_map.h delete mode 100644 test/unit/context/stacking_map_black.h delete mode 100644 test/unit/theory/stacking_map_black.h diff --git a/src/Makefile.am b/src/Makefile.am index d5223773e..f16c5408b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -54,7 +54,6 @@ libcvc4_la_SOURCES = \ context/cdhashset_forward.h \ context/cdvector.h \ context/cdmaybe.h \ - context/stacking_map.h \ context/stacking_vector.h \ context/cddense_set.h \ decision/decision_attributes.h \ diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h deleted file mode 100644 index 4ce1b2d33..000000000 --- a/src/context/stacking_map.h +++ /dev/null @@ -1,162 +0,0 @@ -/********************* */ -/*! \file stacking_map.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic - ** 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 Backtrackable map using an undo stack - ** - ** Backtrackable map using an undo stack rather than storing items in - ** a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__STACKING_MAP_H -#define __CVC4__CONTEXT__STACKING_MAP_H - -#include -#include -#include - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { -namespace context { - -template -struct StackingMapArgType { - typedef T argtype; -};/* struct StackingMapArgType */ - -template <> -struct StackingMapArgType { - typedef TNode argtype; -};/* struct StackingMapArgType */ - - -template -struct StackingMapRestoreValue { - typedef typename StackingMapArgType::argtype ArgType; - static void restore(__gnu_cxx::hash_map& map, const ArgType& k, const ValueType& v) { - map[k] = v; - } -};/* struct StackingMapRestoreValue */ - -template -struct StackingMapRestoreValue { - typedef typename StackingMapArgType::argtype ArgType; - static void restore(__gnu_cxx::hash_map& map, const ArgType& k, TNode v) { - if(v.isNull()) { - map.erase(k); - } else { - map[k] = v; - } - } -};/* struct StackingMapRestoreValue */ - -template -struct StackingMapRestoreValue { - typedef typename StackingMapArgType::argtype ArgType; - static void restore(__gnu_cxx::hash_map& map, const ArgType& k, TNode v) { - if(v.isNull()) { - map.erase(k); - } else { - map[k] = v; - } - } -};/* struct StackingMapRestoreValue */ - - -template -class StackingMap : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map MapType; - - /** - * The type for arguments being passed in. It's the same as - * KeyType, unless KeyType is Node, then it's TNode for efficiency. - */ - typedef typename StackingMapArgType::argtype ArgType; - - /** Our map of keys to their values. */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO d_offset; - -protected: - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::contextNotifyPop(). - */ - void contextNotifyPop(); - -public: - typedef typename MapType::const_iterator const_iterator; - - StackingMap(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~StackingMap() throw() { } - - const_iterator find(ArgType n) const { return d_map.find(n); } - const_iterator end() const { return d_map.end(); } - - /** - * Return a key's value in the key-value map. If n is not a key in - * the map, this function returns a default-constructed value. - */ - ValueType operator[](ArgType n) const { - const_iterator it = find(n); - if(it == end()) { - return ValueType(); - } else { - return (*it).second; - } - } - //ValueType& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic - - /** - * Set the value in the key-value map for Node n to newValue. - */ - void set(ArgType n, const ValueType& newValue); - -};/* class StackingMap<> */ - -template -void StackingMap::set(ArgType n, const ValueType& newValue) { - Trace("sm") << "SM setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl; - ValueType& ref = d_map[n]; - d_trace.push_back(std::make_pair(n, ValueType(ref))); - d_offset = d_trace.size(); - ref = newValue; -} - -template -void StackingMap::contextNotifyPop() { - Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; - while(d_offset < d_trace.size()) { - std::pair p = d_trace.back(); - StackingMapRestoreValue::restore(d_map, p.first, p.second); - d_trace.pop_back(); - } - Trace("sm") << "SM cancelling finished." << std::endl; -} - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__CONTEXT__STACKING_MAP_H */ 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 - -#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* 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(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& 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 - -#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* 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(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()); - } -}; -- 2.30.2