Addressed sharing map review comments

Author: danpoe

src/util/sharing_map.h

@@ -12,8 +12,6 @@ Author: Daniel Poetzl
 #ifndef CPROVER_UTIL_SHARING_MAP_H
 #define CPROVER_UTIL_SHARING_MAP_H
 
-//#define SM_DEBUG
-
 #ifdef SM_DEBUG
 #include <iostream>
 #endif
@@ -31,22 +29,22 @@ Author: Daniel Poetzl
 #include "sharing_node.h"
 #include "threeval.h"
 
-//#define SM_INTERNAL_CHECKS
-
 #ifdef SM_INTERNAL_CHECKS
 #define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant")
 #else
 #define SM_ASSERT(b)
 #endif
 
-#define SHARING_MAPT(R)                                                        \
-  template <class keyT, class valueT, class hashT, class equalT>               \
+// clang-format off
+#define SHARING_MAPT(R) \
+  template <class keyT, class valueT, class hashT, class equalT> \
   R sharing_mapt<keyT, valueT, hashT, equalT>
 
-#define SHARING_MAPT2(CV, ST)                                                  \
-  template <class keyT, class valueT, class hashT, class equalT>               \
-  CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST                    \
+#define SHARING_MAPT2(CV, ST) \
+  template <class keyT, class valueT, class hashT, class equalT> \
+  CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \
     sharing_mapt<keyT, valueT, hashT, equalT>
+// clang-format on
 
 // Note: Due to a bug in Visual Studio we need to add an additional "const"
 // qualifier to the return values of insert(), place(), and find(). The type
@@ -299,7 +297,17 @@ class sharing_mapt
   innert *get_container_node(const key_type &k);
   const innert *get_container_node(const key_type &k) const;
 
-  const leaft *get_leaf_node(const key_type &k) const;
+  const leaft *get_leaf_node(const key_type &k) const
+  {
+    const innert *cp = get_container_node(k);
+    if(cp == nullptr)
+      return nullptr;
+
+    const leaft *lp;
+    lp = cp->find_leaf(k);
+
+    return lp;
+  }
 
   void iterate(
     const baset &n,
@@ -468,6 +476,13 @@ ::get_delta_view(
   typedef std::tuple<unsigned, const baset *, const baset *> stack_itemt;
   std::stack<stack_itemt> stack;
 
+  // We do a DFS "in lockstep" simultaneously on both maps. For
+  // corresponding nodes we check whether they are shared between the
+  // maps, and if not, we recurse into the corresponding subtrees.
+
+  // The stack contains the children of already visited nodes that we
+  // still have to visit during the traversal.
+
   stack.push(stack_itemt(0, &map, &other.map));
 
   do
@@ -543,11 +558,9 @@ SHARING_MAPT2(, innert *)::get_container_node(const key_type &k)
   std::size_t key = hash()(k);
   innert *ip = &map;
 
-  std::size_t bit;
-
   for(std::size_t i = 0; i < steps; i++)
   {
-    bit = key & mask;
+    std::size_t bit = key & mask;
 
     ip = ip->add_child(bit);
 
@@ -565,11 +578,9 @@ SHARING_MAPT2(const, innert *)::get_container_node(const key_type &k) const
   std::size_t key = hash()(k);
   const innert *ip = &map;
 
-  std::size_t bit;
-
   for(std::size_t i = 0; i < steps; i++)
   {
-    bit = key & mask;
+    std::size_t bit = key & mask;
 
     ip = ip->find_child(bit);
     if(ip == nullptr)
@@ -581,18 +592,6 @@ SHARING_MAPT2(const, innert *)::get_container_node(const key_type &k) const
   return ip;
 }
 
-SHARING_MAPT2(const, leaft *)::get_leaf_node(const key_type &k) const
-{
-  const innert *cp = get_container_node(k);
-  if(cp == nullptr)
-    return nullptr;
-
-  const leaft *lp;
-  lp = cp->find_leaf(k);
-
-  return lp;
-}
-
 /// Erase element
 ///
 /// Complexity:
@@ -618,11 +617,9 @@ SHARING_MAPT2(, size_type)::erase(const key_type &k, const tvt &key_exists)
   std::size_t key = hash()(k);
   innert *ip = &map;
 
-  std::size_t bit;
-
   for(std::size_t i = 0; i < steps; i++)
   {
-    bit = key & mask;
+    std::size_t bit = key & mask;
 
     const to_mapt &m = as_const(ip)->get_to_map();
 

src/util/sharing_node.h

@@ -12,9 +12,7 @@ Author: Daniel Poetzl
 #ifndef CPROVER_UTIL_SHARING_NODE_H
 #define CPROVER_UTIL_SHARING_NODE_H
 
-//#define DEBUG
-
-#ifdef DEBUG
+#ifdef SN_DEBUG
 #include <iostream>
 #endif
 
@@ -40,8 +38,6 @@ Author: Daniel Poetzl
 #include "small_shared_ptr.h"
 #include "small_shared_two_way_ptr.h"
 
-//#define SN_INTERNAL_CHECKS
-
 #ifdef SN_INTERNAL_CHECKS
 #define SN_ASSERT(b) INVARIANT(b, "Sharing node internal invariant")
 #define SN_ASSERT_USE(v, b) SN_ASSERT(b)
@@ -50,13 +46,15 @@ Author: Daniel Poetzl
 #define SN_ASSERT_USE(v, b) v = v;
 #endif
 
-#define SN_TYPE_PAR_DECL                                                       \
-  template <typename keyT,                                                     \
-            typename valueT,                                                   \
+// clang-format off
+#define SN_TYPE_PAR_DECL \
+  template <typename keyT, \
+            typename valueT, \
             typename equalT = std::equal_to<keyT>>
 
-#define SN_TYPE_PAR_DEF                                                        \
+#define SN_TYPE_PAR_DEF \
   template <typename keyT, typename valueT, typename equalT>
+// clang-format on
 
 #define SN_TYPE_ARGS keyT, valueT, equalT