Add a cache for eval in string dependences

This improves the performances since the model for one string can depend
on the model for two other strings, which model may have already been
computed.
The cache must be cleared every time the model changes.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -757,6 +757,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };
+  dependencies.clean_cache();
   const decision_proceduret::resultt res=supert::dec_solve();
   if(res==resultt::D_SATISFIABLE)
   {
@@ -804,6 +805,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
   while((loop_bound_--)>0)
   {
+    dependencies.clean_cache();
     const decision_proceduret::resultt res=supert::dec_solve();
 
     if(res==resultt::D_SATISFIABLE)

src/solvers/refinement/string_refinement_util.cpp

@@ -172,7 +172,8 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
   return equations_containing[expr];
 }
 
-string_transformation_builtin_functiont::string_transformation_builtin_functiont(
+string_transformation_builtin_functiont
+::string_transformation_builtin_functiont(
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
 {
@@ -507,17 +508,36 @@ 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 &it = node_index_pool.find(s);
+  if(it == node_index_pool.end())
+    return {};
+
+  if(eval_string_cache[it->second])
+    return eval_string_cache[it->second];
+
+  const auto node = string_nodes[it->second];
+
+  if(node.dependencies.size() == 1)
   {
-    const auto &f = get_builtin_function(node->dependencies[0]);
+    const auto &f = get_builtin_function(node.dependencies[0]);
     const auto result = f.string_result();
     if(result && *result == s)
-      return f.eval(get_value);
+    {
+      const auto value_opt = f.eval(get_value);
+      eval_string_cache[it->second] = value_opt;
+      return value_opt;
+    }
   }
   return {};
 }
 
+void string_dependenciest::clean_cache()
+{
+  eval_string_cache.resize(string_nodes.size());
+  for(auto &e : eval_string_cache)
+    e = {};
+}
+
 bool add_node(
   string_dependenciest &dependencies,
   const equal_exprt &equation,

src/solvers/refinement/string_refinement_util.h

@@ -332,10 +332,15 @@ class string_dependenciest
 
   /// 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
+  /// given by get_value can change.
   optionalt<exprt> eval(
     const array_string_exprt &s,
     const std::function<exprt(const exprt&)> &get_value) const;
 
+  /// Clean the cache used by `eval`
+  void clean_cache();
+
   void output_dot(std::ostream &stream) const;
 
 private:
@@ -345,6 +350,8 @@ class string_dependenciest
   /// Set of nodes representing strings
   std::vector<string_nodet> string_nodes;
 
+  mutable std::vector<optionalt<exprt>> eval_string_cache;
+
   /// Nodes describing dependencies of a string: values of the map correspond
   /// to indexes in the vector `string_nodes`.
   std::unordered_map<array_string_exprt, std::size_t, irep_hash>