Skip to content

Commit 69f67d4

Browse files
author
Daniel Kroening
committed
move string solver into directory of its own
The string solver is now large enough to justify a separate directory.
1 parent 75f7c9d commit 69f67d4

File tree

46 files changed

+91
-77
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

46 files changed

+91
-77
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include <goto-symex/path_storage.h>
3131

32-
#include <solvers/refinement/string_refinement.h>
32+
#include <solvers/strings/string_refinement.h>
3333

3434
#include <java_bytecode/java_bytecode_language.h>
3535

‎jbmc/unit/Makefile

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,9 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
5454
java_bytecode/java_virtual_functions/virtual_functions.cpp \
5555
java_bytecode/load_method_by_regex.cpp \
5656
pointer-analysis/custom_value_set_analysis.cpp \
57-
solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
58-
solvers/refinement/string_refinement/dependency_graph.cpp \
59-
solvers/refinement/string_refinement/string_symbol_resolution.cpp \
57+
solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp \
58+
solvers/strings/string_refinement/dependency_graph.cpp \
59+
solvers/strings/string_refinement/string_symbol_resolution.cpp \
6060
util/expr_iterator.cpp \
6161
util/has_subtype.cpp \
6262
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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Jesse Sigal, [email protected]
1515
#include <langapi/mode.h>
1616
#include <langapi/language_util.h>
1717

18-
#include <solvers/refinement/string_constraint_instantiation.h>
18+
#include <solvers/strings/string_constraint_instantiation.h>
1919
#include <solvers/sat/satcheck.h>
2020

2121
#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

File renamed without changes.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Diffblue Ltd.
1313
#include <util/std_types.h>
1414
#include <util/std_expr.h>
1515
#include <java_bytecode/java_types.h>
16-
#include <solvers/refinement/string_refinement_util.h>
16+
#include <solvers/strings/string_refinement_util.h>
1717

1818
#ifdef DEBUG
1919
#include <iostream>

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

File renamed without changes.

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,11 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12+
#include <solvers/strings/string_refinement.h>
13+
1214
#include <util/arith_tools.h>
1315
#include <util/c_types.h>
1416
#include <util/std_expr.h>
15-
#include <solvers/refinement/string_refinement.h>
1617
#include <util/symbol_table.h>
1718
#include <langapi/mode.h>
1819
#include <java_bytecode/java_bytecode_language.h>

‎src/cbmc/cbmc_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include <goto-programs/goto_trace.h>
3131

32-
#include <solvers/refinement/string_refinement.h>
32+
#include <solvers/strings/string_refinement.h>
3333

3434
#include "bmc.h"
3535
#include "xml_interface.h"

‎src/goto-checker/solver_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Author: Daniel Kroening, Peter Schrammel
2929
#include <solvers/prop/prop.h>
3030
#include <solvers/prop/prop_conv.h>
3131
#include <solvers/refinement/bv_refinement.h>
32-
#include <solvers/refinement/string_refinement.h>
32+
#include <solvers/strings/string_refinement.h>
3333
#include <solvers/sat/dimacs_cnf.h>
3434
#include <solvers/sat/satcheck.h>
3535

