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,47 +336,59 @@ 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,
+  const 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
-        {
-          std::cout << "Warning no node for " << format(current) << std::endl;
-          //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
+      {
+        std::cout << "Warning no node for " << format(current) << std::endl;
+        //UNREACHABLE;
       }
     }
   }
-  else if(node.kind == nodet::STRING)
+}
+
+void string_dependenciest::for_each_dependency(
+  const string_nodet &node,
+  const std::function<void(const builtin_function_nodet &)> &f) const
+{
+  for(const std::size_t &index : node.dependencies)
+    f(builtin_function_nodes[index]);
+}
+
+void string_dependenciest::for_each_successor(
+  const nodet &node,
+  const std::function<void(const nodet &)> &f) const
+{
+  switch(node.kind)
   {
-    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]));
-      });
+  case nodet::BUILTIN:
+    for_each_dependency(
+      builtin_function_nodes[node.index],
+      [&](const string_nodet &n) { return f(nodet(n)); });
+    break;
+
+  case nodet::STRING:
+    for_each_dependency(
+      string_nodes[node.index],
+      [&](const builtin_function_nodet &n) { return f(nodet(n)); });
+    break;
   }
-  else
-    UNREACHABLE;
 }
 
 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,
+    const std::function<void(const builtin_function_nodet &)> &f) const;
+  void for_each_dependency(
+    const builtin_function_nodet &node,
+    const 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