70 strings_differ_at_witness);
101 args.size() == 2 ?
from_integer(0, s0.length().type()) : args[2];
110 DEPRECATED(
"should use `string_length(s)==0` instead")
147 DEPRECATED(
"should use `strings_startwith(s0, s1, s1.length - s0.length)`")
162 lemmas.push_back(a1);
170 constraints.push_back(a2);
176 s0.axiom_for_length_gt(
s1.length()),
181 s0.axiom_for_length_gt(witness),
182 axiom_for_is_positive_index(witness))));
185 lemmas.push_back(a3);
235 const plus_exprt qvar_shifted(qvar, startpos);
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
std::vector< string_not_contains_constraintt > not_contains_constraints
A generic base class for relations, i.e., binary predicates.
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
application of (mathematical) function
equal_exprt axiom_for_has_length(const exprt &rhs) const
exprt add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
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
const irep_idt & id() const
Constraints to encode non containement of strings.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
bitvector_typet index_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.
exprt add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
bool is_empty(const std::string &s)
Universally quantified string constraint
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
std::vector< string_constraintt > constraints
std::map< string_not_contains_constraintt, symbol_exprt > witness
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive