116 s1[qvar],
s2[qvar], char_a, char_A, char_Z);
133 and_exprt(bound_witness, witness_diff)));
151 std::map<irep_idt, string_exprt>::iterator it;
153 if(
hash.find(it->second)==
hash.end())
172 str.axiom_for_is_strictly_longer_than(i),
204 assert(return_type.
id()==ID_signedbv);
227 s1.axiom_for_is_strictly_longer_than(x)),
229 s2.axiom_for_is_strictly_longer_than(x)));
233 s1.axiom_for_has_length(x)),
235 s2.axiom_for_has_length(x)));
236 and_exprt cond2(ret_length_diff, guard2);
263 std::map<irep_idt, string_exprt>::iterator it;
265 if(
pool.find(it->second)==
pool.end())
290 not_exprt(str.axiom_for_has_same_length_as(it->second)),
292 str.axiom_for_has_same_length_as(it->second),
295 and_exprt(str.axiom_for_is_strictly_longer_than(i),
exprt add_axioms_for_compare_to(const function_application_exprt &f)
add axioms corresponding to the String.compareTo java function
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
application of (mathematical) function
exprt add_axioms_for_equals(const function_application_exprt &f)
add axioms stating that the result is true exactly when the strings represented by the arguments are ...
std::map< string_exprt, symbol_exprt > pool
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
std::map< irep_idt, string_exprt > symbol_to_string
const irep_idt & id() const
const exprt & length() const
exprt add_axioms_for_hash_code(const function_application_exprt &f)
add axioms stating that if two strings are equal then their hash codes are equals ...
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
symbol_exprt add_axioms_for_intern(const function_application_exprt &f)
add axioms stating that the return value for two equal string should be the same
std::list< exprt > axioms
std::map< string_exprt, symbol_exprt > hash
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
add axioms corresponding to the String.equalsIgnoreCase java function
bitvector_typet index_type()
The boolean constant false.
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
Base class for all expressions.
static exprt character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z)
returns an expression which is true when the two given characters are equal when ignoring case for AS...
Expression to hold a symbol (variable)
std::map< string_not_contains_constraintt, symbol_exprt > witness
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
bitvector_typet char_type()
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive