summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/context/cdchunk_list.h (renamed from src/context/cdlist_context_memory.h)63
-rw-r--r--src/context/cdlist.h58
-rw-r--r--src/context/cdlist_forward.h18
-rw-r--r--src/context/cdqueue.h45
-rw-r--r--src/context/cdvector.h131
-rw-r--r--src/theory/arith/partial_model.h8
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/datatypes/theory_datatypes.h4
-rw-r--r--src/util/congruence_closure.h6
-rw-r--r--test/unit/context/cdlist_black.h36
-rw-r--r--test/unit/context/cdlist_context_memory_black.h32
-rw-r--r--test/unit/context/cdmap_black.h12
-rw-r--r--test/unit/context/cdvector_black.h8
13 files changed, 236 insertions, 187 deletions
diff --git a/src/context/cdlist_context_memory.h b/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 <iterator>
#include <memory>
-#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 T>
-class CDList<T, ContextMemoryAllocator<T> > : 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<T> 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<T, ContextMemoryAllocator<T> >::ListSegment */
+ };/* struct CDChunkList<T>::ListSegment */
/**
* The first segment of list memory.
@@ -126,12 +125,12 @@ protected:
Allocator d_allocator;
/**
- * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >.
+ * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
*/
- struct CDListSave : public ContextObj {
+ struct CDChunkListSave : public ContextObj {
ListSegment* d_tail;
size_t d_tailSize, d_size, d_sizeAlloc;
- CDListSave(const CDList<T, Allocator>& list, ListSegment* tail,
+ CDChunkListSave(const CDChunkList<T>& 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<T, ContextMemoryAllocator<T> >::CDListSave */
+ };/* struct CDChunkList<T>::CDChunkListSave */
/**
* Private copy constructor undefined (no copy permitted).
*/
- CDList(const CDList<T, Allocator>& l) CVC4_UNDEFINED;
+ CDChunkList(const CDChunkList<T>& 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<CDListSave*>(data);
+ CDChunkListSave* save = static_cast<CDChunkListSave*>(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<T, Allocator>;
+ friend class CDChunkList<T>;
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<T, ContextMemoryAllocator<T> > */
+};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
}/* 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 <boost/static_assert.hpp>
+
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 <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;
@@ -84,6 +89,11 @@ private:
size_t d_sizeAlloc;
/**
+ * The CleanUp functor.
+ */
+ CleanUp d_cleanUp;
+
+ /**
* Our allocator.
*/
Allocator d_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<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
@@ -157,7 +168,7 @@ private:
* 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
@@ -179,7 +190,7 @@ protected:
<< " 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
@@ -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<T, Allocator>;
+ friend class CDList<T, CleanUp, Allocator>;
public:
@@ -412,6 +429,23 @@ 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 */
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 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 */
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 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. */
@@ -48,8 +54,8 @@ protected:
/**
* 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) {}
@@ -60,7 +66,7 @@ protected:
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
@@ -80,7 +86,7 @@ protected:
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);
}
@@ -88,26 +94,29 @@ protected:
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);
}
/**
@@ -117,13 +126,13 @@ public:
*/
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;
}
}
@@ -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<T>::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<T>::d_list[CDList<T>::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 <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();
}
@@ -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<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 */
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<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;
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<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;
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<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;
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<int> list(d_context, callDestructor);
+ CDList_BE<int> 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<int>::const_iterator j = list.begin();
+ for(CDList_BE<int>::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<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);
@@ -136,15 +135,10 @@ public:
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 */
@@ -155,7 +149,7 @@ public:
#else /* __APPLE__ */
- CDList<unsigned> list(d_context);
+ CDList_BE<unsigned> 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<int, ContextMemoryAllocator<int> >
+ CDChunkList<int>
list(d_context, callDestructor, ContextMemoryAllocator<int>(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<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++);
@@ -91,6 +91,14 @@ public:
}
}
+ 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;
@@ -98,8 +106,8 @@ public:
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);
@@ -142,7 +150,7 @@ public:
#else /* __APPLE__ */
- CDList<unsigned, ContextMemoryAllocator<unsigned> > list(d_context);
+ CDChunkList<unsigned> 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, 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());
@@ -947,10 +947,10 @@ public:
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);
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<unsigned> copy(CDVector<unsigned>& v){
@@ -87,8 +87,8 @@ public:
}
}
- 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) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback