boolbvt: introduce scopes

Author: Daniel Kroening

src/solvers/flattening/boolbv.h

@@ -119,6 +119,10 @@ class boolbvt:public arrayst
   typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
   bv_cachet bv_cache;
 
+  // record the subexpressions that use the scoped variable,
+  // in order to clear them from the cache after we are done
+  std::vector<bv_cachet::iterator> bv_cache_iterators;
+
   bool type_conversion(
     const typet &src_type, const bvt &src,
     const typet &dest_type, bvt &dest);

src/solvers/flattening/boolbv_let.cpp

@@ -15,16 +15,30 @@ bvt boolbvt::convert_let(const let_exprt &expr)
 {
   const bvt value_bv=convert_bv(expr.value());
 
-  // We expect the identifiers of the bound symbols to be unique,
-  // and thus, these can go straight into the symbol to literal map.
-  // This property also allows us to cache any subexpressions.
-  const irep_idt &id=expr.symbol().get_identifier();
+  const irep_idt &id = 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?
 
   // the symbol shall be visible during the recursive call
   // to convert_bv
   map.set_literals(id, expr.symbol().type(), value_bv);
+
+  bool previous_record_cache_iterators = record_cache_iterators;
+  std::size_t previous_prop_cache_iterators_size = prop_cache_iterators.size();
+  std::size_t previous_bv_cache_iterators_size = bv_cache_iterators.size();
+  record_cache_iterators = true;
+
+  // recursive call
   bvt result_bv=convert_bv(expr.where());
 
+  // clear cache_iterators that use the bound symbol from the cache
+  bv_cache_iterators.resize(previous_prop_cache_iterators_size);
+  bv_cache_iterators.resize(previous_bv_cache_iterators_size);
+  record_cache_iterators = previous_record_cache_iterators;
+
   // now remove, no longer needed
   map.erase_literals(id, expr.symbol().type());