move string solver into directory of its own

Daniel Kroening · svorenova · commit 39a03aad7e17 · 2019-01-21T15:21:51.000Z
The string solver is now large enough to justify a separate directory.
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -28,7 +28,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
 
-#include <solvers/refinement/string_refinement.h>
+#include <goto-symex/path_storage.h>
+
+#include <solvers/strings/string_refinement.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
@@ -11,4 +11,5 @@ langapi # should go away
 linking
 pointer-analysis
 solvers/refinement
+solvers/strings
 util
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
@@ -54,9 +54,9 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_virtual_functions/virtual_functions.cpp \
        java_bytecode/load_method_by_regex.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \
-       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
-       solvers/refinement/string_refinement/dependency_graph.cpp \
-       solvers/refinement/string_refinement/string_symbol_resolution.cpp \
+       solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \
+       solvers/strings/string_refinement/dependency_graph.cpp \
+       solvers/strings/string_refinement/string_symbol_resolution.cpp \
        util/expr_iterator.cpp \
        util/has_subtype.cpp \
        util/parameter_indices.cpp \
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -15,7 +15,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 #include <langapi/mode.h>
 #include <langapi/language_util.h>
 
-#include <solvers/refinement/string_constraint_instantiation.h>
+#include <solvers/strings/string_constraint_instantiation.h>
 #include <solvers/sat/satcheck.h>
 
 #include <util/simplify_expr.h>
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt b/jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt
@@ -2,6 +2,7 @@ java_bytecode
 langapi # should go away
 solvers/refinement
 solvers/sat
+solvers/strings
 string_constraint_instantiation
 testing-utils
 util
diff --git a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp
@@ -13,7 +13,7 @@ Author: Diffblue Ltd.
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <java_bytecode/java_types.h>
-#include <solvers/refinement/string_refinement_util.h>
+#include <solvers/strings/string_refinement_util.h>
 
 #ifdef DEBUG
 #include <iostream>
diff --git a/jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt b/jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt
@@ -2,5 +2,6 @@ java_bytecode
 langapi # should go away
 string_refinement
 solvers/refinement
+solvers/strings
 testing-utils
 util
diff --git a/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp
@@ -9,10 +9,11 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/catch.hpp>
 
+#include <solvers/strings/string_refinement.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_expr.h>
-#include <solvers/refinement/string_refinement.h>
 #include <util/symbol_table.h>
 #include <langapi/mode.h>
 #include <java_bytecode/java_bytecode_language.h>
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_trace.h>
 
-#include <solvers/refinement/string_refinement.h>
+#include <solvers/strings/string_refinement.h>
 
 #include "bmc.h"
 #include "xml_interface.h"
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
@@ -28,7 +28,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 #include <solvers/refinement/bv_refinement.h>
-#include <solvers/refinement/string_refinement.h>
+#include <solvers/strings/string_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/satcheck.h>
 
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -161,23 +161,23 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/bv_refinement_loop.cpp \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
-      refinement/string_builtin_function.cpp \
-      refinement/string_refinement.cpp \
-      refinement/string_refinement_util.cpp \
-      refinement/string_constraint.cpp \
-      refinement/string_constraint_generator_code_points.cpp \
-      refinement/string_constraint_generator_comparison.cpp \
-      refinement/string_constraint_generator_concat.cpp \
-      refinement/string_constraint_generator_constants.cpp \
-      refinement/string_constraint_generator_indexof.cpp \
-      refinement/string_constraint_generator_insert.cpp \
-      refinement/string_constraint_generator_float.cpp \
-      refinement/string_constraint_generator_format.cpp \
-      refinement/string_constraint_generator_main.cpp \
-      refinement/string_constraint_generator_testing.cpp \
-      refinement/string_constraint_generator_transformation.cpp \
-      refinement/string_constraint_generator_valueof.cpp \
-      refinement/string_constraint_instantiation.cpp \
+      strings/string_builtin_function.cpp \
+      strings/string_refinement.cpp \
+      strings/string_refinement_util.cpp \
+      strings/string_constraint.cpp \
+      strings/string_constraint_generator_code_points.cpp \
+      strings/string_constraint_generator_comparison.cpp \
+      strings/string_constraint_generator_concat.cpp \
+      strings/string_constraint_generator_constants.cpp \
+      strings/string_constraint_generator_indexof.cpp \
+      strings/string_constraint_generator_insert.cpp \
+      strings/string_constraint_generator_float.cpp \
+      strings/string_constraint_generator_format.cpp \
+      strings/string_constraint_generator_main.cpp \
+      strings/string_constraint_generator_testing.cpp \
+      strings/string_constraint_generator_transformation.cpp \
+      strings/string_constraint_generator_valueof.cpp \
+      strings/string_constraint_instantiation.cpp \
       sat/cnf.cpp \
       sat/cnf_clause_list.cpp \
       sat/dimacs_cnf.cpp \
