20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 119 std::ostringstream out;
135 exprt univ_bound_sup,
137 exprt exists_bound_inf,
138 exprt exists_bound_sup,
141 :
exprt(ID_string_not_contains_constraint)
191 std::ostringstream out;
197 <<
"[x+y] != " <<
format(expr.
s1()) <<
"[y])";
string_constraintt(symbol_exprt _univ_var, exprt lower_bound, exprt upper_bound, exprt body)
A generic base class for relations, i.e., binary predicates.
const exprt & univ_lower_bound() const
string_not_contains_constraintt(exprt univ_lower_bound, exprt univ_bound_sup, exprt premise, exprt exists_bound_inf, exprt exists_bound_sup, const array_string_exprt &s0, const array_string_exprt &s1)
const string_not_contains_constraintt & to_string_not_contains_constraint(const exprt &expr)
void copy_to_operands(const exprt &expr)
Type for string expressions used by the string solver.
void replace_expr(union_find_replacet &replace_map)
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
exprt univ_within_bounds() const
const exprt & exists_lower_bound() const
const irep_idt & id() const
Constraints to encode non containement of strings.
#define PRECONDITION(CONDITION)
const exprt & premise() const
string_constraintt()=delete
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
String expressions for the string solver.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
const exprt & exists_upper_bound() const
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define string_refinement_invariantt(reason)
Universally quantified string constraint
const exprt & univ_upper_bound() const
Expression to hold a symbol (variable)
Abstraction Refinement Loop.
#define DATA_INVARIANT(CONDITION, REASON)
const array_string_exprt & s0() const
array_string_exprt & to_array_string_expr(exprt &expr)
const array_string_exprt & s1() const