75 strings_differ_at_witness);
79 return {isprefix, std::move(constraints)};
113 args.size() == 2 ?
from_integer(0, s0.length().type()) : args[2];
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)`")
188 constraints.existential.push_back(a1);
196 constraints.universal.push_back(a2);
209 constraints.existential.push_back(a3);
210 return {tc_issuffix, std::move(constraints)};
248 constraints.existential.push_back(a1);
254 constraints.existential.push_back(a2);
259 constraints.existential.push_back(a3);
262 const plus_exprt qvar_shifted(qvar, startpos);
267 constraints.universal.push_back(a4);
277 constraints.not_contains.push_back(a5);
The type of an expression, extends irept.
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Semantic type conversion.
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Application of (mathematical) function.
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.
Generation of fresh symbols of a given type.
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.
typet & type()
Return the type of the expression.
exprt is_positive(const exprt &x)
Correspondance between arrays and pointers string representations.
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.
Collection of constraints of different types: existential formulas, universal formulas,...
const irep_idt & id() const
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...
Constraints to encode non containement of strings.
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
The plus expression Associativity is not specified.
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
bitvector_typet index_type()
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...
exprt maximum(const exprt &a, const exprt &b)
std::vector< exprt > existential
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Base class for all expressions.
std::vector< string_constraintt > universal
bool is_empty(const std::string &s)
Expression to hold a symbol (variable)