Skip to content

Commit 73e410a

Browse files
JohnDumbellJohnDumbell
authored
Merge pull request #4957 from JohnDumbell/jd/feature/string_refine_combine_simplify
Simplify when combining string-refinement result constraints
2 parents 153062c + 303ec4d commit 73e410a

14 files changed

+590
-941
lines changed

‎src/solvers/README.md

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -419,92 +419,92 @@ This is described in more detail \link string_builtin_functiont here. \endlink
419419
* `cprover_string_associate_length_to_array` : Link the length of the array
420420
with the given integer value.
421421
* `cprover_string_char_at` :
422-
\copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
423-
\link add_axioms_for_char_at More... \endlink
422+
\copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
423+
\link string_constraint_generatort::add_axioms_for_char_at More... \endlink
424424
* `cprover_string_length` :
425-
\copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
426-
\link add_axioms_for_length More... \endlink
425+
\copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
426+
\link string_constraint_generatort::add_axioms_for_length More... \endlink
427427

428428
\subsection comparisons Comparisons:
429429

430430
* `cprover_string_compare_to` :
431-
\copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
432-
\link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
431+
\copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
432+
\link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
433433
* `cprover_string_contains` :
434-
\copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
435-
\link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
434+
\copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
435+
\link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
436436
* `cprover_string_equals` :
437-
\copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
438-
\link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
437+
\copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
438+
\link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
439439
* `cprover_string_equals_ignore_case` :
440-
\copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
441-
\link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
440+
\copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
441+
\link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
442442
* `cprover_string_is_prefix` :
443-
\copybrief add_axioms_for_is_prefix
444-
\link add_axioms_for_is_prefix More... \endlink
443+
\copybrief string_constraint_generatort::add_axioms_for_is_prefix
444+
\link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
445445
* `cprover_string_index_of` :
446-
\copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
447-
\link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
446+
\copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f=)
447+
\link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
448448
* `cprover_string_last_index_of` :
449-
\copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
450-
\link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
449+
\copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
450+
\link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink
451451

452452
\subsection transformations Transformations:
453453

454454
* `cprover_string_char_set` :
455455
\copybrief string_set_char_builtin_functiont::constraints
456456
\link string_set_char_builtin_functiont::constraints More... \endlink
457457
* `cprover_string_concat` :
458-
\copybrief add_axioms_for_concat
459-
\link add_axioms_for_concat More... \endlink
458+
\copybrief string_constraint_generatort::add_axioms_for_concat
459+
\link string_constraint_generatort::add_axioms_for_concat More... \endlink
460460
* `cprover_string_delete` :
461-
\copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
462-
\link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
461+
\copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
462+
\link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
463463
* `cprover_string_insert` :
464464
\copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const
465465
\link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const More... \endlink
466466
* `cprover_string_replace` :
467-
\copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
468-
\link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
467+
\copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
468+
\link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
469469
* `cprover_string_set_length` :
470-
\copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
471-
\link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
470+
\copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
471+
\link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
472472
* `cprover_string_substring` :
473-
\copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
474-
\link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
473+
\copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
474+
\link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
475475
* `cprover_string_to_lower_case` :
476476
\copybrief string_to_lower_case_builtin_functiont::constraints
477477
\link string_to_lower_case_builtin_functiont::constraints More... \endlink
478478
* `cprover_string_to_upper_case` :
479479
\copybrief string_to_upper_case_builtin_functiont::constraints
480480
\link string_to_upper_case_builtin_functiont::constraints More... \endlink
481481
* `cprover_string_trim` :
482-
\copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
483-
\link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
482+
\copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
483+
\link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink
484484

485485
\subsection conversions Conversions:
486486

487487
* `cprover_string_format` :
488488
\copybrief add_axioms_for_format
489489
\link add_axioms_for_format More... \endlink
490490
* `cprover_string_from_literal` :
491-
\copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
492-
\link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
491+
\copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
492+
\link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
493493
* `cprover_string_of_int` :
494-
\copybrief add_axioms_for_string_of_int
495-
\link add_axioms_for_string_of_int More... \endlink
494+
\copybrief string_constraint_generatort::add_axioms_for_string_of_int
495+
\link string_constraint_generatort::add_axioms_for_string_of_int More... \endlink
496496
* `cprover_string_of_float` :
497-
\copybrief add_axioms_for_string_of_float
498-
\link add_axioms_for_string_of_float More... \endlink
497+
\copybrief string_constraint_generatort::add_axioms_for_string_of_float
498+
\link string_constraint_generatort::add_axioms_for_string_of_float More... \endlink
499499
* `cprover_string_of_float_scientific_notation` :
500-
\copybrief add_axioms_from_float_scientific_notation
501-
\link add_axioms_from_float_scientific_notation More... \endlink
500+
\copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation
501+
\link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink
502502
* `cprover_string_of_char` :
503-
\copybrief add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
504-
\link add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) More... \endlink
503+
\copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
504+
\link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
505505
* `cprover_string_parse_int` :
506-
\copybrief add_axioms_for_parse_int
507-
\link add_axioms_for_parse_int More... \endlink
506+
\copybrief string_constraint_generatort::add_axioms_for_parse_int
507+
\link string_constraint_generatort::add_axioms_for_parse_int More... \endlink
508508

