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

* Proposal for adding map utility functions to CVC4.

4 files changed, 129 insertions, 8 deletions

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index 3619b226e..3706f57a3 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -26,6 +26,7 @@ libbase_la_SOURCES = \
 	exception.h \
 	listener.cpp \
 	listener.h \
+	map_util.h \
 	modal_exception.h \
 	output.cpp \
 	output.h
diff --git a/src/base/map_util.h b/src/base/map_util.h
new file mode 100644
index 000000000..2e17c9290
--- /dev/null
+++ b/src/base/map_util.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file map_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility functions for dealing with maps in a mostly uniform fashion.
+ **
+ ** Utility functions for dealing with maps and related classed in a mostly
+ ** uniform fashion. These are stylistically encouraged (but not required) in
+ ** new code. Supports:
+ ** - std::map
+ ** - std::unordered_map
+ ** - CVC4::context::CDHashmap
+ ** - CVC4::context::CDInsertHashmap
+ ** The ContainsKey function is also compatible with std::[unordered_]set.
+ **
+ ** Currently implemented classes of functions:
+ ** - ContainsKey
+ **   Returns true if a map contains a key. (Also Supports std::set and
+ **   std::unordered_set.)
+ ** - FindOr*
+ **   Finds an data element mapped to by the map. Variants include FindOrNull
+ **   and FindOrDie.
+ **
+ ** Potential future classes of functions:
+ ** - InsertOrUpdate
+ ** - InsertIfNotPresent
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BASE__MAP_UTIL_H
+#define __CVC4__BASE__MAP_UTIL_H
+
+#include "base/cvc4_check.h"
+
+namespace CVC4 {
+
+// Returns true if the `map` contains the `key`.
+//
+// Supports sets as well.
+template <class M, class Key>
+bool ContainsKey(const M& map, const Key& key)
+{
+  return map.find(key) != map.end();
+}
+
+template <typename M>
+using MapKeyTypeT = typename M::value_type::first_type;
+template <typename M>
+using MapMappedTypeT = typename M::value_type::second_type;
+
+// Returns a pointer to the const value mapped by `key` if it exists, or nullptr
+// otherwise.
+template <class M>
+const MapMappedTypeT<M>* FindOrNull(const M& map, const MapKeyTypeT<M>& key)
+{
+  auto it = map.find(key);
+  if (it == map.end())
+  {
+    return nullptr;
+  }
+  return &((*it).second);
+}
+
+// Returns a pointer to the non-const value mapped by `key` if it exists, or
+// nullptr otherwise.
+template <class M>
+MapMappedTypeT<M>* FindOrNull(M& map, const MapKeyTypeT<M>& key)
+{
+  auto it = map.find(key);
+  if (it == map.end())
+  {
+    return nullptr;
+  }
+  return &((*it).second);
+}
+
+// Returns a const reference to the value mapped by `key` if it exists. Dies
+// if the element is not there.
+template <class M>
+const MapMappedTypeT<M>& FindOrDie(const M& map, const MapKeyTypeT<M>& key)
+{
+  auto it = map.find(key);
+  CVC4_CHECK(it != map.end()) << "The map does not contain the key.";
+  return (*it).second;
+}
+
+}  // namespace CVC4
+
+#endif /* __CVC4__BASE__MAP_UTIL_H */
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;
 
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 7094ad541..cfa50bef8 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/quantifiers/fmf/bounded_integers.h"
+
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -451,11 +452,20 @@ void BoundedIntegers::checkOwnership(Node f)
           success = true;
           //set Attributes on literals
           for( unsigned b=0; b<2; b++ ){
-            if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){
-              Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );
+            if (bound_lit_map[b].find(v) != bound_lit_map[b].end())
+            {
+              // WARNING_CANDIDATE:
+              // This assertion may fail. We intentionally do not enable this in
+              // production as it is considered safe for this to fail. We fail
+              // in debug mode to have this instances raised to our attention.
+              Assert(bound_lit_pol_map[b].find(v)
+                     != bound_lit_pol_map[b].end());
               BoundIntLitAttribute bila;
-              bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );
-            }else{
+              bound_lit_map[b][v].setAttribute(bila,
+                                               bound_lit_pol_map[b][v] ? 1 : 0);
+            }
+            else
+            {
               Assert( it->second!=BOUND_INT_RANGE );
             }
           }