From 88b9d2b384f6625df3853a64b240e3cf1f3a19aa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 7 Jul 2017 15:25:04 -0700 Subject: [PATCH] Remove unused stacking_vector class (#185) --- src/Makefile.am | 1 - src/context/stacking_vector.h | 114 ---------------- test/unit/Makefile.am | 1 - test/unit/context/stacking_vector_black.h | 159 ---------------------- 4 files changed, 275 deletions(-) delete mode 100644 src/context/stacking_vector.h delete mode 100644 test/unit/context/stacking_vector_black.h diff --git a/src/Makefile.am b/src/Makefile.am index e44bd920c..157fe33d2 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -55,7 +55,6 @@ libcvc4_la_SOURCES = \ context/context.h \ context/context_mm.cpp \ context/context_mm.h \ - context/stacking_vector.h \ decision/decision_attributes.h \ decision/decision_engine.cpp \ decision/decision_engine.h \ diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h deleted file mode 100644 index 5ef0404e4..000000000 --- a/src/context/stacking_vector.h +++ /dev/null @@ -1,114 +0,0 @@ -/********************* */ -/*! \file stacking_vector.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Backtrackable vector using an undo stack - ** - ** Backtrackable vector using an undo stack rather than storing items in - ** a CDVector<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__STACKING_VECTOR_H -#define __CVC4__CONTEXT__STACKING_VECTOR_H - -#include -#include - -#include "context/cdo.h" - -namespace CVC4 { -namespace context { - -template -class StackingVector : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef std::vector VectorType; - - /** Our map of indices to their values. */ - VectorType 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; - -public: - typedef typename VectorType::const_iterator const_iterator; - - StackingVector(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~StackingVector() { } - - /** - * Return a value from the vector. If n is not a key in - * the map, this function returns a default-constructed T. - */ - T operator[](size_t n) const { - return n < d_map.size() ? d_map[n] : T(); - } - //T& 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(size_t n, const T& newValue); - - /** - * Return the current size of the vector. Note that once a certain - * size is achieved, the size never goes down again, although the - * elements off the old end of the vector will be replaced with - * default-constructed T values. - */ - size_t size() const { - return d_map.size(); - } - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void contextNotifyPop(); - -};/* class StackingVector<> */ - -template -void StackingVector::set(size_t n, const T& newValue) { - Trace("sv") << "SV setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl; - if(n >= d_map.size()) { - d_map.resize(n + 1); - } - T& ref = d_map[n]; - d_trace.push_back(std::make_pair(n, T(ref))); - d_offset = d_trace.size(); - ref = newValue; -} - -template -void StackingVector::contextNotifyPop() { - Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; - while(d_offset < d_trace.size()) { - std::pair p = d_trace.back(); - Trace("sv") << "SV cancelling: " << p.first << " back to " << p.second << std::endl; - d_map[p.first] = p.second; - d_trace.pop_back(); - } - Trace("sv") << "SV cancelling finished." << std::endl; -} - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__CONTEXT__STACKING_VECTOR_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 129d086df..c2f2b24e2 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_vector_black \ util/array_store_all_black \ util/assert_white \ util/binary_heap_black \ diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h deleted file mode 100644 index 0dd96ea57..000000000 --- a/test/unit/context/stacking_vector_black.h +++ /dev/null @@ -1,159 +0,0 @@ -/********************* */ -/*! \file stacking_vector_black.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 - -#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* 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(NULL); - d_scope = new NodeManagerScope(d_nm); - d_vectorPtr = new StackingVector(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_vectorPtr; - delete d_scope; - delete d_nm; - delete d_ctxt; - } - - void testSimpleContextual() { - StackingVector& 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()); - } -}; -- 2.30.2