51 lemmas.push_back(res.axiom_for_has_length(k));
97 const exprt &i = args[3];
98 const exprt j = args.size() == 5 ? args[4] : str.length();
188 exprt a3=str.axiom_for_length_ge(idx);
191 exprt a4=res.axiom_for_length_ge(
195 exprt a5 = res.axiom_for_length_le(str.length());
222 str[index_before], ID_gt, space_char);
257 upper_case.push_back(
264 upper_case.push_back(
273 upper_case.push_back(
317 const exprt conditional_convert = [&] {
360 const exprt converted =
424 const exprt &position,
425 const exprt &character)
467 if((expr1.
type().
id()==ID_unsignedbv
468 || expr1.
type().
id()==ID_char)
469 && (expr2.
type().
id()==ID_char
470 || expr2.
type().
id()==ID_unsignedbv))
471 return std::make_pair(expr1, expr2);
472 const auto expr1_str = get_string_expr(expr1);
473 const auto expr2_str = get_string_expr(expr2);
474 const auto expr1_length =
numeric_cast<std::size_t>(expr1_str.length());
475 const auto expr2_length =
numeric_cast<std::size_t>(expr2_str.length());
476 if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
477 return std::make_pair(
exprt(expr1_str[0]),
exprt(expr2_str[0]));
508 const auto maybe_chars =
513 const auto old_char=maybe_chars->first;
514 const auto new_char=maybe_chars->second;
577 const exprt return_code2 =
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
application of (mathematical) function
const signedbv_typet get_return_code_type()
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
The trinary if-then-else operator.
exprt add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr)
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 s...
exprt add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
exprt minimum(const exprt &a, const exprt &b)
const irep_idt & id() const
exprt add_axioms_for_to_lower_case(const array_string_exprt &res, const array_string_exprt &str)
Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lower...
exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
exprt::operandst argumentst
Fixed-width bit-vector with two's complement interpretation.
exprt add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
exprt add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
bitvector_typet index_type()
exprt add_axioms_for_char_set(const function_application_exprt &f)
Set a character to a specific value at an index of the string.
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
exprt maximum(const exprt &a, const exprt &b)
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
exprt add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
exprt add_axioms_for_substring(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(star...
Base class for all expressions.
exprt add_axioms_for_set_char(const array_string_exprt &res, const array_string_exprt &str, const exprt &position, const exprt &character)
Add axioms ensuring that the result res is similar to input string str where the character at index p...
Universally quantified string constraint
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
std::vector< string_constraintt > constraints
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
bitvector_typet char_type()
exprt add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...