Go to the documentation of this file.
37 std::pair<exprt, string_constraintst>
41 const exprt &from_index)
82 return {index, std::move(constraints)};
109 std::pair<exprt, string_constraintst>
113 const exprt &from_index)
176 return {offset, std::move(constraints)};
209 std::pair<exprt, string_constraintst>
213 const exprt &from_index)
280 return {offset, std::move(constraints)};
301 std::pair<exprt, string_constraintst>
308 const exprt &c = args[1];
312 const exprt from_index =
315 if(c.
type().
id() == ID_unsignedbv || c.
type().
id() == ID_signedbv)
325 "c can only be a (un)signedbv or a refined "
326 "string and the (un)signedbv case is already handled"));
355 std::pair<exprt, string_constraintst>
359 const exprt &from_index)
380 const plus_exprt from_index_plus_one(from_index, index1);
402 return {index, std::move(constraints)};
423 std::pair<exprt, string_constraintst>
430 const exprt c = args[1];
435 const exprt from_index =
438 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...
std::size_t size() const
Amount of nodes this expression tree contains.
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.
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
std::vector< string_constraintt > universal