19 #ifndef CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H 20 #define CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H 86 assert(type.
id()==ID_struct);
The type of an expression.
static bool is_java_string_pointer_type(const typet &type)
const typet & get_char_type() const
static bool is_java_string_builder_type(const typet &type)
Deprecated expression utility functions.
static bool is_java_char_sequence_type(const typet &type)
static bool is_c_string_type(const typet &type)
const componentst & components() const
A constant literal expression.
const array_typet & get_content_type() const
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
static bool is_java_string_type(const typet &type)
static bool is_unrefined_string_type(const typet &type)
const refined_string_typet & to_refined_string_type(const typet &type)
API to expression classes.
static bool is_unrefined_string(const exprt &expr)
const exprt & size() const
const typet & get_index_type() const
bitvector_typet index_type()
Base class for all expressions.
constant_exprt index_of_int(int i) const
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()