Merge pull request #4510 from diffblue/solver-scopes

prop_conv_solvert: introduce scopes

Author: kroening

regression/smt2_solver/let1/let-scoping1.desc renamed to regression/smt2_solver/let/let-scoping1.desc

@@ -0,0 +1,7 @@
+CORE
+let-with-bv2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/let1/let-scoping1.smt2 renamed to regression/smt2_solver/let/let-scoping1.smt2

@@ -0,0 +1,26 @@
+(set-logic QF_BV)
+
+(define-fun x () (_ BitVec 8) #x12)
+
+; let hides the function 'x'
+(define-fun let1 () Bool (let ((x #x4567)) (= x #x4567)))
+
+; the binding isn't visible immediately
+(define-fun let2 () Bool (= (let ((x x)) x) #x12))
+
+; parallel let
+(define-fun let3 () Bool (= (let ((x #x45) (y x)) y) #x12))
+
+; limited scope
+(define-fun let4 () Bool (and (let ((x true)) x) (= x #x12)))
+
+; all must be true
+
+(assert (not (and
+  let1
+  let2
+  let3
+  let4
+  )))
+
+(check-sat)

regression/smt2_solver/let-with-bv1/test.desc renamed to regression/smt2_solver/let/let-with-bv1.desc

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

regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 renamed to regression/smt2_solver/let/let-with-bv1.smt2

@@ -9,32 +9,84 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <util/range.h>
+#include <util/replace_symbol.h>
 #include <util/std_expr.h>
 
 bvt boolbvt::convert_let(const let_exprt &expr)
 {
   const auto &variables = expr.variables();
   const auto &values = expr.values();
 
+  DATA_INVARIANT(
+    expr.type() == expr.where().type(),
+    "let must have the type of the 'where' operand");
+
+  // Check the types.
   for(auto &binding : make_range(variables).zip(values))
   {
-    const bvt value_bv = convert_bv(binding.second);
+    DATA_INVARIANT(
+      binding.first.type() == binding.second.type(),
+      "let value must have the type of the let symbol");
+  }
+
+  // A let expression can bind multiple symbols simultaneously.
+  // This is a 'concurrent' binding, i.e., the symbols are not yet
+  // visible when evaluating the values. SMT-LIB also has this
+  // semantics. We therefore first convert all values,
+  // and only then assign them.
+  std::vector<bvt> converted_values;
+  converted_values.reserve(variables.size());
+
+  for(auto &value : values)
+    converted_values.push_back(convert_bv(value));
+
+  scope_counter++;
+
+  // for renaming the bound symbols
+  replace_symbolt replace_symbol;
+
+  // Now assign
+  for(const auto &binding : make_range(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);
 
-    // 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 = 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];
+    }
+    else
+      map.set_literals(new_identifier, binding.first.type(), binding.second);
 
-    // the symbol shall be visible during the recursive call
-    // to convert_bv
-    map.set_literals(id, binding.first.type(), value_bv);
+    // remember the renaming
+    replace_symbol.insert(
+      binding.first, symbol_exprt(new_identifier, binding.first.type()));
   }
 
-  bvt result_bv=convert_bv(expr.where());
+  // rename the bound symbols in 'where'
+  exprt where_renamed = expr.where();
+  replace_symbol(where_renamed);
 
-  // now remove, no longer needed
-  for(auto &variable : variables)
-    map.erase_literals(variable.get_identifier(), variable.type());
+  // recursive call
+  bvt result_bv = convert_bv(where_renamed);
+
+  // the mapping can now be deleted
+  for(const auto &entry : replace_symbol.get_expr_map())
+  {
+    const auto &new_symbol = to_symbol_expr(entry.second);
+    const auto &type = new_symbol.type();
+    if(type.id() == ID_bool)
+      symbols.erase(new_symbol.get_identifier());
+    else
+      map.erase_literals(new_symbol.get_identifier(), type);
+  }
 
   return result_bv;
 }

regression/smt2_solver/let/let-with-bv2.desc

@@ -172,8 +172,8 @@ literalt prop_conv_solvert::convert(const exprt &expr)
   literalt literal = convert_bool(expr);
 
   // insert into cache
-
   result.first->second = literal;
+
   if(freeze_all && !literal.is_constant())
     prop.set_frozen(literal);
 
@@ -295,41 +295,6 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
       return equal ? prop.lequal(tmp1, tmp2) : prop.lxor(tmp1, tmp2);
     }
   }
-  else if(expr.id() == ID_let)
-  {
-    const let_exprt &let_expr = to_let_expr(expr);
-    const auto &variables = let_expr.variables();
-    const auto &values = let_expr.values();
-
-    // first check whether this is all boolean
-    const bool all_boolean =
-      let_expr.where().type().id() == ID_bool &&
-      std::all_of(values.begin(), values.end(), [](const exprt &e) {
-        return e.type().id() == ID_bool;
-      });
-
-    if(all_boolean)
-    {
-      for(auto &binding : make_range(variables).zip(values))
-      {
-        literalt value_converted = convert(binding.second);
-
-        // 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 = binding.first.get_identifier();
-        symbols[id] = value_converted;
-      }
-
-      literalt result = convert(let_expr.where());
-
-      // remove again
-      for(auto &variable : variables)
-        symbols.erase(variable.get_identifier());
-
-      return result;
-    }
-  }
 
   return convert_rest(expr);
 }