Go to the documentation of this file.
34 const exprt &lower_bound,
35 const exprt &upper_bound,
37 : univ_var(_univ_var),
38 lower_bound(lower_bound),
39 upper_bound(upper_bound),
44 "String constraints must have non-negative lower bound.\n" +
48 "String constraints must have non-negative upper bound.\n" +
57 std::ostringstream out;
63 <<
"[x+y] != " <<
format(expr.
s1) <<
"[y])";
string_constraintt()=delete
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Base class for all expressions.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
Defines string constraints.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
int solver(std::istream &in)
A base class for relations, i.e., binary predicates whose two operands have the same type.
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be non-negative.
Constraints to encode non containement of strings.
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
null_message_handlert null_message_handler