Merge pull request #8400 from tautschnig/bugfixes/smt2-8399

SMT2 back-end: fix inconsistent array flattening

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/json.h>
 #include <util/message.h>
 #include <util/replace_expr.h>
+#include <util/replace_symbol.h>
 #include <util/std_expr.h>
 
 #include <solvers/prop/literal_expr.h>
@@ -237,6 +238,11 @@ void arrayst::collect_arrays(const exprt &a)
   else if(a.id() == ID_array_comprehension)
   {
   }
+  else if(auto let_expr = expr_try_dynamic_cast<let_exprt>(a))
+  {
+    arrays.make_union(a, let_expr->where());
+    collect_arrays(let_expr->where());
+  }
   else
   {
     DATA_INVARIANT(
@@ -528,6 +534,33 @@ void arrayst::add_array_constraints(
   else if(expr.id()==ID_index)
   {
   }
+  else if(auto let_expr = expr_try_dynamic_cast<let_exprt>(expr))
+  {
+    // we got x=let(a=e, A)
+    // add x[i]=A[a/e][i]
+
+    exprt where = let_expr->where();
+    replace_symbolt replace_symbol;
+    for(const auto &binding :
+        make_range(let_expr->variables()).zip(let_expr->values()))
+    {
+      replace_symbol.insert(binding.first, binding.second);
+    }
+    replace_symbol(where);
+
+    for(const auto &index : index_set)
+    {
+      index_exprt index_expr{expr, index};
+      index_exprt where_indexed{where, index};
+
+      // add constraint
+      lazy_constraintt lazy{
+        lazy_typet::ARRAY_LET, equal_exprt{index_expr, where_indexed}};
+
+      add_array_constraint(lazy, false); // added immediately
+      array_constraint_count[constraint_typet::ARRAY_LET]++;
+    }
+  }
   else
   {
     DATA_INVARIANT(
@@ -875,6 +908,8 @@ std::string arrayst::enum_to_string(constraint_typet type)
     return "arrayComprehension";
   case constraint_typet::ARRAY_EQUALITY:
     return "arrayEquality";
+  case constraint_typet::ARRAY_LET:
+    return "arrayLet";
   default:
     UNREACHABLE;
   }

src/solvers/flattening/arrays.h

@@ -93,7 +93,8 @@ class arrayst:public equalityt
     ARRAY_OF,
     ARRAY_TYPECAST,
     ARRAY_CONSTANT,
-    ARRAY_COMPREHENSION
+    ARRAY_COMPREHENSION,
+    ARRAY_LET
   };
 
   struct lazy_constraintt
@@ -124,7 +125,8 @@ class arrayst:public equalityt
     ARRAY_TYPECAST,
     ARRAY_CONSTANT,
     ARRAY_COMPREHENSION,
-    ARRAY_EQUALITY
+    ARRAY_EQUALITY,
+    ARRAY_LET
   };
 
   typedef std::map<constraint_typet, size_t> array_constraint_countt;

src/solvers/smt2/smt2_conv.cpp

@@ -4445,15 +4445,22 @@ void smt2_convt::convert_member(const member_exprt &expr)
     CHECK_RETURN_WITH_DIAGNOSTICS(
       width != 0, "failed to get union member width");
 
-    unflatten(wheret::BEGIN, expr.type());
+    if(use_datatypes)
+    {
+      unflatten(wheret::BEGIN, expr.type());
 
-    out << "((_ extract "
-           << (width-1)
-           << " 0) ";
-    convert_expr(struct_op);
-    out << ")";
+      out << "((_ extract " << (width - 1) << " 0) ";
+      convert_expr(struct_op);
+      out << ")";
 
-    unflatten(wheret::END, expr.type());
+      unflatten(wheret::END, expr.type());
+    }
+    else
+    {
+      out << "((_ extract " << (width - 1) << " 0) ";
+      convert_expr(struct_op);
+      out << ")";
+    }
   }
   else
     UNEXPECTEDCASE(
@@ -4565,57 +4572,50 @@ void smt2_convt::unflatten(
   }
   else if(type.id() == ID_array)
   {
-    if(use_datatypes)
+    PRECONDITION(use_as_const);
+
+    if(where == wheret::BEGIN)
+      out << "(let ((?ufop" << nesting << " ";
+    else
     {
-      PRECONDITION(use_as_const);
+      out << ")) ";
 
-      if(where == wheret::BEGIN)
-        out << "(let ((?ufop" << nesting << " ";
-      else
-      {
-        out << ")) ";
+      const array_typet &array_type = to_array_type(type);
 
-        const array_typet &array_type = to_array_type(type);
+      std::size_t subtype_width = boolbv_width(array_type.element_type());
 
-        std::size_t subtype_width = boolbv_width(array_type.element_type());
+      DATA_INVARIANT(
+        array_type.size().is_constant(),
+        "cannot unflatten arrays of non-constant size");
+      mp_integer size =
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
-        DATA_INVARIANT(
-          array_type.size().is_constant(),
-          "cannot unflatten arrays of non-constant size");
-        mp_integer size =
-          numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+      for(mp_integer i = 1; i < size; ++i)
+        out << "(store ";
 
-        for(mp_integer i = 1; i < size; ++i)
-          out << "(store ";
+      out << "((as const ";
+      convert_type(array_type);
+      out << ") ";
+      // use element at index 0 as default value
+      unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
+      out << "((_ extract " << subtype_width - 1 << " "
+          << "0) ?ufop" << nesting << ")";
+      unflatten(wheret::END, array_type.element_type(), nesting + 1);
+      out << ") ";
 
-        out << "((as const ";
-        convert_type(array_type);
-        out << ") ";
-        // use element at index 0 as default value
+      std::size_t offset = subtype_width;
+      for(mp_integer i = 1; i < size; ++i, offset += subtype_width)
+      {
+        convert_expr(from_integer(i, array_type.index_type()));
+        out << ' ';
         unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
-        out << "((_ extract " << subtype_width - 1 << " "
-            << "0) ?ufop" << nesting << ")";
+        out << "((_ extract " << offset + subtype_width - 1 << " " << offset
+            << ") ?ufop" << nesting << ")";
         unflatten(wheret::END, array_type.element_type(), nesting + 1);
-        out << ") ";
-
-        std::size_t offset = subtype_width;
-        for(mp_integer i = 1; i < size; ++i, offset += subtype_width)
-        {
-          convert_expr(from_integer(i, array_type.index_type()));
-          out << ' ';
-          unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1);
-          out << "((_ extract " << offset + subtype_width - 1 << " " << offset
-              << ") ?ufop" << nesting << ")";
-          unflatten(wheret::END, array_type.element_type(), nesting + 1);
-          out << ")"; // store
-        }
-
-        out << ")"; // let
+        out << ")"; // store
       }
-    }
-    else
-    {
-      // nop, already a bv
+
+      out << ")"; // let
     }
   }
   else if(type.id() == ID_struct || type.id() == ID_struct_tag)
@@ -4767,19 +4767,22 @@ void smt2_convt::set_to(const exprt &expr, bool value)
         {
           out << "(define-fun " << smt2_identifier;
           out << " () ";
+          convert_type(equal_expr.lhs().type());
+          out << ' ';
           if(
             equal_expr.lhs().type().id() != ID_array ||
             use_array_theory(prepared_rhs))
           {
-            convert_type(equal_expr.lhs().type());
+            convert_expr(prepared_rhs);
           }
           else
           {
-            std::size_t width = boolbv_width(equal_expr.lhs().type());
-            out << "(_ BitVec " << width << ")";
+            unflatten(wheret::BEGIN, equal_expr.lhs().type());
+
+            convert_expr(prepared_rhs);
+
+            unflatten(wheret::END, equal_expr.lhs().type());
           }
-          out << ' ';
-          convert_expr(prepared_rhs);
           out << ')' << '\n';
         }