Skip to content

Commit 71f80e1

Browse files
Deprecates add_axioms_for_is_suffix
We can get the same result using is_prefix with an offset which is the difference of the two lengths.
1 parent 8ee1c16 commit 71f80e1

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

src/solvers/README.md

+2-3
Original file line numberDiff line numberDiff line change
@@ -231,9 +231,6 @@ allocates a new string before calling a primitive.
231231
* `cprover_string_is_prefix` :
232232
\copybrief string_constraint_generatort::add_axioms_for_is_prefix
233233
\link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
234-
* `cprover_string_is_suffix` :
235-
\copybrief string_constraint_generatort::add_axioms_for_is_suffix
236-
\link string_constraint_generatort::add_axioms_for_is_suffix More... \endlink
237234
* `cprover_string_index_of` :
238235
\copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f)
239236
\link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
@@ -319,6 +316,8 @@ allocates a new string before calling a primitive.
319316
* `cprover_string_intern` : Never tested.
320317
* `cprover_string_is_empty` :
321318
Should use `cprover_string_length(s) == 0` instead.
319+
* `cprover_string_is_suffix` : Should use `cprover_string_is_prefix` with an
320+
offset argument.
322321
* `cprover_string_empty_string` : Can use literal of empty string instead.
323322
* `cprover_string_of_long` : Should be the same as `cprover_string_of_int`.
324323
* `cprover_string_delete_char_at` : A call to

src/solvers/refinement/string_constraint_generator_testing.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,7 @@ exprt string_constraint_generatort::add_axioms_for_is_empty(
135135
/// \param swap_arguments: boolean flag telling whether the suffix is the second
136136
/// argument or the first argument
137137
/// \return Boolean expression `issuffix`
138+
DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`")
138139
exprt string_constraint_generatort::add_axioms_for_is_suffix(
139140
const function_application_exprt &f, bool swap_arguments)
140141
{

0 commit comments

Comments
 (0)