42 const exprt &from_index)
47 symbol_exprt contains = fresh_symbol(
"contains_in_index_of");
83 return {index, std::move(constraints)};
115 const exprt &from_index)
120 symbol_exprt contains = fresh_symbol(
"contains_substring");
171 return {offset, std::move(constraints)};
209 const exprt &from_index)
214 symbol_exprt contains = fresh_symbol(
"contains_substring");
268 return {offset, std::move(constraints)};
299 const exprt &c=args[1];
303 const exprt from_index =
306 if(c.
type().
id()==ID_unsignedbv || c.
type().
id()==ID_signedbv)
316 "string and the (un)signedbv case is already handled"));
350 const exprt &from_index)
355 const symbol_exprt contains = fresh_symbol(
"contains_in_last_index_of");
371 const plus_exprt from_index_plus_one(from_index, index1);
392 return {index, std::move(constraints)};
423 const exprt c = args[1];
428 const exprt from_index = args.size() == 2 ? str.length() : args[2];
430 if(c.
type().
id()==ID_unsignedbv || c.
type().
id()==ID_signedbv)
439 fresh_symbol, str, sub, from_index);
The type of an expression, extends irept.
Semantic type conversion.
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Application of (mathematical) function.
Generation of fresh symbols of a given type.
std::pair< exprt, string_constraintst > add_axioms_for_index_of_string(symbol_generatort &fresh_symbol, 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...
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of_string(symbol_generatort &fresh_symbol, 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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const irep_idt & id() const
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...
Constraints to encode non containement of strings.
std::vector< string_not_contains_constraintt > not_contains
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
The plus expression Associativity is not specified.
bitvector_typet index_type()
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, 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 ...
std::vector< exprt > existential
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Base class for all expressions.
bool is_refined_string_type(const typet &type)
std::vector< string_constraintt > universal
#define string_refinement_invariantt(reason)
Universally quantified string constraint
std::pair< exprt, string_constraintst > add_axioms_for_index_of(symbol_generatort &fresh_symbol, 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...
Expression to hold a symbol (variable)
const typet & subtype() const
bitvector_typet char_type()