‎src/solvers/Makefile

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -161,23 +161,23 @@ SRC = $(BOOLEFORCE_SRC) \
161161
refinement/bv_refinement_loop.cpp \
162162
refinement/refine_arithmetic.cpp \
163163
refinement/refine_arrays.cpp \
164-
refinement/string_builtin_function.cpp \
165-
refinement/string_refinement.cpp \
166-
refinement/string_refinement_util.cpp \
167-
refinement/string_constraint.cpp \
168-
refinement/string_constraint_generator_code_points.cpp \
169-
refinement/string_constraint_generator_comparison.cpp \
170-
refinement/string_constraint_generator_concat.cpp \
171-
refinement/string_constraint_generator_constants.cpp \
172-
refinement/string_constraint_generator_indexof.cpp \
173-
refinement/string_constraint_generator_insert.cpp \
174-
refinement/string_constraint_generator_float.cpp \
175-
refinement/string_constraint_generator_format.cpp \
176-
refinement/string_constraint_generator_main.cpp \
177-
refinement/string_constraint_generator_testing.cpp \
178-
refinement/string_constraint_generator_transformation.cpp \
179-
refinement/string_constraint_generator_valueof.cpp \
180-
refinement/string_constraint_instantiation.cpp \
164+
strings/string_builtin_function.cpp \
165+
strings/string_refinement.cpp \
166+
strings/string_refinement_util.cpp \
167+
strings/string_constraint.cpp \
168+
strings/string_constraint_generator_code_points.cpp \
169+
strings/string_constraint_generator_comparison.cpp \
170+
strings/string_constraint_generator_concat.cpp \
171+
strings/string_constraint_generator_constants.cpp \
172+
strings/string_constraint_generator_indexof.cpp \
173+
strings/string_constraint_generator_insert.cpp \
174+
strings/string_constraint_generator_float.cpp \
175+
strings/string_constraint_generator_format.cpp \
176+
strings/string_constraint_generator_main.cpp \
177+
strings/string_constraint_generator_testing.cpp \
178+
strings/string_constraint_generator_transformation.cpp \
179+
strings/string_constraint_generator_valueof.cpp \
180+
strings/string_constraint_instantiation.cpp \
181181
sat/cnf.cpp \
182182
sat/cnf_clause_list.cpp \
183183
sat/dimacs_cnf.cpp \

‎src/solvers/refinement/string_builtin_function.cpp renamed to ‎src/solvers/strings/string_builtin_function.cpp

File renamed without changes.

‎src/solvers/refinement/string_builtin_function.h renamed to ‎src/solvers/strings/string_builtin_function.h

File renamed without changes.

‎src/solvers/refinement/string_constraint.cpp renamed to ‎src/solvers/strings/string_constraint.cpp

File renamed without changes.

‎src/solvers/refinement/string_constraint.h renamed to ‎src/solvers/strings/string_constraint.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,10 @@ Author: Romain Brenguier, [email protected]
2020
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
2121
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
2222

23-
#include "bv_refinement.h"
2423
#include "string_refinement_invariant.h"
2524

25+
#include <solvers/refinement/bv_refinement.h>
26+
2627
#include <util/format_expr.h>
2728
#include <util/format_type.h>
2829
#include <util/refined_string_type.h>

‎src/solvers/refinement/string_constraint_generator.h renamed to ‎src/solvers/strings/string_constraint_generator.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Author: Romain Brenguier, [email protected]
2626
#include <util/refined_string_type.h>
2727
#include <util/constexpr.def>
2828
#include <util/deprecate.h>
29-
#include <solvers/refinement/string_constraint.h>
29+
#include <solvers/strings/string_constraint.h>
3030

3131
/// Generation of fresh symbols of a given type
3232
class symbol_generatort final

‎src/solvers/refinement/string_constraint_generator_code_points.cpp renamed to ‎src/solvers/strings/string_constraint_generator_code_points.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Author: Romain Brenguier, [email protected]
1010
/// \file
1111
/// Generates string constraints for Java functions dealing with code points
1212

13-
#include <solvers/refinement/string_constraint_generator.h>
13+
#include "string_constraint_generator.h"
1414

1515
/// add axioms for the conversion of an integer representing a java
1616
/// code point to a utf-16 string

‎src/solvers/refinement/string_constraint_generator_comparison.cpp renamed to ‎src/solvers/strings/string_constraint_generator_comparison.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for function comparing strings, such as:
1212
/// equals, equalsIgnoreCase, compareTo, hashCode, intern
1313

14-
#include <solvers/refinement/string_constraint_generator.h>
14+
#include "string_constraint_generator.h"
15+
1516
#include <util/deprecate.h>
1617

1718
/// Equality of the content of two strings