509509
\subsection solvers-deprecated Deprecated primitives:
510510

‎src/solvers/strings/string_builtin_function.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -407,8 +407,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
407407
string_constraintst string_of_int_builtin_functiont::constraints(
408408
string_constraint_generatort &generator) const
409409
{
410-
auto pair = add_axioms_for_string_of_int_with_radix(
411-
result, arg, radix, 0, generator.ns, array_pool);
410+
auto pair =
411+
generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
412412
pair.second.existential.push_back(equal_exprt(pair.first, return_code));
413413
return pair.second;
414414
}

‎src/solvers/strings/string_concatenation_builtin_function.cpp

Lines changed: 15 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -43,22 +43,19 @@ string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
4343
/// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
4444
/// 3. \f$\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\f$
4545
///
46-
/// \param fresh_symbol: generator of fresh symbols
4746
/// \param res: an array of characters expression
4847
/// \param s1: an array of characters expression
4948
/// \param s2: an array of characters expression
5049
/// \param start_index: integer expression
5150
/// \param end_index: integer expression
52-
/// \param array_pool: pool of arrays representing strings
5351
/// \return integer expression `0`
54-
std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
55-
symbol_generatort &fresh_symbol,
52+
std::pair<exprt, string_constraintst>
53+
string_constraint_generatort::add_axioms_for_concat_substr(
5654
const array_string_exprt &res,
5755
const array_string_exprt &s1,
5856
const array_string_exprt &s2,
5957
const exprt &start_index,
60-
const exprt &end_index,
61-
array_poolt &array_pool)
58+
const exprt &end_index)
6259
{
6360
string_constraintst constraints;
6461
const typet &index_type = start_index.type();
@@ -153,40 +150,28 @@ exprt length_constraint_for_concat_char(
153150
/// `s2`.
154151
///
155152
/// \deprecated should use concat_substr instead
156-
/// \param fresh_symbol: generator of fresh symbols
157153
/// \param res: string_expression corresponding to the result
158154
/// \param s1: the string expression to append to
159155
/// \param s2: the string expression to append to the first one
160-
/// \param array_pool: pool of arrays representing strings
161156
/// \return an integer expression
162-
std::pair<exprt, string_constraintst> add_axioms_for_concat(
163-
symbol_generatort &fresh_symbol,
157+
std::pair<exprt, string_constraintst>
158+
string_constraint_generatort::add_axioms_for_concat(
164159
const array_string_exprt &res,
165160
const array_string_exprt &s1,
166-
const array_string_exprt &s2,
167-
array_poolt &array_pool)
161+
const array_string_exprt &s2)
168162
{
169163
exprt index_zero = from_integer(0, s2.length_type());
170164
return add_axioms_for_concat_substr(
171-
fresh_symbol,
172-
res,
173-
s1,
174-
s2,
175-
index_zero,
176-
array_pool.get_or_create_length(s2),
177-
array_pool);
165+
res, s1, s2, index_zero, array_pool.get_or_create_length(s2));
178166
}
179167

180168
/// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
181169
/// \deprecated java specific
182-
/// \param fresh_symbol: generator of fresh symbols
183170
/// \param f: function application with two arguments: a string and a code point
184-
/// \param array_pool: pool of arrays representing strings
185171
/// \return an expression
186-
std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
187-
symbol_generatort &fresh_symbol,
188-
const function_application_exprt &f,
189-
array_poolt &array_pool)
172+
std::pair<exprt, string_constraintst>
173+
string_constraint_generatort::add_axioms_for_concat_code_point(
174+
const function_application_exprt &f)
190175
{
191176
PRECONDITION(f.arguments().size() == 4);
192177
const array_string_exprt res =
@@ -197,8 +182,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
197182
const array_string_exprt code_point =
198183
array_pool.fresh_string(index_type, char_type);
199184
return combine_results(
200-
add_axioms_for_code_point(code_point, f.arguments()[3], array_pool),
201-
add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool));
185+
add_axioms_for_code_point(code_point, f.arguments()[3]),
186+
add_axioms_for_concat(res, s1, code_point));
202187
}
203188

204189
std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
@@ -228,18 +213,11 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
228213
{
229214
auto pair = [&]() -> std::pair<exprt, string_constraintst> {
230215
if(args.size() == 0)
231-
return add_axioms_for_concat(
232-
generator.fresh_symbol, result, input1, input2, array_pool);
216+
return generator.add_axioms_for_concat(result, input1, input2);
233217
if(args.size() == 2)
234218
{
235-
return add_axioms_for_concat_substr(
236-
generator.fresh_symbol,
237-
result,
238-
input1,
239-
input2,
240-
args[0],
241-
args[1],
242-
array_pool);
219+
return generator.add_axioms_for_concat_substr(
220+
result, input1, input2, args[0], args[1]);
243221
}
244222
UNREACHABLE;
245223
}();

0 commit comments

Comments
 (0)