12 #ifndef CPROVER_UTIL_STRING_EXPR_H 13 #define CPROVER_UTIL_STRING_EXPR_H 122 const exprt &_length,
123 const exprt &_content,
178 return base.id() == ID_struct && base.operands().size() == 2;
183 INVARIANT(x.
id() == ID_struct,
"refined string exprs are struct");
186 x.
length().
type().
id() == ID_signedbv,
"length should be a signed int");
The type of an expression, extends irept.
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
A base class for relations, i.e., binary predicates.
const exprt & length() const
const exprt & content() const
exprt operator[](const exprt &i) const
Type for string expressions used by the string solver.
const exprt & content() const
typet & type()
Return the type of the expression.
bool can_cast_expr< refined_string_exprt >(const exprt &base)
friend refined_string_exprt & to_string_expr(exprt &expr)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const irep_idt & id() const
void validate_expr(const refined_string_exprt &x)
API to expression classes.
refined_string_exprt & to_string_expr(exprt &expr)
#define PRECONDITION(CONDITION)
const exprt & size() const
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
equal_exprt length_eq(const T &lhs, const exprt &rhs)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
const exprt & length() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
refined_string_exprt(const exprt &_length, const exprt &_content)
index_exprt operator[](int i) const
Struct constructor from list of elements.
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
array_string_exprt & to_array_string_expr(exprt &expr)