From 9bbd8b190ab81218c2f0c946d3082d500dbadca6 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 22 May 2019 15:14:39 +0100 Subject: [PATCH 1/2] Move import line --- src/solvers/strings/string_refinement.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 7f69b14b3a1..917ac67cd6b 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -18,7 +18,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com /// Ghosh. #include "string_refinement.h" -#include "string_constraint_instantiation.h" #include #include @@ -30,6 +29,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include +#include "string_constraint_instantiation.h" + static bool is_valid_string_constraint( messaget::mstreamt &stream, const namespacet &ns, From 8e9f6bdf8362e5c8783415ac780b4e0c4ea386b0 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 22 May 2019 15:15:48 +0100 Subject: [PATCH 2/2] Extract equation_symbol_mapping to its own files Because we can. --- src/solvers/Makefile | 1 + .../strings/equation_symbol_mapping.cpp | 27 ++++++++++++ src/solvers/strings/equation_symbol_mapping.h | 43 +++++++++++++++++++ src/solvers/strings/string_refinement.cpp | 1 + .../strings/string_refinement_util.cpp | 18 -------- src/solvers/strings/string_refinement_util.h | 26 ----------- 6 files changed, 72 insertions(+), 44 deletions(-) create mode 100644 src/solvers/strings/equation_symbol_mapping.cpp create mode 100644 src/solvers/strings/equation_symbol_mapping.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 9fbafd0b4ac..02fc6453e16 100644 --- a/src/solvers/Makefile +++ b/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 \ diff --git a/src/solvers/strings/equation_symbol_mapping.cpp b/src/solvers/strings/equation_symbol_mapping.cpp new file mode 100644 index 00000000000..9f72a64d604 --- /dev/null +++ b/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 +equation_symbol_mappingt::find_expressions(const std::size_t i) +{ + return strings_in_equation[i]; +} + +std::vector +equation_symbol_mappingt::find_equations(const exprt &expr) +{ + return equations_containing[expr]; +} diff --git a/src/solvers/strings/equation_symbol_mapping.h b/src/solvers/strings/equation_symbol_mapping.h new file mode 100644 index 00000000000..55e8c15e86f --- /dev/null +++ b/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 +#include + +#include + +/// 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 find_expressions(const std::size_t i); + + /// \param expr: an expression + /// \return vector of equations containing the given expression `expr` + std::vector find_equations(const exprt &expr); + +private: + /// Record index of the equations that contain a given expression + std::map> equations_containing; + /// Record expressions that are contained in the equation with the given index + std::unordered_map> strings_in_equation; +}; + +#endif // CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 917ac67cd6b..fd2db24e300 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -29,6 +29,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include +#include "equation_symbol_mapping.h" #include "string_constraint_instantiation.h" static bool is_valid_string_constraint( diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp index e05b909e44b..e0d366b6d41 100644 --- a/src/solvers/strings/string_refinement_util.cpp +++ b/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 -equation_symbol_mappingt::find_expressions(const std::size_t i) -{ - return strings_in_equation[i]; -} - -std::vector -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 to_string_builtin_function( diff --git a/src/solvers/strings/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h index 89cf37d81b5..678ebc34a99 100644 --- a/src/solvers/strings/string_refinement_util.h +++ b/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 find_expressions(const std::size_t i); - - /// \param expr: an expression - /// \return vector of equations containing the given expression `expr` - std::vector find_equations(const exprt &expr); - -private: - /// Record index of the equations that contain a given expression - std::map> equations_containing; - /// Record expressions that are contained in the equation with the given index - std::unordered_map> 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.