diff --git a/src/solvers/strings/module_dependencies.txt b/src/solvers/strings/module_dependencies.txt
@@ -0,0 +1,6 @@
+solvers/flattening
+solvers/floatbv
+solvers/refinement
+solvers/sat
+solvers/strings
+util
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
diff --git a/src/solvers/strings/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
diff --git a/src/solvers/strings/string_constraint.h b/src/solvers/strings/string_constraint.h
@@ -20,9 +20,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 
-#include "bv_refinement.h"
 #include "string_refinement_invariant.h"
 
+#include <solvers/refinement/bv_refinement.h>
+
 #include <util/format_expr.h>
 #include <util/format_type.h>
 #include <util/refined_string_type.h>
diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h
@@ -26,7 +26,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/refined_string_type.h>
 #include <util/constexpr.def>
 #include <util/deprecate.h>
-#include <solvers/refinement/string_constraint.h>
+#include <solvers/strings/string_constraint.h>
 
 /// Generation of fresh symbols of a given type
 class symbol_generatort final
diff --git a/src/solvers/strings/string_constraint_generator_code_points.cpp b/src/solvers/strings/string_constraint_generator_code_points.cpp
@@ -10,7 +10,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for Java functions dealing with code points
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint_generator.h"
 
 /// add axioms for the conversion of an integer representing a java
 /// code point to a utf-16 string
diff --git a/src/solvers/strings/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp
@@ -11,7 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for function comparing strings, such as:
 ///   equals, equalsIgnoreCase, compareTo, hashCode, intern
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint_generator.h"
+
 #include <util/deprecate.h>
 
 /// Equality of the content of two strings
diff --git a/src/solvers/strings/string_constraint_generator_concat.cpp b/src/solvers/strings/string_constraint_generator_concat.cpp
@@ -11,7 +11,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for functions adding content add the end of
 ///   strings
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint_generator.h"
 
 /// Add axioms enforcing that `res` is the concatenation of `s1` with
 /// the substring of `s2` starting at index `start_index'` and ending
diff --git a/src/solvers/strings/string_constraint_generator_constants.cpp b/src/solvers/strings/string_constraint_generator_constants.cpp
@@ -9,7 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for constant strings
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint_generator.h"
 
 #include <util/prefix.h>
 #include <util/unicode.h>
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp
diff --git a/src/solvers/strings/string_constraint_generator_indexof.cpp b/src/solvers/strings/string_constraint_generator_indexof.cpp
@@ -11,8 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for the family of indexOf and lastIndexOf java
 ///   functions
 
-#include <solvers/refinement/string_refinement_invariant.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_refinement_invariant.h"
+#include "string_constraint_generator.h"
 
 /// Add axioms stating that the returned value is the index within `haystack`
 /// (`str`) of the first occurrence of `needle` (`c`) starting the search at
diff --git a/src/solvers/strings/string_constraint_generator_insert.cpp b/src/solvers/strings/string_constraint_generator_insert.cpp
@@ -9,8 +9,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for the family of insert Java functions
 
-#include <solvers/refinement/string_refinement_invariant.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_refinement_invariant.h"
+#include "string_constraint_generator.h"
+
 #include <util/deprecate.h>
 
 /// Add axioms ensuring the result `res` corresponds to `s1` where we
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -17,11 +17,11 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 ///   Li and Indradeep Ghosh, which gives examples of constraints for several
 ///   functions.
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint_generator.h"
+#include "string_refinement_invariant.h"
 
 #include <iterator>
 #include <limits>
-#include <solvers/refinement/string_refinement_invariant.h>
 
 #include <util/arith_tools.h>
 #include <util/pointer_predicates.h>
diff --git a/src/solvers/strings/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp
@@ -10,8 +10,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for string functions that return Boolean values
 
-#include <solvers/refinement/string_refinement_invariant.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_refinement_invariant.h"
+#include "string_constraint_generator.h"
+
 #include <util/deprecate.h>
 
 /// Add axioms stating that the returned expression is true exactly when the
diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp
@@ -11,8 +11,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for string transformations, that is, functions
 ///   taking one string and returning another
 
-#include <solvers/refinement/string_refinement_invariant.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_refinement_invariant.h"
+#include "string_constraint_generator.h"
+
 #include <util/arith_tools.h>
 
 /// Reduce or extend a string to have the given length
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -11,8 +11,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for functions generating strings from other
 ///   types, in particular int, long, float, double, char, bool
 
-#include <solvers/refinement/string_refinement_invariant.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_refinement_invariant.h"
+#include "string_constraint_generator.h"
+
 #include <util/simplify_expr.h>
 #include <util/deprecate.h>
 
diff --git a/src/solvers/strings/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp
@@ -9,7 +9,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 /// \file
 /// Defines related function for string constraints.
 
-#include <solvers/refinement/string_constraint_instantiation.h>
+#include "string_constraint_instantiation.h"
 
 /// Instantiates a quantified formula representing `not_contains` by
 /// substituting the quantifiers and generating axioms.