‎src/solvers/refinement/string_constraint_generator_concat.cpp renamed to ‎src/solvers/strings/string_constraint_generator_concat.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for functions adding content add the end of
1212
/// strings
1313

14-
#include <solvers/refinement/string_constraint_generator.h>
14+
#include "string_constraint_generator.h"
1515

1616
/// Add axioms enforcing that `res` is the concatenation of `s1` with
1717
/// the substring of `s2` starting at index `start_index'` and ending

‎src/solvers/refinement/string_constraint_generator_constants.cpp renamed to ‎src/solvers/strings/string_constraint_generator_constants.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Romain Brenguier, [email protected]
99
/// \file
1010
/// Generates string constraints for constant strings
1111

12-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include "string_constraint_generator.h"
1313

1414
#include <util/prefix.h>
1515
#include <util/unicode.h>

‎src/solvers/refinement/string_constraint_generator_float.cpp renamed to ‎src/solvers/strings/string_constraint_generator_float.cpp

File renamed without changes.

‎src/solvers/refinement/string_constraint_generator_format.cpp renamed to ‎src/solvers/strings/string_constraint_generator_format.cpp

File renamed without changes.

‎src/solvers/refinement/string_constraint_generator_indexof.cpp renamed to ‎src/solvers/strings/string_constraint_generator_indexof.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for the family of indexOf and lastIndexOf java
1212
/// functions
1313

14-
#include <solvers/refinement/string_refinement_invariant.h>
15-
#include <solvers/refinement/string_constraint_generator.h>
14+
#include "string_refinement_invariant.h"
15+
#include "string_constraint_generator.h"
1616

1717
/// Add axioms stating that the returned value is the index within `haystack`
1818
/// (`str`) of the first occurrence of `needle` (`c`) starting the search at

‎src/solvers/refinement/string_constraint_generator_insert.cpp renamed to ‎src/solvers/strings/string_constraint_generator_insert.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,9 @@ Author: Romain Brenguier, [email protected]
99
/// \file
1010
/// Generates string constraints for the family of insert Java functions
1111

12-
#include <solvers/refinement/string_refinement_invariant.h>
13-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include "string_refinement_invariant.h"
13+
#include "string_constraint_generator.h"
14+
1415
#include <util/deprecate.h>
1516

1617
/// Add axioms ensuring the result `res` corresponds to `s1` where we

‎src/solvers/refinement/string_constraint_generator_main.cpp renamed to ‎src/solvers/strings/string_constraint_generator_main.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,11 @@ Author: Romain Brenguier, [email protected]
1717
/// Li and Indradeep Ghosh, which gives examples of constraints for several
1818
/// functions.
1919

20-
#include <solvers/refinement/string_constraint_generator.h>
20+
#include "string_constraint_generator.h"
21+
#include "string_refinement_invariant.h"
2122

2223
#include <iterator>
2324
#include <limits>
24-
#include <solvers/refinement/string_refinement_invariant.h>
2525

2626
#include <util/arith_tools.h>
2727
#include <util/pointer_predicates.h>

‎src/solvers/refinement/string_constraint_generator_testing.cpp renamed to ‎src/solvers/strings/string_constraint_generator_testing.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,9 @@ Author: Romain Brenguier, [email protected]
1010
/// \file
1111
/// Generates string constraints for string functions that return Boolean values
1212

13-
#include <solvers/refinement/string_refinement_invariant.h>
14-
#include <solvers/refinement/string_constraint_generator.h>
13+
#include "string_refinement_invariant.h"
14+
#include "string_constraint_generator.h"
15+
1516
#include <util/deprecate.h>
1617

1718
/// Add axioms stating that the returned expression is true exactly when the

‎src/solvers/refinement/string_constraint_generator_transformation.cpp renamed to ‎src/solvers/strings/string_constraint_generator_transformation.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,9 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for string transformations, that is, functions
1212
/// taking one string and returning another
1313

