boolbvt: introduce scopes

This is the biggest change to the solver interface since it got added to the
codebase.

Currently, bound identifiers (exists, forall, let) must be unique; the
solver looses soundness if that assumption is violated.

This change introduces scopes, i.e., the uniqueness requirement is dropped.
Nested scoping works as expected.  This matches what SMT-LIB does, i.e., the
renaming done in the SMT-LIB front-end can be dropped (which is the next
commit).

Author: Daniel Kroening

src/solvers/flattening/boolbv.h

@@ -263,6 +263,9 @@ class boolbvt:public arrayst
 
   // strings
   numbering<irep_idt> string_numbering;
+
+  // scopes
+  std::size_t scope_counter = 0;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H

src/solvers/flattening/boolbv_let.cpp

@@ -13,20 +13,55 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_let(const let_exprt &expr)
 {
-  const bvt value_bv=convert_bv(expr.value());
+  DATA_INVARIANT(
+    expr.value().type() == expr.symbol().type(),
+    "let value must have the type of the let symbol");
+  DATA_INVARIANT(
+    expr.type() == expr.where().type(),
+    "let must have the type of the 'where' operand");
 
-  // 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 bvt value_bv = convert_bv(expr.value());
+
+  bool is_boolean = expr.value().type().id() == ID_bool;
+  const auto &old_identifier = expr.symbol().get_identifier();
+
+  // produce a new identifier
+  const irep_idt new_identifier =
+    "boolbvt::scope::" + std::to_string(scope_counter) +
+    "::" + id2string(old_identifier);
+
+  scope_counter++;
 
   // the symbol shall be visible during the recursive call
-  // to convert_bv
-  map.set_literals(id, expr.symbol().type(), value_bv);
-  bvt result_bv=convert_bv(expr.where());
+  // to convert_bv for 'where'
+  if(is_boolean)
+  {
+    DATA_INVARIANT(value_bv.size() == 1, "boolean values have one bit");
+    symbols[new_identifier] = value_bv[0];
+  }
+  else
+    map.set_literals(new_identifier, expr.symbol().type(), value_bv);
+
+  // rename bound symbol in 'where'
+  exprt where_renamed = expr.where();
+
+  where_renamed.visit_post([old_identifier, new_identifier](exprt &expr) {
+    if(expr.id() == ID_symbol)
+    {
+      auto &symbol_expr = to_symbol_expr(expr);
+      if(symbol_expr.get_identifier() == old_identifier)
+        symbol_expr.set_identifier(new_identifier);
+    }
+  });
+
+  // recursive call
+  bvt result_bv = convert_bv(where_renamed);
 
-  // now remove, no longer needed
-  map.erase_literals(id, expr.symbol().type());
+  // the mapping can now be deleted
+  if(is_boolean)
+    symbols.erase(new_identifier);
+  else
+    map.erase_literals(new_identifier, expr.symbol().type());
 
   return result_bv;
 }