diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /src/context | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* public/private code untangled (smt/smt_engine.h no longer #includes
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/Makefile.am | 7 | ||||
-rw-r--r-- | src/context/cdlist.h | 222 | ||||
-rw-r--r-- | src/context/cdmap.h | 407 | ||||
-rw-r--r-- | src/context/cdo.h | 122 | ||||
-rw-r--r-- | src/context/cdset.h | 33 | ||||
-rw-r--r-- | src/context/context.cpp | 54 | ||||
-rw-r--r-- | src/context/context.h | 532 | ||||
-rw-r--r-- | src/context/context_mm.cpp | 21 | ||||
-rw-r--r-- | src/context/context_mm.h | 26 |
9 files changed, 973 insertions, 451 deletions
diff --git a/src/context/Makefile.am b/src/context/Makefile.am index b36d5e69c..54accdd6e 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -9,5 +9,8 @@ libcontext_la_SOURCES = \ context.cpp \ context.h \ context_mm.cpp \ - context_mm.h - + context_mm.h \ + cdo.h \ + cdlist.h \ + cdmap.h \ + cdset.h diff --git a/src/context/cdlist.h b/src/context/cdlist.h new file mode 100644 index 000000000..5b4ba639a --- /dev/null +++ b/src/context/cdlist.h @@ -0,0 +1,222 @@ +/********************* */ +/** cdlist.h + ** 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. + ** + ** Context-dependent list class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDLIST_H +#define __CVC4__CONTEXT__CDLIST_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * 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> +class CDList : public ContextObj { + /** + * d_list is a dynamic array of objects of type T. + */ + T* d_list; + + /** + * 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 d_list + */ + unsigned d_size; + + /** + * Allocated size of d_list. + */ + unsigned 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. + */ + 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; + } + } + + /** + * Privae 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. + */ + CDList(const CDList<T>& l) : + ContextObj(l), + d_list(NULL), + d_size(l.d_size), + d_sizeAlloc(0) { + } + + /** + * Reallocate the array with more space. + * Throws bad_alloc if memory allocation fails. + */ + 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); + 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) { + throw std::bad_alloc(); + } + d_list = tmpList; + } + } + +public: + /** + * Main constructor: d_list starts as NULL, size is 0 + */ + CDList(Context* context, bool callDestructor = true) + : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), + d_size(0), d_sizeAlloc(0) { } + + /** + * Destructor: delete the list + */ + ~CDList() throw() { + if(d_list != NULL) { + if(d_callDestructor) { + while(d_size != 0) { + --d_size; + d_list[d_size].~T(); + } + } + free(d_list); + } + } + + /** + * Return the current size of (i.e. valid number of objects in) the list + */ + unsigned 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) { + makeCurrent(); + if(d_size == d_sizeAlloc) grow(); + ::new((void*)(d_list + d_size)) T(data); + ++ d_size; + } + + /** + * operator[]: return the ith item in the list + */ + const T& operator[](unsigned i) const { + Assert(i < d_size, "index out of bounds in CDList::operator[]"); + return d_list[i]; + } + + /** + * return the most recent item added to the list + */ + const T& back() const { + Assert(d_size > 0, "CDList::back() called on empty list"); + return d_list[d_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 { + friend class CDList<T>; + T* d_it; + const_iterator(T* it) : d_it(it) {}; + public: + const_iterator() : d_it(NULL) {} + bool operator==(const const_iterator& i) const { return d_it == i.d_it; } + bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } + const T& operator*() const { return *d_it; } + /** Prefix increment */ + const_iterator& operator++() { ++d_it; return *this; } + /** Prefix decrement */ + const_iterator& operator--() { --d_it; return *this; } + }; /* class const_iterator */ + + /** + * Returns an iterator pointing to the first item in the list. + */ + const_iterator begin() const { + return const_iterator(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); + } + +};/* class CDList */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_H */ diff --git a/src/context/cdmap.h b/src/context/cdmap.h new file mode 100644 index 000000000..994ff76b4 --- /dev/null +++ b/src/context/cdmap.h @@ -0,0 +1,407 @@ +/********************* */ +/** cdmap.h + ** 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. + ** + ** Context-dependent map class. Generic templated class for a map + ** which must be saved and restored as contexts are pushed and + ** popped. Requires that operator= be defined for the data class, + ** and operator== for the key class. For key types that don't have a + ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDMAP_H +#define __CVC4__CONTEXT__CDMAP_H + +#include "context/context.h" +#include "util/Assert.h" + +#include <iterator> +#include <ext/hash_map> + +namespace CVC4 { +namespace context { + +// Auxiliary class: almost the same as CDO (see cdo.h), but on +// setNull() call it erases itself from the map. + +template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap; + +template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > +class CDOmap : public ContextObj { + Key d_key; + Data d_data; + bool d_inMap; // whether the data must be in the map + CDMap<Key, Data, HashFcn>* d_cdmap; + + // Doubly-linked list for keeping track of elements in order of insertion + CDOmap<Key, Data, HashFcn>* d_prev; + CDOmap<Key, Data, HashFcn>* d_next; + + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDOmap<Key, Data, HashFcn>(*this); + } + + virtual void restore(ContextObj* data) { + CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data); + if(p->d_inMap) { + d_data = p->d_data; + d_inMap = true; + } else { + // Erase itself from the map and put itself into trash. We cannot + // "delete this" here, because it will break context operations in + // a non-trivial way. + if(d_cdmap->d_map.count(d_key) > 0) { + d_cdmap->d_map.erase(d_key); + d_cdmap->d_trash.push_back(this); + } + + d_prev->d_next = d_next; + d_next->d_prev = d_prev; + + if(d_cdmap->d_first == this) { + d_cdmap->d_first = d_next; + + if(d_next == this) { + d_cdmap->d_first = NULL; + } + } + } + } + +public: + + CDOmap(Context* context, + CDMap<Key, Data, HashFcn>* cdmap, + const Key& key, + const Data& data) : + ContextObj(context), + d_key(key), + d_inMap(false), + d_cdmap(cdmap) { + + set(data); + + CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first; + if(first == NULL) { + first = d_next = d_prev = this; + } else { + d_prev = first->d_prev; + d_next = first; + d_prev->d_next = first->d_prev = this; + } + } + + ~CDOmap() throw(AssertionException) {} + + void set(const Data& data) { + makeCurrent(); + d_data = data; + d_inMap = true; + } + + const Key& getKey() const { + return d_key; + } + + const Data& get() const { + return d_data; + } + + operator Data() { + return get(); + } + + CDOmap<Key, Data, HashFcn>& operator=(const Data& data) { + set(data); + return *this; + } + + CDOmap<Key, Data, HashFcn>* next() const { + if(d_next == d_cdmap->d_first) { + return NULL; + } else { + return d_next; + } + } +};/* class CDOmap */ + +// Dummy subclass of ContextObj to serve as our data class +class CDMapData : public ContextObj { + // befriend CDMap<> so that it can allocate us + template <class Key, class Data, class HashFcn> + friend class CDMap; + + ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDMapData(*this); + } + + void restore(ContextObj* data) {} + +public: + + CDMapData(Context* context) : ContextObj(context) {} + CDMapData(const ContextObj& co) : ContextObj(co) {} +}; + +/** + * Generic templated class for a map which must be saved and restored + * as contexts are pushed and popped. Requires that operator= be + * defined for the data class, and operator== for the key class. + */ +template <class Key, class Data, class HashFcn> +class CDMap : public ContextObj { + + friend class CDOmap<Key, Data, HashFcn>; + + __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map; + + // The vector of CDOmap objects to be destroyed + std::vector<CDOmap<Key, Data, HashFcn>*> d_trash; + CDOmap<Key, Data, HashFcn>* d_first; + Context* d_context; + + // Nothing to save; the elements take care of themselves + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDMapData(*this); + } + + // Similarly, nothing to restore + virtual void restore(ContextObj* data) {} + + // Destroy stale CDOmap objects from trash + void emptyTrash() { + for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator + i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) { + /* + delete *i; + free(*i); + */ + } + d_trash.clear(); + } + +public: + + CDMap(Context* context) : + ContextObj(context), + d_first(NULL), + d_context(context) { + } + + ~CDMap() throw(AssertionException) { + // Delete all the elements and clear the map + for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator + i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { + /* + delete (*i).second; + free((*i).second); + */ + } + d_map.clear(); + emptyTrash(); + } + + // The usual operators of map + + size_t size() const { + return d_map.size(); + } + + size_t count(const Key& k) const { + return d_map.count(k); + } + + typedef CDOmap<Key, Data, HashFcn>& ElementReference; + + // If a key is not present, a new object is created and inserted + CDOmap<Key, Data, HashFcn>& operator[](const Key& k) { + emptyTrash(); + + typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator + i(d_map.find(k)); + + CDOmap<Key, Data, HashFcn>* obj; + if(i == d_map.end()) { // Create new object + obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data()); + d_map[k] = obj; + } else { + obj = (*i).second; + } + return *obj; + } + + void insert(const Key& k, const Data& d) { + emptyTrash(); + + typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator + i(d_map.find(k)); + + if(i == d_map.end()) { // Create new object + CDOmap<Key, Data, HashFcn>* + obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d)); + d_map[k] = obj; + } else { + (*i).second->set(d); + } + } + // FIXME: no erase(), too much hassle to implement efficiently... + + // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>; + // in most cases, this will be functionally similar to pair<const Key, Data>. + class iterator : public std::iterator<std::input_iterator_tag, std::pair<const Key, Data>, std::ptrdiff_t> { + + // Private members + typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator d_it; + + public: + + // Constructor from __gnu_cxx::hash_map + iterator(const typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator& i) : d_it(i) {} + + // Copy constructor + iterator(const iterator& i) : d_it(i.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair<const Key, Data> operator*() const { + const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it); + return std::pair<const Key, Data>(p.first, *p.second); + } + + // Who needs an operator->() for maps anyway?... + // It'd be nice, but not possible by design. + //std::pair<const Key, Data>* operator->() const { + // return &(operator*()); + //} + + // Prefix and postfix increment + iterator& operator++() { + ++d_it; + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair<const Key, Data>* d_pair; + public: + Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {} + std::pair<const Key, Data>& operator*() { + return *d_pair; + } + };/* class CDMap<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the iterator. However, don't try to use Proxy for + // anything else. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; + + iterator begin() const { + return iterator(d_map.begin()); + } + + iterator end() const { + return iterator(d_map.end()); + } + + class orderedIterator { + const CDOmap<Key, Data, HashFcn>* d_it; + + public: + + orderedIterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {} + orderedIterator(const orderedIterator& i) : d_it(i.d_it) {} + + // Default constructor + orderedIterator() {} + + // (Dis)equality + bool operator==(const orderedIterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const orderedIterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair<const Key, Data> operator*() const { + return std::pair<const Key, Data>(d_it->getKey(), d_it->get()); + } + + // Prefix and postfix increment + orderedIterator& operator++() { + d_it = d_it->next(); + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair<const Key, Data>* d_pair; + + public: + + Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {} + + std::pair<const Key, Data>& operator*() { + return *d_pair; + } + };/* class CDMap<>::orderedIterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the orderedIterator. However, don't try to use + // Proxy for anything else. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::orderedIterator */ + + orderedIterator orderedBegin() const { + return orderedIterator(d_first); + } + + orderedIterator orderedEnd() const { + return orderedIterator(NULL); + } + + iterator find(const Key& k) const { + return iterator(d_map.find(k)); + } + +};/* class CDMap<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_H */ diff --git a/src/context/cdo.h b/src/context/cdo.h new file mode 100644 index 000000000..6c30a70f4 --- /dev/null +++ b/src/context/cdo.h @@ -0,0 +1,122 @@ +/********************* */ +/** cdo.h + ** 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. + ** + ** A context-dependent object. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDO_H +#define __CVC4__CONTEXT__CDO_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * Most basic template for context-dependent objects. Simply makes a copy + * (using the copy constructor) of class T when saving, and copies it back + * (using operator=) during restore. + */ +template <class T> +class CDO : public ContextObj { + + /** + * The data of type T being stored in this context-dependent object. + */ + T d_data; + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current data to a copy using the copy constructor. Memory is allocated + * using the ContextMemoryManager. + */ + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDO<T>(*this); + } + + /** + * Implementation of mandatory ContextObj method restore: simply copies the + * saved data back from the saved copy using operator= for T. + */ + virtual void restore(ContextObj* pContextObj) { + d_data = ((CDO<T>*) pContextObj)->d_data; + } + + /** + * Copy constructor - it's private to ensure it is only used by save(). + * Basic CDO objects, cannot be copied-they have to be unique. + */ + CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {} + + /** + * operator= for CDO is private to ensure CDO object is not copied. + */ + CDO<T>& operator=(const CDO<T>& cdo) {} + +public: + /** + * Main constructor - uses default constructor for T to create the initial + * value of d_data. + */ + CDO(Context* context) : ContextObj(context) {} + + /** + * Constructor from object of type T. Creates a ContextObj and sets the data + * to the given data value. Note that this value is only valid in the + * current Scope. If the Scope is popped, the value will revert to whatever + * is assigned by the default constructor for T + */ + CDO(Context* context, const T& data) : ContextObj(context) { + makeCurrent(); + d_data = data; + } + + /** + * Destructor - no need to do anything. + */ + ~CDO() throw() {} + + /** + * Set the data in the CDO. First call makeCurrent. + */ + void set(const T& data) { + makeCurrent(); + d_data = data; + } + + /** + * Get the current data from the CDO. Read-only. + */ + const T& get() const { return d_data; } + + /** + * For convenience, define operator T to be the same as get(). + */ + operator T() { return get(); } + + /** + * For convenience, define operator= that takes an object of type T. + */ + CDO<T>& operator=(const T& data) { + set(data); + return *this; + } + +};/* class CDO */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDO_H */ diff --git a/src/context/cdset.h b/src/context/cdset.h new file mode 100644 index 000000000..48ad12daa --- /dev/null +++ b/src/context/cdset.h @@ -0,0 +1,33 @@ +/********************* */ +/** cdset.h + ** 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. + ** + ** Context-dependent set class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDSET_H +#define __CVC4__CONTEXT__CDSET_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +template <class K, class HashFcn> +class CDSet; + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDSET_H */ diff --git a/src/context/context.cpp b/src/context/context.cpp index 5ff377194..8e87741b5 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -29,7 +29,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) { } -Context::~Context() { +Context::~Context() throw(AssertionException) { // Delete all Scopes popto(0); @@ -38,13 +38,13 @@ Context::~Context() { // Clear ContextNotifyObj lists so there are no dangling pointers ContextNotifyObj* pCNO; - while (d_pCNOpre != NULL) { + while(d_pCNOpre != NULL) { pCNO = d_pCNOpre; pCNO->d_ppCNOprev = NULL; d_pCNOpre = pCNO->d_pCNOnext; pCNO->d_pCNOnext = NULL; } - while (d_pCNOpost != NULL) { + while(d_pCNOpost != NULL) { pCNO = d_pCNOpost; pCNO->d_ppCNOprev = NULL; d_pCNOpost = pCNO->d_pCNOnext; @@ -69,7 +69,7 @@ void Context::pop() { // Notify the (pre-pop) ContextNotifyObj objects ContextNotifyObj* pCNO = d_pCNOpre; - while (pCNO != NULL) { + while(pCNO != NULL) { pCNO->notify(); pCNO = pCNO->d_pCNOnext; } @@ -88,7 +88,7 @@ void Context::pop() { // Notify the (post-pop) ContextNotifyObj objects pCNO = d_pCNOpost; - while (pCNO != NULL) { + while(pCNO != NULL) { pCNO->notify(); pCNO = pCNO->d_pCNOnext; } @@ -99,8 +99,8 @@ void Context::pop() { void Context::popto(int toLevel) { // Pop scopes until there are none left or toLevel is reached - if (toLevel < 0) toLevel = 0; - while (toLevel < getLevel()) pop(); + if(toLevel < 0) toLevel = 0; + while(toLevel < getLevel()) pop(); } @@ -147,19 +147,17 @@ void ContextObj::update() { } -ContextObj* ContextObj::restoreAndContinue() -{ +ContextObj* ContextObj::restoreAndContinue() { // Variable to hold next object in list ContextObj* pContextObjNext; // Check the restore pointer. If NULL, this must be the bottom Scope - if (d_pContextObjRestore == NULL) { + if(d_pContextObjRestore == NULL) { Assert(d_pScope == d_pScope->getContext()->getBottomScope(), "Expected bottom scope"); pContextObjNext = d_pContextObjNext; // Nothing else to do - } - else { + } else { // Call restore to update the subclass data restore(d_pContextObjRestore); @@ -177,48 +175,48 @@ ContextObj* ContextObj::restoreAndContinue() } -ContextObj::ContextObj(Context* pContext) - : d_pContextObjRestore(NULL) -{ +ContextObj::ContextObj(Context* pContext) : + d_pContextObjRestore(NULL) { + Assert(pContext != NULL, "NULL context pointer"); + d_pScope = pContext->getBottomScope(); d_pScope->addToChain(this); } -ContextObj::~ContextObj() -{ +ContextObj::~ContextObj() throw(AssertionException) { for(;;) { - if (next() != NULL) { + if(next() != NULL) { next()->prev() = prev(); } *(prev()) = next(); - if (d_pContextObjRestore == NULL) break; + if(d_pContextObjRestore == NULL) { + break; + } restoreAndContinue(); } } ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { - if (preNotify) { + if(preNotify) { pContext->addNotifyObjPre(this); - } - else { + } else { pContext->addNotifyObjPost(this); } } -ContextNotifyObj::~ContextNotifyObj() -{ - if (d_pCNOnext != NULL) { + +ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) { + if(d_pCNOnext != NULL) { d_pCNOnext->d_ppCNOprev = d_ppCNOprev; } - if (d_ppCNOprev != NULL) { + if(d_ppCNOprev != NULL) { *(d_ppCNOprev) = d_pCNOnext; } } -} /* CVC4::context namespace */ - +} /* CVC4::context namespace */ } /* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 6a35945b7..4e10347d7 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -20,6 +20,7 @@ #include "context/context_mm.h" #include "util/Assert.h" + #include <cstdlib> #include <cstring> #include <new> @@ -32,28 +33,27 @@ class Scope; class ContextObj; class ContextNotifyObj; - /** - * A Context encapsulates all of the dynamic state of the system. Its main - * methods are push() and pop(). A call to push() saves the current state, - * and a call to pop() restores the state saved by the most recent call to - * push(). - * - * Objects which want to participate in this global save and restore - * mechanism must inherit from ContextObj (see below). - * - * For more flexible context-dependent behavior, objects may implement the - * ContextNotifyObj interface and simply get a notification when a pop has - * occurred. - * - * Context also uses a helper class called Scope which stores information - * specific to the portion of the Context since the last call to push() (see - * below). - * - * Memory allocation in Contexts is done with the help of the - * ContextMemoryManager. A copy is stored in each Scope object for quick - * access. - * - */ +/** + * A Context encapsulates all of the dynamic state of the system. Its main + * methods are push() and pop(). A call to push() saves the current state, + * and a call to pop() restores the state saved by the most recent call to + * push(). + * + * Objects which want to participate in this global save and restore + * mechanism must inherit from ContextObj (see below). + * + * For more flexible context-dependent behavior, objects may implement the + * ContextNotifyObj interface and simply get a notification when a pop has + * occurred. + * + * Context also uses a helper class called Scope which stores information + * specific to the portion of the Context since the last call to push() (see + * below). + * + * Memory allocation in Contexts is done with the help of the + * ContextMemoryManager. A copy is stored in each Scope object for quick + * access. + */ class Context { /** @@ -87,7 +87,7 @@ public: /** * Destructor: pop all scopes, delete ContextMemoryManager */ - ~Context(); + ~Context() throw(AssertionException); /** * Return the current (top) scope @@ -107,7 +107,7 @@ public: /** * Return the ContextMemoryManager associated with the context. */ - ContextMemoryManager* getCMM(){ return d_pCMM; } + ContextMemoryManager* getCMM() { return d_pCMM; } /** * Save the current state, create a new Scope @@ -182,15 +182,18 @@ public: * Constructor: Create a new Scope; set the level and the previous Scope * if any. */ - Scope(Context* pContext, ContextMemoryManager* pCMM, int level) - : d_pContext(pContext), d_pCMM(pCMM), d_level(level), - d_pContextObjList(NULL) { } + Scope(Context* pContext, ContextMemoryManager* pCMM, int level) : + d_pContext(pContext), + d_pCMM(pCMM), + d_level(level), + d_pContextObjList(NULL) { + } /** * Destructor: Restore all of the objects in ContextObjList. Defined inline * below. */ - ~Scope(); + ~Scope() throw(); /** * Get the Context for this Scope @@ -223,8 +226,9 @@ public: * Overload operator new for use with ContextMemoryManager to allow creation * of new Scope objects in the current memory region. */ - static void* operator new(size_t size, ContextMemoryManager* pCMM) - { return pCMM->newData(size); } + static void* operator new(size_t size, ContextMemoryManager* pCMM) { + return pCMM->newData(size); + } /** * Overload operator delete for Scope objects allocated using @@ -232,44 +236,44 @@ public: * automatically when the ContextMemoryManager pop() method is called. * Include both placement and standard delete for completeness. */ - static void operator delete(void* pMem, ContextMemoryManager* pCMM) { } - static void operator delete(void* pMem) { } + static void operator delete(void* pMem, ContextMemoryManager* pCMM) {} + static void operator delete(void* pMem) {} //FIXME: //! Check for memory leaks // void check(void); -}; /* class Scope */ - - /** - * This is an abstract base class from which all objects that are context-dependent - * should inherit. For any data structure that you want to have be - * automatically backtracked, do the following: - * 1. Create a class for the data structure that inherits from ContextObj - * 2. Implement save() - * The role of save() is to create a new ContexObj object that contains - * enough information to restore the object to its current state, even if - * it gets changed later. Note that save should call the (default) - * ContextObj Copy Constructor to copy the information in the base class. - * It is recommended that any memory allocated by save() should be done - * through the ContextMemoryManager. This way, it does not need to be - * explicitly freed when restore is called. However, it is only required - * that the ContextObj itself be allocated using the - * ContextMemoryManager. If other memory is allocated not using the - * ContextMemoryManager, it should be freed when restore() is called. In - * fact, any clean-up work on a saved object must be done by restore(). - * This is because the destructor is never called explicitly on saved - * objects. - * 3. Implement restore() - * The role of restore() is, given the ContextObj returned by a previous - * call to save(), to restore the current object to the state it was in - * when save() was called. Note that the implementation of restore does - * *not* need to worry about restoring the base class data. This is done - * automatically. Ideally, restore() should not have to free any memory - * as any memory allocated by save() should have been done using the - * ContextMemoryManager (see item 2 above). - * 4. In the subclass implementation, any time the state is about to be - * changed, first call makeCurrent(). - */ +};/* class Scope */ + +/** + * This is an abstract base class from which all objects that are context-dependent + * should inherit. For any data structure that you want to have be + * automatically backtracked, do the following: + * 1. Create a class for the data structure that inherits from ContextObj + * 2. Implement save() + * The role of save() is to create a new ContexObj object that contains + * enough information to restore the object to its current state, even if + * it gets changed later. Note that save should call the (default) + * ContextObj Copy Constructor to copy the information in the base class. + * It is recommended that any memory allocated by save() should be done + * through the ContextMemoryManager. This way, it does not need to be + * explicitly freed when restore is called. However, it is only required + * that the ContextObj itself be allocated using the + * ContextMemoryManager. If other memory is allocated not using the + * ContextMemoryManager, it should be freed when restore() is called. In + * fact, any clean-up work on a saved object must be done by restore(). + * This is because the destructor is never called explicitly on saved + * objects. + * 3. Implement restore() + * The role of restore() is, given the ContextObj returned by a previous + * call to save(), to restore the current object to the state it was in + * when save() was called. Note that the implementation of restore does + * *not* need to worry about restoring the base class data. This is done + * automatically. Ideally, restore() should not have to free any memory + * as any memory allocated by save() should have been done using the + * ContextMemoryManager (see item 2 above). + * 4. In the subclass implementation, any time the state is about to be + * changed, first call makeCurrent(). + */ class ContextObj { /** * Pointer to Scope in which this object was last modified. @@ -325,6 +329,7 @@ class ContextObj { ContextObj* restoreAndContinue(); protected: + /** * This is a method that must be implemented by all classes inheriting from * ContextObj. See the comment before the class declaration. @@ -341,57 +346,70 @@ protected: * This method checks if the object has been modified in this Scope yet. If * not, it calls update(). */ - void makeCurrent() { if (!(d_pScope->isCurrent())) update(); } + void makeCurrent() { + if(!(d_pScope->isCurrent())) { + update(); + } + } /** - * operator new using ContextMemoryManager (common case used by subclasses - * during save() ). No delete is required for memory allocated this way, - * since it is automatically released when the context is popped. Also note - * that allocations using this operator never have their destructor called, - * so any clean-up has to be done using the restore method. + * operator new using ContextMemoryManager (common case used by + * subclasses during save() ). No delete is required for memory + * allocated this way, since it is automatically released when the + * context is popped. Also note that allocations using this + * operator never have their destructor called, so any clean-up has + * to be done using the restore method. */ static void* operator new(size_t size, ContextMemoryManager* pCMM) { return pCMM->newData(size); } /** - * Corresponding placement delete. Note that this is provided just to - * satisfy the requirement that a placement delete should be provided for - * every placement new. It would only be called if a ContextObj Constructor - * throws an exception after a successful call to the above new operator. + * Corresponding placement delete. Note that this is provided just + * to satisfy the requirement that a placement delete should be + * provided for every placement new. It would only be called if a + * ContextObj constructor throws an exception after a successful + * call to the above new operator. */ - static void operator delete(void* pMem, ContextMemoryManager* pCMM) { } + static void operator delete(void* pMem, ContextMemoryManager* pCMM) {} public: + /** * Create a new ContextObj. The initial scope is set to the bottom - * scope of the Context. Note that in the common case, the copy constructor - * is called to create new ContextObj objects. The default copy constructor - * does the right thing, so we do not explicitly define it. + * scope of the Context. Note that in the common case, the copy + * constructor is called to create new ContextObj objects. The + * default copy constructor does the right thing, so we do not + * explicitly define it. */ ContextObj(Context* context); /** - * Destructor: Calls restore until restored to initial version. Also removes - * object from all Scope lists. Note that this doesn't actually free the - * memory allocated by the ContextMemoryManager for this object. This isn't - * done until the corresponding Scope is popped. + * Destructor: Calls restore until restored to initial version. + * Also removes object from all Scope lists. Note that this doesn't + * actually free the memory allocated by the ContextMemoryManager + * for this object. This isn't done until the corresponding Scope + * is popped. */ - virtual ~ContextObj(); + virtual ~ContextObj() throw(AssertionException); /** - * If you want to allocate a ContextObj object on the heap, use this special - * new operator. To free this memory, instead of "delete p", use - * "p->deleteSelf()". + * If you want to allocate a ContextObj object on the heap, use this + * special new operator. To free this memory, instead of + * "delete p", use "p->deleteSelf()". */ - static void* operator new(size_t size, bool) { return ::operator new(size); } + static void* operator new(size_t size, bool) { + return ::operator new(size); + } /** - * Corresponding placement delete. Note that this is provided for the - * compiler in case the ContextObj constructor throws an exception. The - * client can't call it. + * Corresponding placement delete. Note that this is provided for + * the compiler in case the ContextObj constructor throws an + * exception. The client can't call it. */ - static void operator delete(void* pMem, bool) { ::operator delete(pMem); } + static void operator delete(void* pMem, bool) { + ::operator delete(pMem); + } /** * Use this instead of delete to delete memory allocated using the special @@ -399,7 +417,9 @@ public: * function on memory allocated using the new that takes a * ContextMemoryManager as an argument. */ - void deleteSelf() { ::operator delete(this); } + void deleteSelf() { + ::operator delete(this); + } /** * Disable delete: objects allocated with new(ContextMemorymanager) should @@ -407,23 +427,23 @@ public: * calling deleteSelf(). */ static void operator delete(void* pMem) { - AlwaysAssert(false, "Not Allowed!"); + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); } -}; /* class ContextObj */ +};/* class ContextObj */ /** - * For more flexible context-dependent behavior than that provided by - * ContextObj, objects may implement the ContextNotifyObj interface and - * simply get a notification when a pop has occurred. See Context class for - * how to register a ContextNotifyObj with the Context (you can choose to - * have notification come before or after the ContextObj objects have been - * restored). + * For more flexible context-dependent behavior than that provided + * by ContextObj, objects may implement the ContextNotifyObj + * interface and simply get a notification when a pop has occurred. + * See Context class for how to register a ContextNotifyObj with the + * Context (you can choose to have notification come before or after + * the ContextObj objects have been restored). */ class ContextNotifyObj { /** - * Context is our friend so that when the Context is deleted, any remaining - * ContextNotifyObj can be removed from the Context list. + * Context is our friend so that when the Context is deleted, any + * remaining ContextNotifyObj can be removed from the Context list. */ friend class Context; @@ -451,18 +471,19 @@ class ContextNotifyObj { public: /** - * Constructor for ContextNotifyObj. Parameters are the context to which - * this notify object will be added, and a flag which, if true, tells the - * context to notify this object *before* the ContextObj objects are - * restored. Otherwise, the context notifies the object after the ContextObj - * objects are restored. The default is for notification after. + * Constructor for ContextNotifyObj. Parameters are the context to + * which this notify object will be added, and a flag which, if + * true, tells the context to notify this object *before* the + * ContextObj objects are restored. Otherwise, the context notifies + * the object after the ContextObj objects are restored. The + * default is for notification after. */ ContextNotifyObj(Context* pContext, bool preNotify = false); /** * Destructor: removes object from list */ - virtual ~ContextNotifyObj(); + virtual ~ContextNotifyObj() throw(AssertionException); /** * This is the method called to notify the object of a pop. It must be @@ -473,11 +494,11 @@ public: // Inline functions whose definitions had to be delayed: -inline Scope::~Scope() { +inline Scope::~Scope() throw() { // Call restore() method on each ContextObj object in the list. - // Note that it is the responsibility of restore() to return the next item in - // the list. - while (d_pContextObjList != NULL) { + // Note that it is the responsibility of restore() to return the + // next item in the list. + while(d_pContextObjList != NULL) { d_pContextObjList = d_pContextObjList->restoreAndContinue(); } } @@ -490,290 +511,7 @@ inline void Scope::addToChain(ContextObj* pContextObj) { d_pContextObjList = pContextObj; } - /** - * Most basic template for context-dependent objects. Simply makes a copy - * (using the copy constructor) of class T when saving, and copies it back - * (using operator=) during restore. - */ -template <class T> -class CDO :public ContextObj { - - /** - * The data of type T being stored in this context-dependent object. - */ - T d_data; - - /** - * Implementation of mandatory ContextObj method save: simply copies the - * current data to a copy using the copy constructor. Memory is allocated - * using the ContextMemoryManager. - */ - virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDO<T>(*this); - } - - /** - * Implementation of mandatory ContextObj method restore: simply copies the - * saved data back from the saved copy using operator= for T. - */ - virtual void restore(ContextObj* pContextObj) { - d_data = ((CDO<T>*)pContextObj)->d_data; - } - - /** - * Copy constructor - it's private to ensure it is only used by save(). - * Basic CDO objects, cannot be copied-they have to be unique. - */ - CDO(const CDO<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { } - - /** - * operator= for CDO is private to ensure CDO object is not copied. - */ - CDO<T>& operator=(const CDO<T>& cdo) {} - -public: - /** - * Main constructor - uses default constructor for T to create the initial - * value of d_data. - */ - CDO(Context* context) : ContextObj(context) {} - - /** - * Constructor from object of type T. Creates a ContextObj and sets the data - * to the given data value. Note that this value is only valid in the - * current Scope. If the Scope is popped, the value will revert to whatever - * is assigned by the default constructor for T - */ - CDO(Context* context, const T& data) : ContextObj(context) { - makeCurrent(); d_data = data; - } - - /** - * Destructor - no need to do anything. - */ - ~CDO() {} - - /** - * Set the data in the CDO. First call makeCurrent. - */ - void set(const T& data) { makeCurrent(); d_data = data; } - - /** - * Get the current data from the CDO. Read-only. - */ - const T& get() const { return d_data; } - - /** - * For convenience, define operator T to be the same as get(). - */ - operator T() { return get(); } - - /** - * For convenience, define operator= that takes an object of type T. - */ - CDO<T>& operator=(const T& data) { set(data); return *this; } - -}; /* class CDO */ - - /** - * 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> -class CDList :public ContextObj { - /** - * d_list is a dynamic array of objects of type T. - */ - T* d_list; - - /** - * 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 d_list - */ - unsigned d_size; - - /** - * Allocated size of d_list. - */ - unsigned 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. - */ - 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; - } - } - - /** - * Privae 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. - */ - CDList(const CDList<T>& l): ContextObj(l), d_list(NULL), - d_size(l.d_size), d_sizeAlloc(0) { } - - /** - * Reallocate the array with more space. - * Throws bad_alloc if memory allocation fails. - */ - 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); - 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){ - throw std::bad_alloc(); - } - d_list = tmpList; - } - } - -public: - /** - * Main constructor: d_list starts as NULL, size is 0 - */ - CDList(Context* context, bool callDestructor = true) - : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), - d_size(0), d_sizeAlloc(0) { } - - /** - * Destructor: delete the list - */ - ~CDList() { - if(d_list != NULL) { - if (d_callDestructor) { - while (d_size != 0) { - --d_size; - d_list[d_size].~T(); - } - } - delete d_list; - } - } - - /** - * Return the current size of (i.e. valid number of objects in) the list - */ - unsigned 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) { - makeCurrent(); - if (d_size == d_sizeAlloc) grow(); - ::new((void*)(d_list + d_size)) T(data); - ++ d_size; - } - - /** - * operator[]: return the ith item in the list - */ - const T& operator[](unsigned i) const { - Assert(i < d_size, "index out of bounds in CDList::operator[]"); - return d_list[i]; - } - - /** - * return the most recent item added to the list - */ - const T& back() const { - Assert(d_size > 0, "CDList::back() called on empty list"); - return d_list[d_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 { - friend class CDList<T>; - T* d_it; - const_iterator(T* it) : d_it(it) {}; - public: - const_iterator() : d_it(NULL) {} - bool operator==(const const_iterator& i) const { return d_it == i.d_it; } - bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } - const T& operator*() const { return *d_it; } - /** Prefix increment */ - const_iterator& operator++() { ++d_it; return *this; } - /** Prefix decrement */ - const_iterator& operator--() { --d_it; return *this; } - }; /* class const_iterator */ - - /** - * Returns an iterator pointing to the first item in the list. - */ - const_iterator begin() const { - return const_iterator(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); - } - -}; /* class CDList */ - -template <class T> -class CDMap; - -template <class T> -class CDSet; - -} /* CVC4::context namespace */ - -} /* CVC4 namespace */ +}/* CVC4::context namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__CONTEXT__CONTEXT_H */ - diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index df7d82987..ab81c7486 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -32,9 +32,9 @@ void ContextMemoryManager::newChunk() { "Index should be at the end of the list"); // Create new chunk if no free chunk available - if (d_freeChunks.empty()) { + if(d_freeChunks.empty()) { d_chunkList.push_back((char*)malloc(chunkSizeBytes)); - if (d_chunkList.back() == NULL) { + if(d_chunkList.back() == NULL) { throw std::bad_alloc(); } } @@ -53,31 +53,32 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { // Create initial chunk d_chunkList.push_back((char*)malloc(chunkSizeBytes)); d_nextFree = d_chunkList.back(); - if (d_nextFree == NULL) { + if(d_nextFree == NULL) { throw std::bad_alloc(); } d_endChunk = d_nextFree + chunkSizeBytes; } -ContextMemoryManager::~ContextMemoryManager() { +ContextMemoryManager::~ContextMemoryManager() throw() { // Delete all chunks - while (!d_chunkList.empty()) { + while(!d_chunkList.empty()) { free(d_chunkList.back()); d_chunkList.pop_back(); } - while (!d_freeChunks.empty()) { + while(!d_freeChunks.empty()) { free(d_freeChunks.back()); d_freeChunks.pop_back(); } } + void* ContextMemoryManager::newData(size_t size) { // Use next available free location in current chunk void* res = (void*)d_nextFree; d_nextFree += size; // Check if the request is too big for the chunk - if (d_nextFree > d_endChunk) { + if(d_nextFree > d_endChunk) { newChunk(); res = (void*)d_nextFree; d_nextFree += size; @@ -104,7 +105,7 @@ void ContextMemoryManager::pop() { d_endChunkStack.pop_back(); // Free all the new chunks since the last push - while (d_indexChunkList > d_indexChunkListStack.back()) { + while(d_indexChunkList > d_indexChunkListStack.back()) { d_freeChunks.push_back(d_chunkList.back()); d_chunkList.pop_back(); --d_indexChunkList; @@ -112,7 +113,7 @@ void ContextMemoryManager::pop() { d_indexChunkListStack.pop_back(); // Delete excess free chunks - while (d_freeChunks.size() > maxFreeChunks) { + while(d_freeChunks.size() > maxFreeChunks) { free(d_freeChunks.front()); d_freeChunks.pop_front(); } @@ -120,6 +121,4 @@ void ContextMemoryManager::pop() { } /* CVC4::context namespace */ - - } /* CVC4 namespace */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index c4e5aba4f..04b0c8167 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -25,17 +25,16 @@ namespace CVC4 { namespace context { - - /** - * Region-based memory manager for contexts. Calls to newData provide memory - * from the current region. This memory will persist until the entire - * region is deallocated (by calling pop). - * - * If push is called, the current region is deactivated and pushed on a - * stack, and a new current region is created. A subsequent call to pop - * releases the new region and restores the top region from the stack. - * - */ +/** + * Region-based memory manager for contexts. Calls to newData provide memory + * from the current region. This memory will persist until the entire + * region is deallocated (by calling pop). + * + * If push is called, the current region is deactivated and pushed on a + * stack, and a new current region is created. A subsequent call to pop + * releases the new region and restores the top region from the stack. + * + */ class ContextMemoryManager { /** @@ -102,6 +101,7 @@ class ContextMemoryManager { void newChunk(); public: + /** * Constructor - creates an initial region and an empty stack */ @@ -110,7 +110,7 @@ class ContextMemoryManager { /** * Destructor - deletes all memory in all regions */ - ~ContextMemoryManager(); + ~ContextMemoryManager() throw(); /** * Allocate size bytes from the current region @@ -128,7 +128,7 @@ class ContextMemoryManager { */ void pop(); -}; /* class ContextMemoryManager */ +};/* class ContextMemoryManager */ }/* CVC4::context namespace */ }/* CVC4 namespace */ |