Merge pull request #6189 from diffblue/quantifier_scoping

Quantifier scoping

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -552,6 +552,29 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   return false;
 }
 
+binding_exprt::variablest boolbvt::fresh_binding(const binding_exprt &binding)
+{
+  // to ensure freshness of the new identifiers
+  scope_counter++;
+
+  binding_exprt::variablest result;
+  result.reserve(binding.variables().size());
+
+  for(const auto &binding : binding.variables())
+  {
+    const auto &old_identifier = binding.get_identifier();
+
+    // produce a new identifier
+    const irep_idt new_identifier =
+      "boolbvt::scope::" + std::to_string(scope_counter) +
+      "::" + id2string(old_identifier);
+
+    result.emplace_back(new_identifier, binding.type());
+  }
+
+  return result;
+}
+
 void boolbvt::print_assignment(std::ostream &out) const
 {
   arrayst::print_assignment(out);

src/solvers/flattening/boolbv.h

@@ -274,6 +274,9 @@ class boolbvt:public arrayst
 
   // scopes
   std::size_t scope_counter = 0;
+
+  /// create new, unique variables for the given binding
+  binding_exprt::variablest fresh_binding(const binding_exprt &);
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H

src/solvers/flattening/boolbv_let.cpp

@@ -40,36 +40,31 @@ bvt boolbvt::convert_let(const let_exprt &expr)
   for(auto &value : values)
     converted_values.push_back(convert_bv(value));
 
-  scope_counter++;
-
-  // for renaming the bound symbols
-  replace_symbolt replace_symbol;
+  // get fresh bound symbols
+  auto fresh_variables = fresh_binding(expr.binding());
 
   // Now assign
-  for(const auto &binding : make_range(variables).zip(converted_values))
+  for(const auto &binding : make_range(fresh_variables).zip(converted_values))
   {
     bool is_boolean = binding.first.type().id() == ID_bool;
-    const auto &old_identifier = binding.first.get_identifier();
-
-    // produce a new identifier
-    const irep_idt new_identifier =
-      "boolbvt::scope::" + std::to_string(scope_counter) +
-      "::" + id2string(old_identifier);
+    const auto &identifier = binding.first.get_identifier();
 
     // make the symbol visible
     if(is_boolean)
     {
       DATA_INVARIANT(binding.second.size() == 1, "boolean values have one bit");
-      symbols[new_identifier] = binding.second[0];
+      symbols[identifier] = binding.second[0];
     }
     else
-      map.set_literals(new_identifier, binding.first.type(), binding.second);
-
-    // remember the renaming
-    replace_symbol.insert(
-      binding.first, symbol_exprt(new_identifier, binding.first.type()));
+      map.set_literals(identifier, binding.first.type(), binding.second);
   }
 
+  // for renaming the bound symbols
+  replace_symbolt replace_symbol;
+
+  for(const auto &pair : make_range(variables).zip(fresh_variables))
+    replace_symbol.insert(pair.first, pair.second);
+
   // rename the bound symbols in 'where'
   exprt where_renamed = expr.where();
   replace_symbol(where_renamed);
@@ -78,14 +73,13 @@ bvt boolbvt::convert_let(const let_exprt &expr)
   bvt result_bv = convert_bv(where_renamed);
 
   // the mapping can now be deleted
-  for(const auto &entry : replace_symbol.get_expr_map())
+  for(const auto &entry : fresh_variables)
   {
-    const auto &new_symbol = to_symbol_expr(entry.second);
-    const auto &type = new_symbol.type();
+    const auto &type = entry.type();
     if(type.id() == ID_bool)
-      symbols.erase(new_symbol.get_identifier());
+      symbols.erase(entry.get_identifier());
     else
-      map.erase_literals(new_symbol.get_identifier(), type);
+      map.erase_literals(entry.get_identifier(), type);
   }
 
   return result_bv;

src/solvers/flattening/boolbv_quantifier.cpp

@@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/optional.h>
+#include <util/range.h>
 #include <util/replace_expr.h>
+#include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
 /// A method to detect equivalence between experts that can contain typecast
@@ -206,6 +208,22 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
+  // We first worry about the scoping of the symbols bound by the quantifier.
+  auto fresh_symbols = fresh_binding(src);
+
+  // replace in where()
+  replace_symbolt replace_symbol;
+
+  for(const auto &pair : make_range(src.variables()).zip(fresh_symbols))
+    replace_symbol.insert(pair.first, pair.second);
+
+  exprt renamed_where = src.where();
+  replace_symbol(renamed_where);
+
+  // produce new quantifier expression
+  auto new_src =
+    quantifier_exprt(src.id(), std::move(fresh_symbols), renamed_where);
+
   const auto res = instantiate_quantifier(src, ns);
 
   if(res)

src/solvers/smt2/smt2_parser.cpp

@@ -131,30 +131,6 @@ exprt::operandst smt2_parsert::operands()
   return result;
 }
 
