81 else if(args.size()==3)
116 assert(args.size()==2);
141 qvar, s0.length(), issuffix,
equal_exprt(s0[qvar], s1[qvar_shifted]));
148 s0.axiom_for_is_strictly_longer_than(s1),
152 s0.axiom_for_is_strictly_longer_than(witness),
The type of an expression.
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 ...
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_contains(const function_application_exprt &f)
add axioms corresponding to the String.contains java function
equal_exprt axiom_for_has_length(const exprt &rhs) 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
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 ...
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const irep_idt & id() const
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 ...
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
add axioms corresponding to the String.isSuffix java function
std::list< exprt > axioms
bitvector_typet index_type()
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
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.
bool is_empty(const std::string &s)
binary_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
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)
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive