cprover
|
Generates string constraints for string transformations, that is, functions taking one string and returning another. More...
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/arith_tools.h>
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_set_length (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Reduce or extend a string to have the given length. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_substring (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Substring of a string between two indices. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_substring (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) |
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_trim (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Remove leading and trailing whitespaces. More... | |
static optionalt< std::pair< exprt, exprt > > | to_char_pair (exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr) |
Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_replace (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Replace a character by another in a string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_delete_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
add axioms corresponding to the StringBuilder.deleteCharAt java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_delete (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool) |
Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_delete (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Remove a portion of a string. More... | |
Generates string constraints for string transformations, that is, functions taking one string and returning another.
Definition in file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_delete | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | str, | ||
const exprt & | start, | ||
const exprt & | end, | ||
array_poolt & | array_pool | ||
) |
Add axioms stating that res
corresponds to the input str
where we removed characters between the positions start
(included) and end
(not included).
These axioms are the same as would be generated for: concat(substring(str, 0, start), substring(end, |str|))
(see add_axioms_for_substring and add_axioms_for_concat_substr).
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
array_pool | pool of arrays representing strings |
Definition at line 374 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_delete | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Remove a portion of a string.
Add axioms stating that res
corresponds to the input str
where we removed characters between the positions start
(included) and end
(not included). (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start and integer end |
array_pool | pool of arrays representing strings |
Definition at line 412 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the StringBuilder.deleteCharAt java function
fresh_symbol | generator of fresh symbols |
f | function application with two arguments, the first is a string and the second is an index |
array_pool | pool of arrays representing strings |
Definition at line 339 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_replace | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Replace a character by another in a string.
Add axioms ensuring that res
corresponds to str
where occurences of old_char
have been replaced by new_char
. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , character old_char and character new_char |
array_pool | pool of arrays representing strings |
Definition at line 297 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_set_length | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Reduce or extend a string to have the given length.
Add axioms ensuring the returned string expression res
has length k
and characters at position i
in res
are equal to the character at position i
in s1
if i
is smaller that the length of s1
, otherwise it is the null character \u0000
.
These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , integer k |
array_pool | pool of arrays representing strings |
0
Definition at line 37 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_substring | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Substring of a string between two indices.
Add axioms ensuring that res
corresponds to the substring of str
between indexes ‘start’ = max(start, 0)and
end' = max(min(end, |str|), start')`. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start , optional integer end with default value |str| . |
array_pool | pool of arrays representing strings |
Definition at line 94 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_substring | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | str, | ||
const exprt & | start, | ||
const exprt & | end | ||
) |
Add axioms ensuring that res
corresponds to the substring of str
between indexes ‘start’ = max(start, 0)and
end' = max(min(end, |str|), start')`.
These axioms are:
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
Definition at line 124 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_trim | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Remove leading and trailing whitespaces.
Add axioms ensuring res
corresponds to str
from which leading and trailing whitespaces have been removed. Are considered whitespaces, characters whose ascii code are smaller than that of ' ' (space).
These axioms are:
idx
represents the index of the first non-space character.fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str . |
array_pool | pool of arrays representing strings |
Definition at line 183 of file string_constraint_generator_transformation.cpp.
|
static |
Convert two expressions to pair of chars If both expressions are characters, return pair of them If both expressions are 1-length strings, return first character of each Otherwise return empty optional.
expr1 | First expression |
expr2 | Second expression |
get_string_expr | Function that yields an array_string_exprt corresponding to either expr1 or expr2 , for the case where they are not primitive chars. |
Definition at line 257 of file string_constraint_generator_transformation.cpp.