add_axioms_for_char_at(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_char_literal(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_char_set(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_code_point(const exprt &code_point, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_for_code_point_at(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_code_point_before(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_code_point_count(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_compare_to(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2) | string_constraint_generatort | private |
add_axioms_for_concat(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_bool(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_code_point(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_double(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_float(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_concat_long(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_constant(irep_idt sval, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_for_contains(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_copy(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_delete(const string_exprt &str, const exprt &start, const exprt &end) | string_constraint_generatort | private |
add_axioms_for_delete(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_delete_char_at(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_empty_string(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_equals(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_equals_ignore_case(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_function_application(const function_application_exprt &expr) | string_constraint_generatort | |
add_axioms_for_hash_code(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_if(const if_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_index_of(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset) | string_constraint_generatort | private |
add_axioms_for_insert(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_bool(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_char_array(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_double(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_float(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_insert_long(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_intern(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_is_empty(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt &offset) | string_constraint_generatort | private |
add_axioms_for_is_prefix(const function_application_exprt &f, bool swap_arguments=false) | string_constraint_generatort | private |
add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false) | string_constraint_generatort | private |
add_axioms_for_java_char_array(const exprt &char_array) | string_constraint_generatort | private |
add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_last_index_of(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_last_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index) | string_constraint_generatort | private |
add_axioms_for_length(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_offset_by_code_point(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_parse_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_replace(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_set_length(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_string_expr(const exprt &expr) | string_constraint_generatort | |
add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end) | string_constraint_generatort | private |
add_axioms_for_substring(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_to_char_array(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_for_to_lower_case(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_to_upper_case(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_trim(const function_application_exprt &expr) | string_constraint_generatort | private |
add_axioms_for_value_of(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_bool(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_bool(const exprt &i, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_from_char(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_char(const exprt &i, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_from_char_array(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_char_array(const exprt &length, const exprt &data, const exprt &offset, const exprt &count) | string_constraint_generatort | private |
add_axioms_from_double(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_float(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_float(const exprt &f, bool double_precision=false) | string_constraint_generatort | private |
add_axioms_from_int(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_int(const exprt &i, size_t max_size, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_from_int_hex(const exprt &i, const refined_string_typet &ref_type) | string_constraint_generatort | private |
add_axioms_from_int_hex(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_literal(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_long(const function_application_exprt &f) | string_constraint_generatort | private |
add_axioms_from_long(const exprt &i, size_t max_size) | string_constraint_generatort | private |
args(const function_application_exprt &expr, size_t nb) | string_constraint_generatort | inlineprivatestatic |
assign_to_symbol(const symbol_exprt &sym, const string_exprt &expr) | string_constraint_generatort | inline |
axiom_for_is_positive_index(const exprt &x) | string_constraint_generatort | private |
axioms | string_constraint_generatort | |
boolean_symbols | string_constraint_generatort | |
character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z) | string_constraint_generatort | privatestatic |
constant_char(int i, const typet &char_type) | string_constraint_generatort | static |
extract_java_string(const symbol_exprt &s) | string_constraint_generatort | privatestatic |
find_or_add_string_of_symbol(const symbol_exprt &sym) | string_constraint_generatort | |
fresh_boolean(const irep_idt &prefix) | string_constraint_generatort | |
fresh_exist_index(const irep_idt &prefix, const typet &type) | string_constraint_generatort | |
fresh_string(const refined_string_typet &type) | string_constraint_generatort | |
fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet()) | string_constraint_generatort | static |
fresh_univ_index(const irep_idt &prefix, const typet &type) | string_constraint_generatort | |
get_mode() | string_constraint_generatort | inline |
get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const | string_constraint_generatort | inline |
hash | string_constraint_generatort | private |
index_symbols | string_constraint_generatort | |
int_of_hex_char(const exprt &chr) const | string_constraint_generatort | private |
is_high_surrogate(const exprt &chr) const | string_constraint_generatort | private |
is_low_surrogate(const exprt &chr) const | string_constraint_generatort | private |
MAX_DOUBLE_LENGTH | string_constraint_generatort | private |
MAX_FLOAT_LENGTH | string_constraint_generatort | private |
MAX_INTEGER_LENGTH | string_constraint_generatort | private |
MAX_LONG_LENGTH | string_constraint_generatort | private |
mode | string_constraint_generatort | private |
next_symbol_id | string_constraint_generatort | static |
pool | string_constraint_generatort | private |
set_mode(irep_idt _mode) | string_constraint_generatort | inline |
set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str) | string_constraint_generatort | |
string_constraint_generatort() | string_constraint_generatort | inline |
symbol_to_string | string_constraint_generatort | |
witness | string_constraint_generatort | |