Using cache to speed up generation of GrapML file.

Expression-to-string conversion is costly.

Author: marek-trtik

src/goto-programs/graphml_witness.cpp

@@ -61,10 +61,41 @@ void graphml_witnesst::remove_l0_l1(exprt &expr)
     remove_l0_l1(*it);
 }
 
+template <typename T>
+inline void hash_combine(std::size_t &seed, const T &v)
+{
+  std::hash<T> hasher;
+  seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+}
+
+namespace std
+{
+template <typename S, typename T>
+struct hash<pair<S, T>>
+{
+  inline size_t operator()(const pair<S, T> &v) const
+  {
+    size_t seed = 0;
+    ::hash_combine(seed, v.first);
+    ::hash_combine(seed, v.second);
+    return seed;
+  }
+};
+} // namespace std
+
 std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
+  static std::
+    unordered_map<std::pair<unsigned int, const irept::dt *>, std::string>
+      cache;
+  {
+    const auto cit = cache.find({identifier.get_no(), &assign.read()});
+    if(cit != cache.end())
+      return cit->second;
+  }
+
   std::string result;
 
   if(assign.rhs().id() == ID_array_list)
@@ -195,6 +226,7 @@ std::string graphml_witnesst::convert_assign_rec(
     result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
   }
 
+  cache.insert({{identifier.get_no(), &assign.read()}, result});
   return result;
 }