Cache expensive circuits for given input bvts

This makes solving trivial in presence of temporary intermediate
variables.

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -976,13 +976,23 @@ bvt bv_utilst::multiplier(
   const bvt &op1,
   representationt rep)
 {
+  auto cache_entry =
+    circuit_cache[{ID_mult, rep}].insert({{op0, op1}, {bvt{}}});
+  if(!cache_entry.second)
+    return cache_entry.first->second[0];
+
   switch(rep)
   {
-  case representationt::SIGNED: return signed_multiplier(op0, op1);
-  case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
+  case representationt::SIGNED:
+    cache_entry.first->second[0] = signed_multiplier(op0, op1);
+  case representationt::UNSIGNED:
+    cache_entry.first->second[0] = unsigned_multiplier(op0, op1);
   }
 
-  UNREACHABLE;
+  // multiplication is commutative
+  circuit_cache[{ID_mult, rep}][{op1, op0}] = {cache_entry.first->second};
+
+  return cache_entry.first->second[0];
 }
 
 bvt bv_utilst::multiplier_no_overflow(
@@ -1045,13 +1055,25 @@ void bv_utilst::divider(
 {
   PRECONDITION(prop.has_set_to());
 
+  auto cache_entry =
+    circuit_cache[{ID_div, rep}].insert({{op0, op1}, {bvt{}, bvt{}}});
+  if(!cache_entry.second)
+  {
+    result = cache_entry.first->second[0];
+    remainer = cache_entry.first->second[1];
+    return;
+  }
+
   switch(rep)
   {
   case representationt::SIGNED:
     signed_divider(op0, op1, result, remainer); break;
   case representationt::UNSIGNED:
     unsigned_divider(op0, op1, result, remainer); break;
   }
+
+  cache_entry.first->second[0] = result;
+  cache_entry.first->second[1] = remainer;
 }
 
 void bv_utilst::unsigned_divider(

src/solvers/flattening/bv_utils.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/prop/prop.h>
 
+#include <map>
+
 // Shares variables between var == const tests for registered variables.
 // Gives ~15% memory savings on some programs using constant arrays
 // but seems to give a run-time penalty.
@@ -245,6 +247,11 @@ class bv_utilst
   bvt cond_negate_no_overflow(const bvt &bv, const literalt cond);
 
   bvt wallace_tree(const std::vector<bvt> &pps);
+
+  using circuit_cachet = std::map<
+    std::pair<irep_idt, representationt>,
+    std::map<std::vector<bvt>, std::vector<bvt>>>;
+  circuit_cachet circuit_cache;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H