12#ifndef CPROVER_UTIL_STRING_EXPR_H
13#define CPROVER_UTIL_STRING_EXPR_H
177 x.length().type().id() ==
ID_signedbv,
"length should be a signed int");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
exprt operator[](const exprt &i) const
const exprt & content() const
const typet & length_type() const
index_exprt operator[](int i) const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
const exprt & length() const
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
refined_string_exprt(const exprt &_length, const exprt &_content)
const exprt & content() const
friend refined_string_exprt & to_string_expr(exprt &expr)
Struct constructor from list of elements.
The type of an expression, extends irept.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Type for string expressions used by the string solver.
bool is_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
binary_relation_exprt less_than(exprt lhs, exprt rhs)
void validate_expr(const refined_string_exprt &x)
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
array_string_exprt & to_array_string_expr(exprt &expr)
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
refined_string_exprt & to_string_expr(exprt &expr)
equal_exprt equal_to(exprt lhs, exprt rhs)
bool can_cast_expr< refined_string_exprt >(const exprt &base)