40 const exprt &from_index)
110 const exprt &from_index)
202 const exprt &from_index)
287 const exprt &c=args[1];
291 const exprt from_index =
294 if(c.
type().
id()==ID_unsignedbv || c.
type().
id()==ID_signedbv)
304 "string and the (un)signedbv case is already handled"));
336 const exprt &from_index)
356 const plus_exprt from_index_plus_one(from_index, index1);
404 const exprt c = args[1];
409 const exprt from_index = args.size() == 2 ? str.length() : args[2];
411 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()
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
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)
exprt add_axioms_for_index_of(const function_application_exprt &f)
Index of the first occurence of a target inside the string.
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 ...