20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H 111 std::ostringstream out;
A base class for relations, i.e., binary predicates.
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 the representative element of the set they belong to...
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
exprt univ_within_bounds() const
Constraints to encode non containement of strings.
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...
size_t operator()(const string_not_contains_constraintt &constraint) const
Base class for all expressions.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Universally quantified string constraint
Expression to hold a symbol (variable)
Abstraction Refinement Loop.