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" +
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be.
A generic base class for relations, i.e., binary predicates.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
#define INVARIANT(CONDITION, REASON)
Defines string constraints.
int solver(std::istream &in)
string_constraintt()=delete
Base class for all expressions.
Expression to hold a symbol (variable)