20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 65 const exprt &bound_inf,
66 const exprt &bound_sup,
69 exprt(ID_string_constraint)
78 const exprt &bound_sup,
92 const exprt &bound_sup,
107 assert(expr.
id()==ID_string_constraint && expr.
operands().size()==5);
113 assert(expr.
id()==ID_string_constraint && expr.
operands().size()==5);
124 exprt univ_lower_bound,
125 exprt univ_bound_sup,
127 exprt exists_bound_inf,
128 exprt exists_bound_sup,
131 exprt(ID_string_not_contains_constraint)
177 assert(expr.
id()==ID_string_not_contains_constraint);
185 assert(expr.
id()==ID_string_not_contains_constraint);
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_sup, const exprt &prem, const exprt &body)
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_sup, const exprt &body)
A generic base class for relations, i.e., binary predicates.
const exprt & univ_lower_bound() const
string_exprt & to_string_expr(exprt &expr)
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.
const symbol_exprt & univ_var() const
exprt univ_within_bounds() const
const exprt & upper_bound() const
const exprt & exists_lower_bound() const
const irep_idt & id() const
The boolean constant true.
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_inf, const exprt &bound_sup, const exprt &prem, const exprt &body)
const exprt & 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 string_exprt &s0, const string_exprt &s1)
const exprt & premise() const
const exprt & exists_upper_bound() const
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const exprt & univ_upper_bound() const
Expression to hold a symbol (variable)
Abstraction Refinement Loop.
const string_constraintt & to_string_constraint(const exprt &expr)
const exprt & premise() const
const exprt & body() const
const string_exprt & s0() const
const string_exprt & s1() const