From fb676d54d1c284d8fa93a153237410f7fbf607d6 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 8 Mar 2018 16:54:03 +0000
Subject: [PATCH] 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.
---
 src/solvers/refinement/string_refinement.cpp  |  2 ++
 .../refinement/string_refinement_util.cpp     | 27 ++++++++++++++++---
 .../refinement/string_refinement_util.h       |  7 +++++
 3 files changed, 32 insertions(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 6ac7393eead..b994d73b16c 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/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)
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index e55e3292a8d..6cea38e4c19 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -537,17 +537,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.reset();
+}
+
 bool add_node(
   string_dependenciest &dependencies,
   const equal_exprt &equation,
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index d23c03fb690..e8c18ad3cf6 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -339,10 +339,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:
@@ -352,6 +357,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>