10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
65 {std::move(_op0), std::move(_op1), std::move(_op2)})
106 set(ID_identifier, identifier);
111 return get(ID_identifier);
143 return get_bool(ID_C_static_lifetime);
148 return set(ID_C_static_lifetime,
true);
153 remove(ID_C_static_lifetime);
163 return set(ID_C_thread_local,
true);
168 remove(ID_C_thread_local);
175 return base.
id() == ID_symbol;
234 set(ID_identifier, identifier);
239 return get(ID_identifier);
246 return base.
id() == ID_nondet_symbol;
356 return base.
id() == ID_abs;
393 :
unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
406 return base.
id() == ID_unary_minus;
450 return base.
id() == ID_unary_plus;
517 return base.
id() == ID_sign;
558 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
569 "binary expression must have two operands");
666 expr.
type().
id() == ID_bool,
667 "result of binary predicate expression should be of type bool");
701 expr_binary.op0().type() == expr_binary.op1().type(),
702 "lhs and rhs of binary relation expression should have same type");
730 return base.
id() == ID_gt;
751 return base.
id() == ID_ge;
772 return base.
id() == ID_lt;
793 return base.
id() == ID_le;
838 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
939 return base.
id() == ID_plus;
976 :
binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
984 return base.
id() == ID_minus;
1030 return base.
id() == ID_mult;
1067 :
binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1099 return base.
id() == ID_div;
1138 :
binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1146 return base.
id() == ID_mod;
1182 :
binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
1190 return base.
id() == ID_euclidean_mod;
1251 return base.
id() == ID_equal;
1294 return base.
id() == ID_notequal;
1331 :
binary_exprt(_array, ID_index, std::move(_index), _array.
type().subtype())
1368 return base.
id() == ID_index;
1405 :
unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1433 return base.
id() == ID_array_of;
1488 return base.
id() == ID_array;
1516 :
multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1540 return base.
id() == ID_array_list;
1577 return base.
id() == ID_vector;
1605 :
unary_exprt(ID_union, std::move(_value), std::move(_type))
1612 return get(ID_component_name);
1617 set(ID_component_name, component_name);
1627 set_size_t(ID_component_number, component_number);
1634 return base.
id() == ID_union;
1682 return base.
id() == ID_struct;
1742 return base.
id() == ID_complex;
1786 return base.
id() == ID_complex_real;
1792 expr, 1,
"real part retrieval operation must have one operand");
1831 return base.
id() == ID_complex_imag;
1837 expr, 1,
"imaginary part retrieval operation must have one operand");
1886 return base.
id() == ID_typecast;
1930 {std::move(
op0), std::move(
op1), std::move(
op2)},
1938 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
1958 return base.
id() == ID_and;
1970 return static_cast<const and_exprt &
>(expr);
1994 return base.
id() == ID_implies;
2038 {std::move(
op0), std::move(
op1), std::move(
op2)},
2046 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
2066 return base.
id() == ID_or;
2078 return static_cast<const or_exprt &
>(expr);
2085 return static_cast<or_exprt &
>(expr);
2102 return base.
id() == ID_xor;
2114 return static_cast<const xor_exprt &
>(expr);
2138 return base.
id() == ID_not;
2223 return base.
id() == ID_if;
2264 {_old, std::move(_where), std::move(_new_value)})
2302 return base.
id() == ID_with;
2308 value, 3,
"array/structure update must have at least 3 operands",
true);
2311 "array/structure update must have an odd number of operands");
2359 return base.
id() == ID_index_designator;
2396 set(ID_component_name, _component_name);
2401 return get(ID_component_name);
2408 return base.
id() == ID_member_designator;
2448 std::move(_designator),
2449 std::move(_new_value),
2492 return base.
id() == ID_update;
2498 value, 3,
"Array/structure update must have three operands");
2531 const exprt &_array,
2532 const exprt &_index,
2533 const exprt &_new_value):
2534 exprt(ID_array_update, _array.type())
2549 const exprt &array()
const
2559 const exprt &index()
const
2569 const exprt &new_value()
const
2575 template<>
inline bool can_cast_expr<array_update_exprt>(
const exprt &base)
2577 return base.
id()==ID_array_update;
2591 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
2594 const array_update_exprt &ret =
static_cast<const array_update_exprt &
>(expr);
2600 inline array_update_exprt &to_array_update_expr(
exprt &expr)
2603 array_update_exprt &ret =
static_cast<array_update_exprt &
>(expr);
2629 return get(ID_component_name);
2634 set(ID_component_name, component_name);
2671 "member expression must have one operand");
2683 return base.
id() == ID_member;
2727 return base.
id() == ID_type;
2763 return get(ID_value);
2768 set(ID_value, value);
2777 return base.
id() == ID_constant;
2831 return base.
id() == ID_nil;
2899 binding_expr, 2,
"Binding expressions must have two operands");
2911 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda);
3029 return base.
id() == ID_let;
3087 return base.
id() == ID_cond;
3093 value.
operands().size() % 2 == 0,
"cond must have even number of operands");
3135 ID_array_comprehension,
3180 return base.
id() == ID_array_comprehension;
3245 set(ID_identifier, std::move(
id));
3257 return get(ID_component_name);
3265 return get(ID_C_class);
3272 return get(ID_C_base_name);
3280 return get(ID_identifier);
3289 "class method descriptor must have a mangled method name.");
3291 !value.
class_id().
empty(),
"class method descriptor must have a class id.");
3294 "class method descriptor must have a base method name.");
3298 "class method descriptor must have an identifier in the expected format.");
3320 return base.
id() == ID_virtual_function;
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
and_exprt(exprt op0, exprt op1, exprt op2)
and_exprt(exprt op0, exprt op1)
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
and_exprt(exprt::operandst _operands)
Expression to define a mapping from an argument (index) to elements.
const exprt & body() const
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
const array_typet & type() const
const symbol_exprt & arg() const
Array constructor from list of elements.
array_exprt(operandst _operands, array_typet _type)
const array_typet & type() const
Array constructor from a list of index-element pairs Operands are index/value pairs,...
void add(exprt index, exprt value)
add an index/value pair
const array_typet & type() const
array_list_exprt(operandst _operands, array_typet _type)
Array constructor from single element.
const exprt & what() const
array_of_exprt(exprt _what, array_typet _type)
const array_typet & type() const
A base class for binary expressions.
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & lhs() const
const exprt & rhs() const
const exprt & op2() const =delete
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
const exprt & op3() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
A base class for relations, i.e., binary predicates whose two operands have the same type.
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
A base class for variable bindings (quantifiers, let, lambda)
const exprt & where() const
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
const variablest & variables() const
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
std::vector< symbol_exprt > variablest
An expression describing a method on a class.
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Complex constructor from a pair of numbers.
const exprt & imag() const
const exprt & real() const
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Imaginary part of the expression describing a complex number.
complex_imag_exprt(const exprt &op)
Real part of the expression describing a complex number.
complex_real_exprt(const exprt &op)
Complex numbers made of pair of given subtype.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
cond_exprt(operandst _operands, typet _type)
A constant literal expression.
const irep_idt & get_value() const
bool value_is_zero_string() const
constant_exprt(const irep_idt &_value, typet _type)
void set_value(const irep_idt &value)
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
void clear_thread_local()
decorated_symbol_exprt(const irep_idt &identifier, typet type)
void set_static_lifetime()
bool is_static_lifetime() const
bool is_thread_local() const
void clear_static_lifetime()
div_exprt(exprt _lhs, exprt _rhs)
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
exprt & dividend()
The dividend of a division is the number that is being divided.
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
const exprt & dividend() const
The dividend of a division is the number that is being divided.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
equal_exprt(exprt _lhs, exprt _rhs)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
euclidean_mod_exprt(exprt _lhs, exprt _rhs)
Base class for all expressions.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
Binary greater than operator expression.
greater_than_exprt(exprt _lhs, exprt _rhs)
Binary greater than or equal operator expression.
greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
The trinary if-then-else operator.
const exprt & false_case() const
if_exprt(exprt cond, const exprt &t, exprt f)
const exprt & true_case() const
const exprt & cond() const
if_exprt(exprt cond, exprt t, exprt f, typet type)
implies_exprt(exprt op0, exprt op1)
index_designatort(exprt _index)
const exprt & index() const
index_exprt(exprt _array, exprt _index, typet _type)
const exprt & index() const
index_exprt(const exprt &_array, exprt _index)
const exprt & array() const
An expression denoting infinity.
infinity_exprt(typet _type)
std::size_t get_size_t(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
void set_size_t(const irep_namet &name, const std::size_t value)
bool get_bool(const irep_namet &name) const
const irep_idt & id() const
void remove(const irep_namet &name)
const irep_idt & get(const irep_namet &name) const
Binary less than operator expression.
less_than_exprt(exprt _lhs, exprt _rhs)
Binary less than or equal operator expression.
less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
const binding_exprt & binding() const
exprt & where()
convenience accessor for binding().where()
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
const operandst & values() const
static void validate(const exprt &, validation_modet)
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
exprt & value()
convenience accessor for the value of a single binding
binding_exprt & binding()
const exprt & value() const
convenience accessor for the value of a single binding
const exprt & where() const
convenience accessor for binding().where()
irep_idt get_component_name() const
member_designatort(const irep_idt &_component_name)
Extract member of struct or union.
const exprt & compound() const
const exprt & struct_op() const
irep_idt get_component_name() const
void set_component_name(const irep_idt &component_name)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
member_exprt(exprt op, const irep_idt &component_name, typet _type)
std::size_t get_component_number() const
member_exprt(exprt op, const struct_typet::componentt &c)
minus_exprt(exprt _lhs, exprt _rhs)
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
mod_exprt(exprt _lhs, exprt _rhs)
Binary multiplication Associativity is not specified.
mult_exprt(exprt _lhs, exprt _rhs)
A base class for multi-ary expressions Associativity is not specified.
const exprt & op0() const
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
const exprt & op3() const
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
const exprt & op1() const
const exprt & op2() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a nondeterministic choice.
void set_identifier(const irep_idt &identifier)
nondet_symbol_exprt(const irep_idt &identifier, typet type)
const irep_idt & get_identifier() const
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
notequal_exprt(exprt _lhs, exprt _rhs)
An expression without operands.
void move_to_operands(exprt &, exprt &)=delete
const operandst & operands() const =delete
operandst & operands()=delete
remove all operand methods
nullary_exprt(const irep_idt &_id, typet _type)
const exprt & op0() const =delete
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
void move_to_operands(exprt &)=delete
void copy_to_operands(const exprt &expr)=delete
void copy_to_operands(const exprt &, const exprt &)=delete
void move_to_operands(exprt &, exprt &, exprt &)=delete
const exprt & op3() const =delete
const exprt & op1() const =delete
const exprt & op2() const =delete
or_exprt(exprt op0, exprt op1, exprt op2)
or_exprt(exprt::operandst _operands)
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
or_exprt(exprt op0, exprt op1)
The plus expression Associativity is not specified.
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
plus_exprt(exprt _lhs, exprt _rhs)
plus_exprt(operandst _operands, typet _type)
A base class for expressions that are predicates, i.e., Boolean-typed.
predicate_exprt(const irep_idt &_id)
Sign of an expression Predicate is true if _op is negative, false otherwise.
Struct constructor from list of elements.
exprt & component(const irep_idt &name, const namespacet &ns)
struct_exprt(operandst _operands, typet _type)
const irep_idt & get_name() const
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
symbol_exprt(const irep_idt &identifier, typet type)
const irep_idt & get_identifier() const
An expression with three operands.
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
const exprt & op3() const =delete
The Boolean constant true.
An expression denoting a type.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
typecast_exprt(exprt op, typet _type)
The type of an expression, extends irept.
Generic base class for unary expressions.
const exprt & op1() const =delete
unary_exprt(const irep_idt &_id, const exprt &_op)
const exprt & op3() const =delete
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
const exprt & op2() const =delete
The unary minus expression.
unary_minus_exprt(exprt _op)
unary_minus_exprt(exprt _op, typet _type)
The unary plus expression.
unary_plus_exprt(exprt op)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Union constructor from single element.
std::size_t get_component_number() const
void set_component_number(std::size_t component_number)
void set_component_name(const irep_idt &component_name)
irep_idt get_component_name() const
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Operator to update elements in structs and arrays.
exprt::operandst & designator()
const exprt & new_value() const
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
const exprt & old() const
const exprt::operandst & designator() const
Vector constructor from list of elements.
vector_exprt(operandst _operands, vector_typet _type)
Operator to update elements in structs and arrays.
const exprt & new_value() const
const exprt & old() const
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
const exprt & where() const
xor_exprt(exprt _op0, exprt _op1)
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const irept & get_nil_irep()
dstring_hash irep_id_hash
const std::string & id2string(const irep_idt &d)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
bool can_cast_expr< equal_exprt >(const exprt &base)
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
bool can_cast_expr< notequal_exprt >(const exprt &base)
bool can_cast_expr< complex_exprt >(const exprt &base)
bool can_cast_expr< not_exprt >(const exprt &base)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
bool can_cast_expr< typecast_exprt >(const exprt &base)
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
bool can_cast_expr< struct_exprt >(const exprt &base)
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
bool can_cast_expr< xor_exprt >(const exprt &base)
bool can_cast_expr< mult_exprt >(const exprt &base)
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
bool can_cast_expr< if_exprt >(const exprt &base)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
bool can_cast_expr< member_designatort >(const exprt &base)
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
bool can_cast_expr< abs_exprt >(const exprt &base)
bool can_cast_expr< sign_exprt >(const exprt &base)
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
bool can_cast_expr< type_exprt >(const exprt &base)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
void validate_expr(const symbol_exprt &value)
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
bool can_cast_expr< less_than_exprt >(const exprt &base)
const array_list_exprt & to_array_list_expr(const exprt &expr)
bool can_cast_expr< with_exprt >(const exprt &base)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
bool can_cast_expr< minus_exprt >(const exprt &base)
bool can_cast_expr< let_exprt >(const exprt &base)
bool can_cast_expr< plus_exprt >(const exprt &base)
bool can_cast_expr< array_of_exprt >(const exprt &base)
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
bool can_cast_expr< constant_exprt >(const exprt &base)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool can_cast_expr< index_exprt >(const exprt &base)
bool can_cast_expr< symbol_exprt >(const exprt &base)
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
bool can_cast_expr< member_exprt >(const exprt &base)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
bool can_cast_expr< or_exprt >(const exprt &base)
bool can_cast_expr< mod_exprt >(const exprt &base)
bool can_cast_expr< cond_exprt >(const exprt &base)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
bool can_cast_expr< update_exprt >(const exprt &base)
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
bool can_cast_expr< vector_exprt >(const exprt &base)
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
bool can_cast_expr< array_list_exprt >(const exprt &base)
bool can_cast_expr< index_designatort >(const exprt &base)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
bool can_cast_expr< and_exprt >(const exprt &base)
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
bool can_cast_expr< greater_than_exprt >(const exprt &base)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
bool can_cast_expr< array_exprt >(const exprt &base)
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
bool can_cast_expr< binary_exprt >(const exprt &base)
bool can_cast_expr< div_exprt >(const exprt &base)
bool can_cast_expr< nil_exprt >(const exprt &base)
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
bool can_cast_expr< implies_exprt >(const exprt &base)
bool can_cast_expr< unary_exprt >(const exprt &base)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
bool can_cast_expr< union_exprt >(const exprt &base)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
bool can_cast_expr< complex_real_exprt >(const exprt &base)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
size_t operator()(const ::symbol_exprt &sym)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...