48 constraints.existential.push_back(
52 constraints.universal.push_back([&] {
61 constraints.existential.push_back([&] {
75 return {tc_eq, std::move(constraints)};
140 const symbol_exprt eq = fresh_symbol(
"equal_ignore_case");
150 constraints.existential.push_back(a1);
153 const exprt constr2 =
157 constraints.universal.push_back(a2);
160 fresh_symbol(
"witness_unequal_ignore_case",
index_type);
166 s1[witness],
s2[witness], char_a, char_A, char_Z);
167 const not_exprt witness_diff(witness_eq);
172 and_exprt(bound_witness, witness_diff)));
173 constraints.existential.push_back(a3);
189 std::pair<exprt, string_constraintst>
202 std::make_pair(str,
fresh_symbol(
"hash", return_type)));
203 const exprt hash = pair.first->second;
252 const symbol_exprt res = fresh_symbol(
"compare_to", return_type);
257 constraints.existential.push_back(a1);
264 constraints.universal.push_back(a2);
279 const and_exprt cond1(ret_char_diff, guard1);
283 const and_exprt cond2(ret_length_diff, guard2);
290 constraints.existential.push_back(a3);
297 constraints.universal.push_back(a4);
299 return {res, std::move(constraints)};
318 const typet &return_type=f.type();
321 auto pair=intern_of_string.insert(
322 std::make_pair(str, fresh_symbol(
"pool", return_type)));
331 for(
auto it : intern_of_string)
333 constraints.existential.push_back(
disjunction(disj));
336 for(
auto it : intern_of_string)
340 constraints.existential.push_back(
or_exprt(
351 return {intern, std::move(constraints)};
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::map< array_string_exprt, exprt > hash_code_of_string
Generation of fresh symbols of a given type.
typet & type()
Return the type of the expression.
exprt is_positive(const exprt &x)
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
std::pair< exprt, string_constraintst > add_axioms_for_equals(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content of two strings.
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...
#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_compare_to(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Lexicographic comparison of two strings.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< exprt > operandst
string_constraintst constraints
std::vector< exprt > existential
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content ignoring case of characters.
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Base class for all expressions.
Universally quantified string constraint
Expression to hold a symbol (variable)
const typet & subtype() const
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
std::pair< exprt, string_constraintst > add_axioms_for_hash_code(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Value that is identical for strings with the same content.
bitvector_typet char_type()
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...
symbol_generatort fresh_symbol