36 axioms.push_back(res.axiom_for_has_length(k));
65 assert(args.size()>=2);
75 assert(args.size()==2);
105 res.axiom_for_has_length(
minus_exprt(end, start)));
303 res.axiom_for_has_same_length_as(str)));
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.
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
const typet & get_char_type() const
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
string_exprt add_axioms_for_trim(const function_application_exprt &expr)
add axioms corresponding to the String.trim java function
binary_relation_exprt axiom_for_is_shorter_than(const string_exprt &rhs) const
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
const exprt & length() const
exprt::operandst argumentst
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)
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...
std::list< exprt > axioms
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
const typet & get_index_type() const
bitvector_typet index_type()
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
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
string_exprt add_axioms_for_to_lower_case(const function_application_exprt &expr)
add axioms corresponding to the String.toLowerCase java function
Base class for all expressions.
const exprt & content() const
Operator to update elements in structs and arrays.
string_exprt add_axioms_for_to_upper_case(const function_application_exprt &expr)
add axioms corresponding to the String.toUpperCase java function
bool is_empty(const std::string &s)
binary_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
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...
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)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
bitvector_typet char_type()
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...