diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-04 03:58:24 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-04 03:58:24 -0700 |
commit | 714ede2487fb58ea46858380eecfff72c2e2d4ac (patch) | |
tree | 24be60e0bd7b89cf6e65b65ff720427ecc67aac3 /src | |
parent | 9eb2c735f8c34d4980b37e337e711a629f997834 (diff) |
Remove unused CDVector (#2139)
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 1 | ||||
-rw-r--r-- | src/context/cdvector.h | 162 |
2 files changed, 0 insertions, 163 deletions
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 <vector> - -#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<T>. - * 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 T> -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<T>::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<T>::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<T>::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<T> */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDVECTOR_H */ |