cprover
|
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
Go to the source code of this file.
Functions | |
std::pair< exprt, string_constraintst > | add_axioms_for_index_of (symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index) |
Add axioms stating that the returned value is the index within haystack (str ) of the first occurrence of needle (c ) starting the search at from_index , or is -1 if no such character occurs at or after position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) |
Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index , or -1 if needle does not occur at or after position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_last_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) |
Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Index of the first occurence of a target inside the string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index) |
Add axioms stating that the returned value is the index within haystack (str ) of the last occurrence of needle (c ) starting the search backward at from_index , or -1 if no such character occurs at or before position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Index of the last occurence of a target inside the string. More... | |
Generates string constraints for the family of indexOf and lastIndexOf java functions
Definition in file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_index_of | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | str, | ||
const exprt & | c, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value is the index within haystack
(str
) of the first occurrence of needle
(c
) starting the search at from_index
, or is -1
if no such character occurs at or after position from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
str | an array of characters expression |
c | a character expression |
from_index | an integer expression |
index
Definition at line 38 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_index_of | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Index of the first occurence of a target inside the string.
If the target is a character: Add axioms stating that the returned value is the index within haystack
(str
) of the first occurrence of needle
(c
) starting the search at from_index
, or is -1
if no such character occurs at or after position from_index
. (More...)
If the target is a refined_string: Add axioms stating that the returned value index
is the index within haystack
of the first occurrence of needle
starting the search at from_index
, or -1
if needle does not occur at or after position from_index
. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value 0 |
array_pool | pool of arrays representing strings |
Definition at line 291 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_index_of_string | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | haystack, | ||
const array_string_exprt & | needle, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value index
is the index within haystack
of the first occurrence of needle
starting the search at from_index
, or -1
if needle does not occur at or after position from_index
.
If needle is an empty string then the result is from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
haystack | an array of character expression |
needle | an array of character expression |
from_index | an integer expression |
index
representing the first index of needle
in haystack
Definition at line 111 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | str, | ||
const exprt & | c, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value is the index within haystack
(str
) of the last occurrence of needle
(c
) starting the search backward at from_index
, or -1
if no such character occurs at or before position from_index
.
These axioms are :
fresh_symbol | generator of fresh symbols |
str | an array of characters expression |
c | a character expression |
from_index | an integer expression |
index
representing the last index of needle
in haystack
before or at from_index
, or -1
if there is none Definition at line 346 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Index of the last occurence of a target inside the string.
If the target is a character: Add axioms stating that the returned value is the index within haystack
(str
) of the last occurrence of needle
(c
) starting the search backward at from_index
, or -1
if no such character occurs at or before position from_index
. (More...)
If the target is a refined_string: Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value |haystack|-1 |
array_pool | pool of arrays representing strings |
Definition at line 415 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | haystack, | ||
const array_string_exprt & | needle, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index.
If needle
is the empty string, the result is from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
haystack | an array of characters expression |
needle | an array of characters expression |
from_index | integer expression |
index
representing the last index of needle
in haystack
before or at from_index
, or -1 if there is none Definition at line 205 of file string_constraint_generator_indexof.cpp.