From c8e9b1d6422b56476a2efb3fbaf19bce66de4c2b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 12 Mar 2010 23:52:14 +0000 Subject: * 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. --- src/context/cdmap.h | 126 ++++++++++++---------------------------------------- 1 file changed, 28 insertions(+), 98 deletions(-) (limited to 'src/context/cdmap.h') 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; - __gnu_cxx::hash_map*, HashFcn> d_map; + typedef __gnu_cxx::hash_map*, HashFcn> table_type; + table_type d_map; // The vector of CDOmap objects to be destroyed std::vector*> d_trash; @@ -200,7 +201,7 @@ public: ~CDMap() throw(AssertionException) { // Delete all the elements and clear the map - for(typename __gnu_cxx::hash_map*, 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& operator[](const Key& k) { emptyTrash(); - typename __gnu_cxx::hash_map*, HashFcn>::iterator - i(d_map.find(k)); + typename table_type::iterator i = d_map.find(k); CDOmap* obj; - if(i == d_map.end()) { // Create new object + if(i == d_map.end()) {// create new object obj = new(true) CDOmap(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*, 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* @@ -257,19 +256,12 @@ public: // FIXME: no erase(), too much hassle to implement efficiently... - // Iterator for CDMap: points to pair&>; - // in most cases, this will be functionally similar to pair. - class iterator : public std::iterator, std::ptrdiff_t> { - - // Private members - typename __gnu_cxx::hash_map*, HashFcn>::const_iterator d_it; + class iterator { + const CDOmap* d_it; public: - // Constructor from __gnu_cxx::hash_map - iterator(const typename __gnu_cxx::hash_map*, HashFcn>::const_iterator& i) : d_it(i) {} - - // Copy constructor + iterator(const CDOmap* p) : d_it(p) {} iterator(const iterator& i) : d_it(i.d_it) {} // Default constructor @@ -283,82 +275,13 @@ public: return d_it != i.d_it; } - // Dereference operators. - std::pair operator*() const { - const std::pair*>& p(*d_it); - return std::pair(p.first, *p.second); - } - - // Who needs an operator->() for maps anyway?... - // It'd be nice, but not possible by design. - //std::pair* 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* d_pair; - public: - Proxy(const std::pair& p): d_pair(&p) {} - std::pair& 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* d_it; - - public: - - orderedIterator(const CDOmap* 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 operator*() const { return std::pair(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& p): d_pair(&p) {} + Proxy(const std::pair& p) : d_pair(&p) {} - std::pair& operator*() { + const std::pair& 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<> */ -- cgit v1.2.3