cprover
|
Generates string constraints for string functions that return Boolean values. More...
#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_is_prefix (symbol_generatort &fresh_symbol, const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset) |
Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_is_prefix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool) |
Test if the target is a prefix of the string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_is_empty (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Add axioms stating that the returned value is true exactly when the argument string is empty. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_is_suffix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool) |
Test if the target is a suffix of the string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_contains (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Test whether a string contains another. More... | |
Generates string constraints for string functions that return Boolean values.
Definition in file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_contains | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Test whether a string contains another.
Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s0 refined_string s1 |
array_pool | pool of arrays representing strings |
contains
Definition at line 233 of file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_is_empty | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Add axioms stating that the returned value is true exactly when the argument string is empty.
string_length(s)==0
instead fresh_symbol | generator of fresh symbols |
f | function application with a string argument |
array_pool | pool of arrays representing strings |
Definition at line 126 of file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_is_prefix | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | prefix, | ||
const array_string_exprt & | str, | ||
const exprt & | offset | ||
) |
Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset.
These axioms are:
where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|
fresh_symbol | generator of fresh symbols |
prefix | an array of characters |
str | an array of characters |
offset | an integer |
isprefix
Definition at line 37 of file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_is_prefix | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
bool | swap_arguments, | ||
array_poolt & | array_pool | ||
) |
Test if the target is a prefix of the string.
Add axioms ensuring the return value is true when the string starts with the given target. These axioms are detailed here: string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string s0 , refined string s1 and optional integer argument offset whose default value is 0 |
swap_arguments | a Boolean telling whether the prefix is the second argument or the first argument |
array_pool | pool of arrays representing strings |
isprefix
Definition at line 99 of file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_is_suffix | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
bool | swap_arguments, | ||
array_poolt & | array_pool | ||
) |
Test if the target is a suffix of the string.
Add axioms ensuring the return value is true when the first string ends with the given target. These axioms are:
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string s0 and refined_string s1 |
swap_arguments | boolean flag telling whether the suffix is the second argument or the first argument |
array_pool | pool of arrays representing strings |
issuffix
Definition at line 168 of file string_constraint_generator_testing.cpp.