40 const exprt &from_index)
109 const exprt &from_index)
201 const exprt &from_index)
286 const exprt &c=args[1];
290 const exprt from_index =
293 if(c.
type().
id()==ID_unsignedbv || c.
type().
id()==ID_signedbv)
303 "string and the (un)signedbv case is already handled"));
335 const exprt &from_index)
355 const plus_exprt from_index_plus_one(from_index, index1);
403 const exprt c = args[1];
408 const exprt from_index = args.size() == 2 ? str.length() : args[2];
410 if(c.
type().
id()==ID_unsignedbv || c.
type().
id()==ID_signedbv)
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
std::vector< string_not_contains_constraintt > not_contains_constraints
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_index_of(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...
#define INVARIANT(CONDITION, REASON)
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const irep_idt & id() const
Constraints to encode non containement of strings.
exprt::operandst argumentst
exprt add_axioms_for_index_of_string(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...
exprt add_axioms_for_last_index_of_string(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 nee...
#define PRECONDITION(CONDITION)
bitvector_typet index_type()
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.
bool is_refined_string_type(const typet &type)
#define string_refinement_invariantt(reason)
Universally quantified string constraint
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
const typet & subtype() const
std::vector< string_constraintt > constraints
bitvector_typet char_type()
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_last_index_of(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 ...