Merge pull request #5160 from diffblue/let_with_multiple_bindings

Let with multiple bindings

Author: kroening

src/solvers/flattening/boolbv_let.cpp

@@ -8,25 +8,34 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
+#include <util/range.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
 bvt boolbvt::convert_let(const let_exprt &expr)
 {
-  const bvt value_bv=convert_bv(expr.value());
+  const auto &variables = expr.variables();
+  const auto &values = expr.values();
 
-  // 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();
+  for(auto &binding : make_range(variables).zip(values))
+  {
+    const bvt value_bv = convert_bv(binding.second);
+
+    // 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();
+
+    // the symbol shall be visible during the recursive call
+    // to convert_bv
+    map.set_literals(id, binding.first.type(), value_bv);
+  }
 
-  // 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());
 
   // now remove, no longer needed
-  map.erase_literals(id, expr.symbol().type());
+  for(auto &variable : variables)
+    map.erase_literals(variable.get_identifier(), variable.type());
 
   return result_bv;
 }

src/solvers/prop/prop_conv_solver.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "prop_conv_solver.h"
 
+#include <util/range.h>
+
 #include <algorithm>
 
 bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
@@ -308,23 +310,35 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
   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
-    if(
-      let_expr.value().type().id() == ID_bool &&
-      let_expr.where().type().id() == ID_bool)
+    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)
     {
-      literalt value = convert(let_expr.value());
+      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;
+      }
 
-      // 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);
+      for(auto &variable : variables)
+        symbols.erase(variable.get_identifier());
+
       return result;
     }
   }

src/solvers/smt2/smt2_conv.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/pointer_offset_size.h>
+#include <util/range.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string2int.h>
@@ -1855,11 +1856,28 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_let)
   {
     const let_exprt &let_expr=to_let_expr(expr);
-    out << "(let ((";
-    convert_expr(let_expr.symbol());
-    out << ' ';
-    convert_expr(let_expr.value());
-    out << ")) ";
+    const auto &variables = let_expr.variables();
+    const auto &values = let_expr.values();
+
+    out << "(let (";
+    bool first = true;
+
+    for(auto &binding : make_range(variables).zip(values))
+    {
+      if(first)
+        first = false;
+      else
+        out << ' ';
+
+      out << '(';
+      convert_expr(binding.first);
+      out << ' ';
+      convert_expr(binding.second);
+      out << ')';
+    }
+
+    out << ") "; // bindings
+
     convert_expr(let_expr.where());
     out << ')'; // let
   }

src/solvers/smt2/smt2_parser.cpp

@@ -208,21 +208,18 @@ exprt smt2_parsert::let_expression()
     b.first = add_fresh_id(b.first, b.second);
   }
 
-  exprt expr=expression();
+  exprt where = expression();
 
   if(next_token() != smt2_tokenizert::CLOSE)
     throw error("expected ')' after let");
 
-  exprt result=expr;
+  binding_exprt::variablest variables;
+  exprt::operandst values;
 
-  // go backwards, build let_expr
-  for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
+  for(const auto &b : bindings)
   {
-    const let_exprt let(
-      symbol_exprt(r_it->first, r_it->second.type()),
-      r_it->second,
-      result);
-    result=let;
+    variables.push_back(symbol_exprt(b.first, b.second.type()));
+    values.push_back(b.second);
   }
 
   // we keep these in the id_map in order to retain globally
@@ -231,7 +228,7 @@ exprt smt2_parsert::let_expression()
   // restore renamings
   renaming_map=old_renaming_map;
 
-  return result;
+  return let_exprt(variables, values, where);
 }
 
 exprt smt2_parsert::quantifier_expression(irep_idt id)