Create string_refinement_util for utility function

string_refinement.cpp file is becoming too large.
This groups utility classes used by string_refinement in new files to
reduce string_refinement.cpp a bit.

Author: romainbrenguier

src/solvers/Makefile

@@ -179,6 +179,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       refinement/string_refinement.cpp \
+      refinement/string_refinement_util.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \
       refinement/string_constraint_generator_concat.cpp \

src/solvers/refinement/string_refinement.cpp

@@ -488,35 +488,6 @@ static union_find_replacet generate_symbol_resolution_from_equations(
   return solver;
 }
 
-/// Maps equation to expressions contained in them and conversely expressions to
-/// equations that contain them. This can be used on a subset of expressions
-/// which interests us, in particular strings. Equations are identified by an
-/// index of type `std::size_t` for more efficient insertion and lookup.
-class equation_symbol_mappingt
-{
-public:
-  // Record index of the equations that contain a given expression
-  std::map<exprt, std::vector<std::size_t>> equations_containing;
-  // Record expressions that are contained in the equation with the given index
-  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
-
-  void add(const std::size_t i, const exprt &expr)
-  {
-    equations_containing[expr].push_back(i);
-    strings_in_equation[i].push_back(expr);
-  }
-
-  std::vector<exprt> find_expressions(const std::size_t i)
-  {
-    return strings_in_equation[i];
-  }
-
-  std::vector<std::size_t> find_equations(const exprt &expr)
-  {
-    return equations_containing[expr];
-  }
-};
-
 /// This is meant to be used on the lhs of an equation with string subtype.
 /// \param lhs: expression which is either of string type, or a symbol
 ///   representing a struct with some string members
@@ -1219,68 +1190,6 @@ void debug_model(
   stream << messaget::eom;
 }
 
-sparse_arrayt::sparse_arrayt(const with_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());
-    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();
-}
-
-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 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);
-      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:

src/solvers/refinement/string_refinement.h

@@ -27,57 +27,11 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/refinement/string_constraint.h>
 #include <solvers/refinement/string_constraint_generator.h>
 #include <solvers/refinement/string_refinement_invariant.h>
+#include <solvers/refinement/string_refinement_util.h>
 
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 #define CHARACTER_FOR_UNKNOWN '?'
 
-struct index_set_pairt
-{
-  std::map<exprt, std::set<exprt>> cumulative;
-  std::map<exprt, std::set<exprt>> current;
-};
-
-struct string_axiomst
-{
-  std::vector<string_constraintt> universal;
-  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:

src/solvers/refinement/string_refinement_util.cpp

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ Module: String solver
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <algorithm>
+#include <numeric>
+#include <util/arith_tools.h>
+#include <util/std_expr.h>
+#include "string_refinement_util.h"
+
+sparse_arrayt::sparse_arrayt(const with_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());
+    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();
+}
+
+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 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);
+      return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
+    });
+}

src/solvers/refinement/string_refinement_util.h

@@ -0,0 +1,90 @@
+/*******************************************************************\
+
+ Module: String solver
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
+#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
+
+#include "string_constraint.h"
+
+struct index_set_pairt
+{
+  std::map<exprt, std::set<exprt>> cumulative;
+  std::map<exprt, std::set<exprt>> current;
+};
+
+struct string_axiomst
+{
+  std::vector<string_constraintt> universal;
+  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;
+};
+
+/// Maps equation to expressions contained in them and conversely expressions to
+/// equations that contain them. This can be used on a subset of expressions
+/// which interests us, in particular strings. Equations are identified by an
+/// index of type `std::size_t` for more efficient insertion and lookup.
+class equation_symbol_mappingt
+{
+public:
+  // Record index of the equations that contain a given expression
+  std::map<exprt, std::vector<std::size_t>> equations_containing;
+  // Record expressions that are contained in the equation with the given index
+  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
+
+  void add(const std::size_t i, const exprt &expr)
+  {
+    equations_containing[expr].push_back(i);
+    strings_in_equation[i].push_back(expr);
+  }
+
+  std::vector<exprt> find_expressions(const std::size_t i)
+  {
+    return strings_in_equation[i];
+  }
+
+  std::vector<std::size_t> find_equations(const exprt &expr)
+  {
+    return equations_containing[expr];
+  }
+};
+
+#endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H