Extract equation_symbol_mapping to its own files

src/solvers/Makefile

@@ -160,6 +160,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       strings/array_pool.cpp \
+      strings/equation_symbol_mapping.cpp \
       strings/string_builtin_function.cpp \
       strings/string_refinement.cpp \
       strings/string_refinement_util.cpp \

src/solvers/strings/equation_symbol_mapping.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: String solver
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "equation_symbol_mapping.h"
+
+void equation_symbol_mappingt::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>
+equation_symbol_mappingt::find_expressions(const std::size_t i)
+{
+  return strings_in_equation[i];
+}
+
+std::vector<std::size_t>
+equation_symbol_mappingt::find_equations(const exprt &expr)
+{
+  return equations_containing[expr];
+}

src/solvers/strings/equation_symbol_mapping.h

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: String solver
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
+#define CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
+
+#include <map>
+#include <unordered_map>
+
+#include <util/expr.h>
+
+/// 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 the fact that equation `i` contains expression `expr`
+  void add(const std::size_t i, const exprt &expr);
+
+  /// \param i: index corresponding to an equation
+  /// \return vector of expressions contained in the equation with the given
+  ///   index `i`
+  std::vector<exprt> find_expressions(const std::size_t i);
+
+  /// \param expr: an expression
+  /// \return vector of equations containing the given expression `expr`
+  std::vector<std::size_t> find_equations(const exprt &expr);
+
+private:
+  /// 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;
+};
+
+#endif // CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H

src/solvers/strings/string_refinement.cpp

@@ -18,7 +18,6 @@ Author: Alberto Griggio, [email protected]
 ///   Ghosh.
 
 #include "string_refinement.h"
-#include "string_constraint_instantiation.h"
 
 #include <iomanip>
 #include <numeric>
@@ -30,6 +29,9 @@ Author: Alberto Griggio, [email protected]
 #include <util/magic.h>
 #include <util/simplify_expr.h>
 
+#include "equation_symbol_mapping.h"
+#include "string_constraint_instantiation.h"
+
 static bool is_valid_string_constraint(
   messaget::mstreamt &stream,
   const namespacet &ns,

src/solvers/strings/string_refinement_util.cpp

@@ -183,24 +183,6 @@ array_exprt interval_sparse_arrayt::concretize(
   return array;
 }
 
-void equation_symbol_mappingt::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>
-equation_symbol_mappingt::find_expressions(const std::size_t i)
-{
-  return strings_in_equation[i];
-}
-
-std::vector<std::size_t>
-equation_symbol_mappingt::find_equations(const exprt &expr)
-{
-  return equations_containing[expr];
-}
-
 /// Construct a string_builtin_functiont object from a function application
 /// \return a unique pointer to the created object
 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(

src/solvers/strings/string_refinement_util.h

@@ -132,32 +132,6 @@ class interval_sparse_arrayt final : public sparse_arrayt
   }
 };
 
-/// 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 the fact that equation `i` contains expression `expr`
-  void add(const std::size_t i, const exprt &expr);
-
-  /// \param i: index corresponding to an equation
-  /// \return vector of expressions contained in the equation with the given
-  ///   index `i`
-  std::vector<exprt> find_expressions(const std::size_t i);
-
-  /// \param expr: an expression
-  /// \return vector of equations containing the given expression `expr`
-  std::vector<std::size_t> find_equations(const exprt &expr);
-
-private:
-  /// 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;
-};
-
 /// Keep track of dependencies between strings.
 /// Each string points to the builtin_function calls on which it depends.
 /// Each builtin_function points to the strings on which the result depends.