diff options
26 files changed, 1145 insertions, 206 deletions
diff --git a/configure.ac b/configure.ac index de6b3a427..1635f938a 100644 --- a/configure.ac +++ b/configure.ac @@ -305,6 +305,8 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then cd "\`dirname \\"\$0\\"\`" +if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi + current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`) arch=\${current[0]} build=\${current[1]} diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 398de65a3..9e349a06b 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -12,6 +12,10 @@ libcontext_la_SOURCES = \ context_mm.h \ cdo.h \ cdlist.h \ + cdlist_context_memory.h \ + cdlist_forward.h \ cdmap.h \ + cdmap_forward.h \ cdset.h \ + cdset_forward.h \ cdvector.h diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 02418d3df..7edef4121 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -22,23 +22,42 @@ #define __CVC4__CONTEXT__CDLIST_H #include <iterator> +#include <memory> +#include <string> +#include <sstream> #include "context/context.h" +#include "context/context_mm.h" +#include "context/cdlist_forward.h" #include "util/Assert.h" namespace CVC4 { namespace context { /** - * Generic context-dependent dynamic array. Note that for efficiency, this - * implementation makes the following assumptions: + * Generic context-dependent dynamic array. Note that for efficiency, + * this implementation makes the following assumptions: + * * 1. Over time, objects are only added to the list. Objects are only * removed when a pop restores the list to a previous state. + * * 2. T objects can safely be copied using their copy constructor, * operator=, and memcpy. */ -template <class T> +template <class T, class AllocatorT> class CDList : 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 AllocatorT Allocator; + +protected: + + static const size_t INITIAL_SIZE = 10; + static const size_t GROWTH_FACTOR = 2; + /** * d_list is a dynamic array of objects of type T. */ @@ -54,55 +73,33 @@ class CDList : public ContextObj { /** * Number of objects in d_list */ - unsigned d_size; + size_t d_size; /** * Allocated size of d_list. */ - unsigned d_sizeAlloc; - -protected: + size_t d_sizeAlloc; /** - * 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. + * Our allocator. */ - ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDList<T>(*this); - } - - /** - * 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) { - if(d_callDestructor) { - unsigned size = ((CDList<T>*)data)->d_size; - while(d_size != size) { - --d_size; - d_list[d_size].~T(); - } - } else { - d_size = ((CDList<T>*)data)->d_size; - } - } - -private: + Allocator d_allocator; /** - * Private copy constructor used only by save above. d_list and d_sizeAlloc - * are not copied: only the base class information and d_size are needed in - * restore. + * Private copy constructor used only by save(). d_list and + * d_sizeAlloc are not copied: only the base class information and + * d_size are needed in restore. */ - CDList(const CDList<T>& l) : + CDList(const CDList<T, Allocator>& l) : ContextObj(l), d_list(NULL), - d_callDestructor(l.d_callDestructor), + d_callDestructor(false), d_size(l.d_size), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(l.d_allocator) { + Debug("cdlist") << "copy ctor: " << this + << " from " << &l + << " size " << d_size << std::endl; } /** @@ -112,64 +109,133 @@ private: void grow() { if(d_list == NULL) { // Allocate an initial list if one does not yet exist - d_sizeAlloc = 10; - d_list = (T*) malloc(sizeof(T) * d_sizeAlloc); + d_sizeAlloc = INITIAL_SIZE; + Debug("cdlist") << "initial grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << d_sizeAlloc << std::endl; + if(d_sizeAlloc > d_allocator.max_size()) { + d_sizeAlloc = d_allocator.max_size(); + } + d_list = d_allocator.allocate(d_sizeAlloc); if(d_list == NULL) { throw std::bad_alloc(); } } else { // Allocate a new array with double the size - d_sizeAlloc *= 2; - T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc); - if(tmpList == NULL) { + size_t newSize = GROWTH_FACTOR * d_sizeAlloc; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + Assert(newSize > d_sizeAlloc, + "cannot request larger list due to allocator limits"); + } + T* newList = d_allocator.allocate(newSize); + Debug("cdlist") << "2x grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << newSize + << " (from " << d_list + << " to " << newList << ")" << std::endl; + if(newList == NULL) { throw std::bad_alloc(); } - d_list = tmpList; + std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc); + d_allocator.deallocate(d_list, d_sizeAlloc); + d_list = newList; + d_sizeAlloc = 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) CDList<T, Allocator>(*this); + Debug("cdlist") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " sizeAlloc at " << this->d_sizeAlloc + << " d_list is " << this->d_list + << " 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) { + Debug("cdlist") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " call dtor == " << this->d_callDestructor + << " d_list == " << this->d_list << std::endl; + if(this->d_callDestructor) { + const size_t size = ((CDList<T, Allocator>*)data)->d_size; + while(this->d_size != size) { + --this->d_size; + this->d_allocator.destroy(&this->d_list[this->d_size]); + } + } else { + this->d_size = ((CDList<T, Allocator>*)data)->d_size; } + Debug("cdlist") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size + << " sizeAlloc at " << this->d_sizeAlloc << std::endl; } public: + /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(Context* context, bool callDestructor = true) : + CDList(Context* context, bool callDestructor = true, + const Allocator& alloc = Allocator()) : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), d_size(0), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(alloc) { } /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + CDList(bool allocatedInCMM, Context* context, bool callDestructor = true, + const Allocator& alloc = Allocator()) : ContextObj(allocatedInCMM, context), d_list(NULL), d_callDestructor(callDestructor), d_size(0), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(alloc) { } /** * Destructor: delete the list */ ~CDList() throw(AssertionException) { - destroy(); + this->destroy(); - if(d_callDestructor) { - for(unsigned i = 0; i < d_size; ++i) { - d_list[i].~T(); + if(this->d_callDestructor) { + for(size_t i = 0; i < this->d_size; ++i) { + this->d_allocator.destroy(&this->d_list[i]); } } - free(d_list); + this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc); } /** - * Return the current size of (i.e. valid number of objects in) the list + * Return the current size of (i.e. valid number of objects in) the + * list. */ - unsigned size() const { + size_t size() const { return d_size; } @@ -184,20 +250,43 @@ public: * Add an item to the end of the list. */ void push_back(const T& data) { + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": make-current, " + << "d_list == " << d_list << std::endl; makeCurrent(); + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow? " << d_size + << " " << d_sizeAlloc << std::endl; if(d_size == d_sizeAlloc) { + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow!" << std::endl; grow(); } - - ::new((void*)(d_list + d_size)) T(data); + Assert(d_size < d_sizeAlloc); + + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": construct! at " << d_list + << "[" << d_size << "] == " << &d_list[d_size] + << std::endl; + d_allocator.construct(&d_list[d_size], data); + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": done..." << std::endl; ++d_size; + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": size now " << d_size << std::endl; } /** * Access to the ith item in the list. */ - const T& operator[](unsigned i) const { + const T& operator[](size_t i) const { Assert(i < d_size, "index out of bounds in CDList::operator[]"); return d_list[i]; } @@ -211,21 +300,24 @@ public: } /** - * 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). + * 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 { - T* d_it; + T const* d_it; - const_iterator(T* it) : d_it(it) {} + const_iterator(T const* it) : d_it(it) {} - friend class CDList<T>; + friend class CDList<T, Allocator>; public: + // FIXME we support operator--, but do we satisfy all the + // requirements of a bidirectional iterator ? typedef std::input_iterator_tag iterator_category; typedef T value_type; typedef ptrdiff_t difference_type; @@ -289,17 +381,16 @@ public: * Returns an iterator pointing to the first item in the list. */ const_iterator begin() const { - return const_iterator(d_list); + return const_iterator(static_cast<T const*>(d_list)); } /** * Returns an iterator pointing one past the last item in the list. */ const_iterator end() const { - return const_iterator(d_list + d_size); + return const_iterator(static_cast<T const*>(d_list) + d_size); } - -};/* class CDList */ +};/* class CDList<> */ }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h new file mode 100644 index 000000000..f85d3b79e --- /dev/null +++ b/src/context/cdlist_context_memory.h @@ -0,0 +1,493 @@ +/********************* */ +/*! \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 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); + + /** + * 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 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 { + return const_iterator(&d_headSegment, 0); + } + + /** + * 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 */ diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h new file mode 100644 index 000000000..82bc9cc15 --- /dev/null +++ b/src/context/cdlist_forward.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file cdlist_forward.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 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 This is a forward declaration header to declare the + ** CDList<> template + ** + ** This is a forward declaration header to declare the CDList<> + ** template. It's useful if you want to forward-declare CDList<> + ** without including the full cdlist.h or cdlist_context_memory.h + ** header, for example, in a public header context, or to keep + ** compile times low when only a forward declaration is needed. + ** + ** Note that all specializations of the template should be listed + ** here as well, since different specializations are defined in + ** different headers (cdlist.h and cdlist_context_memory.h). + ** Explicitly declaring both specializations here ensure that if you + ** define one, you'll get an error if you didn't include the correct + ** header (avoiding different, incompatible instantiations in + ** different compilation units). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDLIST_FORWARD_H +#define __CVC4__CONTEXT__CDLIST_FORWARD_H + +#include <memory> + +namespace __gnu_cxx { + template <class Key> class hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template <class T> + class ContextMemoryAllocator; + + template <class T, class Allocator = std::allocator<T> > + class CDList; + + template <class T> + class CDList<T, ContextMemoryAllocator<T> >; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */ diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 5a1e52d66..fde69a149 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -23,6 +23,7 @@ #include <new> #include "context/context_mm.h" #include "util/Assert.h" +#include "util/output.h" namespace CVC4 { namespace context { diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 1eb452113..71f7041c7 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -103,7 +103,14 @@ class ContextMemoryManager { */ void newChunk(); - public: +public: + + /** + * Get the maximum allocation size for this memory manager. + */ + static unsigned getMaxAllocationSize() { + return chunkSizeBytes; + } /** * Constructor - creates an initial region and an empty stack @@ -133,6 +140,62 @@ class ContextMemoryManager { };/* class ContextMemoryManager */ +/** + * An STL-like allocator class for allocating from context memory. + */ +template <class T> +class ContextMemoryAllocator { + ContextMemoryManager* d_mm; + +public: + + typedef size_t size_type; + typedef ptrdiff_t difference_type; + typedef T* pointer; + typedef T const* const_pointer; + typedef T& reference; + typedef T const& const_reference; + typedef T value_type; + template <class U> struct rebind { + typedef ContextMemoryAllocator<U> other; + }; + + ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {} + ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {} + ~ContextMemoryAllocator() throw() {} + + ContextMemoryManager* getCMM() { return d_mm; } + T* address(T& v) const { return &v; } + T const* address(T const& v) const { return &v; } + size_t max_size() const throw() { + return ContextMemoryManager::getMaxAllocationSize() / sizeof(T); + } + T* allocate(size_t n, const void* = 0) const { + return static_cast<T*>(d_mm->newData(n * sizeof(T))); + } + void deallocate(T* p, size_t n) const { + /* no explicit delete */ + } + void construct(T* p, T const& v) const { + ::new(reinterpret_cast<void*>(p)) T(v); + } + void destroy(T* p) const { + p->~T(); + } +};/* class ContextMemoryAllocator<T> */ + +template <class T> +inline bool operator==(const ContextMemoryAllocator<T>& a1, + const ContextMemoryAllocator<T>& a2) { + return a1.d_mm == a2.d_mm; +} + +template <class T> +inline bool operator!=(const ContextMemoryAllocator<T>& a1, + const ContextMemoryAllocator<T>& a2) { + return a1.d_mm != a2.d_mm; +} + }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index a336662c3..cb9730d34 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -275,6 +275,25 @@ ${metakind_constPrinters} } } +/** + * Cleanup to be performed when a NodeValue zombie is collected, and + * it has CONSTANT metakind. This calls the destructor for the underlying + * C++ type representing the constant value. See + * NodeManager::reclaimZombies() for more information. + * + * This doesn't support "non-inlined" NodeValues, which shouldn't need this + * kind of cleanup. + */ +inline void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constDeleters} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + inline unsigned getLowerBoundForKind(::CVC4::Kind k) { static const unsigned lbs[] = { 0, /* NULL_EXPR */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 351893feb..c68ba59cd 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -44,6 +44,7 @@ metakind_constantMaps= metakind_compares= metakind_constHashes= metakind_constPrinters= +metakind_constDeleters= metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= @@ -192,6 +193,13 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { out << nv->getConst< $2 >(); break; " + cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'` + metakind_constDeleters="${metakind_constDeleters} + case kind::$1: +#line $lineno \"$kf\" + std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children)); + break; +" } function registerOperatorToKind { @@ -301,6 +309,7 @@ for var in \ metakind_compares \ metakind_constHashes \ metakind_constPrinters \ + metakind_constDeleters \ metakind_ubchildren \ metakind_lbchildren \ metakind_operatorKinds; do diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5c24699b8..4e872ad5c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -164,7 +164,8 @@ void NodeManager::reclaimZombies() { << " [" << nv->d_id << "]: " << *nv << "\n"; // remove from the pool - if(nv->getMetaKind() != kind::metakind::VARIABLE) { + kind::MetaKind mk = nv->getMetaKind(); + if(mk != kind::metakind::VARIABLE) { poolRemove(nv); } @@ -179,6 +180,16 @@ void NodeManager::reclaimZombies() { // decr ref counts of children nv->decrRefCounts(); + if(mk == kind::metakind::CONSTANT) { + // Destroy (call the destructor for) the C++ type representing + // the constant in this NodeValue. This is needed for + // e.g. CVC4::Rational, since it has a gmp internal + // representation that mallocs memory and should be cleaned + // up. (This won't delete a pointer value if used as a + // constant, but then, you should probably use a smart-pointer + // type for a constant payload.) + kind::metakind::deleteNodeValueConstant(nv); + } free(nv); } } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index bc592b4e5..a42f39e15 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -46,6 +46,10 @@ class PlusNodeBuilder; class MultNodeBuilder; class NodeManager; +namespace expr { + class NodeValue; +} + namespace kind { namespace metakind { template < ::CVC4::Kind k, bool pool > @@ -53,6 +57,8 @@ namespace kind { struct NodeValueCompare; struct NodeValueConstPrinter; + + void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv); }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -110,11 +116,13 @@ class NodeValue { friend class ::CVC4::NodeManager; template <Kind k, bool pool> - friend struct ::CVC4::kind::metakind::NodeValueConstCompare; + friend struct ::CVC4::kind::metakind::NodeValueConstCompare; friend struct ::CVC4::kind::metakind::NodeValueCompare; friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; + friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv); + void inc(); void dec(); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 55c158a6f..8bbbbe0be 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -77,7 +77,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Smt*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() @@ -111,7 +111,7 @@ parseCommand returns [CVC4::Command* cmd] * @return the sequence command containing the whole problem */ benchmark returns [CVC4::Command* cmd] - : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK + : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK { $cmd = c; } | EOF { $cmd = 0; } ; @@ -134,7 +134,7 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq] * @return a command corresponding to the attribute */ benchAttribute returns [CVC4::Command* smt_command] -@declarations { +@declarations { std::string name; BenchmarkStatus b_status; Expr expr; @@ -146,12 +146,12 @@ benchAttribute returns [CVC4::Command* smt_command] { smt_command = new AssertCommand(expr); } | FORMULA_TOK annotatedFormula[expr] { smt_command = new CheckSatCommand(expr); } - | STATUS_TOK status[b_status] - { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK - | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK - | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK - | NOTES_TOK STRING_LITERAL + | STATUS_TOK status[b_status] + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK + | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK + | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK + | NOTES_TOK STRING_LITERAL | annotation ; @@ -166,14 +166,14 @@ annotatedFormula[CVC4::Expr& expr] std::string name; std::vector<Expr> args; /* = getExprVector(); */ Expr op; /* Operator expression FIXME: move away kill it */ -} +} : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK + LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); @@ -187,27 +187,27 @@ annotatedFormula[CVC4::Expr& expr] // Semantic predicate not necessary if parenthesized subexpressions // are disallowed - // { isFunction(LT(2)->getText()) }? - LPAREN_TOK + // { isFunction(LT(2)->getText()) }? + LPAREN_TOK parameterizedOperator[op] annotatedFormulas[args,expr] RPAREN_TOK // TODO: check arity { expr = MK_EXPR(op,args); } | /* An ite expression */ - LPAREN_TOK ITE_TOK + LPAREN_TOK ITE_TOK annotatedFormula[expr] - { args.push_back(expr); } + { args.push_back(expr); } annotatedFormula[expr] - { args.push_back(expr); } + { args.push_back(expr); } annotatedFormula[expr] - { args.push_back(expr); } + { args.push_back(expr); } RPAREN_TOK { expr = MK_EXPR(CVC4::kind::ITE, args); } | /* a let/flet binding */ - LPAREN_TOK - (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] + LPAREN_TOK + ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) annotatedFormula[expr] RPAREN_TOK { PARSER_STATE->pushScope(); @@ -222,28 +222,29 @@ annotatedFormula[CVC4::Expr& expr] | NUMERAL_TOK { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } | RATIONAL_TOK - { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string + { // FIXME: This doesn't work because an SMT rational is not a + // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } - | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' + | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ | /* a variable */ ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] - | let_identifier[name,CHECK_DECLARED] + | let_identifier[name,CHECK_DECLARED] | flet_identifier[name,CHECK_DECLARED] ) { expr = PARSER_STATE->getVariable(name); } ; /** - * Matches a sequence of annotated formulas and puts them into the formulas - * vector. + * Matches a sequence of annotated formulas and puts them into the + * formulas vector. * @param formulas the vector to fill with formulas * @param expr an Expr reference for the elements of the sequence - */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every + */ +/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every * time through this rule. */ annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] : ( annotatedFormula[expr] { formulas.push_back(expr); } )+ @@ -317,7 +318,7 @@ builtinOp[CVC4::Kind& kind] /** * Matches an operator. */ -parameterizedOperator[CVC4::Expr& op] +parameterizedOperator[CVC4::Expr& op] : functionSymbol[op] | bitVectorOperator[op] ; @@ -328,7 +329,7 @@ parameterizedOperator[CVC4::Expr& op] bitVectorOperator[CVC4::Expr& op] : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']' { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } - | REPEAT_TOK '[' n = NUMERAL_TOK ']' + | REPEAT_TOK '[' n = NUMERAL_TOK ']' { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']' { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } @@ -337,11 +338,11 @@ bitVectorOperator[CVC4::Expr& op] | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']' { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } + { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } ; /** - * Matches a (possibly undeclared) predicate identifier (returning the string). + * Matches a (possibly undeclared) predicate identifier (returning the string). * @param check what kind of check to do with the symbol */ predicateName[std::string& name, CVC4::parser::DeclarationCheck check] @@ -353,7 +354,7 @@ predicateName[std::string& name, CVC4::parser::DeclarationCheck check] * @param check what kind of check to do with the symbol */ functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_VARIABLE] + : identifier[name,check,SYM_VARIABLE] ; /** @@ -365,9 +366,9 @@ functionSymbol[CVC4::Expr& fun] } : functionName[name,CHECK_DECLARED] { PARSER_STATE->checkFunction(name); - fun = PARSER_STATE->getVariable(name); } + fun = PARSER_STATE->getVariable(name); } ; - + /** * Matches an attribute name from the input (:attribute_name). */ @@ -380,18 +381,18 @@ functionDeclaration std::string name; std::vector<Type> sorts; } - : LPAREN_TOK functionName[name,CHECK_UNDECLARED] + : LPAREN_TOK functionName[name,CHECK_UNDECLARED] t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN_TOK { if( sorts.size() == 1 ) { - Assert( t == sorts[0] ); + Assert( t == sorts[0] ); } else { t = EXPR_MANAGER->mkFunctionType(sorts); } - PARSER_STATE->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); } ; - + /** * Matches the declaration of a predicate and declares it */ @@ -404,13 +405,13 @@ predicateDeclaration { Type t; if( p_sorts.empty() ) { t = EXPR_MANAGER->booleanType(); - } else { + } else { t = EXPR_MANAGER->mkPredicateType(p_sorts); } - PARSER_STATE->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); } ; -sortDeclaration +sortDeclaration @declarations { std::string name; } @@ -418,27 +419,27 @@ sortDeclaration { Debug("parser") << "sort decl: '" << name << "'" << std::endl; PARSER_STATE->mkSort(name); } ; - + /** * Matches a sequence of sort symbols and fills them into the given vector. */ sortList[std::vector<CVC4::Type>& sorts] - : ( t = sortSymbol { sorts.push_back(t); })* + : ( t = sortSymbol { sorts.push_back(t); })* ; /** * Matches the sort symbol, which can be an arbitrary identifier. * @param check the check to perform on the name */ -sortName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_SORT] +sortName[std::string& name, CVC4::parser::DeclarationCheck check] + : identifier[name,check,SYM_SORT] ; sortSymbol returns [CVC4::Type t] @declarations { std::string name; } - : sortName[name,CHECK_NONE] + : sortName[name,CHECK_NONE] { $t = PARSER_STATE->getSort(name); } | BITVECTOR_TOK '[' NUMERAL_TOK ']' { $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); @@ -468,8 +469,8 @@ annotation * @param type the intended namespace for the identifier */ identifier[std::string& id, - CVC4::parser::DeclarationCheck check, - CVC4::parser::SymbolType type] + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] : IDENTIFIER { id = AntlrInput::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id @@ -484,7 +485,7 @@ identifier[std::string& id, * @param check what kinds of check to do on the symbol */ let_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] + CVC4::parser::DeclarationCheck check] : LET_IDENTIFIER { id = AntlrInput::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id @@ -498,7 +499,7 @@ let_identifier[std::string& id, * @param check what kinds of check to do on the symbol */ flet_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] + CVC4::parser::DeclarationCheck check] : FLET_IDENTIFIER { id = AntlrInput::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id @@ -554,7 +555,7 @@ STORE_TOK : 'store'; TILDE_TOK : '~'; XOR_TOK : 'xor'; -// Bitvector tokens +// Bitvector tokens BITVECTOR_TOK : 'BitVec'; BV_TOK : 'bv'; CONCAT_TOK : 'concat'; @@ -612,7 +613,7 @@ IDENTIFIER /** * Matches an identifier starting with a colon. */ -ATTR_IDENTIFIER +ATTR_IDENTIFIER : ':' IDENTIFIER ; @@ -622,7 +623,7 @@ ATTR_IDENTIFIER LET_IDENTIFIER : '?' IDENTIFIER ; - + /** * Matches an identifier starting with a dollar sign. */ @@ -663,14 +664,14 @@ RATIONAL_TOK * Matches a double quoted string literal. Escaping is supported, and escape * character '\' has to be escaped. */ -STRING_LITERAL +STRING_LITERAL : '"' (ESCAPE | ~('"'|'\\'))* '"' ; /** * Matches the comments and ignores them */ -COMMENT +COMMENT : ';' (~('\n' | '\r'))* { $channel = HIDDEN;; } ; @@ -679,7 +680,7 @@ COMMENT * Matches any letter ('a'-'z' and 'A'-'Z'). */ fragment -ALPHA +ALPHA : 'a'..'z' | 'A'..'Z' ; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 594efcc35..e3c8c584c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,6 +26,7 @@ #include "smt/no_such_function_exception.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdset.h" #include "expr/expr.h" #include "expr/command.h" #include "expr/node_builder.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d6940f09f..a3116dfa9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -27,6 +27,7 @@ #include "expr/expr_manager.h" #include "context/cdmap_forward.h" #include "context/cdset_forward.h" +#include "context/cdlist_forward.h" #include "util/result.h" #include "util/model.h" #include "util/sexpr.h" @@ -52,7 +53,6 @@ class DecisionEngine; namespace context { class Context; - template <class T> class CDList; }/* CVC4::context namespace */ namespace prop { diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index 27abd8873..98a202207 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -31,7 +31,7 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithConstants{ +class ArithConstants { public: Rational d_ZERO; Rational d_ONE; @@ -52,10 +52,16 @@ public: d_ONE_NODE(nm->mkConst(d_ONE)), d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE)) {} -}; -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ + ~ArithConstants() { + d_ZERO_NODE = Node::null(); + d_ONE_NODE = Node::null(); + d_NEGATIVE_ONE_NODE = Node::null(); + } +};/* class ArithConstants */ + +}/* namespace CVC4::theory::arith */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ #endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index 4b7dfcef5..415668b49 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -33,7 +33,7 @@ EOF template=$1; shift -theoryof_table_includes= +theoryof_table_forwards= theoryof_table_registers= seen_theory=false @@ -61,7 +61,23 @@ function theory { echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi - theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\" + decl= + last= + num=0 + for ns in `echo "$1" | sed 's,::, ,g'`; do + if [ -n "$last" ]; then + decl="${decl}namespace $last { " + let ++num + fi + last="$ns" + done + decl="${decl}class $last;" + while [ $num -gt 0 ]; do + decl="${decl} }" + let --num + done + + theoryof_table_forwards="${theoryof_table_forwards}$decl // #include \"theory/$b/$2\" " theoryof_table_registers="${theoryof_table_registers} /* from $b */ @@ -103,7 +119,7 @@ function constant { function do_theoryof { check_theory_seen - theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = th; + theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = (Theory*)th; " } @@ -135,7 +151,7 @@ check_builtin_theory_seen ## output text=$(cat "$template") -for var in theoryof_table_includes theoryof_table_registers; do +for var in theoryof_table_forwards theoryof_table_registers; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 384e2fdd6..29aed8426 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -16,6 +16,9 @@ ** The theory engine. **/ +#include <vector> +#include <list> + #include "theory/theory_engine.h" #include "expr/node.h" #include "expr/attribute.h" @@ -23,8 +26,14 @@ #include "expr/node_builder.h" #include "smt/options.h" -#include <vector> -#include <list> +#include "theory/builtin/theory_builtin.h" +#include "theory/booleans/theory_bool.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/morgan/theory_uf_morgan.h" +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/arith/theory_arith.h" +#include "theory/arrays/theory_arrays.h" +#include "theory/bv/theory_bv.h" using namespace std; @@ -141,19 +150,19 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); - d_sharedTermManager->registerTheory(d_builtin); - d_sharedTermManager->registerTheory(d_bool); - d_sharedTermManager->registerTheory(d_uf); - d_sharedTermManager->registerTheory(d_arith); - d_sharedTermManager->registerTheory(d_arrays); - d_sharedTermManager->registerTheory(d_bv); - - d_theoryOfTable.registerTheory(d_builtin); - d_theoryOfTable.registerTheory(d_bool); - d_theoryOfTable.registerTheory(d_uf); - d_theoryOfTable.registerTheory(d_arith); - d_theoryOfTable.registerTheory(d_arrays); - d_theoryOfTable.registerTheory(d_bv); + d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); + d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); + d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); + d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); + d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); + d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); + + d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin)); + d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool)); + d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf)); + d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith)); + d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays)); + d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv)); } TheoryEngine::~TheoryEngine() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2d056af28..85e6d2cfc 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -24,18 +24,8 @@ #include "expr/node.h" #include "theory/theory.h" #include "theory/theoryof_table.h" - #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/arith/theory_arith.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/bv/theory_bv.h" - #include "util/stats.h" namespace CVC4 { @@ -119,21 +109,19 @@ class TheoryEngine { d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } - }; - - + };/* class EngineOutputChannel */ EngineOutputChannel d_theoryOut; /** Pointer to Shared Term Manager */ SharedTermManager* d_sharedTermManager; - theory::builtin::TheoryBuiltin* d_builtin; - theory::booleans::TheoryBool* d_bool; - theory::uf::TheoryUF* d_uf; - theory::arith::TheoryArith* d_arith; - theory::arrays::TheoryArrays* d_arrays; - theory::bv::TheoryBV* d_bv; + theory::Theory* d_builtin; + theory::Theory* d_bool; + theory::Theory* d_uf; + theory::Theory* d_arith; + theory::Theory* d_arrays; + theory::Theory* d_bv; /** * Debugging flag to ensure that shutdown() is called before the diff --git a/src/theory/theoryof_table_template.h b/src/theory/theoryof_table_template.h index e0d6fc8c8..5da28f2d4 100644 --- a/src/theory/theoryof_table_template.h +++ b/src/theory/theoryof_table_template.h @@ -25,7 +25,7 @@ #include "expr/kind.h" #include "util/Assert.h" -${theoryof_table_includes} +${theoryof_table_forwards} namespace CVC4 { namespace theory { diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index fe1f3106e..4ee698721 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -34,12 +34,10 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : d_cc(ctxt, &d_ccChannel), d_unionFind(ctxt), d_disequalities(ctxt), - d_disequality(ctxt), d_conflict(), d_trueNode(), d_falseNode(), - d_trueEqFalseNode(), - d_activeAssertions(ctxt) { + d_trueEqFalseNode() { NodeManager* nm = NodeManager::currentNM(); TypeNode boolType = nm->booleanType(); d_trueNode = nm->mkVar("TRUE_UF", boolType); @@ -51,6 +49,9 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) : } TheoryUFMorgan::~TheoryUFMorgan() { + d_trueNode = Node::null(); + d_falseNode = Node::null(); + d_trueEqFalseNode = Node::null(); } RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) { @@ -189,11 +190,6 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { d_unionFind[a] = b; - if(Debug.isOn("uf") && find(d_trueNode) == find(d_falseNode)) { - Debug("uf") << "ok, pay attention now.." << std::endl; - dump(); - } - DiseqLists::iterator deq_i = d_disequalities.find(a); if(deq_i != d_disequalities.end()) { // a set of other trees we are already disequal to @@ -268,7 +264,8 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { DiseqLists::iterator deq_i = d_disequalities.find(of); DiseqList* deq; if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) DiseqList(true, getContext()); + deq = new(getContext()->getCMM()) DiseqList(true, getContext(), false, + ContextMemoryAllocator<TNode>(getContext()->getCMM())); d_disequalities.insertDataFromContextMemory(of, deq); } else { deq = (*deq_i).second; @@ -298,7 +295,7 @@ void TheoryUFMorgan::check(Effort level) { Node assertion = get(); - d_activeAssertions.push_back(assertion); + //d_activeAssertions.push_back(assertion); Debug("uf") << "uf check(): " << assertion << std::endl; @@ -349,7 +346,6 @@ void TheoryUFMorgan::check(Effort level) { Node b = assertion[0][1]; addDisequality(assertion[0]); - d_disequality.push_back(assertion[0]); d_cc.addTerm(a); d_cc.addTerm(b); @@ -418,14 +414,17 @@ void TheoryUFMorgan::check(Effort level) { Unhandled(assertion.getKind()); } + /* if(Debug.isOn("uf")) { dump(); } + */ } Assert(d_conflict.isNull()); Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl; + /* for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); diseqIter != d_disequality.end(); ++diseqIter) { @@ -443,6 +442,7 @@ void TheoryUFMorgan::check(Effort level) { Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right)); } + */ Debug("uf") << "uf: end check(" << level << ")" << std::endl; } @@ -477,6 +477,7 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { } } +/* void TheoryUFMorgan::dump() { if(!Debug.isOn("uf")) { return; @@ -509,3 +510,4 @@ void TheoryUFMorgan::dump() { } Debug("uf") << "=======================================" << std::endl; } +*/ diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 7a12f216b..023e100a9 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -11,16 +11,13 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. - ** - ** This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. It is based on the Nelson-Oppen algorithm given in - ** "Fast Decision Procedures Based on Congruence Closure" - ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) - ** This has been extended to work in a context-dependent way. - ** This interacts heavily with the data-structures given in ecdata.h . + ** \brief Implementation of the theory of uninterpreted functions with + ** equality ** + ** Implementation of the theory of uninterpreted functions with equality, + ** based on CVC4's congruence closure module (which is in turn based on + ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and + ** Extensions. **/ #include "cvc4_private.h" @@ -35,7 +32,7 @@ #include "theory/uf/theory_uf.h" #include "context/context.h" -#include "context/cdo.h" +#include "context/context_mm.h" #include "context/cdlist.h" #include "util/congruence_closure.h" @@ -81,19 +78,17 @@ private: typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind; UnionFind d_unionFind; - typedef context::CDList<Node> DiseqList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList; typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists; /** List of all disequalities this theory has seen. */ DiseqLists d_disequalities; - context::CDList<Node> d_disequality; - Node d_conflict; Node d_trueNode, d_falseNode, d_trueEqFalseNode; - context::CDList<Node> d_activeAssertions; + //context::CDList<Node> d_activeAssertions; public: diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index cc18a3305..db9d5bc65 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -28,9 +28,11 @@ #include "expr/node_manager.h" #include "expr/node.h" +#include "context/context_mm.h" +#include "context/cdo.h" #include "context/cdmap.h" #include "context/cdset.h" -#include "context/cdlist.h" +#include "context/cdlist_context_memory.h" #include "util/exception.h" namespace CVC4 { @@ -102,9 +104,9 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap; - typedef context::CDList<Node> ClassList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList; typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists; - typedef context::CDList<Node> UseList; + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList; typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists; typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap; @@ -348,7 +350,8 @@ private: UseLists::iterator usei = d_useList.find(of); UseList* ul; if(usei == d_useList.end()) { - ul = new(d_context->getCMM()) UseList(true, d_context); + ul = new(d_context->getCMM()) UseList(true, d_context, false, + context::ContextMemoryAllocator<TNode>(d_context->getCMM())); d_useList.insertDataFromContextMemory(of, ul); } else { ul = (*usei).second; @@ -549,7 +552,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { ClassLists::iterator cl_bpi = d_classList.find(bp); ClassList* cl_bp; if(cl_bpi == d_classList.end()) { - cl_bp = new(d_context->getCMM()) ClassList(true, d_context); + cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false, + context::ContextMemoryAllocator<TNode>(d_context->getCMM())); d_classList.insertDataFromContextMemory(bp, cl_bp); Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl; } else { diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 744ec5775..fca3c4ef8 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -10,7 +10,8 @@ TESTS = bug143.smt \ C880mul.miter.shuffled-as.sat03-348.smt \ comb2.shuffled-as.sat03-420.smt \ hole10.cvc \ - instance_1151.smt + instance_1151.smt \ + NEQ016_size5.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/uf/NEQ016_size5.smt b/test/regress/regress3/NEQ016_size5.smt index ec56385f6..ec56385f6 100644 --- a/test/regress/regress0/uf/NEQ016_size5.smt +++ b/test/regress/regress3/NEQ016_size5.smt diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 83dc888d4..af9e447ed 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -25,6 +25,7 @@ UNIT_TESTS = \ context/context_mm_black \ context/cdo_black \ context/cdlist_black \ + context/cdlist_context_memory_black \ context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h new file mode 100644 index 000000000..2f3c27ddb --- /dev/null +++ b/test/unit/context/cdlist_context_memory_black.h @@ -0,0 +1,158 @@ +/********************* */ +/*! \file cdlist_context_memory_black.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 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 Black box testing of CVC4::context::CDList<>. + ** + ** Black box testing of CVC4::context::CDList<>. + **/ + +#include <cxxtest/TestSuite.h> + +#include <vector> +#include <iostream> + +#include <limits.h> + +#include "memory.h" + +#include "context/context.h" +#include "context/cdlist_context_memory.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4::test; + +struct DtorSensitiveObject { + bool& d_dtorCalled; + DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} + ~DtorSensitiveObject() { d_dtorCalled = true; } +}; + +class CDListContextMemoryBlack : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context(); + } + + void tearDown() { + delete d_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 listTest(int N) { + listTest(N, true); + listTest(N, false); + } + + void listTest(int N, bool callDestructor) { + CDList<int, ContextMemoryAllocator<int> > + list(d_context, callDestructor, ContextMemoryAllocator<int>(d_context->getCMM())); + + TS_ASSERT(list.empty()); + for(int i = 0; i < N; ++i) { + TS_ASSERT_EQUALS(list.size(), unsigned(i)); + list.push_back(i); + TS_ASSERT(!list.empty()); + TS_ASSERT_EQUALS(list.back(), i); + int i2 = 0; + for(CDList<int, ContextMemoryAllocator<int> >::const_iterator j = list.begin(); + j != list.end(); + ++j) { + TS_ASSERT_EQUALS(*j, i2++); + } + } + TS_ASSERT_EQUALS(list.size(), unsigned(N)); + + for(int i = 0; i < N; ++i) { + TS_ASSERT_EQUALS(list[i], i); + } + } + + void testDtorCalled() { + bool shouldRemainFalse = false; + bool shouldFlipToTrue = false; + bool alsoFlipToTrue = 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())); + + DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse); + DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue); + DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue); + DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse); + DtorSensitiveObject aThirdFalseDSO(aThirdFalse); + + listT.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + + d_context->push(); + + listT.push_back(shouldFlipToTrueDSO); + listT.push_back(alsoFlipToTrueDSO); + + listF.push_back(shouldRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(aThirdFalseDSO); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, false); + TS_ASSERT_EQUALS(alsoFlipToTrue, false); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); + + d_context->pop(); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, true); + TS_ASSERT_EQUALS(alsoFlipToTrue, true); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); + } + + /* setrlimit() totally broken on Mac OS X */ + void testOutOfMemory() { +#ifdef __APPLE__ + + TS_WARN("can't run memory tests on Mac OS X"); + +#else /* __APPLE__ */ + + CDList<unsigned, ContextMemoryAllocator<unsigned> > list(d_context); + WithLimitedMemory wlm(1); + + TS_ASSERT_THROWS({ + // We cap it at UINT_MAX, preferring to terminate with a + // failure than run indefinitely. + for(unsigned i = 0; i < UINT_MAX; ++i) { + list.push_back(i); + } + }, bad_alloc); + +#endif /* __APPLE__ */ + } +}; |