Go to the documentation of this file.
75 strings_differ_at_witness);
79 return {isprefix, std::move(constraints)};
125 DEPRECATED(
"should use `string_length(s)==0` instead")
139 std::vector<exprt> constraints;
167 DEPRECATED(
"should use `strings_startwith(s0, s1, s1.length - s0.length)`")
210 return {tc_issuffix, std::move(constraints)};
262 const plus_exprt qvar_shifted(qvar, startpos);
#define PRECONDITION(CONDITION)
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
equal_exprt length_eq(const T &lhs, const exprt &rhs)
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
The plus expression Associativity is not specified.
Base class for all expressions.
Collection of constraints of different types: existential formulas, universal formulas,...
std::pair< exprt, string_constraintst > add_axioms_for_contains(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Test whether a string contains another.
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.
bool is_empty(const std::string &s)
Generation of fresh symbols of a given type.
exprt maximum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(symbol_generatort &fresh_symbol, const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
Application of (mathematical) function.
const irep_idt & id() const
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms stating that the returned value is true exactly when the argument string is empty.
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
Test if the target is a suffix of the string.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
exprt is_positive(const exprt &x)
A base class for relations, i.e., binary predicates.
std::vector< string_not_contains_constraintt > not_contains
Constraints to encode non containement of strings.
Semantic type conversion.
std::vector< exprt > existential
std::vector< string_constraintt > universal