Class for sparse arrays representations

The string solver is implicitely interpreting the array in the result of
the underlying solver as "sparse-arrays" where only the values at some
meaningful indexes are given.

The classes sparse_arrayt and interval_sparse_arrayt make the way we
interpret these results more explicit.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -20,6 +20,7 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/refinement/string_refinement.h>
 
 #include <iomanip>
+#include <numeric>
 #include <stack>
 #include <util/expr_iterator.h>
 #include <util/arith_tools.h>
@@ -1221,62 +1222,87 @@ void debug_model(
   stream << messaget::eom;
 }
 
-/// Create a new expression where 'with' expressions on arrays are replaced by
-/// 'if' expressions. e.g. for an array access arr[index], where: `arr :=
-/// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be:
-/// `index==0 ? 24 : index==2 ? 42 : 12`
-/// If `left_propagate` is set to true, the expression will look like
-/// `index<=0 ? 24 : index<=2 ? 42 : 12`
-/// \param expr: A (possibly nested) 'with' expression on an `array_of`
-///   expression. The function checks that the expression is of the form
-///   `with_expr(with_expr(...(array_of(...)))`. This is the form in which
-///   array valuations coming from the underlying solver are given.
-/// \param index: An index with which to build the equality condition
-/// \return An expression containing no 'with' expression
-static exprt substitute_array_access(
-  const with_exprt &expr,
-  const exprt &index,
-  const bool left_propagate)
+sparse_arrayt::sparse_arrayt(const with_exprt &expr)
 {
-  std::vector<std::pair<std::size_t, exprt>> entries;
-  std::reference_wrapper<const exprt> ref =
-    std::ref(static_cast<const exprt &>(expr));
+  auto ref = std::ref(static_cast<const exprt &>(expr));
   while(can_cast_expr<with_exprt>(ref.get()))
   {
     const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
-    auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
-    entries.push_back(std::make_pair(current_index, with_expr.new_value()));
+    const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
+    entries.emplace_back(current_index, with_expr.new_value());
     ref = with_expr.old();
   }
 
   // This function only handles 'with' and 'array_of' expressions
   PRECONDITION(ref.get().id() == ID_array_of);
+  default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
+}
 
-  // sort entries by increasing index
+exprt sparse_arrayt::to_if_expression(const exprt &index) const
+{
+  return std::accumulate(
+    entries.begin(),
+    entries.end(),
+    default_value,
+    [&](
+      const exprt if_expr,
+      const std::pair<std::size_t, exprt> &entry) { // NOLINT
+      const exprt entry_index = from_integer(entry.first, index.type());
+      const exprt &then_expr = entry.second;
+      CHECK_RETURN(then_expr.type() == if_expr.type());
+      const equal_exprt index_equal(index, entry_index);
+      return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
+    });
+}
+
+interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
+  : sparse_arrayt(expr)
+{
+  // Entries are sorted so that successive entries correspond to intervals
   std::sort(
     entries.begin(),
     entries.end(),
     [](
       const std::pair<std::size_t, exprt> &a,
       const std::pair<std::size_t, exprt> &b) { return a.first < b.first; });
+}
 
-  exprt result = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
-  for(const auto &entry : entries)
-  {
-    const exprt &then_expr = entry.second;
-    const typet &type = then_expr.type();
-    CHECK_RETURN(type == result.type());
-    const exprt entry_index = from_integer(entry.first, index.type());
-    if(left_propagate)
-    {
+exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
+{
+  return std::accumulate(
+    entries.rbegin(),
+    entries.rend(),
+    default_value,
+    [&](
+      const exprt if_expr,
+      const std::pair<std::size_t, exprt> &entry) { // NOLINT
+      const exprt entry_index = from_integer(entry.first, index.type());
+      const exprt &then_expr = entry.second;
+      CHECK_RETURN(then_expr.type() == if_expr.type());
       const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
-      result = if_exprt(index_small_eq, then_expr, result, type);
-    }
-    else
-      result =
-        if_exprt(equal_exprt(index, entry_index), then_expr, result, type);
-  }
-  return result;
+      return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
+    });
+}
+
+/// Create a new expression where 'with' expressions on arrays are replaced by
+/// 'if' expressions. e.g. for an array access arr[index], where: `arr :=
+/// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be:
+/// `index==0 ? 24 : index==2 ? 42 : 12`
+/// If `left_propagate` is set to true, the expression will look like
+/// `index<=0 ? 24 : index<=2 ? 42 : 12`
+/// \param expr: A (possibly nested) 'with' expression on an `array_of`
+///   expression. The function checks that the expression is of the form
+///   `with_expr(with_expr(...(array_of(...)))`. This is the form in which
+///   array valuations coming from the underlying solver are given.
+/// \param index: An index with which to build the equality condition
+/// \return An expression containing no 'with' expression
+static exprt substitute_array_access(
+  const with_exprt &expr,
+  const exprt &index,
+  const bool left_propagate)
+{
+  return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
+                        : sparse_arrayt(expr).to_if_expression(index);
 }
 
 /// Fill an array represented by a list of with_expr by propagating values to

src/solvers/refinement/string_refinement.h

@@ -43,6 +43,41 @@ struct string_axiomst
   std::vector<string_not_contains_constraintt> not_contains;
 };
 
+/// Represents arrays of the form `array_of(x) with {i:=a} with {j:=b} ...`
+/// by a default value `x` and a list of entries `(i,a)`, `(j,b)` etc.
+class sparse_arrayt
+{
+public:
+  /// Initialize a sparse array from an expression of the form
+  /// `array_of(x) with {i:=a} with {j:=b} ...`
+  /// This is the form in which array valuations coming from the underlying
+  /// solver are given.
+  explicit sparse_arrayt(const with_exprt &expr);
+
+  /// Creates an if_expr corresponding to the result of accessing the array
+  /// at the given index
+  virtual exprt to_if_expression(const exprt &index) const;
+
+protected:
+  exprt default_value;
+  std::vector<std::pair<std::size_t, exprt>> entries;
+};
+
+/// Represents arrays by the indexes up to which the value remains the same.
+/// For instance `{'a', 'a', 'a', 'b', 'b', 'c'}` would be represented by
+/// by ('a', 2) ; ('b', 4), ('c', 5).
+/// This is particularly useful when the array is constant on intervals.
+class interval_sparse_arrayt final : public sparse_arrayt
+{
+public:
+  /// An expression of the form `array_of(x) with {i:=a} with {j:=b}` is
+  /// converted to an array `arr` where for all index `k` smaller than `i`,
+  /// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`
+  /// and for the others it is `x`.
+  explicit interval_sparse_arrayt(const with_exprt &expr);
+  exprt to_if_expression(const exprt &index) const override;
+};
+
 class string_refinementt final: public bv_refinementt
 {
 private: