move string solver into directory of its own

The string solver is now large enough to justify a separate directory.

Author: Daniel Kroening

jbmc/src/jbmc/jbmc_parse_options.h

@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-symex/path_storage.h>
 
-#include <solvers/refinement/string_refinement.h>
+#include <solvers/strings/string_refinement.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 

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 \

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp renamed to jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -15,7 +15,7 @@ Author: Jesse Sigal, [email protected]
 #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>

jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt renamed to jbmc/unit/solvers/strings/string_constraint_instantiation/module_dependencies.txt

@@ -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>

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp renamed to jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_expr.h>
-#include <solvers/refinement/string_refinement.h>
+#include <solvers/strings/string_refinement.h>
 #include <util/symbol_table.h>
 #include <langapi/mode.h>
 #include <java_bytecode/java_bytecode_language.h>

jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt renamed to jbmc/unit/solvers/strings/string_refinement/module_dependencies.txt

@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
 
 #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"

jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp renamed to jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp

@@ -29,7 +29,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>
 

src/cbmc/cbmc_parse_options.h

@@ -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 \