Merge pull request #4992 from diffblue/let-is-a-binding

let_exprt can now do multiple bindings

Author: Daniel Kroening

src/util/irep_ids.def

@@ -4,6 +4,7 @@
 
 IREP_ID_TWO(empty_string, )
 IREP_ID_ONE(let)
+IREP_ID_ONE(let_binding)
 IREP_ID_ONE(nil)
 IREP_ID_ONE(type)
 IREP_ID_ONE(bool)

src/util/mathematical_expr.h

@@ -271,47 +271,6 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
   return ret;
 }
 
-/// \brief A base class for variable bindings (quantifiers, let, lambda)
-class binding_exprt : public binary_exprt
-{
-public:
-  using variablest = std::vector<symbol_exprt>;
-
-  /// construct the binding expression
-  binding_exprt(
-    irep_idt _id,
-    const variablest &_variables,
-    exprt _where,
-    typet _type)
-    : binary_exprt(
-        tuple_exprt((const operandst &)_variables),
-        _id,
-        std::move(_where),
-        std::move(_type))
-  {
-  }
-
-  variablest &variables()
-  {
-    return (variablest &)static_cast<tuple_exprt &>(op0()).operands();
-  }
-
-  const variablest &variables() const
-  {
-    return (variablest &)static_cast<const tuple_exprt &>(op0()).operands();
-  }
-
-  exprt &where()
-  {
-    return op1();
-  }
-
-  const exprt &where() const
-  {
-    return op1();
-  }
-};
-
 /// \brief A base class for quantifier expressions
 class quantifier_exprt : public binding_exprt
 {

src/util/std_expr.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include "mathematical_types.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
+#include "range.h"
 #include "simplify_expr.h"
 
 bool constant_exprt::value_is_zero_string() const
@@ -303,3 +304,29 @@ void dereference_exprt::validate(
     "dereference expression's type must match the subtype of the type of its "
     "operand");
 }
+
+void let_exprt::validate(const exprt &expr, const validation_modet vm)
+{
+  check(expr, vm);
+
+  const auto &let_expr = to_let_expr(expr);
+
+  DATA_CHECK(
+    vm,
+    let_expr.values().size() == let_expr.variables().size(),
+    "number of variables must match number of values");
+
+  for(const auto &binding :
+      make_range(let_expr.variables()).zip(let_expr.values()))
+  {
+    DATA_CHECK(
+      vm,
+      binding.first.id() == ID_symbol,
+      "let binding symbols must be symbols");
+
+    DATA_CHECK(
+      vm,
+      binding.first.type() == binding.second.type(),
+      "let bindings must be type consistent");
+  }
+}

src/util/std_expr.h

@@ -4306,49 +4306,157 @@ class infinity_exprt : public nullary_exprt
   }
 };
 
+/// \brief A base class for variable bindings (quantifiers, let, lambda)
+class binding_exprt : public binary_exprt
+{
+public:
+  using variablest = std::vector<symbol_exprt>;
+
+  /// construct the binding expression
+  binding_exprt(
+    irep_idt _id,
+    const variablest &_variables,
+    exprt _where,
+    typet _type)
+    : binary_exprt(
+        multi_ary_exprt(
+          ID_tuple,
+          (const operandst &)_variables,
+          typet(ID_tuple)),
+        _id,
+        std::move(_where),
+        std::move(_type))
+  {
+  }
+
+  variablest &variables()
+  {
+    return (variablest &)to_multi_ary_expr(op0()).operands();
+  }
+
+  const variablest &variables() const
+  {
+    return (variablest &)to_multi_ary_expr(op0()).operands();
+  }
+
+  exprt &where()
+  {
+    return op1();
+  }
+
+  const exprt &where() const
+  {
+    return op1();
+  }
+};
+
 /// \brief A let expression
-class let_exprt : public ternary_exprt
+class let_exprt : public binary_exprt
 {
 public:
-  let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
-    : ternary_exprt(
+  let_exprt(
+    binding_exprt::variablest variables,
+    operandst values,
+    const exprt &where)
+    : binary_exprt(
+        binding_exprt(
+          ID_let_binding,
+          std::move(variables),
+          where,
+          where.type()),
         ID_let,
-        std::move(symbol),
-        std::move(value),
-        where,
+        multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
         where.type())
   {
+    PRECONDITION(this->variables().size() == this->values().size());
   }
 
+  /// convenience constructor for the case of a single binding
+  let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
+    : let_exprt(
+        binding_exprt::variablest{std::move(symbol)},
+        operandst{std::move(value)},
+        where)
+  {
+  }
+
+  binding_exprt &binding()
+  {
+    return static_cast<binding_exprt &>(op0());
+  }
+
+  const binding_exprt &binding() const
+  {
+    return static_cast<const binding_exprt &>(op0());
+  }
+
+  /// convenience accessor for the symbol of a single binding
   symbol_exprt &symbol()
   {
-    return static_cast<symbol_exprt &>(op0());
+    auto &variables = binding().variables();
+    PRECONDITION(variables.size() == 1);
+    return variables.front();
   }
 
+  /// convenience accessor for the symbol of a single binding
   const symbol_exprt &symbol() const
   {
-    return static_cast<const symbol_exprt &>(op0());
+    const auto &variables = binding().variables();
+    PRECONDITION(variables.size() == 1);
+    return variables.front();
   }
 
+  /// convenience accessor for the value of a single binding
   exprt &value()
   {
-    return op1();
+    auto &values = this->values();
+    PRECONDITION(values.size() == 1);
+    return values.front();
   }
 
+  /// convenience accessor for the value of a single binding
   const exprt &value() const
   {
-    return op1();
+    const auto &values = this->values();
+    PRECONDITION(values.size() == 1);
+    return values.front();
   }
 
+  operandst &values()
+  {
+    return static_cast<multi_ary_exprt &>(op1()).operands();
+  }
+
+  const operandst &values() const
+  {
+    return static_cast<const multi_ary_exprt &>(op1()).operands();
+  }
+
+  /// convenience accessor for binding().variables()
+  binding_exprt::variablest &variables()
+  {
+    return binding().variables();
+  }
+
+  /// convenience accessor for binding().variables()
+  const binding_exprt::variablest &variables() const
+  {
+    return binding().variables();
+  }
+
+  /// convenience accessor for binding().where()
   exprt &where()
   {
-    return op2();
+    return binding().where();
   }
 
+  /// convenience accessor for binding().where()
   const exprt &where() const
   {
-    return op2();
+    return binding().where();
   }
+
+  static void validate(const exprt &, validation_modet);
 };
 
 template <>
@@ -4357,9 +4465,9 @@ inline bool can_cast_expr<let_exprt>(const exprt &base)
   return base.id() == ID_let;
 }
 
-inline void validate_expr(const let_exprt &value)
+inline void validate_expr(const let_exprt &let_expr)
 {
-  validate_operands(value, 3, "Let must have three operands");
+  validate_operands(let_expr, 2, "Let must have two operands");
 }
 
 /// \brief Cast an exprt to a \ref let_exprt