diff --git a/src/solvers/strings/string_constraint_instantiation.h b/src/solvers/strings/string_constraint_instantiation.h
@@ -12,8 +12,8 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
 
-#include <solvers/refinement/string_constraint.h>
-#include <solvers/refinement/string_constraint_generator.h>
+#include "string_constraint.h"
+#include "string_constraint_generator.h"
 
 std::vector<exprt> instantiate_not_contains(
   const string_not_contains_constraintt &axiom,
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
@@ -17,7 +17,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 ///   Parameterized Array and Interval Automaton" by Guodong Li and Indradeep
 ///   Ghosh.
 
-#include <solvers/refinement/string_refinement.h>
+#include "string_refinement.h"
+#include "string_constraint_instantiation.h"
 
 #include <iomanip>
 #include <numeric>
@@ -26,7 +27,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
-#include <solvers/refinement/string_constraint_instantiation.h>
 #include <unordered_set>
 #include <util/magic.h>
 
diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h
@@ -24,10 +24,11 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/string_expr.h>
 #include <util/replace_expr.h>
 #include <util/union_find_replace.h>
-#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>
+
+#include "string_constraint.h"
+#include "string_constraint_generator.h"
+#include "string_refinement_invariant.h"
+#include "string_refinement_util.h"
 
 // clang-format off
 #define OPT_STRING_REFINEMENT \
diff --git a/src/solvers/strings/string_refinement_invariant.h b/src/solvers/strings/string_refinement_invariant.h
diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp
diff --git a/src/solvers/strings/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h
diff --git a/unit/Makefile b/unit/Makefile
@@ -34,14 +34,14 @@ SRC += analyses/ai/ai.cpp \
        pointer-analysis/value_set.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/miniBDD/miniBDD.cpp \
-       solvers/refinement/array_pool/array_pool.cpp \
-       solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
-       solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
-       solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
-       solvers/refinement/string_refinement/concretize_array.cpp \
-       solvers/refinement/string_refinement/sparse_array.cpp \
-       solvers/refinement/string_refinement/substitute_array_list.cpp \
-       solvers/refinement/string_refinement/union_find_replace.cpp \
+       solvers/strings/array_pool/array_pool.cpp \
+       solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
+       solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
+       solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \
+       solvers/strings/string_refinement/concretize_array.cpp \
+       solvers/strings/string_refinement/sparse_array.cpp \
+       solvers/strings/string_refinement/substitute_array_list.cpp \
+       solvers/strings/string_refinement/union_find_replace.cpp \
        util/cmdline.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr.cpp \
diff --git a/unit/solvers/strings/array_pool/array_pool.cpp b/unit/solvers/strings/array_pool/array_pool.cpp
@@ -9,10 +9,10 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/catch.hpp>
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include <solvers/strings/string_constraint_generator.h>
 
 SCENARIO(
-  "array_pool", "[core][solvers][refinement][string_constraint_generator]")
+  "array_pool", "[core][solvers][strings][string_constraint_generator]")
 {
   const std::size_t pointer_width = 16;
   const auto char_type = unsignedbv_typet(8);
diff --git a/unit/solvers/strings/array_pool/module_dependencies.txt b/unit/solvers/strings/array_pool/module_dependencies.txt
@@ -1,3 +1,4 @@
 solvers/refinement
+solvers/strings
 testing-utils
 util
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/catch.hpp>
 
-#include <solvers/refinement/string_constraint_generator.h>
+#include <solvers/strings/string_constraint_generator.h>
 #include <util/std_types.h>
 
 /// Get the string length needed to print any value of the given type with the
@@ -106,7 +106,7 @@ static size_t expected_length(unsigned long radix, const typet &type)
 }
 
 SCENARIO("calculate_max_string_length",
-  "[core][solvers][refinement][string_constraint_generator_valueof]")
+  "[core][solvers][strings][string_constraint_generator_valueof]")
 {
   const unsigned long radixes[]={2, 8, 10, 16};
   const typet int_types[]=
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp
diff --git a/unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt b/unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt
diff --git a/unit/solvers/strings/string_refinement/concretize_array.cpp b/unit/solvers/strings/string_refinement/concretize_array.cpp
diff --git a/unit/solvers/strings/string_refinement/module_dependencies.txt b/unit/solvers/strings/string_refinement/module_dependencies.txt
diff --git a/unit/solvers/strings/string_refinement/sparse_array.cpp b/unit/solvers/strings/string_refinement/sparse_array.cpp
diff --git a/unit/solvers/strings/string_refinement/substitute_array_list.cpp b/unit/solvers/strings/string_refinement/substitute_array_list.cpp
diff --git a/unit/solvers/strings/string_refinement/union_find_replace.cpp b/unit/solvers/strings/string_refinement/union_find_replace.cpp
