Added SMT encoding of array_comprehension_exprt

Author: SaswatPadhi

regression/cbmc/byte_update15/test.desc

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

src/solvers/smt2/smt2_conv.cpp

@@ -1289,6 +1289,19 @@ 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");
+
+    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 +4403,27 @@ void smt2_convt::find_symbols(const exprt &expr)
       defined_expressions[expr]=id;
     }
   }
+  else if(expr.id() == ID_array_comprehension)
+  {
+    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 << "(define-fun " << id << " () ";
+      convert_type(array_comprehension.type());
+      out << " (lambda ((";
+      convert_expr(array_comprehension.arg());
+      out << " ";
+      convert_type(array_comprehension.type().size().type());
+      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())