14-
#include <solvers/refinement/string_refinement_invariant.h>
15-
#include <solvers/refinement/string_constraint_generator.h>
14+
#include "string_refinement_invariant.h"
15+
#include "string_constraint_generator.h"
16+
1617
#include <util/arith_tools.h>
1718

1819
/// Reduce or extend a string to have the given length

‎src/solvers/refinement/string_constraint_generator_valueof.cpp renamed to ‎src/solvers/strings/string_constraint_generator_valueof.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,9 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for functions generating strings from other
1212
/// types, in particular int, long, float, double, char, bool
1313

14-
#include <solvers/refinement/string_refinement_invariant.h>
15-
#include <solvers/refinement/string_constraint_generator.h>
14+
#include "string_refinement_invariant.h"
15+
#include "string_constraint_generator.h"
16+
1617
#include <util/simplify_expr.h>
1718
#include <util/deprecate.h>
1819

‎src/solvers/refinement/string_constraint_instantiation.cpp renamed to ‎src/solvers/strings/string_constraint_instantiation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Jesse Sigal, [email protected]
99
/// \file
1010
/// Defines related function for string constraints.
1111

12-
#include <solvers/refinement/string_constraint_instantiation.h>
12+
#include "string_constraint_instantiation.h"
1313

1414
/// Instantiates a quantified formula representing `not_contains` by
1515
/// substituting the quantifiers and generating axioms.

‎src/solvers/refinement/string_constraint_instantiation.h renamed to ‎src/solvers/strings/string_constraint_instantiation.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ Author: Jesse Sigal, [email protected]
1212
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
1313
#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
1414

15-
#include <solvers/refinement/string_constraint.h>
16-
#include <solvers/refinement/string_constraint_generator.h>
15+
#include "string_constraint.h"
16+
#include "string_constraint_generator.h"
1717

1818
std::vector<exprt> instantiate_not_contains(
1919
const string_not_contains_constraintt &axiom,

‎src/solvers/refinement/string_refinement.cpp renamed to ‎src/solvers/strings/string_refinement.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ Author: Alberto Griggio, [email protected]
1717
/// Parameterized Array and Interval Automaton" by Guodong Li and Indradeep
1818
/// Ghosh.
1919

20-
#include <solvers/refinement/string_refinement.h>
20+
#include "string_refinement.h"
21+
#include "string_constraint_instantiation.h"
2122

2223
#include <iomanip>
2324
#include <numeric>
@@ -26,7 +27,6 @@ Author: Alberto Griggio, [email protected]
2627
#include <util/expr_util.h>
2728
#include <util/simplify_expr.h>
2829
#include <solvers/sat/satcheck.h>
29-
#include <solvers/refinement/string_constraint_instantiation.h>
3030
#include <unordered_set>
3131
#include <util/magic.h>
3232

‎src/solvers/refinement/string_refinement.h renamed to ‎src/solvers/strings/string_refinement.h

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,11 @@ Author: Alberto Griggio, [email protected]
2424
#include <util/string_expr.h>
2525
#include <util/replace_expr.h>
2626
#include <util/union_find_replace.h>
27-
#include <solvers/refinement/string_constraint.h>
28-
#include <solvers/refinement/string_constraint_generator.h>
29-
#include <solvers/refinement/string_refinement_invariant.h>
30-
#include <solvers/refinement/string_refinement_util.h>
27+
28+
#include "string_constraint.h"
29+
#include "string_constraint_generator.h"
30+
#include "string_refinement_invariant.h"
31+
#include "string_refinement_util.h"
3132

3233
// clang-format off
3334
#define OPT_STRING_REFINEMENT \

‎src/solvers/refinement/string_refinement_invariant.h renamed to ‎src/solvers/strings/string_refinement_invariant.h

File renamed without changes.

‎src/solvers/refinement/string_refinement_util.cpp renamed to ‎src/solvers/strings/string_refinement_util.cpp

File renamed without changes.

‎src/solvers/refinement/string_refinement_util.h renamed to ‎src/solvers/strings/string_refinement_util.h

File renamed without changes.

‎unit/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -34,14 +34,14 @@ SRC += analyses/ai/ai.cpp \
3434
pointer-analysis/value_set.cpp \
3535
solvers/floatbv/float_utils.cpp \
3636
solvers/miniBDD/miniBDD.cpp \
37-
solvers/refinement/array_pool/array_pool.cpp \
38-
solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
39-
solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
40-
solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
41-
solvers/refinement/string_refinement/concretize_array.cpp \
42-
solvers/refinement/string_refinement/sparse_array.cpp \
43-
solvers/refinement/string_refinement/substitute_array_list.cpp \
44-
solvers/refinement/string_refinement/union_find_replace.cpp \
37+
solvers/strings/array_pool/array_pool.cpp \
38+
solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
39+
solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
40+
solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \
41+
solvers/strings/string_refinement/concretize_array.cpp \
42+
solvers/strings/string_refinement/sparse_array.cpp \
43+
solvers/strings/string_refinement/substitute_array_list.cpp \
44+
solvers/strings/string_refinement/union_find_replace.cpp \
4545
util/cmdline.cpp \
4646
util/expr_cast/expr_cast.cpp \
4747
util/expr.cpp \

‎unit/solvers/refinement/array_pool/array_pool.cpp renamed to ‎unit/solvers/strings/array_pool/array_pool.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include <solvers/strings/string_constraint_generator.h>
1313

1414
SCENARIO(
15-
"array_pool", "[core][solvers][refinement][string_constraint_generator]")
15+
"array_pool", "[core][solvers][strings][string_constraint_generator]")
1616
{
1717
const std::size_t pointer_width = 16;
1818
const auto char_type = unsignedbv_typet(8);

‎unit/solvers/refinement/array_pool/module_dependencies.txt renamed to ‎unit/solvers/strings/array_pool/module_dependencies.txt

File renamed without changes.

‎unit/solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp renamed to ‎unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include <solvers/strings/string_constraint_generator.h>
1313
#include <util/std_types.h>
1414

1515
/// 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)
106106
}
107107

