20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H 41 assert((_mode==ID_java) || (_mode==ID_C));
58 std::map<string_not_contains_constraintt, symbol_exprt>
witness;
62 const exprt &univ_val)
const 194 const exprt &from_index);
203 const exprt &from_index);
215 const exprt &from_index);
221 const exprt &from_index);
234 const exprt &f,
bool double_precision=
false);
296 assert(
args.size()==nb);
307 std::map<string_exprt, symbol_exprt>
pool;
310 std::map<string_exprt, symbol_exprt>
hash;
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.
string_exprt add_axioms_for_insert_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(C) java function
string_exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
string_exprt add_axioms_from_literal(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the string literal ...
exprt add_axioms_for_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt &offset)
add axioms stating that the returned expression is true exactly when the first string is a prefix of ...
string_exprt add_axioms_for_java_char_array(const exprt &char_array)
add axioms corresponding to the String.valueOf([C) java function
void assign_to_symbol(const symbol_exprt &sym, const string_exprt &expr)
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
string_exprt add_axioms_for_concat_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(D) java function
std::list< symbol_exprt > boolean_symbols
string_exprt add_axioms_for_delete(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string corresponds to the input one where we removed characters ...
string_exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
application of (mathematical) function
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt add_axioms_for_concat_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(I) java 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 ...
exprt add_axioms_for_length(const function_application_exprt &f)
add axioms corresponding to the String.length java function
std::map< string_exprt, symbol_exprt > pool
Type for string expressions used by the string solver.
const irep_idt & get_identifier() const
string_exprt add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
string_exprt add_axioms_for_insert_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(F) java function
string_exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
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
exprt add_axioms_for_contains(const function_application_exprt &f)
add axioms corresponding to the String.contains java function
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.codePointCount java function ...
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function...
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
string_exprt add_axioms_from_double(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(D) java function
string_exprt add_axioms_for_insert_long(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(J) java function
The trinary if-then-else operator.
const std::size_t MAX_INTEGER_LENGTH
string_exprt add_axioms_from_long(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(J) java function
const std::size_t MAX_LONG_LENGTH
string_exprt add_axioms_for_trim(const function_application_exprt &expr)
add axioms corresponding to the String.trim java function
A constant literal expression.
exprt add_axioms_for_is_empty(const function_application_exprt &f)
add axioms stating that the returned value is true exactly when the argument string is empty ...
exprt add_axioms_for_last_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
string_exprt add_axioms_for_empty_string(const function_application_exprt &f)
add axioms to say that the returned string expression is empty
string_exprt add_axioms_for_if(const if_exprt &expr)
add axioms for an if expression which should return a string
string_exprt add_axioms_for_concat_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(F) java function
exprt add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
add axioms that the returned value is either -1 or greater than from_index and the character at that ...
exprt add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
void set_mode(irep_idt _mode)
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
string_exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
std::map< irep_idt, string_exprt > symbol_to_string
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
string_exprt add_axioms_for_char_set(const function_application_exprt &expr)
add axioms corresponding stating that the result is similar to that of the StringBuilder.setCharAt java function Warning: this may be underspecified in the case wher the index exceed the length of the string
string_exprt add_axioms_for_concat_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(Z) java function
Defines string constraints.
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_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
exprt::operandst argumentst
string_exprt add_axioms_for_value_of(const function_application_exprt &f)
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions ...
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
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
string_exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
exprt add_axioms_for_parse_int(const function_application_exprt &f)
add axioms corresponding to the Integer.parseInt java function
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
add axioms corresponding to the String.isSuffix java function
string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym)
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding st...
string_constraint_generatort()
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
string_exprt add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset)
add axioms stating that the result correspond to the first string where we inserted the second one at...
const std::size_t MAX_FLOAT_LENGTH
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
exprt is_high_surrogate(const exprt &chr) const
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en...
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
String expressions for the string solver.
exprt add_axioms_for_to_char_array(const function_application_exprt &f)
add axioms corresponding to the String.toCharArray java function
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
void set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str)
add a correspondence to make sure the symbol points to the same string as the second argument ...
string_exprt add_axioms_for_constant(irep_idt sval, const refined_string_typet &ref_type)
add axioms saying the returned string expression should be equal to the string constant ...
string_exprt add_axioms_for_to_lower_case(const function_application_exprt &expr)
add axioms corresponding to the String.toLowerCase java function
exprt add_axioms_for_char_at(const function_application_exprt &f)
add axioms stating that the character of the string at the given position is equal to the returned va...
Base class for all expressions.
exprt is_low_surrogate(const exprt &chr) const
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en...
const std::size_t MAX_DOUBLE_LENGTH
string_exprt add_axioms_for_to_upper_case(const function_application_exprt &expr)
add axioms corresponding to the String.toUpperCase java function
string_exprt add_axioms_for_set_length(const function_application_exprt &f)
add axioms to say that the returned string expression has length given by the second argument and who...
exprt int_of_hex_char(const exprt &chr) const
returns the value represented by the character
std::list< symbol_exprt > index_symbols
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
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...
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
string_exprt add_axioms_for_replace(const function_application_exprt &f)
add axioms corresponding to the String.replace java function
Expression to hold a symbol (variable)
string_exprt add_axioms_from_int_hex(const exprt &i, const refined_string_typet &ref_type)
add axioms stating that the returned string corresponds to the integer argument written in hexadecima...
string_exprt add_axioms_for_concat_long(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.append(J) java function.
string_exprt add_axioms_for_concat_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(C) java function
static unsigned next_symbol_id
exprt add_axioms_for_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
add axioms stating that the returned value is either -1 or greater than from_index and the string beg...
std::map< string_not_contains_constraintt, symbol_exprt > witness
string_exprt add_axioms_for_code_point(const exprt &code_point, const refined_string_typet &ref_type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
bitvector_typet char_type()
string_exprt add_axioms_for_insert_char_array(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java func...
static irep_idt extract_java_string(const symbol_exprt &s)
extract java string from symbol expression when they are encoded inside the symbol name ...
string_exprt add_axioms_from_char_array(const function_application_exprt &f)
add axioms corresponding to the String.
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive
string_exprt add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string expression is equal to the input one starting at start an...