Add eval function to string_dependenciest

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -481,6 +481,21 @@ string_dependenciest::get_string_node(node_indext i) const
   return {};
 }
 
+optionalt<exprt> string_dependenciest::eval(
+  const array_string_exprt &s,
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  const auto node = node_at(s);
+  if(node && node->dependencies.size() == 1)
+  {
+    const auto &f = get_builtin_function(node->dependencies[0]);
+    const auto result = f.string_result();
+    if(result && *result == s)
+      return f.eval(get_value);
+  }
+  return {};
+}
+
 bool add_node(
   string_dependenciest &dependencies,
   const equal_exprt &equation,

src/solvers/refinement/string_refinement_util.h

@@ -306,6 +306,12 @@ class string_dependenciest
   /// Mark node for `e` as depending on unknown builtin_function
   void add_unknown_dependency(const array_string_exprt &e);
 
+  /// Attempt to evaluate the given string from the dependencies and valuation
+  /// of strings on which it depends
+  optionalt<exprt> eval(
+    const array_string_exprt &s,
+    const std::function<exprt(const exprt &)> &get_value) const;
+
   void output_dot(std::ostream &stream) const;
 
 private: