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.
std::vector< exprt > existential
std::vector< string_constraintt > universal