20 satcheck_no_simplifiert sat_check;
32 const exprt &lower_bound,
33 const exprt &upper_bound,
35 : univ_var(_univ_var),
36 lower_bound(lower_bound),
37 upper_bound(upper_bound),
42 "String constraints must have non-negative lower bound.\n" +
46 "String constraints must have non-negative upper bound.\n" +
55 std::ostringstream out;
61 <<
"[x+y] != " <<
format(expr.
s1) <<
"[y])";
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be.
A base class for relations, i.e., binary predicates.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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)
typet & type()
Return the type of the expression.
Defines string constraints.
int solver(std::istream &in)
Constraints to encode non containement of strings.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
string_constraintt()=delete
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Base class for all expressions.
Expression to hold a symbol (variable)