Merge pull request #5973 from padhi-aws-forks/smt2_array_comprehension

Fix SMT encoding of `array_comprehension_exprt`

Author: SaswatPadhi

regression/cbmc/byte_update15/test.desc

@@ -1,8 +1,11 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test currently does not pass with CPROVER SMT2 backend
+because the solver does not fully support quantified expressions.

src/solvers/smt2/smt2_conv.cpp

@@ -57,6 +57,7 @@ smt2_convt::smt2_convt(
     use_as_const(false),
     use_datatypes(false),
     use_array_of_bool(false),
+    use_lambda_for_array(false),
     emit_set_logic(true),
     ns(_ns),
     out(_out),
@@ -101,6 +102,7 @@ smt2_convt::smt2_convt(
   case solvert::Z3:
     use_as_const = true;
     use_array_of_bool = true;
+    use_lambda_for_array = true;
     emit_set_logic = false;
     use_datatypes = true;
     break;
@@ -1304,6 +1306,31 @@ void smt2_convt::convert_expr(const exprt &expr)
       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));
@@ -4408,6 +4435,44 @@ void smt2_convt::find_symbols(const exprt &expr)
       }
     }
   }
+  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 auto &array_size = array_comprehension.type().size();
+
+        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 << "; universally quantified initialization of the array\n";
+        out << "(assert (forall ((";
+        convert_expr(array_comprehension.arg());
+        out << " ";
+        convert_type(array_size.type());
+        out << ")) (=> (and (bvule (_ bv0 " << boolbv_width(array_size.type())
+            << ") ";
+        convert_expr(array_comprehension.arg());
+        out << ") (bvult ";
+        convert_expr(array_comprehension.arg());
+        out << " ";
+        convert_expr(array_size);
+        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

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