12 #ifndef CPROVER_UTIL_STRING_EXPR_H 13 #define CPROVER_UTIL_STRING_EXPR_H 21 template <
typename child_t>
27 return static_cast<child_t *
>(
this)->
length();
31 return static_cast<const child_t *
>(
this)->
length();
35 return static_cast<child_t *
>(
this)->
content();
39 return static_cast<const child_t *
>(
this)->
content();
64 const exprt &rhs)
const 71 const exprt &rhs)
const 95 const exprt &rhs)
const 113 const exprt &rhs)
const 189 const exprt &_length,
190 const exprt &_content,
247 return base.id() == ID_struct && base.operands().size() == 2;
252 INVARIANT(x.
id() == ID_struct,
"refined string exprs are struct");
The type of an expression.
static exprt within_bounds(const exprt &idx, const exprt &bound)
A generic base class for relations, i.e., binary predicates.
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
binary_relation_exprt axiom_for_length_gt(const string_exprt &rhs) const
const exprt & content() const
const exprt & length() const
const exprt & content() const
void copy_to_operands(const exprt &expr)
Type for string expressions used by the string solver.
equal_exprt axiom_for_has_length(const exprt &rhs) const
const exprt & content() const
const exprt & length() const
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)
binary_relation_exprt axiom_for_length_ge(const exprt &rhs) const
const irep_idt & id() const
equal_exprt axiom_for_has_length(mp_integer i) const
binary_relation_exprt axiom_for_length_le(mp_integer i) const
void validate_expr(const refined_string_exprt &x)
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
API to expression classes.
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
binary_relation_exprt axiom_for_length_lt(const exprt &rhs) const
refined_string_exprt & to_string_expr(exprt &expr)
#define PRECONDITION(CONDITION)
const exprt & size() const
binary_relation_exprt axiom_for_length_lt(const string_exprt &rhs) const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
const exprt & length() const
binary_relation_exprt axiom_for_length_le(const exprt &rhs) const
refined_string_exprt(const typet &type)
binary_relation_exprt axiom_for_length_gt(mp_integer i) const
refined_string_exprt(const exprt &_length, const exprt &_content)
struct constructor from list of elements
array_string_exprt & to_array_string_expr(exprt &expr)
exprt operator[](const exprt &i) const