Go to the documentation of this file.
30 std::pair<exprt, string_constraintst>
79 return {tc_eq, std::move(constraints)};
134 std::pair<exprt, string_constraintst>
158 const exprt constr2 =
173 s1[witness],
s2[witness], char_a, char_A, char_Z);
174 const not_exprt witness_diff(witness_eq);
181 and_exprt(bound_witness, witness_diff)));
206 std::pair<exprt, string_constraintst>
255 const and_exprt cond1(ret_char_diff, guard1);
267 const and_exprt cond2(ret_length_diff, guard2);
283 return {res, std::move(constraints)};
const typet & subtype() const
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
The type of an expression, extends irept.
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,...
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
Expression to hold a symbol (variable)
bitvector_typet index_type()
typet & type()
Return the type of the expression.
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
#define PRECONDITION(CONDITION)
Application of (mathematical) function.
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
const irep_idt & id() const
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
bitvector_typet char_type()
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.
equal_exprt equal_to(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
static exprt character_equals_ignore_case(const exprt &char1, const exprt &char2, const exprt &char_a, const exprt &char_A, const exprt &char_Z)
Returns an expression which is true when the two given characters are equal when ignoring case for AS...
Semantic type conversion.
Generates string constraints to link results from string functions with their arguments.
std::vector< exprt > existential
std::vector< string_constraintt > universal