Added SMT encoding of array_comprehension_exprt

Z3 treats arrays and lambdas as identical, so we can exploit that in the
translation of `array_comprehension_exprt`. For other solvers, we would
fall back to a universally quantified expression to initialize the array.

Author: SaswatPadhi

regression/cbmc/byte_update15/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

src/solvers/smt2/smt2_conv.cpp

@@ -56,6 +56,7 @@ smt2_convt::smt2_convt(
   : use_FPA_theory(false),
     use_datatypes(false),
     use_array_of_bool(false),
+    use_lambda_for_array(false),
     emit_set_logic(true),
     ns(_ns),
     out(_out),
@@ -97,6 +98,7 @@ smt2_convt::smt2_convt(
 
   case solvert::Z3:
     use_array_of_bool = true;
+    use_lambda_for_array = true;
     emit_set_logic = false;
     use_datatypes = true;
     break;
@@ -1289,6 +1291,31 @@ void smt2_convt::convert_expr(const exprt &expr)
     CHECK_RETURN(it != defined_expressions.end());
     out << it->second;
   }
+  else if(expr.id() == ID_array_comprehension)
+  {
+    const auto &array_comprehension = to_array_comprehension_expr(expr);
+
+    DATA_INVARIANT(
+      array_comprehension.type().id() == ID_array,
+      "array_comprehension expression shall have array type");
+
+    if(use_lambda_for_array)
+    {
+      out << "(lambda ((";
+      convert_expr(array_comprehension.arg());
+      out << " ";
+      convert_type(array_comprehension.type().size().type());
+      out << ")) ";
+      convert_expr(array_comprehension.body());
+      out << ")";
+    }
+    else
+    {
+      const auto &it = defined_expressions.find(array_comprehension);
+      CHECK_RETURN(it != defined_expressions.end());
+      out << it->second;
+    }
+  }
   else if(expr.id()==ID_index)
   {
     convert_index(to_index_expr(expr));
@@ -4390,6 +4417,35 @@ void smt2_convt::find_symbols(const exprt &expr)
       defined_expressions[expr]=id;
     }
   }
+  else if(expr.id() == ID_array_comprehension)
+  {
+    if(!use_lambda_for_array)
+    {
+      if(defined_expressions.find(expr) == defined_expressions.end())
+      {
+        const auto &array_comprehension = to_array_comprehension_expr(expr);
+
+        const irep_idt id =
+          "array_comprehension." + std::to_string(defined_expressions.size());
+        out << "(declare-fun " << id << " () ";
+        convert_type(array_comprehension.type());
+        out << ")\n";
+
+        out << "; the following is a substitute for lambda i . x(i)\n";
+        out << "(assert (forall ((";
+        convert_expr(array_comprehension.arg());
+        out << " ";
+        convert_type(array_comprehension.type().size().type());
+        out << ")) (= (select " << id << " ";
+        convert_expr(array_comprehension.arg());
+        out << ") ";
+        convert_expr(array_comprehension.body());
+        out << ")))\n";
+
+        defined_expressions[expr] = id;
+      }
+    }
+  }
   else if(expr.id()==ID_array)
   {
     if(defined_expressions.find(expr)==defined_expressions.end())

src/solvers/smt2/smt2_conv.h

@@ -61,6 +61,7 @@ class smt2_convt : public stack_decision_proceduret
   bool use_FPA_theory;
   bool use_datatypes;
   bool use_array_of_bool;
+  bool use_lambda_for_array;
   bool emit_set_logic;
 
   exprt handle(const exprt &expr) override;