diff options
author | Tim King <taking@cs.nyu.edu> | 2018-08-08 16:50:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-08 16:50:16 -0700 |
commit | 987df3df987768e2ce0c36d17469929f8e92fdec (patch) | |
tree | 6d85a85966084879e55b8ab04c330662a4cfe7f0 /src/context | |
parent | ece17ee2c38fa5769ae3ab7fa3607c0e88c0021f (diff) |
Proposal for adding map utility functions to CVC4. (#2232)
* Proposal for adding map utility functions to CVC4.
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/cdhashmap.h | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 958c48e22..ae530f106 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -101,13 +101,26 @@ class CDOhash_map : public ContextObj { friend class CDHashMap<Key, Data, HashFcn>; public: - // The type of the <Key, Data> value mapped to by this class. - using value_type = std::pair<Key, Data>; + // The type of the <Key, Data> pair mapped by this class. + // + // Implementation: + // The data and key visible to users of CDHashMap are only visible through + // const references. Thus the type of dereferencing a + // CDHashMap<Key, Data>::iterator.second is intended to always be a + // `const Data&`. (Otherwise, to get a Data& safely, access operations + // would need to makeCurrent() to get the Data&, which is an unacceptable + // performance hit.) To allow for the desired updating in other scenarios, we + // store a std::pair<const Key, const Data> and break the const encapsulation + // when necessary. + using value_type = std::pair<const Key, const Data>; private: value_type d_value; - Key& mutable_key() { return d_value.first; } - Data& mutable_data() { return d_value.second; } + + // See documentation of value_type for why this is needed. + Key& mutable_key() { return const_cast<Key&>(d_value.first); } + // See documentation of value_type for why this is needed. + Data& mutable_data() { return const_cast<Data&>(d_value.second); } CDHashMap<Key, Data, HashFcn>* d_map; |