prop_conv_solvert: introduce scopes

Author: Daniel Kroening

src/solvers/prop/prop_conv_solver.cpp

@@ -145,11 +145,16 @@ literalt prop_conv_solvert::convert(const exprt &expr)
   if(!result.second)
     return result.first->second;
 
+  // new entry
+  if(record_cache_iterators)
+    cache_iterators.push_back(result.first);
+
   literalt literal = convert_bool(expr);
 
   // insert into cache
 
   result.first->second = literal;
+
   if(freeze_all && !literal.is_constant())
     prop.set_frozen(literal);
 
@@ -276,23 +281,47 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
     const let_exprt &let_expr = to_let_expr(expr);
 
     // first check whether this is all boolean
-    if(
-      let_expr.value().type().id() == ID_bool &&
-      let_expr.where().type().id() == ID_bool)
+    DATA_INVARIANT(
+      let_expr.value().type().id() == ID_bool,
+      "Boolean let must have Boolean value");
+    DATA_INVARIANT(
+      let_expr.where().type().id() == ID_bool,
+      "Boolean let must have Boolean subexpression");
+
+    literalt value = convert(let_expr.value());
+
+    const irep_idt &id = let_expr.symbol().get_identifier();
+    auto emplace_result = symbols.emplace(id, literalt());
+    literalt old_variable;
+
+    // We do not expect the identifier to be unique; in particular, nesting
+    // is supported. Thus, do we need to save a value from an outer scope?
+    if(!emplace_result.second)
     {
-      literalt value = convert(let_expr.value());
-
-      // We expect the identifier of the bound symbols to be unique,
-      // and thus, these can go straight into the symbol map.
-      // This property also allows us to cache any subexpressions.
-      const irep_idt &id = let_expr.symbol().get_identifier();
-      symbols[id] = value;
-      literalt result = convert(let_expr.where());
-
-      // remove again
-      symbols.erase(id);
-      return result;
+      // insertion did not take place
+      old_variable = emplace_result.first->second;
+      emplace_result.first->second = value;
     }
+
+    // record all newly added cache entries
+    bool previous_record_cache_iterators = record_cache_iterators;
+    std::size_t previous_cache_iterators_size = cache_iterators.size();
+    record_cache_iterators = true;
+
+    // recursive call
+    literalt result = convert(let_expr.where());
+
+    // clear cache_iterators that use the bound symbol from the cache
+    cache_iterators.resize(previous_cache_iterators_size);
+    record_cache_iterators = previous_record_cache_iterators;
+
+    // remove/restore symbol
+    if(emplace_result.second)
+      emplace_result.first->second = old_variable;
+    else
+      symbols.erase(emplace_result.first);
+
+    return result;
   }
 
   return convert_rest(expr);

src/solvers/prop/prop_conv_solver.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
 
 #include <map>
+#include <stack>
 #include <string>
 
 #include <util/expr.h>
@@ -127,6 +128,11 @@ class prop_conv_solvert : public prop_convt, public solver_resource_limitst
   // cache
   cachet cache;
 
+  // record the subexpressions that use the scoped variable,
+  // in order to clear them from the cache after we are done
+  std::vector<cachet::iterator> cache_iterators;
+  bool record_cache_iterators = false;
+
   virtual void ignoring(const exprt &expr);
 
   // deliberately protected now to protect lower-level API