let_exprt can now do multiple bindings

This matches what the SMT-LIB standard does.  It also matches what our own
binding_exprt can do, i.e., 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.h

@@ -4283,47 +4283,109 @@ class infinity_exprt : public nullary_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(
+  class let_binding_exprt : public binary_exprt
+  {
+  public:
+    let_binding_exprt(symbol_exprt symbol, exprt value)
+      : binary_exprt(
+          std::move(symbol),
+          ID_let,
+          std::move(value),
+          typet(ID_tuple))
+    {
+    }
+
+    const symbol_exprt &symbol() const
+    {
+      return static_cast<const symbol_exprt &>(op0());
+    }
+
+    symbol_exprt &symbol()
+    {
+      return static_cast<symbol_exprt &>(op0());
+    }
+
+    const exprt &value() const
+    {
+      return op1();
+    }
+
+    exprt &value()
+    {
+      return op1();
+    }
+  };
+
+  using bindingst = std::vector<let_binding_exprt>;
+
+  let_exprt(const bindingst &bindings, const exprt &where)
+    : binary_exprt(
+        multi_ary_exprt(ID_tuple, (const operandst &)bindings, typet(ID_tuple)),
         ID_let,
-        std::move(symbol),
-        std::move(value),
         where,
         where.type())
   {
   }
 
+  /// convenience constructor for the case of a single binding
+  let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
+    : let_exprt({ let_binding_exprt(std::move(symbol), std::move(value)) }, where)
+  {
+  }
+
+  bindingst &bindings()
+  {
+    return (bindingst &)op0().operands();
+  }
+
+  const bindingst &bindings() const
+  {
+    return (bindingst &)op0().operands();
+  }
+
+  /// convenience accessor for the symbol of a single binding
   symbol_exprt &symbol()
   {
-    return static_cast<symbol_exprt &>(op0());
+    auto &bindings = this->bindings();
+    PRECONDITION(bindings.size() == 1);
+    return bindings.front().symbol();
   }
 
+  /// convenience accessor for the symbol of a single binding
   const symbol_exprt &symbol() const
   {
-    return static_cast<const symbol_exprt &>(op0());
+    const auto &bindings = this->bindings();
+    PRECONDITION(bindings.size() == 1);
+    return bindings.front().symbol();
   }
 
+  /// convenience accessor for the value of a single binding
   exprt &value()
   {
-    return op1();
+    auto &bindings = this->bindings();
+    PRECONDITION(bindings.size() == 1);
+    return bindings.front().value();
   }
 
+  /// convenience accessor for the value of a single binding
   const exprt &value() const
   {
-    return op1();
+    const auto &bindings = this->bindings();
+    PRECONDITION(bindings.size() == 1);
+    return bindings.front().value();
   }
 
   exprt &where()
   {
-    return op2();
+    return op1();
   }
 
   const exprt &where() const
   {
-    return op2();
+    return op1();
   }
 };
 
@@ -4335,7 +4397,22 @@ inline bool can_cast_expr<let_exprt>(const exprt &base)
 
 inline void validate_expr(const let_exprt &value)
 {
-  validate_operands(value, 3, "Let must have three operands");
+  validate_operands(value, 2, "Let must have two operands");
+
+  // symbols and assignments alternate
+  for(const auto &binding : value.bindings())
+  {
+    DATA_INVARIANT(
+      binding.id() == ID_let_binding, "let bindings must have correct id");
+
+    DATA_INVARIANT(
+      binding.symbol().id() == ID_symbol,
+      "let binding symbols must be symbols");
+
+    DATA_INVARIANT(
+      binding.symbol().type() == binding.value().type(),
+      "let bindings must be type consistent");
+  }
 }
 
 /// \brief Cast an exprt to a \ref let_exprt