Go to the documentation of this file.
104 const exprt &i = args[3];
105 const exprt j = args.size() == 5 ? args[4] : str.
length();
238 str[index_before], ID_gt, space_char);
262 if((expr1.
type().
id()==ID_unsignedbv
263 || expr1.
type().
id()==ID_char)
264 && (expr2.
type().
id()==ID_char
265 || expr2.
type().
id()==ID_unsignedbv))
266 return std::make_pair(expr1, expr2);
269 const auto expr1_length = numeric_cast<std::size_t>(expr1_str.length());
270 const auto expr2_length = numeric_cast<std::size_t>(expr2_str.length());
271 if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
272 return std::make_pair(
exprt(expr1_str[0]),
exprt(expr2_str[0]));
308 const auto maybe_chars =
310 return get_string_expr(array_pool, e);
313 const auto old_char=maybe_chars->first;
314 const auto new_char=maybe_chars->second;
#define PRECONDITION(CONDITION)
const typet & subtype() const
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
equal_exprt length_eq(const T &lhs, const exprt &rhs)
exprt minimum(const exprt &a, const exprt &b)
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
The plus expression Associativity is not specified.
Base class for all expressions.
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Collection of constraints of different types: existential formulas, universal formulas,...
Expression to hold a symbol (variable)
bitvector_typet index_type()
exprt::operandst argumentst
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
typet & type()
Return the type of the expression.
Generation of fresh symbols of a given type.
exprt maximum(const exprt &a, const exprt &b)
Application of (mathematical) function.
const irep_idt & id() const
nonstd::optional< T > optionalt
signedbv_typet get_return_code_type()
bitvector_typet char_type()
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
A base class for relations, i.e., binary predicates.
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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 fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
std::vector< exprt > existential
std::vector< string_constraintt > universal