Fixed SMT encoding of array_of_exprt

Instead of using quantifers to encode array_of expressions -- which, as indicated in the comments, doesn't seem to work on existing solvers -- we can use the `as const` construct for CVC4 and Z3.

Author: SaswatPadhi

src/solvers/smt2/smt2_conv.cpp

@@ -53,7 +53,8 @@ smt2_convt::smt2_convt(
   const std::string &_logic,
   solvert _solver,
   std::ostream &_out)
-  : use_FPA_theory(false),
+  : use_as_const(false),
+    use_FPA_theory(false),
     use_datatypes(false),
     use_array_of_bool(false),
     emit_set_logic(true),
@@ -87,6 +88,7 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::CVC4:
+    use_as_const = true;
     break;
 
   case solvert::MATHSAT:
@@ -96,6 +98,7 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::Z3:
+    use_as_const = true;
     use_array_of_bool = true;
     emit_set_logic = false;
     use_datatypes = true;
@@ -1276,18 +1279,29 @@ void smt2_convt::convert_expr(const exprt &expr)
     convert_address_of_rec(
       address_of_expr.object(), to_pointer_type(address_of_expr.type()));
   }
-  else if(expr.id()==ID_array_of)
+  else if(expr.id() == ID_array_of)
   {
-    const array_of_exprt &array_of_expr = to_array_of_expr(expr);
+    const auto &array_of_expr = to_array_of_expr(expr);
 
     DATA_INVARIANT(
       array_of_expr.type().id() == ID_array,
       "array of expression shall have array type");
 
-    defined_expressionst::const_iterator it =
-      defined_expressions.find(array_of_expr);
-    CHECK_RETURN(it != defined_expressions.end());
-    out << it->second;
+    if(use_as_const)
+    {
+      out << "((as const ";
+      convert_type(array_of_expr.type());
+      out << ") ";
+      convert_expr(array_of_expr.what());
+      out << ")";
+    }
+    else
+    {
+      defined_expressionst::const_iterator it =
+        defined_expressions.find(array_of_expr);
+      CHECK_RETURN(it != defined_expressions.end());
+      out << it->second;
+    }
   }
   else if(expr.id()==ID_index)
   {
@@ -4367,27 +4381,31 @@ void smt2_convt::find_symbols(const exprt &expr)
       out << ")" << "\n";
     }
   }
-  else if(expr.id()==ID_array_of)
+  else if(expr.id() == ID_array_of)
   {
-    if(defined_expressions.find(expr)==defined_expressions.end())
+    if(!use_as_const)
     {
-      const irep_idt id =
-        "array_of." + std::to_string(defined_expressions.size());
-      out << "; the following is a substitute for lambda i. x" << "\n";
-      out << "(declare-fun " << id << " () ";
-      convert_type(expr.type());
-      out << ")" << "\n";
-
-      // use a quantifier instead of the lambda
-      #if 0 // not really working in any solver yet!
-      out << "(assert (forall ((i ";
-      convert_type(array_index_type());
-      out << ")) (= (select " << id << " i) ";
-      convert_expr(expr.op0());
-      out << ")))" << "\n";
-      #endif
+      if(defined_expressions.find(expr) == defined_expressions.end())
+      {
+        const auto &array_of = to_array_of_expr(expr);
 
-      defined_expressions[expr]=id;
+        const irep_idt id =
+          "array_of." + std::to_string(defined_expressions.size());
+        out << "; the following is a substitute for lambda i. x\n";
+        out << "(declare-fun " << id << " () ";
+        convert_type(array_of.type());
+        out << ")\n";
+
+        // use a quantifier instead of the lambda
+        // may not work with existing solver, but is a sound translation
+        out << "(assert (forall ((i ";
+        convert_type(array_of.type().size().type());
+        out << ")) (= (select " << id << " i) ";
+        convert_expr(array_of.what());
+        out << ")))\n";
+
+        defined_expressions[expr] = id;
+      }
     }
   }
   else if(expr.id()==ID_array)

src/solvers/smt2/smt2_conv.h

@@ -58,6 +58,7 @@ class smt2_convt : public stack_decision_proceduret
 
   ~smt2_convt() override = default;
 
+  bool use_as_const;
   bool use_FPA_theory;
   bool use_datatypes;
   bool use_array_of_bool;