From 1f9d6d3c9d836d6219b8aaf717f7129c7710c9c8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 29 Jul 2018 19:02:44 -0700 Subject: [PATCH] Storing a std::pair on CDOhash_map. Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing. --- src/context/cdhashmap.h | 85 +++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 41 deletions(-) diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 83a8f22c4..94b507a7e 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -100,8 +100,15 @@ template > class CDOhash_map : public ContextObj { friend class CDHashMap; - Key d_key; - Data d_data; + public: + // The type of the value mapped to by this class. + using value_type = std::pair; + + private: + value_type d_value; + Key& mutable_key() { return d_value.first; } + Data& mutable_data() { return d_value.second; } + CDHashMap* d_map; /** never put this cdhashmapelement on the trash */ @@ -121,10 +128,10 @@ class CDOhash_map : public ContextObj { CDOhash_map* p = static_cast(data); if(d_map != NULL) { if(p->d_map == NULL) { - Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && - (*d_map->d_map.find(d_key)).second == this); + Assert(d_map->d_map.find(getKey()) != d_map->d_map.end() + && (*d_map->d_map.find(getKey())).second == this); // no longer in map (popped beyond first level in which it was) - d_map->d_map.erase(d_key); + d_map->d_map.erase(getKey()); // If we call deleteSelf() here, it re-enters restore(). So, // put it on a "trash heap" instead, for later deletion. // @@ -150,42 +157,40 @@ class CDOhash_map : public ContextObj { enqueueToGarbageCollect(); } } else { - d_data = p->d_data; + mutable_data() = p->get(); } } // Explicitly call destructors for the key and the data as they will not // otherwise get called. - p->d_key.~Key(); - p->d_data.~Data(); + p->mutable_key().~Key(); + p->mutable_data().~Data(); } /** ensure copy ctor is only called by us */ - CDOhash_map(const CDOhash_map& other) : - ContextObj(other), - // don't need to save the key---and if we do we can get - // refcounts for Node keys messed up and leak memory - d_key(), - d_data(other.d_data), - d_map(other.d_map), - d_prev(NULL), - d_next(NULL) { + CDOhash_map(const CDOhash_map& other) + : ContextObj(other), + // don't need to save the key---and if we do we can get + // refcounts for Node keys messed up and leak memory + d_value(Key(), other.d_value.second), + d_map(other.d_map), + d_prev(NULL), + d_next(NULL) + { } CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED; -public: - + public: CDOhash_map(Context* context, - CDHashMap* map, - const Key& key, - const Data& data, - bool atLevelZero = false, - bool allocatedInCMM = false) : - ContextObj(allocatedInCMM, context), - d_key(key), - d_data(data), - d_map(NULL), - d_noTrash(allocatedInCMM) { - + CDHashMap* map, + const Key& key, + const Data& data, + bool atLevelZero = false, + bool allocatedInCMM = false) + : ContextObj(allocatedInCMM, context), + d_value(key, data), + d_map(NULL), + d_noTrash(allocatedInCMM) + { // untested, probably unsafe. Assert(!(atLevelZero && allocatedInCMM)); @@ -194,7 +199,7 @@ public: // removed from the map, it's inserted at level 0 as an // "initializing" element. See // CDHashMap<>::insertAtContextLevelZero(). - d_data = data; + mutable_data() = data; } else { // Normal map insertion: first makeCurrent(), then set the data // and then, later, the map. Order is important; we can't @@ -232,16 +237,14 @@ public: void set(const Data& data) { makeCurrent(); - d_data = data; + mutable_data() = data; } - const Key& getKey() const { - return d_key; - } + const Key& getKey() const { return d_value.first; } - const Data& get() const { - return d_data; - } + const Data& get() const { return d_value.second; } + + const value_type& getValue() const { return d_value; } operator Data() { return get(); @@ -395,6 +398,8 @@ public: // FIXME: no erase(), too much hassle to implement efficiently... + using value_type = typename CDOhash_map::value_type; + class iterator { const Element* d_it; @@ -415,9 +420,7 @@ public: } // Dereference operators. - std::pair operator*() const { - return std::pair(d_it->getKey(), d_it->get()); - } + const value_type& operator*() const { return d_it->getValue(); } // Prefix increment iterator& operator++() { -- 2.30.2