-irep_idt smt2_parsert::add_fresh_id(
-  const irep_idt &id,
-  idt::kindt kind,
-  const exprt &expr)
-{
-  auto &count=renaming_counters[id];
-  irep_idt new_id;
-  do
-  {
-    new_id=id2string(id)+'#'+std::to_string(count);
-    count++;
-  } while(!id_map
-             .emplace(
-               std::piecewise_construct,
-               std::forward_as_tuple(new_id),
-               std::forward_as_tuple(kind, expr))
-             .second);
-
-  // record renaming
-  renaming_map[id] = new_id;
-
-  return new_id;
-}
-
 void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr)
 {
   if(!id_map
@@ -169,16 +145,6 @@ void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr)
   }
 }
 
-irep_idt smt2_parsert::rename_id(const irep_idt &id) const
-{
-  auto it=renaming_map.find(id);
-
-  if(it==renaming_map.end())
-    return id;
-  else
-    return it->second;
-}
-
 exprt smt2_parsert::let_expression()
 {
   if(next_token() != smt2_tokenizert::OPEN)
@@ -254,7 +220,7 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   if(next_token() != smt2_tokenizert::OPEN)
     throw error() << "expected bindings after " << id;
 
-  std::vector<symbol_exprt> bindings;
+  binding_exprt::variablest bindings;
 
   while(smt2_tokenizer.peek() == smt2_tokenizert::OPEN)
   {
@@ -276,18 +242,23 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   if(next_token() != smt2_tokenizert::CLOSE)
     throw error("expected ')' at end of bindings");
 
-  // save the renaming map
-  renaming_mapt old_renaming_map = renaming_map;
+  // we may hide identifiers in outer scopes
+  std::vector<std::pair<irep_idt, idt>> saved_ids;
 
-  // go forwards, add to id_map, renaming if need be
+  // add the bindings to the id_map
   for(auto &b : bindings)
   {
-    const irep_idt id =
-      add_fresh_id(b.get_identifier(), idt::BINDING, exprt(ID_nil, b.type()));
-
-    b.set_identifier(id);
+    auto insert_result =
+      id_map.insert({b.get_identifier(), idt{idt::BINDING, b.type()}});
+    if(!insert_result.second) // already there
+    {
+      auto &id_entry = *insert_result.first;
+      saved_ids.emplace_back(id_entry.first, std::move(id_entry.second));
+      id_entry.second = idt{idt::BINDING, b.type()};
+    }
   }
 
+  // now parse, with bindings in place
   exprt expr=expression();
 
   if(next_token() != smt2_tokenizert::CLOSE)
@@ -299,8 +270,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   for(const auto &b : bindings)
     id_map.erase(b.get_identifier());
 
-  // restore renaming map
-  renaming_map = old_renaming_map;
+  // restore any previous ids
+  for(auto &saved_id : saved_ids)
+    id_map.insert(std::move(saved_id));
 
   // go backwards, build quantified expression
   for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
@@ -603,20 +575,18 @@ exprt smt2_parsert::function_application()
       auto op = operands();
 
       // rummage through id_map
-      const irep_idt final_id = rename_id(id);
-      auto id_it = id_map.find(final_id);
+      auto id_it = id_map.find(id);
       if(id_it != id_map.end())
       {
         if(id_it->second.type.id() == ID_mathematical_function)
         {
-          return function_application(
-            symbol_exprt(final_id, id_it->second.type), op);
+          return function_application(symbol_exprt(id, id_it->second.type), op);
         }
         else
-          return symbol_exprt(final_id, id_it->second.type);
+          return symbol_exprt(id, id_it->second.type);
       }
-
-      throw error() << "unknown function symbol '" << id << '\'';
+      else
+        throw error() << "unknown function symbol '" << id << '\'';
     }
     break;
 
@@ -916,11 +886,10 @@ exprt smt2_parsert::expression()
         return e_it->second();
 
       // rummage through id_map
-      const irep_idt final_id = rename_id(identifier);
-      auto id_it = id_map.find(final_id);
+      auto id_it = id_map.find(identifier);
       if(id_it != id_map.end())
       {
-        symbol_exprt symbol_expr(final_id, id_it->second.type);
+        symbol_exprt symbol_expr(identifier, id_it->second.type);
         if(smt2_tokenizer.token_is_quoted_symbol())
           symbol_expr.set(ID_C_quoted, true);
         return std::move(symbol_expr);
@@ -1393,9 +1362,7 @@ smt2_parsert::function_signature_definition()
 
     irep_idt id = smt2_tokenizer.get_buffer();
     domain.push_back(sort());
-
-    parameters.push_back(
-      add_fresh_id(id, idt::PARAMETER, exprt(ID_nil, domain.back())));
+    parameters.push_back(id);
 
     if(next_token() != smt2_tokenizert::CLOSE)
       throw error("expected ')' at end of parameter");
@@ -1497,16 +1464,35 @@ void smt2_parsert::setup_commands()
     if(next_token() != smt2_tokenizert::SYMBOL)
       throw error("expected a symbol after define-fun");
 
-    // save the renaming map
-    renaming_mapt old_renaming_map = renaming_map;
-
     const irep_idt id = smt2_tokenizer.get_buffer();
 
     const auto signature = function_signature_definition();
+
+    // put the parameters into the scope and take care of hiding
+    std::vector<std::pair<irep_idt, idt>> hidden_ids;
+
+    for(const auto &pair : signature.ids_and_types())
+    {
+      auto insert_result =
+        id_map.insert({pair.first, idt{idt::PARAMETER, pair.second}});
+      if(!insert_result.second) // already there
+      {
+        auto &id_entry = *insert_result.first;
+        hidden_ids.emplace_back(id_entry.first, std::move(id_entry.second));
+        id_entry.second = idt{idt::PARAMETER, pair.second};
+      }
+    }
+
+    // now parse body with parameter ids in place
     const auto body = expression();
 
-    // restore renamings
-    std::swap(renaming_map, old_renaming_map);
+    // remove the parameter ids
+    for(auto &id : signature.parameters)
+      id_map.erase(id);
+
+    // restore the hidden ids, if any
+    for(auto &hidden_id : hidden_ids)
+      id_map.insert(std::move(hidden_id));
 
     // check type of body
     if(signature.type.id() == ID_mathematical_function)

src/solvers/smt2/smt2_parser.h

@@ -42,6 +42,11 @@ class smt2_parsert
     {
     }
 
+    idt(kindt _kind, typet __type)
+      : kind(_kind), type(std::move(__type)), definition(nil_exprt())
+    {
+    }
+
     kindt kind;
     typet type;
     exprt definition;
@@ -88,14 +93,9 @@ class smt2_parsert
   std::size_t parenthesis_level;
   smt2_tokenizert::tokent next_token();
 
-  // for let/quantifier bindings, function parameters
-  using renaming_mapt=std::map<irep_idt, irep_idt>;
-  renaming_mapt renaming_map;
-  using renaming_counterst=std::map<irep_idt, unsigned>;
-  renaming_counterst renaming_counters;
-  irep_idt add_fresh_id(const irep_idt &, idt::kindt, const exprt &);
+  // add the given identifier to the id_map but
+  // complain if that identifier is used already
   void add_unique_id(const irep_idt &, const exprt &);
-  irep_idt rename_id(const irep_idt &) const;
 
   struct signature_with_parameter_idst
   {
@@ -117,6 +117,22 @@ class smt2_parsert
            _parameters.size()) ||
         (_type.id() != ID_mathematical_function && _parameters.empty()));
     }
+
+    // a convenience helper for iterating over identifiers and types
+    std::vector<std::pair<irep_idt, typet>> ids_and_types() const
+    {
+      if(parameters.empty())
+        return {};
+      else
+      {
+        std::vector<std::pair<irep_idt, typet>> result;
+        result.reserve(parameters.size());
+        const auto &domain = to_mathematical_function_type(type).domain();
+        for(std::size_t i = 0; i < parameters.size(); i++)
+          result.emplace_back(parameters[i], domain[i]);
+        return result;
+      }
+    }
   };
 
   // expressions