diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-12 23:52:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-12 23:52:14 +0000 |
commit | c8e9b1d6422b56476a2efb3fbaf19bce66de4c2b (patch) | |
tree | aa2b6400b7a5663599eff687310c509156ca788d /src/context | |
parent | 856567b63c56b238db8a5bb84ad0da7990c1f1eb (diff) |
* src/context/cdmap.h: rename orderedIterator to iterator, do away
with old iterator (closes bug #47).
* src/context/cdset.h: implemented.
* src/expr/node_builder.h: fixed all the strict-aliasing warnings.
* Remove Node::hash() and Expr::hash() (they had been aliases for
getId()). There's now a NodeValue::internalHash(), for internal
expr package purposes only, that doesn't depend on the ID. That's
the only hashing of Nodes or Exprs.
* Automake-quiet generation of kind.h, theoryof_table.h, and CVC and
SMT parsers.
* various minor code cleanups.
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/cdlist.h | 102 | ||||
-rw-r--r-- | src/context/cdmap.h | 126 | ||||
-rw-r--r-- | src/context/cdo.h | 2 | ||||
-rw-r--r-- | src/context/cdset.h | 96 | ||||
-rw-r--r-- | src/context/context.h | 52 |
5 files changed, 231 insertions, 147 deletions
diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 5b4ba639a..fd50d4149 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -56,6 +56,8 @@ class CDList : public ContextObj { */ unsigned d_sizeAlloc; +protected: + /** * Implementation of mandatory ContextObj method save: simply copies the * current size to a copy using the copy constructor (the pointer and the @@ -83,8 +85,10 @@ class CDList : public ContextObj { } } +private: + /** - * Privae copy constructor used only by save above. d_list and d_sizeAlloc + * 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. */ @@ -122,14 +126,18 @@ 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) { } + 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() { + ~CDList() throw(AssertionException) { if(d_list != NULL) { if(d_callDestructor) { while(d_size != 0) { @@ -144,26 +152,33 @@ public: /** * Return the current size of (i.e. valid number of objects in) the list */ - unsigned size() const { return d_size; } - + unsigned size() const { + return d_size; + } /** * Return true iff there are no valid objects in the list. */ - bool empty() const { return d_size == 0; } + 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(); + + if(d_size == d_sizeAlloc) { + grow(); + } + ::new((void*)(d_list + d_size)) T(data); - ++ d_size; + ++d_size; } /** - * operator[]: return the ith item in the list + * Access to the ith item in the list. */ const T& operator[](unsigned i) const { Assert(i < d_size, "index out of bounds in CDList::operator[]"); @@ -171,11 +186,11 @@ public: } /** - * return the most recent item added to the list + * 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_list[d_size-1]; + return d_list[d_size - 1]; } /** @@ -186,19 +201,66 @@ public: * 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) {}; + + const_iterator(T* it) : d_it(it) {} + + friend class CDList<T>; + 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; } + + inline bool operator==(const const_iterator& i) const { + return d_it == i.d_it; + } + + inline bool operator!=(const const_iterator& i) const { + return d_it != i.d_it; + } + + inline const T& operator*() const { + return *d_it; + } + /** Prefix increment */ - const_iterator& operator++() { ++d_it; return *this; } + const_iterator& operator++() { + ++d_it; + return *this; + } + /** Prefix decrement */ const_iterator& operator--() { --d_it; return *this; } - }; /* class const_iterator */ + + // Postfix operations on iterators: requires a Proxy object to + // hold the intermediate value for dereferencing + class Proxy { + const T* d_t; + + public: + + Proxy(const T& p): d_t(&p) {} + + T& operator*() { + return *d_t; + } + };/* class CDList<>::const_iterator::Proxy */ + + /** Postfix increment: returns Proxy with the old value. */ + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + + /** Postfix decrement: returns Proxy with the old value. */ + Proxy operator--(int) { + Proxy e(*(*this)); + --(*this); + return e; + } + + };/* class CDList<>::const_iterator */ /** * Returns an iterator pointing to the first item in the list. diff --git a/src/context/cdmap.h b/src/context/cdmap.h index dc3448e52..b1bb47c4c 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -163,7 +163,8 @@ class CDMap : public ContextObj { friend class CDOmap<Key, Data, HashFcn>; - __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map; + typedef __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> table_type; + table_type d_map; // The vector of CDOmap objects to be destroyed std::vector<CDOmap<Key, Data, HashFcn>*> d_trash; @@ -200,7 +201,7 @@ public: ~CDMap() throw(AssertionException) { // Delete all the elements and clear the map - for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator + for(typename table_type::iterator i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { /* delete (*i).second; @@ -227,11 +228,10 @@ public: 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)); + typename table_type::iterator i = d_map.find(k); CDOmap<Key, Data, HashFcn>* obj; - if(i == d_map.end()) { // Create new object + 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 { @@ -243,8 +243,7 @@ public: 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); + typename table_type::iterator i = d_map.find(k); if(i == d_map.end()) {// create new object CDOmap<Key, Data, HashFcn>* @@ -257,19 +256,12 @@ public: // 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; + class iterator { + const CDOmap<Key, Data, HashFcn>* 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 CDOmap<Key, Data, HashFcn>* p) : d_it(p) {} iterator(const iterator& i) : d_it(i.d_it) {} // Default constructor @@ -285,80 +277,11 @@ public: // 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++() { + // Prefix increment + iterator& operator++() { d_it = d_it->next(); return *this; } @@ -370,34 +293,41 @@ public: public: - Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {} + Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {} - std::pair<const Key, Data>& operator*() { + const std::pair<const Key, Data>& operator*() const { return *d_pair; } - };/* class CDMap<>::orderedIterator::Proxy */ + };/* 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 orderedIterator. However, don't try to use // Proxy for anything else. - Proxy operator++(int) { + const Proxy operator++(int) { Proxy e(*(*this)); ++(*this); return e; } - };/* class CDMap<>::orderedIterator */ + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; - orderedIterator orderedBegin() const { - return orderedIterator(d_first); + iterator begin() const { + return iterator(d_first); } - orderedIterator orderedEnd() const { - return orderedIterator(NULL); + iterator end() const { + return iterator(NULL); } iterator find(const Key& k) const { - return iterator(d_map.find(k)); + typename table_type::const_iterator i = d_map.find(k); + if(i == d_map.end()) { + return end(); + } else { + return iterator((*i).second); + } } };/* class CDMap<> */ diff --git a/src/context/cdo.h b/src/context/cdo.h index 6c30a70f4..aca48d264 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -63,7 +63,7 @@ class CDO : public ContextObj { /** * operator= for CDO is private to ensure CDO object is not copied. */ - CDO<T>& operator=(const CDO<T>& cdo) {} + CDO<T>& operator=(const CDO<T>& cdo); public: /** diff --git a/src/context/cdset.h b/src/context/cdset.h index 48ad12daa..f51e689d5 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -24,8 +24,100 @@ namespace CVC4 { namespace context { -template <class K, class HashFcn> -class CDSet; +template <class V, class HashFcn> +class CDSet : protected CDMap<V, V, HashFcn> { + typedef CDMap<V, V, HashFcn> super; + +public: + + CDSet(Context* context) : + super(context) { + } + + size_t size() const { + return super::size(); + } + + size_t count(const V& v) const { + return super::count(v); + } + + void insert(const V& v) { + super::insert(v, v); + } + + // FIXME: no erase(), too much hassle to implement efficiently... + + class iterator { + typename super::iterator d_it; + + public: + + iterator(const typename super::iterator& it) : d_it(it) {} + iterator(const iterator& it) : d_it(it.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. + V operator*() const { + return (*d_it).first; + } + + // Prefix increment + iterator& operator++() { + ++d_it; + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const V& d_val; + + public: + + Proxy(const V& v) : d_val(v) {} + + V operator*() const { + return d_val; + } + };/* class CDSet<>::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 orderedIterator. However, don't try to use + // Proxy for anything else. + const Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDSet<>::iterator */ + + typedef iterator const_iterator; + + const_iterator begin() const { + return iterator(super::begin()); + } + + const_iterator end() const { + return iterator(super::end()); + } + + const_iterator find(const V& v) const { + return iterator(super::find(v)); + } + +};/* class CDSet */ }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 4e10347d7..69e8fe776 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -134,23 +134,23 @@ public: */ void addNotifyObjPost(ContextNotifyObj* pCNO); -}; /* class Context */ - - /** - * Conceptually, a Scope encapsulates that portion of the context that - * changes after a call to push() and must be undone on a subsequent call to - * pop(). In particular, each call to push() creates a new Scope object . - * This new Scope object becomes the top scope and it points (via the - * d_pScopePrev member) to the previous top Scope. Each call to pop() - * deletes the current top scope and restores the previous one. The main - * purpose of a Scope is to maintain a linked list of ContexObj objects which - * change while the Scope is the top scope and which must be restored when - * the Scope is deleted. - * - * A Scope is also associated with a ContextMemoryManager. All memory - * allocated by the Scope is allocated in a single region using the - * ContextMemoryManager and released all at once when the Scope is popped. - */ +};/* class Context */ + +/** + * Conceptually, a Scope encapsulates that portion of the context that + * changes after a call to push() and must be undone on a subsequent call to + * pop(). In particular, each call to push() creates a new Scope object . + * This new Scope object becomes the top scope and it points (via the + * d_pScopePrev member) to the previous top Scope. Each call to pop() + * deletes the current top scope and restores the previous one. The main + * purpose of a Scope is to maintain a linked list of ContexObj objects which + * change while the Scope is the top scope and which must be restored when + * the Scope is deleted. + * + * A Scope is also associated with a ContextMemoryManager. All memory + * allocated by the Scope is allocated in a single region using the + * ContextMemoryManager and released all at once when the Scope is popped. + */ class Scope { /** @@ -432,14 +432,14 @@ public: };/* 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 @@ -490,7 +490,7 @@ public: * implemented by the subclass. */ virtual void notify() = 0; -}; /* class ContextNotifyObj */ +};/* class ContextNotifyObj */ // Inline functions whose definitions had to be delayed: |