- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.
--- /dev/null
+/********************* */
+/*! \file cdchunk_list.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent list class designed for use with a
+ ** context memory allocator.
+ **
+ ** Context-dependent list class designed for use with a context
+ ** memory allocator.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
+#define __CVC4__CONTEXT__CDCHUNK_LIST_H
+
+#include <iterator>
+#include <memory>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+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 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 T>
+class CDChunkList : public ContextObj {
+public:
+
+ /** The value type with which this CDChunkList<> was instantiated. */
+ typedef T value_type;
+ /** The allocator type with which this CDChunkList<> was instantiated. */
+ typedef ContextMemoryAllocator<T> Allocator;
+
+protected:
+
+ static const size_t INITIAL_SEGMENT_SIZE = 10;
+ static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
+
+ /**
+ * ListSegment is itself allocated in Context memory, but it is
+ * never updated; it serves as information about the d_list segment
+ * pointer it contains only.
+ */
+ class ListSegment {
+ ListSegment* d_nextSegment;
+ size_t d_segmentSize;
+ T* d_list;
+ public:
+ ListSegment() :
+ d_nextSegment(NULL),
+ d_segmentSize(0),
+ d_list(NULL) {
+ }
+ void initialize(T* list) {
+ Assert( d_nextSegment == NULL &&
+ d_segmentSize == 0 &&
+ d_list == NULL,
+ "Double-initialization of ListSegment not permitted" );
+ d_list = list;
+ }
+ void linkTo(ListSegment* nextSegment) {
+ Assert( d_nextSegment == NULL,
+ "Double-linking of ListSegment not permitted" );
+ d_nextSegment = nextSegment;
+ }
+ void cutLink() {
+ d_nextSegment = NULL;
+ }
+ ListSegment* getNextSegment() const { return d_nextSegment; }
+ size_t& size() { return d_segmentSize; }
+ size_t size() const { return d_segmentSize; }
+ 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 CDChunkList<T>::ListSegment */
+
+ /**
+ * The first segment of list memory.
+ */
+ ListSegment d_headSegment;
+
+ /**
+ * A pointer to the final segment of list memory.
+ */
+ ListSegment* d_tailSegment;
+
+ /**
+ * Whether to call the destructor when items are popped from the
+ * list. True by default, but can be set to false by setting the
+ * second argument in the constructor to false.
+ */
+ bool d_callDestructor;
+
+ /**
+ * Number of objects in list across all segments.
+ */
+ size_t d_size;
+
+ /**
+ * Total allocated size across all segments.
+ */
+ size_t d_totalSizeAlloc;
+
+ /**
+ * Our allocator.
+ */
+ Allocator d_allocator;
+
+ /**
+ * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
+ */
+ struct CDChunkListSave : public ContextObj {
+ ListSegment* d_tail;
+ size_t d_tailSize, d_size, d_sizeAlloc;
+ CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
+ size_t size, size_t sizeAlloc) :
+ ContextObj(list),
+ d_tail(tail),
+ d_tailSize(tail->size()),
+ d_size(size),
+ d_sizeAlloc(sizeAlloc) {
+ }
+ ~CDChunkListSave() {
+ this->destroy();
+ }
+ ContextObj* save(ContextMemoryManager* pCMM) {
+ // This type of object _is_ the save/restore object. It isn't
+ // itself saved or restored.
+ Unreachable();
+ }
+ void restore(ContextObj* data) {
+ // This type of object _is_ the save/restore object. It isn't
+ // itself saved or restored.
+ Unreachable();
+ }
+ };/* struct CDChunkList<T>::CDChunkListSave */
+
+ /**
+ * Private copy constructor undefined (no copy permitted).
+ */
+ CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
+
+ /**
+ * Allocate the first list segment.
+ */
+ void allocateHeadSegment() {
+ Assert(d_headSegment.list() == NULL);
+ Assert(d_totalSizeAlloc == 0 && d_size == 0);
+
+ // Allocate an initial list if one does not yet exist
+ size_t newSize = INITIAL_SEGMENT_SIZE;
+ Debug("cdlist:cmm") << "initial grow of cdlist " << this
+ << " level " << getContext()->getLevel()
+ << " to " << newSize << std::endl;
+ if(newSize > d_allocator.max_size()) {
+ newSize = d_allocator.max_size();
+ }
+ T* newList = d_allocator.allocate(newSize);
+ if(newList == NULL) {
+ throw std::bad_alloc();
+ }
+ d_totalSizeAlloc = newSize;
+ d_headSegment.initialize(newList);
+ }
+
+ /**
+ * Allocate a new segment with more space.
+ * Throws bad_alloc if memory allocation fails.
+ */
+ void grow() {
+ Assert(d_totalSizeAlloc == d_size);
+
+ // Allocate a new segment
+ typedef typename Allocator::template rebind<ListSegment>::other
+ SegmentAllocator;
+ ContextMemoryManager* cmm = d_allocator.getCMM();
+ SegmentAllocator segAllocator = SegmentAllocator(cmm);
+ ListSegment* newSegment = segAllocator.allocate(1);
+ if(newSegment == NULL) {
+ throw std::bad_alloc();
+ }
+ segAllocator.construct(newSegment, ListSegment());
+ size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
+ if(newSize > d_allocator.max_size()) {
+ newSize = d_allocator.max_size();
+ }
+ T* newList = d_allocator.allocate(newSize);
+ Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
+ << " level " << getContext()->getLevel()
+ << " to " << newSize
+ << " (from " << d_tailSegment->list()
+ << " to " << newList << ")" << std::endl;
+ if(newList == NULL) {
+ throw std::bad_alloc();
+ }
+ d_tailSegment->linkTo(newSegment);
+ d_tailSegment = newSegment;
+ d_tailSegment->initialize(newList);
+ d_totalSizeAlloc += newSize;
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method save: simply copies the
+ * current size to a copy using the copy constructor (the pointer and the
+ * allocated size are *not* copied as they are not restored on a pop).
+ * The saved information is allocated using the ContextMemoryManager.
+ */
+ ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment,
+ d_size, d_totalSizeAlloc);
+ Debug("cdlist:cmm") << "save " << this
+ << " at level " << this->getContext()->getLevel()
+ << " size at " << this->d_size
+ << " totalSizeAlloc at " << this->d_totalSizeAlloc
+ << " data:" << data << std::endl;
+ return data;
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method restore: simply restores the
+ * previous size. Note that the list pointer and the allocated size are not
+ * changed.
+ */
+ void restore(ContextObj* data) {
+ CDChunkListSave* save = static_cast<CDChunkListSave*>(data);
+ Debug("cdlist:cmm") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " data == " << data
+ << " call dtor == " << this->d_callDestructor
+ << " d_tail == " << this->d_tailSegment << std::endl;
+ if(this->d_callDestructor) {
+ ListSegment* seg = &d_headSegment;
+ size_t i = save->d_size;
+ while(i >= seg->size()) {
+ i -= seg->size();
+ seg = seg->getNextSegment();
+ }
+ do {
+ while(i < seg->size()) {
+ this->d_allocator.destroy(&(*seg)[i++]);
+ }
+ i = 0;
+ } while((seg = seg->getNextSegment()) != NULL);
+ }
+
+ this->d_size = save->d_size;
+ this->d_tailSegment = save->d_tail;
+ this->d_tailSegment->size() = save->d_tailSize;
+ this->d_tailSegment->cutLink();
+ this->d_totalSizeAlloc = save->d_sizeAlloc;
+ Debug("cdlist:cmm") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_size
+ << " totalSizeAlloc at " << this->d_totalSizeAlloc
+ << std::endl;
+ }
+
+public:
+
+ CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) :
+ ContextObj(context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(alloc) {
+ allocateHeadSegment();
+ }
+
+ CDChunkList(Context* context, bool callDestructor = true) :
+ ContextObj(context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(Allocator(context->getCMM())) {
+ allocateHeadSegment();
+ }
+
+ CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor,
+ const Allocator& alloc) :
+ ContextObj(allocatedInCMM, context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(alloc) {
+ allocateHeadSegment();
+ }
+
+ CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+ ContextObj(allocatedInCMM, context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(Allocator(context->getCMM())) {
+ allocateHeadSegment();
+ }
+
+ /**
+ * Destructor: delete the list
+ */
+ ~CDChunkList() throw(AssertionException) {
+ this->destroy();
+
+ if(this->d_callDestructor) {
+ for(ListSegment* segment = &d_headSegment;
+ segment != NULL;
+ segment = segment->getNextSegment()) {
+ for(size_t i = 0; i < segment->size(); ++i) {
+ this->d_allocator.destroy(&(*segment)[i]);
+ }
+ }
+ }
+ }
+
+ /**
+ * Return the current size of (i.e. valid number of objects in) the
+ * list.
+ */
+ size_t size() const {
+ return d_size;
+ }
+
+ /**
+ * Return true iff there are no valid objects in the list.
+ */
+ bool empty() const {
+ return d_size == 0;
+ }
+
+ /**
+ * Add an item to the end of the list.
+ */
+ void push_back(const T& data) {
+ Debug("cdlist:cmm") << "push_back " << this
+ << " level " << getContext()->getLevel()
+ << ": make-current, "
+ << "d_list == " << d_tailSegment->list() << std::endl;
+ makeCurrent();
+
+ Debug("cdlist:cmm") << "push_back " << this
+ << " level " << getContext()->getLevel()
+ << ": grow? " << d_size
+ << " size_alloc " << d_totalSizeAlloc
+ << std::endl;
+
+ if(d_size == d_totalSizeAlloc) {
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": grow!\n";
+ grow();
+ }
+ Assert(d_size < d_totalSizeAlloc);
+
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": construct! at [" << d_size << "] == "
+ << &(*d_tailSegment)[d_tailSegment->size()]
+ << std::endl;
+ d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": done..." << std::endl;
+ ++d_tailSegment->size();
+ ++d_size;
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": size now " << d_size << std::endl;
+ }
+
+ /**
+ * 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 CDChunkList::operator[]");
+ const ListSegment* seg = &d_headSegment;
+ while(i >= seg->size()) {
+ i -= seg->size();
+ seg = seg->getNextSegment();
+ }
+ return (*seg)[i];
+ }
+
+ /**
+ * Returns the most recent item added to the list.
+ */
+ const T& back() const {
+ Assert(d_size > 0, "CDChunkList::back() called on empty list");
+ return (*d_tailSegment)[d_tailSegment->size() - 1];
+ }
+
+ /**
+ * 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
+ * create an iterator from an empty, uninitialized list, as begin()
+ * and end() will have the same value (NULL).
+ */
+ class const_iterator {
+ const ListSegment* d_segment;
+ size_t d_index;
+
+ const_iterator(const ListSegment* segment, size_t i) :
+ d_segment(segment),
+ d_index(i) {
+ }
+
+ friend class CDChunkList<T>;
+
+ public:
+
+ typedef std::input_iterator_tag iterator_category;
+ typedef T value_type;
+ typedef std::ptrdiff_t difference_type;
+ typedef const T* pointer;
+ typedef const T& reference;
+
+ const_iterator() : d_segment(NULL), d_index(0) {}
+
+ inline bool operator==(const const_iterator& i) const {
+ return d_segment == i.d_segment && d_index == i.d_index;
+ }
+
+ inline bool operator!=(const const_iterator& i) const {
+ return !(*this == i);
+ }
+
+ inline const T& operator*() const {
+ return (*d_segment)[d_index];
+ }
+
+ /** Prefix increment */
+ const_iterator& operator++() {
+ if(++d_index >= d_segment->size()) {
+ d_segment = d_segment->getNextSegment();
+ d_index = 0;
+ }
+ return *this;
+ }
+
+ /** Postfix increment: returns new iterator with the old value. */
+ const_iterator operator++(int) {
+ const_iterator i = *this;
+ ++(*this);
+ return i;
+ }
+ };/* class CDChunkList<>::const_iterator */
+
+ /**
+ * Returns an iterator pointing to the first item in the list.
+ */
+ const_iterator begin() const {
+ // This looks curious, but we have to make sure that begin() == end()
+ // for an empty list, and begin() == (head,0) for a nonempty one.
+ // Since the segment spill-over is implemented in
+ // iterator::operator++(), let's reuse it. */
+ return ++const_iterator(&d_headSegment, -1);
+ }
+
+ /**
+ * Returns an iterator pointing one past the last item in the list.
+ */
+ const_iterator end() const {
+ return const_iterator(NULL, 0);
+ }
+};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */
#include "context/cdlist_forward.h"
#include "util/Assert.h"
+#include <boost/static_assert.hpp>
+
namespace CVC4 {
namespace context {
* 2. T objects can safely be copied using their copy constructor,
* operator=, and memcpy.
*/
-template <class T, class AllocatorT>
+template <class T, class CleanUpT, class AllocatorT>
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;
*/
size_t d_sizeAlloc;
+ /**
+ * The CleanUp functor.
+ */
+ CleanUp d_cleanUp;
+
/**
* Our allocator.
*/
* d_sizeAlloc are not copied: only the base class information and
* d_size are needed in restore.
*/
- CDList(const CDList<T, Allocator>& l) :
+ CDList(const CDList<T, CleanUp, Allocator>& 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
* ContextMemoryManager.
*/
ContextObj* save(ContextMemoryManager* pCMM) {
- ContextObj* data = new(pCMM) CDList<T, Allocator>(*this);
+ ContextObj* data = new(pCMM) CDList<T, CleanUp, Allocator>(*this);
Debug("cdlist") << "save " << this
<< " at level " << this->getContext()->getLevel()
<< " size at " << this->d_size
<< " data == " << data
<< " call dtor == " << this->d_callDestructor
<< " d_list == " << this->d_list << std::endl;
- truncateList(((CDList<T, Allocator>*)data)->d_size);
+ truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
Debug("cdlist") << "restore " << this
<< " level " << this->getContext()->getLevel()
<< " size back to " << this->d_size
if(d_callDestructor) {
while(d_size != size) {
--d_size;
+ d_cleanUp(&d_list[d_size]);
d_allocator.destroy(&d_list[d_size]);
}
} else {
/**
* 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) {
}
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);
const_iterator(T const* it) : d_it(it) {}
- friend class CDList<T, Allocator>;
+ friend class CDList<T, CleanUp, Allocator>;
public:
}
};/* class CDList<> */
+
+template <class T, class CleanUp>
+class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
+ /* CDList is incompatible for use with a ContextMemoryAllocator.
+ * Consider using CDChunkList<T> 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 */
+++ /dev/null
-/********************* */
-/*! \file cdlist_context_memory.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Context-dependent list class specialized for use with a
- ** context memory allocator.
- **
- ** Context-dependent list class specialized 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
-
-#include <iterator>
-#include <memory>
-
-#include "context/cdlist_forward.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-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
- * O(log n). As with CDList<>, update is not permitted, only
- * appending to the end of the list.
- */
-template <class T>
-class CDList<T, ContextMemoryAllocator<T> > : public ContextObj {
-public:
-
- /** The value type with which this CDList<> was instantiated. */
- typedef T value_type;
- /** The allocator type with which this CDList<> was instantiated. */
- typedef ContextMemoryAllocator<T> Allocator;
-
-protected:
-
- static const size_t INITIAL_SEGMENT_SIZE = 10;
- static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
-
- /**
- * ListSegment is itself allocated in Context memory, but it is
- * never updated; it serves as information about the d_list segment
- * pointer it contains only.
- */
- class ListSegment {
- ListSegment* d_nextSegment;
- size_t d_segmentSize;
- T* d_list;
- public:
- ListSegment() :
- d_nextSegment(NULL),
- d_segmentSize(0),
- d_list(NULL) {
- }
- void initialize(T* list) {
- Assert( d_nextSegment == NULL &&
- d_segmentSize == 0 &&
- d_list == NULL,
- "Double-initialization of ListSegment not permitted" );
- d_list = list;
- }
- void linkTo(ListSegment* nextSegment) {
- Assert( d_nextSegment == NULL,
- "Double-linking of ListSegment not permitted" );
- d_nextSegment = nextSegment;
- }
- void cutLink() {
- d_nextSegment = NULL;
- }
- ListSegment* getNextSegment() const { return d_nextSegment; }
- size_t& size() { return d_segmentSize; }
- size_t size() const { return d_segmentSize; }
- 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<T, ContextMemoryAllocator<T> >::ListSegment */
-
- /**
- * The first segment of list memory.
- */
- ListSegment d_headSegment;
-
- /**
- * A pointer to the final segment of list memory.
- */
- ListSegment* d_tailSegment;
-
- /**
- * Whether to call the destructor when items are popped from the
- * list. True by default, but can be set to false by setting the
- * second argument in the constructor to false.
- */
- bool d_callDestructor;
-
- /**
- * Number of objects in list across all segments.
- */
- size_t d_size;
-
- /**
- * Total allocated size across all segments.
- */
- size_t d_totalSizeAlloc;
-
- /**
- * Our allocator.
- */
- Allocator d_allocator;
-
- /**
- * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >.
- */
- struct CDListSave : public ContextObj {
- ListSegment* d_tail;
- size_t d_tailSize, d_size, d_sizeAlloc;
- CDListSave(const CDList<T, Allocator>& list, ListSegment* tail,
- size_t size, size_t sizeAlloc) :
- ContextObj(list),
- d_tail(tail),
- d_tailSize(tail->size()),
- d_size(size),
- d_sizeAlloc(sizeAlloc) {
- }
- ~CDListSave() {
- this->destroy();
- }
- ContextObj* save(ContextMemoryManager* pCMM) {
- // This type of object _is_ the save/restore object. It isn't
- // itself saved or restored.
- Unreachable();
- }
- void restore(ContextObj* data) {
- // This type of object _is_ the save/restore object. It isn't
- // itself saved or restored.
- Unreachable();
- }
- };/* struct CDList<T, ContextMemoryAllocator<T> >::CDListSave */
-
- /**
- * Private copy constructor undefined (no copy permitted).
- */
- CDList(const CDList<T, Allocator>& l) CVC4_UNDEFINED;
-
- /**
- * Allocate the first list segment.
- */
- void allocateHeadSegment() {
- Assert(d_headSegment.list() == NULL);
- Assert(d_totalSizeAlloc == 0 && d_size == 0);
-
- // Allocate an initial list if one does not yet exist
- size_t newSize = INITIAL_SEGMENT_SIZE;
- Debug("cdlist:cmm") << "initial grow of cdlist " << this
- << " level " << getContext()->getLevel()
- << " to " << newSize << std::endl;
- if(newSize > d_allocator.max_size()) {
- newSize = d_allocator.max_size();
- }
- T* newList = d_allocator.allocate(newSize);
- if(newList == NULL) {
- throw std::bad_alloc();
- }
- d_totalSizeAlloc = newSize;
- d_headSegment.initialize(newList);
- }
-
- /**
- * Allocate a new segment with more space.
- * Throws bad_alloc if memory allocation fails.
- */
- void grow() {
- Assert(d_totalSizeAlloc == d_size);
-
- // Allocate a new segment
- typedef typename Allocator::template rebind<ListSegment>::other
- SegmentAllocator;
- ContextMemoryManager* cmm = d_allocator.getCMM();
- SegmentAllocator segAllocator = SegmentAllocator(cmm);
- ListSegment* newSegment = segAllocator.allocate(1);
- if(newSegment == NULL) {
- throw std::bad_alloc();
- }
- segAllocator.construct(newSegment, ListSegment());
- size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
- if(newSize > d_allocator.max_size()) {
- newSize = d_allocator.max_size();
- }
- T* newList = d_allocator.allocate(newSize);
- Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
- << " level " << getContext()->getLevel()
- << " to " << newSize
- << " (from " << d_tailSegment->list()
- << " to " << newList << ")" << std::endl;
- if(newList == NULL) {
- throw std::bad_alloc();
- }
- d_tailSegment->linkTo(newSegment);
- d_tailSegment = newSegment;
- d_tailSegment->initialize(newList);
- d_totalSizeAlloc += newSize;
- }
-
- /**
- * Implementation of mandatory ContextObj method save: simply copies the
- * current size to a copy using the copy constructor (the pointer and the
- * allocated size are *not* copied as they are not restored on a pop).
- * The saved information is allocated using the ContextMemoryManager.
- */
- ContextObj* save(ContextMemoryManager* pCMM) {
- ContextObj* data = new(pCMM) CDListSave(*this, d_tailSegment,
- d_size, d_totalSizeAlloc);
- Debug("cdlist:cmm") << "save " << this
- << " at level " << this->getContext()->getLevel()
- << " size at " << this->d_size
- << " totalSizeAlloc at " << this->d_totalSizeAlloc
- << " data:" << data << std::endl;
- return data;
- }
-
- /**
- * Implementation of mandatory ContextObj method restore: simply restores the
- * previous size. Note that the list pointer and the allocated size are not
- * changed.
- */
- void restore(ContextObj* data) {
- CDListSave* save = static_cast<CDListSave*>(data);
- Debug("cdlist:cmm") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " data == " << data
- << " call dtor == " << this->d_callDestructor
- << " d_tail == " << this->d_tailSegment << std::endl;
- if(this->d_callDestructor) {
- ListSegment* seg = &d_headSegment;
- size_t i = save->d_size;
- while(i >= seg->size()) {
- i -= seg->size();
- seg = seg->getNextSegment();
- }
- do {
- while(i < seg->size()) {
- this->d_allocator.destroy(&(*seg)[i++]);
- }
- i = 0;
- } while((seg = seg->getNextSegment()) != NULL);
- }
-
- this->d_size = save->d_size;
- this->d_tailSegment = save->d_tail;
- this->d_tailSegment->size() = save->d_tailSize;
- this->d_tailSegment->cutLink();
- this->d_totalSizeAlloc = save->d_sizeAlloc;
- Debug("cdlist:cmm") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " size back to " << this->d_size
- << " totalSizeAlloc at " << this->d_totalSizeAlloc
- << std::endl;
- }
-
-public:
-
- CDList(Context* context, bool callDestructor, const Allocator& alloc) :
- ContextObj(context),
- d_headSegment(),
- d_tailSegment(&d_headSegment),
- d_callDestructor(callDestructor),
- d_size(0),
- d_totalSizeAlloc(0),
- d_allocator(alloc) {
- allocateHeadSegment();
- }
-
- CDList(Context* context, bool callDestructor = true) :
- ContextObj(context),
- d_headSegment(),
- d_tailSegment(&d_headSegment),
- d_callDestructor(callDestructor),
- d_size(0),
- d_totalSizeAlloc(0),
- d_allocator(Allocator(context->getCMM())) {
- allocateHeadSegment();
- }
-
- CDList(bool allocatedInCMM, Context* context, bool callDestructor,
- const Allocator& alloc) :
- ContextObj(allocatedInCMM, context),
- d_headSegment(),
- d_tailSegment(&d_headSegment),
- d_callDestructor(callDestructor),
- d_size(0),
- d_totalSizeAlloc(0),
- d_allocator(alloc) {
- allocateHeadSegment();
- }
-
- CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
- ContextObj(allocatedInCMM, context),
- d_headSegment(),
- d_tailSegment(&d_headSegment),
- d_callDestructor(callDestructor),
- d_size(0),
- d_totalSizeAlloc(0),
- d_allocator(Allocator(context->getCMM())) {
- allocateHeadSegment();
- }
-
- /**
- * Destructor: delete the list
- */
- ~CDList() throw(AssertionException) {
- this->destroy();
-
- if(this->d_callDestructor) {
- for(ListSegment* segment = &d_headSegment;
- segment != NULL;
- segment = segment->getNextSegment()) {
- for(size_t i = 0; i < segment->size(); ++i) {
- this->d_allocator.destroy(&(*segment)[i]);
- }
- }
- }
- }
-
- /**
- * Return the current size of (i.e. valid number of objects in) the
- * list.
- */
- size_t size() const {
- return d_size;
- }
-
- /**
- * Return true iff there are no valid objects in the list.
- */
- bool empty() const {
- return d_size == 0;
- }
-
- /**
- * Add an item to the end of the list.
- */
- void push_back(const T& data) {
- Debug("cdlist:cmm") << "push_back " << this
- << " level " << getContext()->getLevel()
- << ": make-current, "
- << "d_list == " << d_tailSegment->list() << std::endl;
- makeCurrent();
-
- Debug("cdlist:cmm") << "push_back " << this
- << " level " << getContext()->getLevel()
- << ": grow? " << d_size
- << " size_alloc " << d_totalSizeAlloc
- << std::endl;
-
- if(d_size == d_totalSizeAlloc) {
- Debug("cdlist:cmm") << "push_back " << this
- << " " << getContext()->getLevel()
- << ": grow!\n";
- grow();
- }
- Assert(d_size < d_totalSizeAlloc);
-
- Debug("cdlist:cmm") << "push_back " << this
- << " " << getContext()->getLevel()
- << ": construct! at [" << d_size << "] == "
- << &(*d_tailSegment)[d_tailSegment->size()]
- << std::endl;
- d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
- Debug("cdlist:cmm") << "push_back " << this
- << " " << getContext()->getLevel()
- << ": done..." << std::endl;
- ++d_tailSegment->size();
- ++d_size;
- Debug("cdlist:cmm") << "push_back " << this
- << " " << getContext()->getLevel()
- << ": size now " << d_size << std::endl;
- }
-
- /**
- * Access to the ith item in the list.
- */
- const T& operator[](size_t i) const {
- Assert(i < d_size, "index out of bounds in CDList::operator[]");
- const ListSegment* seg = &d_headSegment;
- while(i >= seg->size()) {
- i -= seg->size();
- seg = seg->getNextSegment();
- }
- return (*seg)[i];
- }
-
- /**
- * Returns the most recent item added to the list.
- */
- const T& back() const {
- Assert(d_size > 0, "CDList::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
- * 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
- * create an iterator from an empty, uninitialized list, as begin()
- * and end() will have the same value (NULL).
- */
- class const_iterator {
- const ListSegment* d_segment;
- size_t d_index;
-
- const_iterator(const ListSegment* segment, size_t i) :
- d_segment(segment),
- d_index(i) {
- }
-
- friend class CDList<T, Allocator>;
-
- public:
-
- typedef std::input_iterator_tag iterator_category;
- typedef T value_type;
- typedef std::ptrdiff_t difference_type;
- typedef const T* pointer;
- typedef const T& reference;
-
- const_iterator() : d_segment(NULL), d_index(0) {}
-
- inline bool operator==(const const_iterator& i) const {
- return d_segment == i.d_segment && d_index == i.d_index;
- }
-
- inline bool operator!=(const const_iterator& i) const {
- return !(*this == i);
- }
-
- inline const T& operator*() const {
- return (*d_segment)[d_index];
- }
-
- /** Prefix increment */
- const_iterator& operator++() {
- if(++d_index >= d_segment->size()) {
- d_segment = d_segment->getNextSegment();
- d_index = 0;
- }
- return *this;
- }
-
- /** Postfix increment: returns new iterator with the old value. */
- const_iterator operator++(int) {
- const_iterator i = *this;
- ++(*this);
- return i;
- }
- };/* class CDList<>::const_iterator */
-
- /**
- * Returns an iterator pointing to the first item in the list.
- */
- const_iterator begin() const {
- // This looks curious, but we have to make sure that begin() == end()
- // for an empty list, and begin() == (head,0) for a nonempty one.
- // Since the segment spill-over is implemented in
- // iterator::operator++(), let's reuse it. */
- return ++const_iterator(&d_headSegment, -1);
- }
-
- /**
- * Returns an iterator pointing one past the last item in the list.
- */
- const_iterator end() const {
- return const_iterator(NULL, 0);
- }
-};/* class CDList<T, ContextMemoryAllocator<T> > */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */
}/* __gnu_cxx namespace */
namespace CVC4 {
- namespace context {
- template <class T>
- class ContextMemoryAllocator;
+namespace context {
- template <class T, class Allocator = std::allocator<T> >
- class CDList;
+template <class T>
+class DefaultCleanUp {
+public:
+ inline void operator()(T* t) const{}
+};
- template <class T>
- class CDList<T, ContextMemoryAllocator<T> >;
- }/* CVC4::context namespace */
+template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
+class CDList;
+
+}/* CVC4::context namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */
namespace CVC4 {
namespace context {
+template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
+class CDQueue;
+
/** We don't define a template with Allocator for the first implementation */
-template <class T>
-class CDQueue : public CDList<T> {
+template <class T, class CleanUp, class Allocator>
+class CDQueue : public CDList<T, CleanUp, Allocator> {
+private:
+ typedef CDList<T, CleanUp, Allocator> ParentType;
+
protected:
/** Points to the next element in the current context to dequeue. */
/**
* Private copy constructor used only by save().
*/
- CDQueue(const CDQueue<T>& l):
- CDList<T>(l),
+ CDQueue(const CDQueue<T, CleanUp, Allocator>& l):
+ ParentType(l),
d_iter(l.d_iter),
d_lastsave(l.d_lastsave) {}
ContextObj* data = new(pCMM) CDQueue<T>(*this);
// We save the d_size in d_lastsave and we should never destruct below this
// indices before the corresponding restore.
- d_lastsave = CDList<T>::d_size;
+ d_lastsave = ParentType::d_size;
Debug("cdqueue") << "save " << this
<< " at level " << this->getContext()->getLevel()
<< " size at " << this->d_size
CDQueue<T>* qdata = static_cast<CDQueue<T>*>(data);
d_iter = qdata->d_iter;
d_lastsave = qdata->d_lastsave;
- CDList<T>::restore(data);
+ ParentType::restore(data);
}
public:
/** Creates a new CDQueue associated with the current context. */
- CDQueue(Context* context)
- : CDList<T>(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<T>::d_size);
- return d_iter == CDList<T>::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<T>::d_size - d_iter;
+ return ParentType::d_size - d_iter;
}
/** Enqueues an element in the current context. */
void push(const T& data){
- CDList<T>::push_back(data);
+ ParentType::push_back(data);
}
/**
*/
void pop(){
Assert(!empty(), "Attempting to pop from an empty queue.");
- CDList<T>::makeCurrent();
+ ParentType::makeCurrent();
d_iter = d_iter + 1;
- if (empty() && d_lastsave != CDList<T>::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<T>::truncateList(d_lastsave);
- Assert(CDList<T>::d_size == d_lastsave);
+ ParentType::truncateList(d_lastsave);
+ Assert(ParentType::d_size == d_lastsave);
d_iter = d_lastsave;
}
}
/** Returns a reference to the next element on the queue. */
const T& front() const{
Assert(!empty(), "No front in an empty queue.");
- return CDList<T>::d_list[d_iter];
+ return ParentType::d_list[d_iter];
}
/**
*/
const T& back() const {
Assert(!empty(), "CDQueue::back() called on empty list");
- return CDList<T>::d_list[CDList<T>::d_size - 1];
+ return ParentType::d_list[ParentType::d_size - 1];
}
};/* class CDQueue<> */
#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 <vector>
+
namespace CVC4 {
namespace context {
-template <class T>
-struct UpdatableElement {
-public:
- T d_data;
- int d_contextLevelOfLastUpdate;
-
- UpdatableElement(const T& data) :
- d_data(data),
- d_contextLevelOfLastUpdate(0) {
- }
-};/* struct UpdatableElement<T> */
-
-template <class T>
-struct HistoryElement {
-public:
- UpdatableElement<T> d_cached;
- unsigned d_index;
- HistoryElement(const UpdatableElement<T>& cache, unsigned index) :
- d_cached(cache), d_index(index) {
- }
-};/* struct HistoryElement<T> */
-
/**
* Generic context-dependent dynamic vector.
+ * This is quite different than CDList<T>.
* 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<T>.
+ * 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:
- typedef DynamicArray< UpdatableElement<T> > CurrentVector;
- typedef DynamicArray< HistoryElement<T> > HistoryVector;
+ static const int ImpossibleLevel = -1;
- Context* d_context;
+ struct UpdatableElement {
+ public:
+ T d_data;
+ int d_contextLevelOfLastUpdate;
- DynamicArray< UpdatableElement<T> > d_current;
- DynamicArray< HistoryElement<T> > d_history;
+ 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 */
- CDO<unsigned> 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<T>& 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<T>::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();
}
* Assigns its state at level 0 to be equal to data.
*/
void push_back(const T& data) {
- d_current.push_back(UpdatableElement<T>(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<T>(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<T> */
}/* CVC4::context namespace */
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(),
void notifyCongruent(TNode a, TNode b);
- typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
+ typedef context::CDChunkList<TNode> CTNodeListAlloc;
typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
class TheoryDatatypes : public Theory {
private:
- typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList;
+ typedef context::CDChunkList<TNode> EqList;
typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists;
- typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN;
+ typedef context::CDChunkList<Node> EqListN;
typedef context::CDHashMap<Node, EqListN*, NodeHashFunction> EqListsN;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
#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"
// typedef all of these so that iterators are easy to define
typedef context::StackingMap<Node, Node, NodeHashFunction> RepresentativeMap;
- typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
+ typedef context::CDChunkList<TNode> ClassList;
typedef context::CDHashMap<Node, ClassList*, NodeHashFunction> ClassLists;
- typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
+ typedef context::CDChunkList<TNode> UseList;
typedef context::CDHashMap<TNode, UseList*, TNodeHashFunction> UseLists;
typedef context::CDHashMap<Node, Node, NodeHashFunction> LookupMap;
#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;
// 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);
}
void listTest(int N, bool callDestructor) {
- CDList<int> list(d_context, callDestructor);
+ CDList_BE<int> list(d_context, callDestructor);
TS_ASSERT(list.empty());
for(int i = 0; i < N; ++i) {
TS_ASSERT(!list.empty());
TS_ASSERT_EQUALS(list.back(), i);
int i2 = 0;
- for(CDList<int>::const_iterator j = list.begin();
+ for(CDList_BE<int>::const_iterator j = list.begin();
j != list.end();
++j) {
TS_ASSERT_EQUALS(*j, i2++);
bool shouldAlsoRemainFalse = false;
bool aThirdFalse = false;
- CDList<DtorSensitiveObject> listT(d_context, true);
- CDList<DtorSensitiveObject> listF(d_context, false);
+ CDList_BE<DtorSensitiveObject> listT(d_context, true);
+ CDList_BE<DtorSensitiveObject> listF(d_context, false);
DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
TS_ASSERT_EQUALS(aThirdFalse, false);
}
- void testEmptyIterators() {
- CDList<int>* list1 = new(true) CDList<int>(d_context);
- CDList< int, ContextMemoryAllocator<int> >* list2 =
- new(d_context->getCMM())
- CDList< int, ContextMemoryAllocator<int> >(true, d_context, false,
- ContextMemoryAllocator<int>(d_context->getCMM()));
- TS_ASSERT_EQUALS(list1->begin(), list1->end());
- TS_ASSERT_EQUALS(list2->begin(), list2->end());
- list1->deleteSelf();
+ void testEmptyIterator() {
+ CDList_BE<int>* list = new(true) CDList_BE<int>(d_context);
+ TS_ASSERT_EQUALS(list->begin(), list->end());
+ list->deleteSelf();
}
/* setrlimit() totally broken on Mac OS X */
#else /* __APPLE__ */
- CDList<unsigned> list(d_context);
+ CDList_BE<unsigned> list(d_context);
WithLimitedMemory wlm(1);
TS_ASSERT_THROWS({
#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;
// 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);
}
void listTest(int N, bool callDestructor) {
- CDList<int, ContextMemoryAllocator<int> >
+ CDChunkList<int>
list(d_context, callDestructor, ContextMemoryAllocator<int>(d_context->getCMM()));
TS_ASSERT(list.empty());
TS_ASSERT(!list.empty());
TS_ASSERT_EQUALS(list.back(), i);
int i2 = 0;
- for(CDList<int, ContextMemoryAllocator<int> >::const_iterator j = list.begin();
+ for(CDChunkList<int>::const_iterator j = list.begin();
j != list.end();
++j) {
TS_ASSERT_EQUALS(*j, i2++);
}
}
+ void testEmptyIterator() {
+ CDChunkList< int>* list =
+ new(d_context->getCMM())
+ CDChunkList< int >(true, d_context, false,
+ ContextMemoryAllocator<int>(d_context->getCMM()));
+ TS_ASSERT_EQUALS(list->begin(), list->end());
+ }
+
void testDtorCalled() {
bool shouldRemainFalse = false;
bool shouldFlipToTrue = false;
bool shouldAlsoRemainFalse = false;
bool aThirdFalse = false;
- CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listT(d_context, true, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
- CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listF(d_context, false, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+ CDChunkList<DtorSensitiveObject> listT(d_context, true, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+ CDChunkList<DtorSensitiveObject> listF(d_context, false, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
#else /* __APPLE__ */
- CDList<unsigned, ContextMemoryAllocator<unsigned> > list(d_context);
+ CDChunkList<unsigned> list(d_context);
WithLimitedMemory wlm(1);
TS_ASSERT_THROWS({
//Debug.on("gc");
//Debug.on("context");
- CDHashMap<int, CDList<myint>*, int_hasher> map(d_context);
+ CDHashMap<int, CDList_BE<myint>*, int_hasher> map(d_context);
- CDList<myint> *list1, *list2, *list3, *list4;
+ CDList_BE<myint> *list1, *list2, *list3, *list4;
TS_ASSERT(map.find(1) == map.end());
TS_ASSERT(map.find(2) == map.end());
int* x = (int*) d_context->getCMM()->newData(sizeof(int));
- list1 = new(d_context->getCMM()) CDList<myint>(true, d_context);
- list2 = new(d_context->getCMM()) CDList<myint>(true, d_context);
- list3 = new(d_context->getCMM()) CDList<myint>(true, d_context);
- list4 = new(d_context->getCMM()) CDList<myint>(true, d_context);
+ list1 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+ list2 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+ list3 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+ list4 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
list1->push_back(1);
list2->push_back(2);
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<unsigned> copy(CDVector<unsigned>& v){
}
}
- void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r, bool callDestructor) {
- CDVector<unsigned> vec(d_context, callDestructor);
+ void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r) {
+ CDVector<unsigned> vec(d_context);
vector< vector<unsigned> > copies;
copies.push_back( copy(vec) );
projects / cvc5.git / commitdiff