From 1a558a30bec496444742ed75c0a6973d9789daf7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 2 Apr 2012 20:56:55 +0000 Subject: [PATCH] - Merged in the branch cdlist-cleanup. - This adds a CleanUp template argument to CDList. - CDChunkList replaces the CDList specialization for ContextMemoryAllocator. - CDVector has been simplified and improved. - The expected performance impact is negligible. --- ...cdlist_context_memory.h => cdchunk_list.h} | 63 +++++---- src/context/cdlist.h | 58 ++++++-- src/context/cdlist_forward.h | 18 +-- src/context/cdqueue.h | 45 +++--- src/context/cdvector.h | 131 +++++++++--------- src/theory/arith/partial_model.h | 8 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/datatypes/theory_datatypes.h | 4 +- src/util/congruence_closure.h | 6 +- test/unit/context/cdlist_black.h | 36 ++--- .../context/cdlist_context_memory_black.h | 32 +++-- test/unit/context/cdmap_black.h | 12 +- test/unit/context/cdvector_black.h | 8 +- 13 files changed, 236 insertions(+), 187 deletions(-) rename src/context/{cdlist_context_memory.h => cdchunk_list.h} (88%) diff --git a/src/context/cdlist_context_memory.h b/src/context/cdchunk_list.h similarity index 88% rename from src/context/cdlist_context_memory.h rename to src/context/cdchunk_list.h index fcb51fe20..e18d9b972 100644 --- a/src/context/cdlist_context_memory.h +++ b/src/context/cdchunk_list.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file cdlist_context_memory.h +/*! \file cdchunk_list.h ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -11,22 +11,21 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Context-dependent list class specialized for use with a + ** \brief Context-dependent list class designed for use with a ** context memory allocator. ** - ** Context-dependent list class specialized for use with a context + ** Context-dependent list class designed for use with a context ** memory allocator. **/ #include "cvc4_private.h" -#ifndef __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H -#define __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H +#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H +#define __CVC4__CONTEXT__CDCHUNK_LIST_H #include #include -#include "context/cdlist_forward.h" #include "context/context.h" #include "context/context_mm.h" #include "util/Assert.h" @@ -37,17 +36,17 @@ namespace context { /** * Generic context-dependent dynamic array. Like the usual CDList<>, * but allocates all memory from context memory. Elements are kept in - * cascading "list segments." Access to elements is not O(1) but + * cascading "list segments." Access to elements by operator[] is not O(1) but * O(log n). As with CDList<>, update is not permitted, only * appending to the end of the list. */ template -class CDList > : public ContextObj { +class CDChunkList : public ContextObj { public: - /** The value type with which this CDList<> was instantiated. */ + /** The value type with which this CDChunkList<> was instantiated. */ typedef T value_type; - /** The allocator type with which this CDList<> was instantiated. */ + /** The allocator type with which this CDChunkList<> was instantiated. */ typedef ContextMemoryAllocator Allocator; protected: @@ -91,7 +90,7 @@ protected: const T* list() const { return d_list; } T& operator[](size_t i) { return d_list[i]; } const T& operator[](size_t i) const { return d_list[i]; } - };/* struct CDList >::ListSegment */ + };/* struct CDChunkList::ListSegment */ /** * The first segment of list memory. @@ -126,12 +125,12 @@ protected: Allocator d_allocator; /** - * Lightweight save object for CDList >. + * Lightweight save object for CDChunkList >. */ - struct CDListSave : public ContextObj { + struct CDChunkListSave : public ContextObj { ListSegment* d_tail; size_t d_tailSize, d_size, d_sizeAlloc; - CDListSave(const CDList& list, ListSegment* tail, + CDChunkListSave(const CDChunkList& list, ListSegment* tail, size_t size, size_t sizeAlloc) : ContextObj(list), d_tail(tail), @@ -139,7 +138,7 @@ protected: d_size(size), d_sizeAlloc(sizeAlloc) { } - ~CDListSave() { + ~CDChunkListSave() { this->destroy(); } ContextObj* save(ContextMemoryManager* pCMM) { @@ -152,12 +151,12 @@ protected: // itself saved or restored. Unreachable(); } - };/* struct CDList >::CDListSave */ + };/* struct CDChunkList::CDChunkListSave */ /** * Private copy constructor undefined (no copy permitted). */ - CDList(const CDList& l) CVC4_UNDEFINED; + CDChunkList(const CDChunkList& l) CVC4_UNDEFINED; /** * Allocate the first list segment. @@ -225,7 +224,7 @@ protected: * The saved information is allocated using the ContextMemoryManager. */ ContextObj* save(ContextMemoryManager* pCMM) { - ContextObj* data = new(pCMM) CDListSave(*this, d_tailSegment, + ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment, d_size, d_totalSizeAlloc); Debug("cdlist:cmm") << "save " << this << " at level " << this->getContext()->getLevel() @@ -241,7 +240,7 @@ protected: * changed. */ void restore(ContextObj* data) { - CDListSave* save = static_cast(data); + CDChunkListSave* save = static_cast(data); Debug("cdlist:cmm") << "restore " << this << " level " << this->getContext()->getLevel() << " data == " << data @@ -276,7 +275,7 @@ protected: public: - CDList(Context* context, bool callDestructor, const Allocator& alloc) : + CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) : ContextObj(context), d_headSegment(), d_tailSegment(&d_headSegment), @@ -287,7 +286,7 @@ public: allocateHeadSegment(); } - CDList(Context* context, bool callDestructor = true) : + CDChunkList(Context* context, bool callDestructor = true) : ContextObj(context), d_headSegment(), d_tailSegment(&d_headSegment), @@ -298,7 +297,7 @@ public: allocateHeadSegment(); } - CDList(bool allocatedInCMM, Context* context, bool callDestructor, + CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor, const Allocator& alloc) : ContextObj(allocatedInCMM, context), d_headSegment(), @@ -310,7 +309,7 @@ public: allocateHeadSegment(); } - CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) : ContextObj(allocatedInCMM, context), d_headSegment(), d_tailSegment(&d_headSegment), @@ -324,7 +323,7 @@ public: /** * Destructor: delete the list */ - ~CDList() throw(AssertionException) { + ~CDChunkList() throw(AssertionException) { this->destroy(); if(this->d_callDestructor) { @@ -394,10 +393,10 @@ public: } /** - * Access to the ith item in the list. + * Access to the ith item in the list in O(log n). */ const T& operator[](size_t i) const { - Assert(i < d_size, "index out of bounds in CDList::operator[]"); + Assert(i < d_size, "index out of bounds in CDChunkList::operator[]"); const ListSegment* seg = &d_headSegment; while(i >= seg->size()) { i -= seg->size(); @@ -410,12 +409,12 @@ public: * Returns the most recent item added to the list. */ const T& back() const { - Assert(d_size > 0, "CDList::back() called on empty list"); + Assert(d_size > 0, "CDChunkList::back() called on empty list"); return (*d_tailSegment)[d_tailSegment->size() - 1]; } /** - * Iterator for CDList class. It has to be const because we don't + * Iterator for CDChunkList class. It has to be const because we don't * allow items in the list to be changed. It's a straightforward * wrapper around a pointer. Note that for efficiency, we implement * only prefix increment and decrement. Also note that it's OK to @@ -431,7 +430,7 @@ public: d_index(i) { } - friend class CDList; + friend class CDChunkList; public: @@ -470,7 +469,7 @@ public: ++(*this); return i; } - };/* class CDList<>::const_iterator */ + };/* class CDChunkList<>::const_iterator */ /** * Returns an iterator pointing to the first item in the list. @@ -489,9 +488,9 @@ public: const_iterator end() const { return const_iterator(NULL, 0); } -};/* class CDList > */ +};/* class CDChunkList > */ }/* CVC4::context namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */ +#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index cb9be07d3..c22d617b0 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -32,6 +32,8 @@ #include "context/cdlist_forward.h" #include "util/Assert.h" +#include + namespace CVC4 { namespace context { @@ -45,12 +47,15 @@ namespace context { * 2. T objects can safely be copied using their copy constructor, * operator=, and memcpy. */ -template +template class CDList : public ContextObj { public: /** The value type with which this CDList<> was instantiated. */ typedef T value_type; + + typedef CleanUpT CleanUp; + /** The allocator type with which this CDList<> was instantiated. */ typedef AllocatorT Allocator; @@ -83,6 +88,11 @@ private: */ size_t d_sizeAlloc; + /** + * The CleanUp functor. + */ + CleanUp d_cleanUp; + /** * Our allocator. */ @@ -94,12 +104,13 @@ protected: * d_sizeAlloc are not copied: only the base class information and * d_size are needed in restore. */ - CDList(const CDList& l) : + CDList(const CDList& l) : ContextObj(l), d_list(NULL), d_size(l.d_size), d_callDestructor(false), d_sizeAlloc(0), + d_cleanUp(l.d_cleanUp), d_allocator(l.d_allocator) { Debug("cdlist") << "copy ctor: " << this << " from " << &l @@ -157,7 +168,7 @@ private: * ContextMemoryManager. */ ContextObj* save(ContextMemoryManager* pCMM) { - ContextObj* data = new(pCMM) CDList(*this); + ContextObj* data = new(pCMM) CDList(*this); Debug("cdlist") << "save " << this << " at level " << this->getContext()->getLevel() << " size at " << this->d_size @@ -179,7 +190,7 @@ protected: << " data == " << data << " call dtor == " << this->d_callDestructor << " d_list == " << this->d_list << std::endl; - truncateList(((CDList*)data)->d_size); + truncateList(((CDList*)data)->d_size); Debug("cdlist") << "restore " << this << " level " << this->getContext()->getLevel() << " size back to " << this->d_size @@ -200,6 +211,7 @@ protected: if(d_callDestructor) { while(d_size != size) { --d_size; + d_cleanUp(&d_list[d_size]); d_allocator.destroy(&d_list[d_size]); } } else { @@ -213,26 +225,33 @@ public: /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(Context* context, bool callDestructor = true, - const Allocator& alloc = Allocator()) : + CDList(Context* context, + bool callDestructor = true, + const CleanUp& cleanup = CleanUp(), + const Allocator& alloc = Allocator()) : ContextObj(context), d_list(NULL), d_size(0), d_callDestructor(callDestructor), d_sizeAlloc(0), + d_cleanUp(cleanup), d_allocator(alloc) { } /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(bool allocatedInCMM, Context* context, bool callDestructor = true, - const Allocator& alloc = Allocator()) : + CDList(bool allocatedInCMM, + Context* context, + bool callDestructor = true, + const CleanUp& cleanup = CleanUp(), + const Allocator& alloc = Allocator()) : ContextObj(allocatedInCMM, context), d_list(NULL), d_size(0), d_callDestructor(callDestructor), d_sizeAlloc(0), + d_cleanUp(cleanup), d_allocator(alloc) { } @@ -243,9 +262,7 @@ public: this->destroy(); if(this->d_callDestructor) { - for(size_t i = 0; i < this->d_size; ++i) { - this->d_allocator.destroy(&this->d_list[i]); - } + truncateList(0); } this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc); @@ -332,7 +349,7 @@ public: const_iterator(T const* it) : d_it(it) {} - friend class CDList; + friend class CDList; public: @@ -412,6 +429,23 @@ public: } };/* class CDList<> */ + +template +class CDList > : public ContextObj { + /* CDList is incompatible for use with a ContextMemoryAllocator. + * Consider using CDChunkList instead. + * + * Explanation: + * If ContextMemoryAllocator is used and d_list grows at a deeper context level + * the reallocated will be reallocated in a context memory regaion that can be + * detroyed on pop. To support this, a full copy of d_list would have to be made. + * As this is unacceptable for performance in other situations, we do not do + * this. + */ + + BOOST_STATIC_ASSERT(sizeof(T) == 0); +}; + }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h index 90c439085..78557afd2 100644 --- a/src/context/cdlist_forward.h +++ b/src/context/cdlist_forward.h @@ -41,16 +41,18 @@ namespace __gnu_cxx { }/* __gnu_cxx namespace */ namespace CVC4 { - namespace context { - template - class ContextMemoryAllocator; +namespace context { - template > - class CDList; +template +class DefaultCleanUp { +public: + inline void operator()(T* t) const{} +}; - template - class CDList >; - }/* CVC4::context namespace */ +template , class Allocator = std::allocator > +class CDList; + +}/* CVC4::context namespace */ }/* CVC4 namespace */ #endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */ diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index 16f81709e..d8f6c42f1 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -34,9 +34,15 @@ namespace CVC4 { namespace context { +template , class Allocator = std::allocator > +class CDQueue; + /** We don't define a template with Allocator for the first implementation */ -template -class CDQueue : public CDList { +template +class CDQueue : public CDList { +private: + typedef CDList ParentType; + protected: /** Points to the next element in the current context to dequeue. */ @@ -48,8 +54,8 @@ protected: /** * Private copy constructor used only by save(). */ - CDQueue(const CDQueue& l): - CDList(l), + CDQueue(const CDQueue& l): + ParentType(l), d_iter(l.d_iter), d_lastsave(l.d_lastsave) {} @@ -60,7 +66,7 @@ protected: ContextObj* data = new(pCMM) CDQueue(*this); // We save the d_size in d_lastsave and we should never destruct below this // indices before the corresponding restore. - d_lastsave = CDList::d_size; + d_lastsave = ParentType::d_size; Debug("cdqueue") << "save " << this << " at level " << this->getContext()->getLevel() << " size at " << this->d_size @@ -80,7 +86,7 @@ protected: CDQueue* qdata = static_cast*>(data); d_iter = qdata->d_iter; d_lastsave = qdata->d_lastsave; - CDList::restore(data); + ParentType::restore(data); } @@ -88,26 +94,29 @@ protected: public: /** Creates a new CDQueue associated with the current context. */ - CDQueue(Context* context) - : CDList(context), + CDQueue(Context* context, + bool callDestructor = true, + const CleanUp& cleanup = CleanUp(), + const Allocator& alloc = Allocator()) + : ParentType(context, callDestructor, cleanup, alloc), d_iter(0), d_lastsave(0) {} /** Returns true if the queue is empty in the current context. */ bool empty() const{ - Assert(d_iter <= CDList::d_size); - return d_iter == CDList::d_size; + Assert(d_iter <= ParentType::d_size); + return d_iter == ParentType::d_size; } /** Returns the number of elements that have not been dequeued in the context. */ size_t size() const{ - return CDList::d_size - d_iter; + return ParentType::d_size - d_iter; } /** Enqueues an element in the current context. */ void push(const T& data){ - CDList::push_back(data); + ParentType::push_back(data); } /** @@ -117,13 +126,13 @@ public: */ void pop(){ Assert(!empty(), "Attempting to pop from an empty queue."); - CDList::makeCurrent(); + ParentType::makeCurrent(); d_iter = d_iter + 1; - if (empty() && d_lastsave != CDList::d_size) { + if (empty() && d_lastsave != ParentType::d_size) { // Some elements have been enqueued and dequeued in the same // context and now the queue is empty we can destruct them. - CDList::truncateList(d_lastsave); - Assert(CDList::d_size == d_lastsave); + ParentType::truncateList(d_lastsave); + Assert(ParentType::d_size == d_lastsave); d_iter = d_lastsave; } } @@ -131,7 +140,7 @@ public: /** Returns a reference to the next element on the queue. */ const T& front() const{ Assert(!empty(), "No front in an empty queue."); - return CDList::d_list[d_iter]; + return ParentType::d_list[d_iter]; } /** @@ -139,7 +148,7 @@ public: */ const T& back() const { Assert(!empty(), "CDQueue::back() called on empty list"); - return CDList::d_list[CDList::d_size - 1]; + return ParentType::d_list[ParentType::d_size - 1]; } };/* class CDQueue<> */ diff --git a/src/context/cdvector.h b/src/context/cdvector.h index 49d1b67e9..9464f416b 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -23,86 +23,79 @@ #define __CVC4__CONTEXT__CDVECTOR_H #include "context/context.h" -#include "context/cdo.h" +#include "context/cdlist.h" #include "util/Assert.h" -#include "util/dynamic_array.h" +#include + namespace CVC4 { namespace context { -template -struct UpdatableElement { -public: - T d_data; - int d_contextLevelOfLastUpdate; - - UpdatableElement(const T& data) : - d_data(data), - d_contextLevelOfLastUpdate(0) { - } -};/* struct UpdatableElement */ - -template -struct HistoryElement { -public: - UpdatableElement d_cached; - unsigned d_index; - HistoryElement(const UpdatableElement& cache, unsigned index) : - d_cached(cache), d_index(index) { - } -};/* struct HistoryElement */ - /** * Generic context-dependent dynamic vector. + * This is quite different than CDList. * It provides the ability to destructively update the i'th item. - * Note that the size of the vector never decreases. * - * This is quite different than CDList. + * 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: - typedef DynamicArray< UpdatableElement > CurrentVector; - typedef DynamicArray< HistoryElement > HistoryVector; + static const int ImpossibleLevel = -1; - Context* d_context; + struct UpdatableElement { + public: + T d_data; + int d_contextLevelOfLastUpdate; - DynamicArray< UpdatableElement > d_current; - DynamicArray< HistoryElement > d_history; + 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 */ - CDO d_historySize; + typedef std::vector< UpdatableElement > CurrentVector; + CurrentVector d_current; -private: - void restoreConsistency() { - Assert(d_history.size() >= d_historySize.get()); - while(d_history.size() > d_historySize.get()) { - const HistoryElement& back = d_history.back(); - d_current[back.d_index] = back.d_cached; - d_history.pop_back(); - } - } - bool isConsistent() const { - return d_history.size() == d_historySize.get(); - } - void makeConsistent() { - if(!isConsistent()) { - restoreConsistency(); + 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; } - Assert(isConsistent()); - } + };/* class CDVector::HistoryListCleanUp */ + + typedef CDList< HistoryElement, HistoryListCleanUp > HistoryVector; + HistoryVector d_history; + + Context* d_context; public: - CDVector(Context* c, bool callDestructor = false) : - d_context(c), - d_current(callDestructor), - d_history(callDestructor), - d_historySize(c, 0) { - } + CDVector(Context* c) : + d_current(), + d_history(c, true, HistoryListCleanUp(d_current)), + d_context(c) + {} - unsigned size() const { + size_t size() const { return d_current.size(); } @@ -118,37 +111,47 @@ public: * Assigns its state at level 0 to be equal to data. */ void push_back(const T& data) { - d_current.push_back(UpdatableElement(data)); + d_current.push_back(UpdatableElement(data)); } /** * Access to the ith item in the list. */ - const T& operator[](unsigned i) { + const T& operator[](size_t i) const { return get(i); } - const T& get(unsigned i) { + const T& get(size_t i) const { Assert(i < size(), "index out of bounds in CDVector::get()"); - makeConsistent(); + //makeConsistent(); return d_current[i].d_data; } - void set(unsigned index, const T& data) { + void set(size_t index, const T& data) { Assert(index < size(), "index out of bounds in CDVector::set()"); - makeConsistent(); + //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_historySize.set(d_historySize.get() + 1); + 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 */ diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 7a2a97726..7e2211595 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -74,10 +74,10 @@ public: d_hasSafeAssignment(), d_assignment(), d_safeAssignment(), - d_upperBound(c, true), - d_lowerBound(c, true), - d_upperConstraint(c,true), - d_lowerConstraint(c,true), + d_upperBound(c), + d_lowerBound(c), + d_upperConstraint(c), + d_lowerConstraint(c), d_deltaIsSafe(false), d_delta(-1,1), d_history(), diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index fcb6ee382..dcae47dc7 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -151,7 +151,7 @@ private: void notifyCongruent(TNode a, TNode b); - typedef context::CDList > CTNodeListAlloc; + typedef context::CDChunkList CTNodeListAlloc; typedef context::CDHashMap CNodeTNodesMap; typedef context::CDHashMap*, TNodeHashFunction > EqLists; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 921df028e..281b11a93 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -39,9 +39,9 @@ namespace datatypes { class TheoryDatatypes : public Theory { private: - typedef context::CDList > EqList; + typedef context::CDChunkList EqList; typedef context::CDHashMap EqLists; - typedef context::CDList > EqListN; + typedef context::CDChunkList EqListN; typedef context::CDHashMap EqListsN; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index ed1cecd7b..d7b8b0a22 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -32,7 +32,7 @@ #include "context/cdo.h" #include "context/cdhashmap.h" #include "context/cdhashset.h" -#include "context/cdlist_context_memory.h" +#include "context/cdchunk_list.h" #include "util/exception.h" #include "context/stacking_map.h" #include "util/stats.h" @@ -140,9 +140,9 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::StackingMap RepresentativeMap; - typedef context::CDList > ClassList; + typedef context::CDChunkList ClassList; typedef context::CDHashMap ClassLists; - typedef context::CDList > UseList; + typedef context::CDChunkList UseList; typedef context::CDHashMap UseLists; typedef context::CDHashMap LookupMap; diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index fcc6a7e55..ccdbb210b 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -28,7 +28,6 @@ #include "util/exception.h" #include "context/context.h" #include "context/cdlist.h" -#include "context/cdlist_context_memory.h" using namespace std; using namespace CVC4::context; @@ -58,12 +57,12 @@ public: // test at different sizes. this triggers grow() behavior differently. // grow() was completely broken in revision 256 - void testCDList10() { listTest(10); } - void testCDList15() { listTest(15); } - void testCDList20() { listTest(20); } - void testCDList35() { listTest(35); } - void testCDList50() { listTest(50); } - void testCDList99() { listTest(99); } + void testCDList_BE10() { listTest(10); } + void testCDList_BE15() { listTest(15); } + void testCDList_BE20() { listTest(20); } + void testCDList_BE35() { listTest(35); } + void testCDList_BE50() { listTest(50); } + void testCDList_BE99() { listTest(99); } void listTest(int N) { listTest(N, true); @@ -71,7 +70,7 @@ public: } void listTest(int N, bool callDestructor) { - CDList list(d_context, callDestructor); + CDList_BE list(d_context, callDestructor); TS_ASSERT(list.empty()); for(int i = 0; i < N; ++i) { @@ -80,7 +79,7 @@ public: TS_ASSERT(!list.empty()); TS_ASSERT_EQUALS(list.back(), i); int i2 = 0; - for(CDList::const_iterator j = list.begin(); + for(CDList_BE::const_iterator j = list.begin(); j != list.end(); ++j) { TS_ASSERT_EQUALS(*j, i2++); @@ -100,8 +99,8 @@ public: bool shouldAlsoRemainFalse = false; bool aThirdFalse = false; - CDList listT(d_context, true); - CDList listF(d_context, false); + CDList_BE listT(d_context, true); + CDList_BE listF(d_context, false); DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse); DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue); @@ -136,15 +135,10 @@ public: TS_ASSERT_EQUALS(aThirdFalse, false); } - void testEmptyIterators() { - CDList* list1 = new(true) CDList(d_context); - CDList< int, ContextMemoryAllocator >* list2 = - new(d_context->getCMM()) - CDList< int, ContextMemoryAllocator >(true, d_context, false, - ContextMemoryAllocator(d_context->getCMM())); - TS_ASSERT_EQUALS(list1->begin(), list1->end()); - TS_ASSERT_EQUALS(list2->begin(), list2->end()); - list1->deleteSelf(); + void testEmptyIterator() { + CDList_BE* list = new(true) CDList_BE(d_context); + TS_ASSERT_EQUALS(list->begin(), list->end()); + list->deleteSelf(); } /* setrlimit() totally broken on Mac OS X */ @@ -155,7 +149,7 @@ public: #else /* __APPLE__ */ - CDList list(d_context); + CDList_BE list(d_context); WithLimitedMemory wlm(1); TS_ASSERT_THROWS({ diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h index a57fd131d..83fb20fd8 100644 --- a/test/unit/context/cdlist_context_memory_black.h +++ b/test/unit/context/cdlist_context_memory_black.h @@ -26,7 +26,7 @@ #include "memory.h" #include "context/context.h" -#include "context/cdlist_context_memory.h" +#include "context/cdchunk_list.h" using namespace std; using namespace CVC4::context; @@ -55,12 +55,12 @@ public: // test at different sizes. this triggers grow() behavior differently. // grow() was completely broken in revision 256 - void testCDList10() { listTest(10); } - void testCDList15() { listTest(15); } - void testCDList20() { listTest(20); } - void testCDList35() { listTest(35); } - void testCDList50() { listTest(50); } - void testCDList99() { listTest(99); } + void testCDChunkList10() { listTest(10); } + void testCDChunkList15() { listTest(15); } + void testCDChunkList20() { listTest(20); } + void testCDChunkList35() { listTest(35); } + void testCDChunkList50() { listTest(50); } + void testCDChunkList99() { listTest(99); } void listTest(int N) { listTest(N, true); @@ -68,7 +68,7 @@ public: } void listTest(int N, bool callDestructor) { - CDList > + CDChunkList list(d_context, callDestructor, ContextMemoryAllocator(d_context->getCMM())); TS_ASSERT(list.empty()); @@ -78,7 +78,7 @@ public: TS_ASSERT(!list.empty()); TS_ASSERT_EQUALS(list.back(), i); int i2 = 0; - for(CDList >::const_iterator j = list.begin(); + for(CDChunkList::const_iterator j = list.begin(); j != list.end(); ++j) { TS_ASSERT_EQUALS(*j, i2++); @@ -91,6 +91,14 @@ public: } } + void testEmptyIterator() { + CDChunkList< int>* list = + new(d_context->getCMM()) + CDChunkList< int >(true, d_context, false, + ContextMemoryAllocator(d_context->getCMM())); + TS_ASSERT_EQUALS(list->begin(), list->end()); + } + void testDtorCalled() { bool shouldRemainFalse = false; bool shouldFlipToTrue = false; @@ -98,8 +106,8 @@ public: bool shouldAlsoRemainFalse = false; bool aThirdFalse = false; - CDList > listT(d_context, true, ContextMemoryAllocator(d_context->getCMM())); - CDList > listF(d_context, false, ContextMemoryAllocator(d_context->getCMM())); + CDChunkList listT(d_context, true, ContextMemoryAllocator(d_context->getCMM())); + CDChunkList listF(d_context, false, ContextMemoryAllocator(d_context->getCMM())); DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse); DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue); @@ -142,7 +150,7 @@ public: #else /* __APPLE__ */ - CDList > list(d_context); + CDChunkList list(d_context); WithLimitedMemory wlm(1); TS_ASSERT_THROWS({ diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 0358d1edd..281d814aa 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -933,9 +933,9 @@ public: //Debug.on("gc"); //Debug.on("context"); - CDHashMap*, int_hasher> map(d_context); + CDHashMap*, int_hasher> map(d_context); - CDList *list1, *list2, *list3, *list4; + CDList_BE *list1, *list2, *list3, *list4; TS_ASSERT(map.find(1) == map.end()); TS_ASSERT(map.find(2) == map.end()); @@ -947,10 +947,10 @@ public: int* x = (int*) d_context->getCMM()->newData(sizeof(int)); - list1 = new(d_context->getCMM()) CDList(true, d_context); - list2 = new(d_context->getCMM()) CDList(true, d_context); - list3 = new(d_context->getCMM()) CDList(true, d_context); - list4 = new(d_context->getCMM()) CDList(true, d_context); + list1 = new(d_context->getCMM()) CDList_BE(true, d_context); + list2 = new(d_context->getCMM()) CDList_BE(true, d_context); + list3 = new(d_context->getCMM()) CDList_BE(true, d_context); + list4 = new(d_context->getCMM()) CDList_BE(true, d_context); list1->push_back(1); list2->push_back(2); diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h index b49186dd0..0f13d957e 100644 --- a/test/unit/context/cdvector_black.h +++ b/test/unit/context/cdvector_black.h @@ -68,8 +68,8 @@ public: void vectorTest(unsigned P, unsigned m){ for(unsigned g=2; g< P; g++){ - vectorTest(P, g, m, 1, false); - vectorTest(P, g, m, 3, false); + vectorTest(P, g, m, 1); + vectorTest(P, g, m, 3); } } vector copy(CDVector& v){ @@ -87,8 +87,8 @@ public: } } - void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r, bool callDestructor) { - CDVector vec(d_context, callDestructor); + void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r) { + CDVector vec(d_context); vector< vector > copies; copies.push_back( copy(vec) ); -- 2.30.2