cprover
|
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/deprecate.h>
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset) |
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset . More... | |
exprt | length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2 . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) |
Insertion of a string in another at a specific index. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
add axioms corresponding to the StringBuilder.insert(I) java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert_bool (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
add axioms corresponding to the StringBuilder.insert(Z) java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert_char (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Add axioms corresponding to the StringBuilder.insert(C) java function. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
add axioms corresponding to the StringBuilder.insert(D) java function More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
Add axioms corresponding to the StringBuilder.insert(F) java function. More... | |
Generates string constraints for the family of insert Java functions
Definition in file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | offset | ||
) |
Add axioms ensuring the result res
corresponds to s1
where we inserted s2
at position offset
.
We write offset' for max(0, min(res.length, offset))
. These axioms are:
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
s1 | array of characters expression |
s2 | array of characters expression |
offset | integer expression |
Definition at line 33 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Insertion of a string in another at a specific index.
Add axioms ensuring the result res
corresponds to s1
where we inserted s2
at position offset
. (More...)
If start
and end
arguments are given then substring(s2, start, end)
is considered instead of s2
.
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , refined_strings2 , integer offset , optional integer start and optional integer end |
pool | pool of arrays representing strings |
Definition at line 106 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert_bool | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the StringBuilder.insert(Z) java function
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a Boolean |
array_pool | pool of arrays representing strings |
Definition at line 171 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert_char | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Add axioms corresponding to the StringBuilder.insert(C) java function.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a character |
array_pool | pool of arrays representing strings |
Definition at line 196 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert_double | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
add axioms corresponding to the StringBuilder.insert(D) java function
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a double |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 223 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert_float | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms corresponding to the StringBuilder.insert(F) java function.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a float |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 252 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert_int | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
add axioms corresponding to the StringBuilder.insert(I) java function
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and an integer |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 144 of file string_constraint_generator_insert.cpp.
exprt length_constraint_for_insert | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms ensuring the length of res
corresponds to that of s1
where we inserted s2
.
Definition at line 80 of file string_constraint_generator_insert.cpp.