Made selectively_mutate a free function

Its use of depth iterators is specific to exprt

Author: Owen

src/goto-symex/renaming_level.h

@@ -89,28 +89,8 @@ class renamedt
     (void)::simplify(value, ns);
   }
 
-  typedef std::function<optionalt<renamedt<exprt, level>>(const exprt &)>
-    expr_mutator_functiont;
-
-  /// This permits replacing subexpressions of the renamed value, so long as
-  /// each replacement is consistent with our current renaming level (for
-  /// example, replacing subexpressions of L2 expressions with ones which are
-  /// themselves L2 renamed).
-  /// The passed function will be called with each expression node in preorder
-  /// (i.e. parent expressions before children), and should return an empty
-  /// optional to make no change or a renamed expression to make a change.
-  void selectively_mutate(expr_mutator_functiont get_mutated_expr)
-  {
-    for(
-      auto it = value.depth_begin(), itend = value.depth_end();
-      it != itend;
-      ++it)
-    {
-      auto replacement = get_mutated_expr(*it);
-      if(replacement)
-        it.mutate() = replacement->get();
-    }
-  }
+  using mutator_functiont =
+    std::function<optionalt<renamedt<underlyingt, level>>(const underlyingt &)>;
 
 private:
   underlyingt value;
@@ -119,8 +99,16 @@ class renamedt
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;
+
   template <levelt make_renamed_level>
-  friend renamedt<exprt, make_renamed_level> make_renamed(constant_exprt constant);
+  friend renamedt<exprt, make_renamed_level>
+  make_renamed(constant_exprt constant);
+
+  template <levelt selectively_mutate_level>
+  friend void selectively_mutate(
+    renamedt<exprt, selectively_mutate_level> &renamed,
+    typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
+      get_mutated_expr);
 
   /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : value(std::move(value))
@@ -133,6 +121,28 @@ renamedt<exprt, level> make_renamed(constant_exprt constant) {
   return renamedt<exprt, level>(std::move(constant));
 }
 
+/// This permits replacing subexpressions of the renamed value, so long as
+/// each replacement is consistent with our current renaming level (for
+/// example, replacing subexpressions of L2 expressions with ones which are
+/// themselves L2 renamed).
+/// The passed function will be called with each expression node in preorder
+/// (i.e. parent expressions before children), and should return an empty
+/// optional to make no change or a renamed expression to make a change.
+template <levelt level>
+void selectively_mutate(renamedt<exprt, level> &renamed,
+  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
+{
+  for(
+    auto it = renamed.value.depth_begin(), itend = renamed.value.depth_end();
+    it != itend;
+    ++it)
+  {
+    auto replacement = get_mutated_expr(*it);
+    if(replacement)
+      it.mutate() = replacement->get();
+  }
+}
+
 /// Functor to set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.

src/goto-symex/symex_goto.cpp

@@ -224,7 +224,8 @@ static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
   const irep_idt language_mode,
   const namespacet &ns)
 {
-  condition.selectively_mutate(
+  selectively_mutate(
+    condition,
     [&value_set, &language_mode, &ns](const exprt &expr) {
       return try_evaluate_pointer_comparison(
         expr, value_set, language_mode, ns);