Go to the documentation of this file.
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);
#define PRECONDITION(CONDITION)
const typet & subtype() const
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 ...
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
The plus expression Associativity is not specified.
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Collection of constraints of different types: existential formulas, universal formulas,...
Expression to hold a symbol (variable)
bitvector_typet index_type()
exprt::operandst argumentst
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.
Application of (mathematical) function.
const irep_idt & id() const
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...
bitvector_typet char_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...
#define string_refinement_invariantt(reason)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
A base class for relations, i.e., binary predicates.
bool is_refined_string_type(const typet &type)
std::vector< string_not_contains_constraintt > not_contains
Constraints to encode non containement of strings.
Semantic type conversion.
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...
std::vector< exprt > existential
std::vector< string_constraintt > universal