51 lemmas.push_back(res.axiom_for_has_length(k));
95 const exprt &i = args[3];
96 const exprt j = args.size() == 5 ? args[4] : str.length();
184 exprt a3=str.axiom_for_length_ge(idx);
187 exprt a4=res.axiom_for_length_ge(
191 exprt a5 = res.axiom_for_length_le(str.length());
218 str[index_before], ID_gt, space_char);
292 if_exprt conditional_convert(is_upper_case, converted, non_converted);
434 if((expr1.
type().
id()==ID_unsignedbv
435 || expr1.
type().
id()==ID_char)
436 && (expr2.
type().
id()==ID_char
437 || expr2.
type().
id()==ID_unsignedbv))
438 return std::make_pair(expr1, expr2);
439 const auto expr1_str = get_string_expr(expr1);
440 const auto expr2_str = get_string_expr(expr2);
441 const auto expr1_length =
numeric_cast<std::size_t>(expr1_str.length());
442 const auto expr2_length =
numeric_cast<std::size_t>(expr2_str.length());
443 if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
444 return std::make_pair(
exprt(expr1_str[0]),
exprt(expr2_str[0]));
475 const auto maybe_chars =
480 const auto old_char=maybe_chars->first;
481 const auto new_char=maybe_chars->second;
543 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
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_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_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
exprt::operandst argumentst
const refined_string_typet & to_refined_string_type(const typet &type)
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.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
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.
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(st...
Base class for all expressions.
Universally quantified string constraint
exprt add_axioms_for_to_lower_case(const function_application_exprt &f)
Conversion of a string to lower case.
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...
exprt add_axioms_for_to_upper_case(const function_application_exprt &f)
Conversion of a string to upper case.