From: Andres Noetzli Date: Wed, 4 Jul 2018 10:58:24 +0000 (-0700) Subject: Remove unused CDVector (#2139) X-Git-Tag: cvc5-1.0.0~4917 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=714ede2487fb58ea46858380eecfff72c2e2d4ac;p=cvc5.git Remove unused CDVector (#2139) --- diff --git a/src/Makefile.am b/src/Makefile.am index b4a083b0a..b5da564cf 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -54,7 +54,6 @@ libcvc4_la_SOURCES = \ context/cdtrail_hashmap.h \ context/cdtrail_hashmap_forward.h \ context/cdtrail_queue.h \ - context/cdvector.h \ context/context.cpp \ context/context.h \ context/context_mm.cpp \ diff --git a/src/context/cdvector.h b/src/context/cdvector.h deleted file mode 100644 index 2622ccdd2..000000000 --- a/src/context/cdvector.h +++ /dev/null @@ -1,162 +0,0 @@ -/********************* */ -/*! \file cdvector.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__CDVECTOR_H -#define __CVC4__CONTEXT__CDVECTOR_H - -#include - -#include "base/cvc4_assert.h" -#include "context/context.h" -#include "context/cdlist.h" - -namespace CVC4 { -namespace context { - - -/** - * Generic context-dependent dynamic vector. - * This is quite different than CDList. - * It provides the ability to destructively update the i'th item. - * - * The back of the vector may only be popped if there have been no updates to it - * at this context level. - */ -template -class CDVector { -private: - static const int ImpossibleLevel = -1; - - struct UpdatableElement { - public: - T d_data; - int d_contextLevelOfLastUpdate; - - UpdatableElement(const T& data) : - d_data(data), - d_contextLevelOfLastUpdate(ImpossibleLevel) { - } - };/* struct CDVector::UpdatableElement */ - - struct HistoryElement { - public: - UpdatableElement d_cached; - size_t d_index; - HistoryElement(const UpdatableElement& cache, size_t index) : - d_cached(cache), d_index(index) { - } - };/* struct CDVector::HistoryElement */ - - typedef std::vector< UpdatableElement > CurrentVector; - CurrentVector d_current; - - - - class HistoryListCleanUp{ - private: - CurrentVector& d_current; - public: - HistoryListCleanUp(CurrentVector& current) - : d_current(current) - {} - - void operator()(HistoryElement* back){ - d_current[back->d_index] = back->d_cached; - } - };/* class CDVector::HistoryListCleanUp */ - - typedef CDList< HistoryElement, HistoryListCleanUp > HistoryVector; - HistoryVector d_history; - - Context* d_context; - - // no copy or assignment - CDVector(const CDVector&) CVC4_UNDEFINED; - CDVector& operator=(const CDVector&) CVC4_UNDEFINED; - -public: - CDVector(Context* c) : - d_current(), - d_history(c, true, HistoryListCleanUp(d_current)), - d_context(c) - {} - - size_t size() const { - return d_current.size(); - } - - /** - * Return true iff there are no valid objects in the list. - */ - bool empty() const { - return d_current.empty(); - } - - /** - * Add an item to the end of the list. - * Assigns its state at level 0 to be equal to data. - */ - void push_back(const T& data) { - d_current.push_back(UpdatableElement(data)); - } - - /** - * Access to the ith item in the list. - */ - const T& operator[](size_t i) const { - return get(i); - } - - const T& get(size_t i) const { - Assert(i < size(), "index out of bounds in CDVector::get()"); - //makeConsistent(); - return d_current[i].d_data; - } - - void set(size_t index, const T& data) { - Assert(index < size(), "index out of bounds in CDVector::set()"); - //makeConsistent(); - - if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) { - d_current[index].d_data = data; - }else{ - d_history.push_back(HistoryElement(d_current[index], index)); - - d_current[index].d_data = data; - d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel(); - } - } - - bool hasUpdates(size_t index) const { - Assert(index < size(), "index out of bounds in CDVector::hasUpdates()"); - return d_current[index].d_contextLevelOfLastUpdate == ImpossibleLevel; - } - - void pop_back() { - Assert(!empty(), "pop_back() on an empty CDVector"); - Assert(!hasUpdates(size() - 1), "popping an element with updates."); - d_current.pop_back(); - } - -};/* class CDVector */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDVECTOR_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 0ab305039..d58ee411f 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -40,7 +40,6 @@ UNIT_TESTS += \ context/cdlist_black \ context/cdmap_black \ context/cdmap_white \ - context/cdvector_black \ util/array_store_all_black \ util/assert_white \ util/check_white \ diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h deleted file mode 100644 index 3769b2cce..000000000 --- a/test/unit/context/cdvector_black.h +++ /dev/null @@ -1,140 +0,0 @@ -/********************* */ -/*! \file cdvector_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include - -#include -#include - -#include - -#include "context/context.h" -#include "context/cdvector.h" - -using namespace std; -using namespace CVC4::context; - -struct DtorSensitiveObject { - bool& d_dtorCalled; - DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} - ~DtorSensitiveObject() { d_dtorCalled = true; } -}; - - - -class CDListBlack : public CxxTest::TestSuite { -private: - - Context* d_context; - -public: - - void setUp() { - d_context = new Context(); - } - - void tearDown() { - delete d_context; - } - - void testCDVector17() { vectorTest(17); } - void testCDVector31() { vectorTest(31); } - void testCDVector191() { vectorTest(113); } - - void vectorTest(unsigned P){ - vectorTest(P, 2); - vectorTest(P, 5); - vectorTest(P, P/3 + 1); - } - - void vectorTest(unsigned P, unsigned m){ - for(unsigned g=2; g< P; g++){ - vectorTest(P, g, m, 1); - vectorTest(P, g, m, 3); - } - } - vector copy(CDVector& v){ - vector ret; - for(unsigned i=0; i < v.size(); ++i){ - ret.push_back(v[i]); - } - return ret; - } - - void equal(vector& copy, CDVector& v){ - TS_ASSERT_EQUALS(copy.size(), v.size()); - for(unsigned i = 0; i < v.size(); ++i){ - TS_ASSERT_EQUALS(copy[i], v[i]); - } - } - - void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r) { - CDVector vec(d_context); - vector< vector > copies; - - copies.push_back( copy(vec) ); - d_context->push(); - - TS_ASSERT(vec.empty()); - for(unsigned i = 0; i < P; ++i){ - vec.push_back(i); - TS_ASSERT_EQUALS(vec.size(), i+1); - } - TS_ASSERT(!vec.empty()); - TS_ASSERT_EQUALS(vec.size(), P); - - copies.push_back( copy(vec) ); - d_context->push(); - - for(unsigned i = 0, g_i = 1; i < r*P; ++i, g_i = (g_i * g)% P){ - if(i % m == 0){ - copies.push_back( copy(vec) ); - d_context->push(); - } - - vec.set(g_i, i); - - TS_ASSERT_EQUALS(vec.get(g_i), i); - } - TS_ASSERT_EQUALS(vec.size(), P); - - copies.push_back( copy(vec) ); - - while(d_context->getLevel() >= 1){ - TS_ASSERT_EQUALS(vec.size(), P); - equal(copies[d_context->getLevel()], vec); - d_context->pop(); - } - } - - void testTreeUpdate() { - CDVector vec(d_context); - vec.push_back(-1); - - vec.set(0, 0); - d_context->push(); - d_context->push(); - vec.set(0, 1); - d_context->pop(); - d_context->pop(); - - d_context->push(); - d_context->push(); - TS_ASSERT_EQUALS(vec.get(0), 0); - } - -};