Go to the documentation of this file.
40 std::pair<exprt, string_constraintst>
44 const exprt &from_index)
85 return {index, std::move(constraints)};
112 std::pair<exprt, string_constraintst>
116 const exprt &from_index)
179 return {offset, std::move(constraints)};
212 std::pair<exprt, string_constraintst>
216 const exprt &from_index)
283 return {offset, std::move(constraints)};
304 std::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"));
358 std::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)};
426 std::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)
const typet & length_type() const
const typet & subtype() const
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...
The type of an expression, extends irept.
The trinary if-then-else operator.
symbol_generatort fresh_symbol
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
The plus expression Associativity is not specified.
Base class for all expressions.
Collection of constraints of different types: existential formulas, universal formulas,...
Expression to hold a symbol (variable)
bitvector_typet index_type()
exprt::operandst argumentst
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...
typet & type()
Return the type of the expression.
#define PRECONDITION(CONDITION)
Application of (mathematical) function.
const irep_idt & id() const
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 ...
bitvector_typet char_type()
#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 whose two operands have the same type.
bool is_refined_string_type(const typet &type)
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
std::vector< string_not_contains_constraintt > not_contains
Constraints to encode non containement of strings.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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...
Semantic type conversion.
Generates string constraints to link results from string functions with their arguments.
std::vector< exprt > existential
API to expression classes for 'mathematical' expressions.
std::vector< string_constraintt > universal