Proposal for adding map utility functions to CVC4. (#2232)

* Proposal for adding map utility functions to CVC4.

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;