Add const node_at function in string dependencies

romainbrenguier · romainbrenguier · commit 357cb4456349 · 2018-03-14T09:08:26.000Z
This is useful to find a node with the guarantee of node modifying the graph.
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
@@ -333,6 +333,15 @@ string_dependenciest::get_node(const array_string_exprt &e)
   return string_nodes.back();
 }
 
+std::unique_ptr<const string_dependenciest::string_nodet>
+string_dependenciest::node_at(const array_string_exprt &e) const
+{
+  const auto &it = node_index_pool.find(e);
+  if(it != node_index_pool.end())
+    return util_make_unique<const string_nodet>(string_nodes.at(it->second));
+  return {};
+}
+
 string_dependenciest::builtin_function_nodet string_dependenciest::make_node(
   std::unique_ptr<string_builtin_functiont> &builtin_function)
 {
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
@@ -287,6 +287,9 @@ class string_dependenciest
 
   string_nodet &get_node(const array_string_exprt &e);
 
+  std::unique_ptr<const string_nodet>
+  node_at(const array_string_exprt &e) const;
+
   /// `builtin_function` is reset to an empty pointer after the node is created
   builtin_function_nodet
   make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
