Merge pull request #4683 from antlechner/antonia/rename-lambda

Rename lambda_exprt to array_comprehension_exprt

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(to_lambda_expr(expr));
+    return convert_lambda(to_array_comprehension_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,7 +316,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   return conversion_failed(expr);
 }
 
-bvt boolbvt::convert_lambda(const lambda_exprt &expr)
+bvt boolbvt::convert_lambda(const array_comprehension_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 

src/solvers/flattening/boolbv.h

@@ -28,7 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 class extractbit_exprt;
 class extractbits_exprt;
-class lambda_exprt;
+class array_comprehension_exprt;
 class member_exprt;
 
 class boolbvt:public arrayst
@@ -149,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 lambda_exprt &expr);
+  virtual bvt convert_lambda(const array_comprehension_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,12 +48,12 @@ bool simplify_exprt::simplify_index(exprt &expr)
   {
     // simplify (lambda i: e)(x) to e[i/x]
 
-    const lambda_exprt &lambda_expr = to_lambda_expr(array);
+    const auto &comprehension = to_array_comprehension_expr(array);
 
-    if(expr.op1().type() == lambda_expr.arg().type())
+    if(expr.op1().type() == comprehension.arg().type())
     {
-      exprt tmp = lambda_expr.body();
-      replace_expr(lambda_expr.arg(), expr.op1(), tmp);
+      exprt tmp = comprehension.body();
+      replace_expr(comprehension.arg(), expr.op1(), tmp);
       expr.swap(tmp);
       simplify_rec(expr);
       return false;

src/util/std_expr.h

@@ -4462,10 +4462,21 @@ inline cond_exprt &to_cond_expr(exprt &expr)
 
 /// \brief Expression to define a mapping from an argument (index) to elements.
 /// This enables constructing an array via an anonymous function.
-class lambda_exprt : public binary_exprt
+/// Not all kinds of array comprehension can be expressed, only those of the
+/// form `[f(x) | x in {0, 1, ... array_size-1}]`.
+/// The LHS and RHS are the argument (`x`) and body (`f(x)`) of the anonymous
+/// function, respectively. The range is given by the type of the expression,
+/// which has to be an \ref array_typet (which includes a value for
+/// `array_size`).
+/// For legacy reasons, the ID of an array_comprehension_exprt is ID_lambda,
+/// even though it cannot be used to represent arbitrary lambda functions.
+class array_comprehension_exprt : public binary_exprt
 {
 public:
-  explicit lambda_exprt(symbol_exprt arg, exprt body, array_typet _type)
+  explicit array_comprehension_exprt(
+    symbol_exprt arg,
+    exprt body,
+    array_typet _type)
     : binary_exprt(std::move(arg), ID_lambda, std::move(body), std::move(_type))
   {
   }
@@ -4502,35 +4513,38 @@ class lambda_exprt : public binary_exprt
 };
 
 template <>
-inline bool can_cast_expr<lambda_exprt>(const exprt &base)
+inline bool can_cast_expr<array_comprehension_exprt>(const exprt &base)
 {
   return base.id() == ID_lambda;
 }
 
-inline void validate_expr(const lambda_exprt &value)
+inline void validate_expr(const array_comprehension_exprt &value)
 {
-  validate_operands(value, 2, "'Lambda' must have two operands");
+  validate_operands(value, 2, "'Array comprehension' must have two operands");
 }
 
-/// \brief Cast an exprt to a \ref lambda_exprt
+/// \brief Cast an exprt to a \ref array_comprehension_exprt
 ///
-/// \a expr must be known to be \ref lambda_exprt.
+/// \a expr must be known to be \ref array_comprehension_exprt.
 ///
 /// \param expr: Source expression
-/// \return Object of type \ref lambda_exprt
-inline const lambda_exprt &to_lambda_expr(const exprt &expr)
+/// \return Object of type \ref array_comprehension_exprt
+inline const array_comprehension_exprt &
+to_array_comprehension_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_lambda);
-  const lambda_exprt &ret = static_cast<const lambda_exprt &>(expr);
+  const array_comprehension_exprt &ret =
+    static_cast<const array_comprehension_exprt &>(expr);
   validate_expr(ret);
   return ret;
 }
 
-/// \copydoc to_lambda_expr(const exprt &)
-inline lambda_exprt &to_lambda_expr(exprt &expr)
+/// \copydoc to_array_comprehension_expr(const exprt &)
+inline array_comprehension_exprt &to_array_comprehension_expr(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_lambda);
-  lambda_exprt &ret = static_cast<lambda_exprt &>(expr);
+  array_comprehension_exprt &ret =
+    static_cast<array_comprehension_exprt &>(expr);
   validate_expr(ret);
   return ret;
 }