40std::pair<exprt, string_constraintst>
44 const exprt &from_index)
85 return {index, std::move(constraints)};
112std::pair<exprt, string_constraintst>
116 const exprt &from_index)
179 return {offset, std::move(constraints)};
212std::pair<exprt, string_constraintst>
216 const exprt &from_index)
283 return {offset, std::move(constraints)};
304std::pair<exprt, string_constraintst>
311 const exprt &c = args[1];
315 const exprt from_index =
318 if(c.
type().
id() == ID_unsignedbv || c.
type().
id() == ID_signedbv)
328 "c can only be a (un)signedbv or a refined "
329 "string and the (un)signedbv case is already handled"));
358std::pair<exprt, string_constraintst>
362 const exprt &from_index)
383 const plus_exprt from_index_plus_one(from_index, index1);
405 return {index, std::move(constraints)};
426std::pair<exprt, string_constraintst>
433 const exprt c = args[1];
438 const exprt from_index =
441 if(c.
type().
id() == ID_unsignedbv || c.
type().
id() == ID_signedbv)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
bitvector_typet index_type()
bitvector_typet char_type()
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const typet & length_type() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
typet & type()
Return the type of the expression.
Application of (mathematical) function.
exprt::operandst argumentst
The trinary if-then-else operator.
const irep_idt & id() const
The plus expression Associativity is not specified.
std::pair< exprt, string_constraintst > 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 ...
std::pair< exprt, string_constraintst > 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...
std::pair< exprt, string_constraintst > 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...
std::pair< exprt, string_constraintst > 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...
symbol_generatort fresh_symbol
Expression to hold a symbol (variable)
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
API to expression classes for 'mathematical' expressions.
bool is_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Generates string constraints to link results from string functions with their arguments.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
#define string_refinement_invariantt(reason)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.
const type_with_subtypet & to_type_with_subtype(const typet &type)