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

* Proposal for adding map utility functions to CVC4.

6 files changed, 346 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 );
             }
           }
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index d58ee411f..b3e0a3808 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -6,6 +6,7 @@ UNIT_TESTS = \
 	util/cardinality_public
 if WHITE_AND_BLACK_TESTS
 UNIT_TESTS += \
+	base/map_util_black \
 	theory/evaluator_white \
 	theory/logic_info_white \
 	theory/theory_arith_white \
diff --git a/test/unit/base/map_util_black.h b/test/unit/base/map_util_black.h
new file mode 100644
index 000000000..6d2d2bbc7
--- /dev/null
+++ b/test/unit/base/map_util_black.h
@@ -0,0 +1,216 @@
+/*********************                                                        */
+/*! \file map_util_black.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 Black box testing of map utility functions.
+ **
+ ** Black box testing of map utility functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <map>
+#include <set>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+
+#include "base/map_util.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+
+using CVC4::ContainsKey;
+using CVC4::FindOrDie;
+using CVC4::FindOrNull;
+using CVC4::context::CDHashMap;
+using CVC4::context::CDInsertHashMap;
+using CVC4::context::Context;
+using std::string;
+
+class MapUtilBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() {}
+  void tearDown() {}
+
+  // Returns a map containing {"key"->"value", "other"->"entry"}.
+  static const std::map<string, string>& DefaultMap()
+  {
+    static const std::map<string, string> static_stored_map{{"key", "value"},
+                                                            {"other", "entry"}};
+    return static_stored_map;
+  }
+
+  void testMap()
+  {
+    std::map<string, string> map = DefaultMap();
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    if (string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+      *found_value = "new value";
+    }
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value");
+  }
+
+  void testConstantMap()
+  {
+    const std::map<string, string> map = DefaultMap();
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+    // Cannot do death tests for FindOrDie.
+  }
+
+  void testUnorderedMap()
+  {
+    std::unordered_map<string, string> map(DefaultMap().begin(),
+                                           DefaultMap().end());
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    if (string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+      *found_value = "new value";
+    }
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value");
+  }
+
+  void testConstUnorderedMap()
+  {
+    const std::unordered_map<string, string> map(DefaultMap().begin(),
+                                                 DefaultMap().end());
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+    // Cannot do death tests for FindOrDie.
+  }
+
+  void testSet()
+  {
+    std::set<string> set{"entry", "other"};
+    TS_ASSERT(ContainsKey(set, "entry"));
+    TS_ASSERT(!ContainsKey(set, "non member"));
+
+    const std::set<string> const_set{"entry", "other"};
+    TS_ASSERT(ContainsKey(const_set, "entry"));
+    TS_ASSERT(!ContainsKey(const_set, "non member"));
+  }
+
+  void testUnorderedSet()
+  {
+    std::unordered_set<string> set{"entry", "other"};
+    TS_ASSERT(ContainsKey(set, "entry"));
+    TS_ASSERT(!ContainsKey(set, "non member"));
+
+    const std::unordered_set<string> const_set{"entry", "other"};
+    TS_ASSERT(ContainsKey(const_set, "entry"));
+    TS_ASSERT(!ContainsKey(const_set, "non member"));
+  }
+
+  // For each <key, value> pair in source, inserts mapping from key to value
+  // using insert into dest.
+  template <class M>
+  void InsertAll(const std::map<string, string>& source, M* dest)
+  {
+    for (const auto& key_value : source)
+    {
+      dest->insert(key_value.first, key_value.second);
+    }
+  }
+
+  void testCDHashMap()
+  {
+    Context context;
+    CDHashMap<string, string> map(&context);
+    InsertAll(DefaultMap(), &map);
+
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+  }
+
+  void testConstCDHashMap()
+  {
+    Context context;
+    CDHashMap<string, string> store(&context);
+    InsertAll(DefaultMap(), &store);
+    const auto& map = store;
+
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+  }
+
+  void testCDInsertHashMap()
+  {
+    Context context;
+    CDInsertHashMap<string, string> map(&context);
+    InsertAll(DefaultMap(), &map);
+
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+  }
+
+  void testConstCDInsertHashMap()
+  {
+    Context context;
+    CDInsertHashMap<string, string> store(&context);
+    InsertAll(DefaultMap(), &store);
+    const auto& map = store;
+
+    TS_ASSERT(ContainsKey(map, "key"));
+    TS_ASSERT(!ContainsKey(map, "non key"));
+    if (const string* found_value = FindOrNull(map, "other"))
+    {
+      TS_ASSERT_EQUALS(*found_value, "entry");
+    }
+    TS_ASSERT(FindOrNull(map, "non key") == nullptr);
+    TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry");
+  }
+
+}; /* class MapUtilBlack */