let_exprt now uses binding_exprt

This enables let_exprt to do multiple binding, which matches what the
SMT-LIB standard does.  The new let_exprt can be re-written into a lambda
binding plus a function application in the standard way.

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/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

@@ -4327,48 +4327,112 @@ class binding_exprt : public binary_exprt
 };
 
 /// \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 <>
@@ -4377,9 +4441,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