summaryrefslogtreecommitdiff
path: root/src/context/cdhashmap.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/context/cdhashmap.h')
-rw-r--r--src/context/cdhashmap.h156
1 files changed, 29 insertions, 127 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 86a7cb141..b6024b65d 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -15,7 +15,7 @@
** 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.
+ ** std::hash<>, you should provide an explicit HashFcn.
**
** See also:
** CDInsertHashMap : An "insert-once" CD hash map.
@@ -58,36 +58,23 @@
** its CDOhash_map object memory freed. Here, the CDOhash_map is restored
** to a "NULL-map" state (see above), signaling it to remove
** itself from the map completely and put itself on a "trash
- ** list" for the map.
+ ** list" for its scope.
**
- ** Third, you might obliterate() the key. This calls the CDOhash_map
- ** destructor, which calls destroy(), which does a successive
- ** restore() until level 0. If the key was in the map since
- ** level 0, the restore() won't remove it, so in that case
- ** obliterate() removes it from the map and frees the CDOhash_map's
- ** memory.
- **
- ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
+ ** Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
** This first calls destroy(), as per ContextObj contract, but
** cdhashmapdoesn't save/restore itself, so that does nothing at the
- ** CDHashMap-level. Then it empties the trash. Then, for each
- ** element in the map, it marks it as being "part of a complete
- ** map destruction", which essentially short-circuits
+ ** CDHashMap-level. Then, for each element in the map, it marks it as being
+ ** "part of a complete map destruction", which essentially short-circuits
** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
- ** it. Finally it asserts that the trash is empty (which it
- ** should be, since restore() was short-circuited).
+ ** it.
**
- ** Fifth, you might clear() the CDHashMap. This does exactly the
+ ** Fourth, you might clear() the CDHashMap. This does exactly the
** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
** on itself.
**
- ** CDHashMap::emptyTrash() simply goes through and calls
- ** ->deleteSelf() on all elements in the trash.
** ContextObj::deleteSelf() calls the CDOhash_map destructor, then
** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map()
- ** calls destroy(), which restores as much as possible. (Note,
- ** though, that since objects placed on the trash have already
- ** restored to the fullest extent possible, it does nothing.)
+ ** calls destroy(), which restores as much as possible.
**/
#include "cvc4_private.h"
@@ -95,8 +82,9 @@
#ifndef __CVC4__CONTEXT__CDHASHMAP_H
#define __CVC4__CONTEXT__CDHASHMAP_H
-#include <ext/hash_map>
+#include <functional>
#include <iterator>
+#include <unordered_map>
#include <vector>
#include "base/cvc4_assert.h"
@@ -108,7 +96,7 @@ namespace context {
// Auxiliary class: almost the same as CDO (see cdo.h)
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDOhash_map : public ContextObj {
friend class CDHashMap<Key, Data, HashFcn>;
@@ -157,7 +145,7 @@ class CDOhash_map : public ContextObj {
} else {
Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
//this->deleteSelf();
- d_map->d_trash.push_back(this);
+ enqueueToGarbageCollect();
}
} else {
d_data = p->d_data;
@@ -281,7 +269,7 @@ template <class Key, class Data, class HashFcn>
class CDHashMap : public ContextObj {
typedef CDOhash_map<Key, Data, HashFcn> Element;
- typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+ typedef std::unordered_map<Key, Element*, HashFcn> table_type;
friend class CDOhash_map<Key, Data, HashFcn>;
@@ -290,8 +278,6 @@ class CDHashMap : public ContextObj {
Element* d_first;
Context* d_context;
- std::vector<Element*> d_trash;
-
// Nothing to save; the elements take care of themselves
virtual ContextObj* save(ContextMemoryManager* pCMM) {
Unreachable();
@@ -302,75 +288,38 @@ class CDHashMap : public ContextObj {
Unreachable();
}
- void emptyTrash() {
- //FIXME multithreading
- for(typename std::vector<Element*>::iterator i = d_trash.begin();
- i != d_trash.end();
- ++i) {
- Debug("gc") << "emptyTrash(): " << *i << std::endl;
- (*i)->deleteSelf();
- }
- d_trash.clear();
- }
-
// no copy or assignment
CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED;
public:
-
- CDHashMap(Context* context) :
- ContextObj(context),
- d_map(),
- d_first(NULL),
- d_context(context),
- d_trash() {
- }
+ CDHashMap(Context* context)
+ : ContextObj(context), d_map(), d_first(NULL), d_context(context) {}
~CDHashMap() {
- Debug("gc") << "cdhashmap" << this
- << " disappearing, destroying..." << std::endl;
+ Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
+ << std::endl;
destroy();
- Debug("gc") << "cdhashmap" << this
- << " disappearing, done destroying" << std::endl;
-
- Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl;
- emptyTrash();
- Debug("gc") << "done emptying trash for " << this << std::endl;
-
- for(typename table_type::iterator i = d_map.begin();
- i != d_map.end();
- ++i) {
- // mark it as being a destruction (short-circuit restore())
- (*i).second->d_map = NULL;
- if(!(*i).second->d_noTrash) {
- (*i).second->deleteSelf();
- }
- }
- d_map.clear();
- d_first = NULL;
-
- Assert(d_trash.empty());
+ Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
+ << std::endl;
+ clear();
}
- void clear() throw(AssertionException) {
- Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl;
- emptyTrash();
+ void clear() {
+ Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
+ << std::endl;
Debug("gc") << "done emptying trash for " << this << std::endl;
- for(typename table_type::iterator i = d_map.begin();
- i != d_map.end();
- ++i) {
+ for (auto& key_element_pair : d_map) {
// mark it as being a destruction (short-circuit restore())
- (*i).second->d_map = NULL;
- if(!(*i).second->d_noTrash) {
- (*i).second->deleteSelf();
+ Element* element = key_element_pair.second;
+ element->d_map = nullptr;
+ if (!element->d_noTrash) {
+ element->deleteSelf();
}
}
d_map.clear();
- d_first = NULL;
-
- Assert(d_trash.empty());
+ d_first = nullptr;
}
// The usual operators of map
@@ -389,8 +338,6 @@ public:
// If a key is not present, a new object is created and inserted
Element& operator[](const Key& k) {
- emptyTrash();
-
typename table_type::iterator i = d_map.find(k);
Element* obj;
@@ -404,8 +351,6 @@ public:
}
bool insert(const Key& k, const Data& d) {
- emptyTrash();
-
typename table_type::iterator i = d_map.find(k);
if(i == d_map.end()) {// create new object
@@ -443,8 +388,6 @@ public:
* insertAtContextLevelZero() a key that already is in the map.
*/
void insertAtContextLevelZero(const Key& k, const Data& d) {
- emptyTrash();
-
AlwaysAssert(d_map.find(k) == d_map.end());
Element* obj = new(true) Element(d_context, this, k, d,
@@ -454,43 +397,6 @@ public:
// FIXME: no erase(), too much hassle to implement efficiently...
- /**
- * "Obliterating" is kind of like erasing, except it's not
- * backtrackable; the key is permanently removed from the map.
- * (Naturally, it can be re-added as a new element.)
- */
- void obliterate(const Key& k) {
- typename table_type::iterator i = d_map.find(k);
- if(i != d_map.end()) {
- Debug("gc") << "key " << k << " obliterated" << std::endl;
- // Restore this object to level 0. If it was inserted after level 0,
- // nothing else to do as restore will put it in the trash.
- (*i).second->destroy();
-
- // Check if object was inserted at level 0: in that case, still have
- // to do some work.
- typename table_type::iterator j = d_map.find(k);
- if(j != d_map.end()) {
- Element* elt = (*j).second;
- if(d_first == elt) {
- if(elt->d_next == elt) {
- Assert(elt->d_prev == elt);
- d_first = NULL;
- } else {
- d_first = elt->d_next;
- }
- }
- elt->d_prev->d_next = elt->d_next;
- elt->d_next->d_prev = elt->d_prev;
- d_map.erase(j);//FIXME multithreading
- Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
- if(!elt->d_noTrash) {
- elt->deleteSelf();
- }
- }
- }
- }
-
class iterator {
const Element* d_it;
@@ -566,10 +472,6 @@ public:
}
}
- iterator find(const Key& k) {
- emptyTrash();
- return const_cast<const CDHashMap*>(this)->find(k);
- }
};/* class CDHashMap<> */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback