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/std_expr.h

@@ -4283,47 +4283,81 @@ 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(
+    : binary_exprt(
+        multi_ary_exprt(
+          ID_tuple,
+          {std::move(symbol), std::move(value)},
+          typet(ID_tuple)),
+        ID_let,
+        where,
+        where.type())
+  {
+  }
+
+  using symbol_value_sequencet = std::vector<exprt>;
+
+  let_exprt(symbol_value_sequencet symbol_value_sequence, const exprt &where)
+    : binary_exprt(
+        multi_ary_exprt(
+          ID_tuple,
+          std::move(symbol_value_sequence),
+          typet(ID_tuple)),
         ID_let,
-        std::move(symbol),
-        std::move(value),
         where,
         where.type())
   {
   }
 
+  symbol_value_sequencet &symbol_value_sequence()
+  {
+    return (symbol_value_sequencet &)op0().operands();
+  }
+
+  const symbol_value_sequencet &symbol_value_sequence() const
+  {
+    return (symbol_value_sequencet &)op0().operands();
+  }
+
   symbol_exprt &symbol()
   {
-    return static_cast<symbol_exprt &>(op0());
+    auto &sequence = symbol_value_sequence();
+    PRECONDITION(sequence.size() == 2);
+    return to_symbol_expr(sequence[0]);
   }
 
   const symbol_exprt &symbol() const
   {
-    return static_cast<const symbol_exprt &>(op0());
+    const auto &sequence = symbol_value_sequence();
+    PRECONDITION(sequence.size() == 2);
+    return to_symbol_expr(sequence[0]);
   }
 
   exprt &value()
   {
-    return op1();
+    auto &sequence = symbol_value_sequence();
+    PRECONDITION(sequence.size() == 2);
+    return sequence[1];
   }
 
   const exprt &value() const
   {
-    return op1();
+    const auto &sequence = symbol_value_sequence();
+    PRECONDITION(sequence.size() == 2);
+    return sequence[1];
   }
 
   exprt &where()
   {
-    return op2();
+    return op1();
   }
 
   const exprt &where() const
   {
-    return op2();
+    return op1();
   }
 };