108108
SCENARIO("calculate_max_string_length",
109-
"[core][solvers][refinement][string_constraint_generator_valueof]")
109+
"[core][solvers][strings][string_constraint_generator_valueof]")
110110
{
111111
const unsigned long radixes[]={2, 8, 10, 16};
112112
const typet int_types[]=

‎unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp renamed to ‎unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include <solvers/strings/string_constraint_generator.h>
13+
1314
#include <util/namespace.h>
1415
#include <util/symbol_table.h>
1516
#include <util/simplify_expr.h>
@@ -34,7 +35,7 @@ static exprt actual(
3435
}
3536

3637
SCENARIO("get_numeric_value_from_character",
37-
"[core][solvers][refinement][string_constraint_generator_valueof]")
38+
"[core][solvers][strings][string_constraint_generator_valueof]")
3839
{
3940
const typet char_type_1=unsignedbv_typet(8);
4041
const typet char_type_2=unsignedbv_typet(16);

‎unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp renamed to ‎unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12-
#include <solvers/refinement/string_constraint_generator.h>
12+
#include <solvers/strings/string_constraint_generator.h>
13+
1314
#include <util/namespace.h>
1415
#include <util/symbol_table.h>
1516
#include <util/simplify_expr.h>
@@ -57,7 +58,7 @@ static exprt actual_without_radix(
5758
}
5859

5960
SCENARIO("is_digit_with_radix without strict formatting",
60-
"[core][solvers][refinement][string_constraint_generator_valueof]")
61+
"[core][solvers][strings][string_constraint_generator_valueof]")
6162
{
6263
WHEN("Radix 10")
6364
{

‎unit/solvers/refinement/string_constraint_generator_valueof/module_dependencies.txt renamed to ‎unit/solvers/strings/string_constraint_generator_valueof/module_dependencies.txt

File renamed without changes.

0 commit comments

Comments
 (0)