Merge pull request #3049 from tautschnig/fix-let-exprt

Remove let_exprt's default constructor

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -4761,13 +4761,10 @@ exprt smt2_convt::letify_rec(
   if(map.find(current)->second.count < LET_COUNT)
     return letify_rec(expr, let_order, map, i+1);
 
-  let_exprt let;
-
-  let.symbol() = map.find(current)->second.let_symbol;
-  let.value() = substitute_let(current, map);
-  let.where() = letify_rec(expr, let_order, map, i+1);
-
-  return let;
+  return let_exprt(
+    map.find(current)->second.let_symbol,
+    substitute_let(current, map),
+    letify_rec(expr, let_order, map, i + 1));
 }
 
 void smt2_convt::collect_bindings(

src/solvers/smt2/smt2_parser.cpp

@@ -188,11 +188,10 @@ exprt smt2_parsert::let_expression()
   // go backwards, build let_expr
   for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
   {
-    let_exprt let;
-    let.symbol()=symbol_exprt(r_it->first, r_it->second.type());
-    let.value()=r_it->second;
-    let.type()=result.type();
-    let.where().swap(result);
+    const let_exprt let(
+      symbol_exprt(r_it->first, r_it->second.type()),
+      r_it->second,
+      result);
     result=let;
   }
 

src/util/std_expr.h

@@ -4520,13 +4520,15 @@ class infinity_exprt : public nullary_exprt
 };
 
 /// \brief A let expression
-class let_exprt:public exprt
+class let_exprt : public ternary_exprt
 {
 public:
-  let_exprt():exprt(ID_let)
+  let_exprt(
+    const symbol_exprt &symbol,
+    const exprt &value,
+    const exprt &where)
+    : ternary_exprt(ID_let, symbol, value, where, where.type())
   {
-    operands().resize(3);
-    op0()=symbol_exprt();
   }
 
   symbol_exprt &symbol()