Use lambda_exprt

The API increases the readability of the code and also enables early
checking for valid expression structure.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -294,7 +294,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_complex_imag)
     return convert_complex_imag(to_complex_imag_expr(expr));
   else if(expr.id()==ID_lambda)
-    return convert_lambda(expr);
+    return convert_lambda(to_lambda_expr(expr));
   else if(expr.id()==ID_array_of)
     return convert_array_of(to_array_of_expr(expr));
   else if(expr.id()==ID_let)
@@ -316,28 +316,21 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   return conversion_failed(expr);
 }
 
-bvt boolbvt::convert_lambda(const exprt &expr)
+bvt boolbvt::convert_lambda(const lambda_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  DATA_INVARIANT(
-    expr.operands().size() == 2, "lambda expression should have two operands");
-
-  if(expr.type().id()!=ID_array)
-    return conversion_failed(expr);
-
-  const exprt &array_size=
-    to_array_type(expr.type()).size();
+  const exprt &array_size = expr.type().size();
 
   const auto size = numeric_cast<mp_integer>(array_size);
 
   if(!size.has_value())
     return conversion_failed(expr);
 
-  typet counter_type=expr.op0().type();
+  typet counter_type = expr.arg().type();
 
   bvt bv;
   bv.resize(width);
@@ -346,10 +339,10 @@ bvt boolbvt::convert_lambda(const exprt &expr)
   {
     exprt counter=from_integer(i, counter_type);
 
-    exprt expr_op1(expr.op1());
-    replace_expr(expr.op0(), counter, expr_op1);
+    exprt body = expr.body();
+    replace_expr(expr.arg(), counter, body);
 
-    const bvt &tmp=convert_bv(expr_op1);
+    const bvt &tmp = convert_bv(body);
 
     INVARIANT(
       *size * tmp.size() == width,

src/solvers/flattening/boolbv.h

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 class extractbit_exprt;
 class extractbits_exprt;
+class lambda_exprt;
 class member_exprt;
 
 class boolbvt:public arrayst
@@ -148,7 +149,7 @@ class boolbvt:public arrayst
   virtual bvt convert_complex(const complex_exprt &expr);
   virtual bvt convert_complex_real(const complex_real_exprt &expr);
   virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
-  virtual bvt convert_lambda(const exprt &expr);
+  virtual bvt convert_lambda(const lambda_exprt &expr);
   virtual bvt convert_let(const let_exprt &);
   virtual bvt convert_array_of(const array_of_exprt &expr);
   virtual bvt convert_union(const union_exprt &expr);

src/util/simplify_expr_array.cpp

@@ -48,15 +48,12 @@ bool simplify_exprt::simplify_index(exprt &expr)
   {
     // simplify (lambda i: e)(x) to e[i/x]
 
-    const exprt &lambda_expr=array;
+    const lambda_exprt &lambda_expr = to_lambda_expr(array);
 
-    if(lambda_expr.operands().size()!=2)
-      return true;
-
-    if(expr.op1().type()==lambda_expr.op0().type())
+    if(expr.op1().type() == lambda_expr.arg().type())
     {
-      exprt tmp=lambda_expr.op1();
-      replace_expr(lambda_expr.op0(), expr.op1(), tmp);
+      exprt tmp = lambda_expr.body();
+      replace_expr(lambda_expr.arg(), expr.op1(), tmp);
       expr.swap(tmp);
       return false;
     }