75 const exprt &from_index)
113 const exprt &from_index)
161 else if(
args.size()==3)
246 else if(
args.size()==3)
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.
static bool is_java_string_pointer_type(const typet &type)
application of (mathematical) function
const typet & get_char_type() const
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
exprt add_axioms_for_last_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
exprt add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
add axioms that the returned value is either -1 or greater than from_index and the character at that ...
exprt add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const exprt & length() const
exprt::operandst argumentst
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
std::list< exprt > axioms
const typet & get_index_type() const
bitvector_typet index_type()
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
Base class for all expressions.
Expression to hold a symbol (variable)
exprt add_axioms_for_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
add axioms stating that the returned value is either -1 or greater than from_index and the string beg...
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)