Define two helper functions for for_each_successor

These two functions deal with one type of node.
Type safety ensures we don't mix the two kinds of node, so these two
functions can be made public.

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -336,44 +336,57 @@ bool add_node(
   return true;
 }
 
-void string_dependenciest::for_each_successor(
-  const nodet &node,
-  const std::function<void(const nodet &)> &f) const
+void string_dependenciest::for_each_dependency(
+  const builtin_function_nodet &node,
+  std::function<void(const string_nodet &)> f) const
 {
-  if(node.kind == nodet::BUILTIN)
+  for(const auto &s : node.data->string_arguments())
   {
-    const auto &builtin = builtin_function_nodes[node.index];
-    for(const auto &s : builtin.data->string_arguments())
+    std::vector<std::reference_wrapper<const exprt>> stack({s});
+    while(!stack.empty())
     {
-      std::vector<std::reference_wrapper<const exprt>> stack({s});
-      while(!stack.empty())
+      const auto current = stack.back();
+      stack.pop_back();
+      if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
       {
-        const auto current = stack.back();
-        stack.pop_back();
-        if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
-        {
-          stack.emplace_back(if_expr->true_case());
-          stack.emplace_back(if_expr->false_case());
-        }
-        else if(const auto node = node_at(to_array_string_expr(current)))
-          f(nodet(*node));
-        else
-          UNREACHABLE;
+        stack.emplace_back(if_expr->true_case());
+        stack.emplace_back(if_expr->false_case());
       }
+      else if(const auto string_node = node_at(to_array_string_expr(current)))
+        f(*string_node);
+      else
+        UNREACHABLE;
     }
   }
-  else if(node.kind == nodet::STRING)
+}
+
+void string_dependenciest::for_each_dependency(
+  const string_nodet &node,
+  std::function<void(const builtin_function_nodet &)> f) const
+{
+  std::for_each(
+    node.dependencies.begin(),
+    node.dependencies.end(),
+    [&](const std::size_t &index) { f(builtin_function_nodes[index]); });
+}
+
+void string_dependenciest::for_each_successor(
+  const nodet &node,
+  const std::function<void(const nodet &)> &f) const
+{
+  if(node.kind == nodet::BUILTIN)
   {
-    const auto &s_node = string_nodes[node.index];
-    std::for_each(
-      s_node.dependencies.begin(),
-      s_node.dependencies.end(),
-      [&](const std::size_t &index) { // NOLINT
-        f(nodet(builtin_function_nodes[index]));
-      });
+    for_each_dependency(
+      builtin_function_nodes[node.index],
+      [&](const string_nodet &n) { return f(nodet(n)); });
   }
   else
-    UNREACHABLE;
+  {
+    INVARIANT(node.kind == nodet::STRING, "nodes are either BUILTIN or STRING");
+    for_each_dependency(
+      string_nodes[node.index],
+      [&](const builtin_function_nodet &n) { return f(nodet(n)); });
+  }
 }
 
 void string_dependenciest::for_each_node(

src/solvers/refinement/string_refinement_util.h

@@ -217,6 +217,14 @@ class string_dependenciest
     const array_string_exprt &e,
     const builtin_function_nodet &builtin_function);
 
+  /// Applies `f` to each node on which `node` depends
+  void for_each_dependency(
+    const string_nodet &node,
+    std::function<void(const builtin_function_nodet &)> f) const;
+  void for_each_dependency(
+    const builtin_function_nodet &node,
+    std::function<void(const string_nodet &)> f) const;
+
   /// Attempt to evaluate the given string from the dependencies and valuation
   /// of strings on which it depends
   /// Warning: eval uses a cache which must be cleaned everytime the valuations