10 #ifndef CPROVER_UTIL_STD_EXPR_H 11 #define CPROVER_UTIL_STD_EXPR_H 62 "Transition systems must have three operands");
63 return static_cast<const transt &
>(expr);
74 "Transition systems must have three operands");
75 return static_cast<transt &
>(expr);
80 return base.id()==ID_trans;
125 set(ID_identifier, identifier);
130 return get(ID_identifier);
171 return get_bool(ID_C_static_lifetime);
176 return set(ID_C_static_lifetime,
true);
181 remove(ID_C_static_lifetime);
191 return set(ID_C_thread_local,
true);
196 remove(ID_C_thread_local);
229 return base.id()==ID_symbol;
255 set(ID_identifier, identifier);
260 return get(ID_identifier);
293 return base.id()==ID_nondet_symbol;
365 "Unary expressions must have one operand");
376 "Unary expressions must have one operand");
382 return base.operands().size()==1;
416 "Absolute value must have one operand");
417 return static_cast<const abs_exprt &
>(expr);
428 "Absolute value must have one operand");
434 return base.id()==ID_abs;
479 "Unary minus must have one operand");
491 "Unary minus must have one operand");
497 return base.id()==ID_unary_minus;
528 set(ID_bits_per_byte, bits_per_byte);
547 expr.
op0().
type() == expr.
type(),
"bswap type must match operand type");
559 expr.
op0().
type() == expr.
type(),
"bswap type must match operand type");
566 return base.id() == ID_bswap;
572 value.
op().
type() == value.
type(),
"bswap type must match operand type");
706 "Binary expressions must have two operands");
717 "Binary expressions must have two operands");
723 return base.operands().size()==2;
807 "Binary relations must have two operands");
818 "Binary relations must have two operands");
931 "Plus must have two or more operands");
943 "Plus must have two or more operands");
949 return base.id()==ID_plus;
989 "Minus must have two or more operands");
1001 "Minus must have two or more operands");
1007 return base.id()==ID_minus;
1047 "Multiply must have two or more operands");
1048 return static_cast<const mult_exprt &
>(expr);
1059 "Multiply must have two or more operands");
1065 return base.id()==ID_mult;
1105 "Divide must have two operands");
1106 return static_cast<const div_exprt &
>(expr);
1117 "Divide must have two operands");
1123 return base.id()==ID_div;
1162 return static_cast<const mod_exprt &
>(expr);
1177 return base.id()==ID_mod;
1216 return static_cast<const rem_exprt &
>(expr);
1231 return base.id()==ID_rem;
1285 return base.id()==ID_power;
1325 "Factorial power must have two operands");
1337 "Factorial power must have two operands");
1344 return base.id()==ID_factorial_power;
1396 return base.id()==ID_equal;
1434 "Inequality must have two operands");
1446 "Inequality must have two operands");
1452 return base.id()==ID_notequal;
1479 const exprt &_array,
1480 const exprt &_index,
1481 const typet &_type):
1522 "Array index must have two operands");
1534 "Array index must have two operands");
1540 return base.id()==ID_index;
1589 "'Array of' must have one operand");
1601 "'Array of' must have one operand");
1607 return base.id()==ID_array_of;
1625 exprt(ID_array, _type)
1657 return base.id()==ID_array;
1666 :
exprt(ID_array_list, _type)
1674 return base.id() == ID_array_list;
1692 exprt(ID_vector, _type)
1724 return base.id()==ID_vector;
1744 const exprt &_value,
1745 const typet &_type):
1753 return get(ID_component_name);
1758 set(ID_component_name, component_name);
1768 set(ID_component_number, component_number);
1787 "Union constructor must have one operand");
1799 "Union constructor must have one operand");
1805 return base.id()==ID_union;
1823 exprt(ID_struct, _type)
1855 return base.id()==ID_struct;
1915 "Complex constructor must have two operands");
1927 "Complex constructor must have two operands");
1933 return base.id()==ID_complex;
1950 op0().
id(ID_unknown);
1951 op1().
id(ID_unknown);
1970 while(p->
id()==ID_member || p->
id()==ID_index)
2006 "Object descriptor must have two operands");
2018 "Object descriptor must have two operands");
2025 return base.id()==ID_object_descriptor;
2040 op0().
id(ID_unknown);
2041 op1().
id(ID_unknown);
2047 op0().
id(ID_unknown);
2048 op1().
id(ID_unknown);
2082 "Dynamic object must have two operands");
2094 "Dynamic object must have two operands");
2100 return base.id()==ID_dynamic_object;
2148 "Typecast must have one operand");
2160 "Typecast must have one operand");
2166 return base.id()==ID_typecast;
2185 const exprt &rounding,
2226 "Float typecast must have two operands");
2238 "Float typecast must have two operands");
2245 return base.id()==ID_floatbv_typecast;
2312 return static_cast<const and_exprt &
>(expr);
2329 return base.id()==ID_and;
2381 return base.id()==ID_implies;
2448 return static_cast<const or_exprt &
>(expr);
2460 return static_cast<or_exprt &
>(expr);
2465 return base.id()==ID_or;
2501 return static_cast<const xor_exprt &
>(expr);
2515 return base.id()==ID_xor;
2573 return base.id()==ID_bitnot;
2630 return base.id()==ID_bitor;
2690 return base.id()==ID_bitxor;
2751 return base.id()==ID_bitand;
2785 const std::size_t _distance);
2822 "Shifts must have two operands");
2833 "Shifts must have two operands");
2963 "Bit-wise replication must have two operands");
2975 "Bit-wise replication must have two operands");
2981 return base.id()==ID_replication;
3006 const std::size_t _index);
3044 "Extract bit must have two operands");
3056 "Extract bit must have two operands");
3062 return base.id()==ID_extractbit;
3083 const exprt &_upper,
3084 const exprt &_lower,
3085 const typet &_type):
exprt(ID_extractbits, _type)
3092 const std::size_t _upper,
3093 const std::size_t _lower,
3094 const typet &_type);
3142 "Extract bits must have three operands");
3154 "Extract bits must have three operands");
3160 return base.id()==ID_extractbits;
3220 return base.id()==ID_address_of;
3258 return static_cast<const not_exprt &
>(expr);
3273 return base.id()==ID_not;
3333 "Dereference must have one operand");
3345 "Dereference must have one operand");
3351 return base.id()==ID_dereference;
3431 "If-then-else must have three operands");
3432 return static_cast<const if_exprt &
>(expr);
3443 "If-then-else must have three operands");
3444 return static_cast<if_exprt &
>(expr);
3449 return base.id()==ID_if;
3466 const exprt &_where,
3467 const exprt &_new_value):
3524 "Array/structure update must have three operands");
3525 return static_cast<const with_exprt &
>(expr);
3536 "Array/structure update must have three operands");
3542 return base.id()==ID_with;
3549 "Array/structure update must have three operands");
3557 exprt(ID_index_designator)
3588 "Index designator must have one operand");
3600 "Index designator must have one operand");
3606 return base.id()==ID_index_designator;
3618 exprt(ID_member_designator)
3620 set(ID_component_name, _component_name);
3625 return get(ID_component_name);
3644 "Member designator must not have operands");
3656 "Member designator must not have operands");
3662 return base.id()==ID_member_designator;
3677 const exprt &_designator,
3678 const exprt &_new_value):
3685 exprt(ID_update, _type)
3693 op1().
id(ID_designator);
3746 "Array/structure update must have three operands");
3758 "Array/structure update must have three operands");
3764 return base.id()==ID_update;
3771 "Array/structure update must have three operands");
3778 class array_update_exprt:
public exprt 3782 const exprt &_array,
3783 const exprt &_index,
3784 const exprt &_new_value):
3785 exprt(ID_array_update, _array.type())
3790 array_update_exprt():
exprt(ID_array_update)
3800 const exprt &array()
const 3810 const exprt &index()
const 3820 const exprt &new_value()
const 3836 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
3841 "Array update must have three operands");
3842 return static_cast<const array_update_exprt &
>(expr);
3848 inline array_update_exprt &to_array_update_expr(
exprt &expr)
3853 "Array update must have three operands");
3854 return static_cast<array_update_exprt &
>(expr);
3857 template<>
inline bool can_cast_expr<array_update_exprt>(
const exprt &base)
3859 return base.id()==ID_array_update;
3877 const typet &_type):
3897 return get(ID_component_name);
3902 set(ID_component_name, component_name);
3936 if(
op.
id()==ID_member)
3960 "Extract member must have one operand");
3972 "Extract member must have one operand");
3978 return base.id()==ID_member;
4030 return base.id()==ID_isnan;
4068 "Is infinite must have one operand");
4080 "Is infinite must have one operand");
4086 return base.id()==ID_isinf;
4138 return base.id()==ID_isfinite;
4190 return base.id()==ID_isnormal;
4228 "IEEE equality must have two operands");
4240 "IEEE equality must have two operands");
4247 return base.id()==ID_ieee_float_equal;
4287 "IEEE inequality must have two operands");
4299 "IEEE inequality must have two operands");
4306 return base.id()==ID_ieee_float_notequal;
4379 "IEEE float operations must have three arguments");
4390 "IEEE float operations must have three arguments");
4436 exprt(ID_constant, _type)
4443 return get(ID_value);
4448 set(ID_value, value);
4482 return base.id()==ID_constant;
4549 function()=_function;
4591 "Function application must have two operands");
4603 "Function application must have two operands");
4610 return base.id()==ID_function_application;
4633 exprt(ID_concatenation, _type)
4639 exprt(ID_concatenation, _type)
4678 return base.id()==ID_concatenation;
4698 exprt(ID_infinity, _type)
4759 return static_cast<const let_exprt &
>(expr);
4774 return base.id()==ID_let;
4794 const exprt &_where)
4833 "quantifier expressions must have two operands");
4843 "quantifier expressions must have two operands");
4849 return base.id() == ID_forall || base.id() == ID_exists;
4855 "quantifier expressions must have two operands");
4938 return base.id() == ID_popcount;
4945 #endif // CPROVER_UTIL_STD_EXPR_H const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
bool can_cast_expr< rem_exprt >(const exprt &base)
const irept & get_nil_irep()
const transt & to_trans_expr(const exprt &expr)
Cast a generic exprt to a transt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_equal_exprt.
const irep_idt & get_name() const
bitnot_exprt(const exprt &op)
bool can_cast_expr< update_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
The type of an expression.
bool can_cast_expr< implies_exprt >(const exprt &base)
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
bool can_cast_expr< isnormal_exprt >(const exprt &base)
const symbol_exprt & symbol() const
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
unary_minus_exprt(const exprt &_op, const typet &_type)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast a generic exprt to a bswap_exprt.
or_exprt(const exprt &op0, const exprt &op1)
const exprt & rhs() const
ieee_float_notequal_exprt()
bool can_cast_expr< mult_exprt >(const exprt &base)
binary_exprt(const irep_idt &_id)
bool can_cast_expr< quantifier_exprt >(const exprt &base)
bool can_cast_expr< bitnot_exprt >(const exprt &base)
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
A generic base class for relations, i.e., binary predicates.
const exprt & value() const
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
const exprt & lhs() const
shift_exprt(const irep_idt &_id, const typet &_type)
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast a generic exprt to a bitand_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
application of (mathematical) function
binary_predicate_exprt(const irep_idt &_id)
void set_identifier(const irep_idt &identifier)
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
bool can_cast_expr< typecast_exprt >(const exprt &base)
index_exprt(const exprt &_array, const exprt &_index)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
bool can_cast_expr< transt >(const exprt &base)
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
complex_exprt(const complex_typet &_type)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Operator to update elements in structs and arrays.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const exprt & pointer() const
Evaluates to true if the operand is infinite.
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
address_of_exprt(const exprt &op)
bool can_cast_expr< with_exprt >(const exprt &base)
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
unsigned int get_instance() const
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast a generic exprt to a bitxor_exprt.
const exprt & real() const
const exprt & array() const
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
unary_predicate_exprt(const irep_idt &_id)
void copy_to_operands(const exprt &expr)
bool can_cast_expr< array_of_exprt >(const exprt &base)
const irep_idt & get_identifier() const
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
exprt::operandst & designator()
shift_exprt(const irep_idt &_id)
const irep_idt & get_value() const
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
The null pointer constant.
An expression denoting a type.
abs_exprt(const exprt &_op)
bool can_cast_expr< member_designatort >(const exprt &base)
type_exprt(const typet &type)
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast a generic exprt to a bitor_exprt.
A transition system, consisting of state invariant, initial state predicate, and transition predicate...
bool is_thread_local() const
const exprt & root_object() const
The trinary if-then-else operator.
std::size_t get_component_number() const
Evaluates to true if the operand is a normal number.
const symbol_exprt & symbol() const
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
bool can_cast_expr< bitand_exprt >(const exprt &base)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
const exprt & where() const
bool can_cast_expr< array_list_exprt >(const exprt &base)
const exprt & where() const
A constant literal expression.
bool can_cast_expr< mod_exprt >(const exprt &base)
function_application_exprt(const symbol_exprt &_function, const typet &_type)
bool can_cast_expr< and_exprt >(const exprt &base)
bool get_bool(const irep_namet &name) const
bool can_cast_expr< index_designatort >(const exprt &base)
const exprt & index() const
symbol_exprt(const typet &type)
Constructor.
const exprt & where() const
irep_idt get_component_name() const
index_exprt(const typet &_type)
bool value_is_zero_string() const
void set_bits_per_byte(std::size_t bits_per_byte)
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_notequal_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
void set_component_number(std::size_t component_number)
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
vector_exprt(const vector_typet &_type)
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Extract member of struct or union.
const exprt & imag() const
const exprt & rounding_mode() const
bool can_cast_expr< not_exprt >(const exprt &base)
void set_instance(unsigned int instance)
Concatenation of bit-vector operands.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast a generic exprt to an notequal_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< plus_exprt >(const exprt &base)
bool can_cast_expr< div_exprt >(const exprt &base)
Templated functions to cast to specific exprt-derived classes.
update_exprt(const typet &_type)
constant_exprt(const irep_idt &_value, const typet &_type)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
void set_component_name(const irep_idt &component_name)
bool can_cast_expr< function_application_exprt >(const exprt &base)
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_op_exprt.
exprt conjunction(const exprt::operandst &)
const exprt & compound() const
replication_exprt(const typet &_type)
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
decorated_symbol_exprt(const irep_idt &identifier)
Constructor.
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
const irep_idt & id() const
unary_exprt(const irep_idt &_id)
dereference_exprt(const exprt &op, const typet &type)
popcount_exprt(const exprt &_op)
void set_value(const irep_idt &value)
const exprt & times() const
Evaluates to true if the operand is NaN.
bool can_cast_expr< isnan_exprt >(const exprt &base)
An expression denoting infinity.
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
bool can_cast_expr< minus_exprt >(const exprt &base)
The boolean constant true.
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Expression to hold a symbol (variable)
division (integer and real)
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
A generic base class for binary expressions.
function_application_exprt(const typet &_type)
const exprt & invar() const
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast a generic exprt to a concatenation_exprt.
const exprt & distance() const
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
const irep_idt & get_identifier() const
const vector_exprt & to_vector_expr(const exprt &expr)
Cast a generic exprt to an vector_exprt.
exprt::operandst argumentst
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
unary_minus_exprt(const exprt &_op)
IEEE floating-point disequality.
bool can_cast_expr< member_exprt >(const exprt &base)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
member_exprt(const exprt &op, const struct_typet::componentt &c)
bool can_cast_expr< vector_exprt >(const exprt &base)
Operator to dereference a pointer.
A constant-size array type.
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
bool can_cast_expr< complex_exprt >(const exprt &base)
union constructor from single element
std::size_t get_component_number() const
factorial_power_exprt(const exprt &_base, const exprt &_exp)
bool can_cast_expr< binary_exprt >(const exprt &base)
const exprt & new_value() const
popcount_exprt(const exprt &_op, const typet &_type)
not_exprt(const exprt &op)
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast a generic exprt to a isinf_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
const exprt & lhs() const
and_exprt(const exprt &op0, const exprt &op1)
binary_exprt(const irep_idt &_id, const typet &_type)
Generic base class for unary expressions.
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
infinity_exprt(const typet &_type)
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
bool can_cast_expr< union_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
const exprt & what() const
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
predicate_exprt(const irep_idt &_id, const exprt &_op)
unary_exprt(const irep_idt &_id, const exprt &_op)
#define PRECONDITION(CONDITION)
const exprt & false_case() const
typecast_exprt(const typet &_type)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
bool can_cast_expr< extractbits_exprt >(const exprt &base)
lshr_exprt(const exprt &_src, const std::size_t _distance)
split an expression into a base object and a (byte) offset
const exprt & cond() const
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
bool can_cast_expr< constant_exprt >(const exprt &base)
symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
const symbol_exprt & symbol() const
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
symbol_exprt(const irep_idt &identifier)
Constructor.
null_pointer_exprt(const pointer_typet &type)
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
void set_static_lifetime()
array constructor from single element
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast a generic exprt to a quantifier_exprt.
bool can_cast_expr< xor_exprt >(const exprt &base)
multi_ary_exprt(const irep_idt &_id)
exprt disjunction(const exprt::operandst &)
bool can_cast_expr< abs_exprt >(const exprt &base)
power_exprt(const exprt &_base, const exprt &_exp)
isfinite_exprt(const exprt &op)
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
vector constructor from list of elements
const exprt & old() const
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast a generic exprt to a isfinite_exprt.
bool can_cast_expr< or_exprt >(const exprt &base)
bool can_cast_expr< dereference_exprt >(const exprt &base)
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
The unary minus expression.
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
implies_exprt(const exprt &op0, const exprt &op1)
predicate_exprt(const irep_idt &_id)
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
bool has_operands() const
const exprt & index() const
bool can_cast_expr< address_of_exprt >(const exprt &base)
The boolean constant false.
const exprt & init() const
bool can_cast_expr< replication_exprt >(const exprt &base)
const exprt & rhs() const
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
decorated_symbol_exprt(const typet &type)
Constructor.
equal_exprt(const exprt &_lhs, const exprt &_rhs)
void validate_expr(const transt &value)
const exprt & trans() const
static exprt conditional_cast(const exprt &expr, const typet &type)
const xor_exprt & to_xor_expr(const exprt &expr)
Cast a generic exprt to a xor_exprt.
std::vector< exprt > operandst
const exprt::operandst & designator() const
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
bool can_cast_expr< notequal_exprt >(const exprt &base)
constant_exprt(const typet &type)
void clear_thread_local()
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
const exprt & object() const
multi_ary_exprt(const irep_idt &_id, const typet &_type)
const power_exprt & to_power_expr(const exprt &expr)
Cast a generic exprt to a power_exprt.
minus_exprt(const exprt &_lhs, const exprt &_rhs)
index_designatort(const exprt &_index)
Complex numbers made of pair of given subtype.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
dynamic_object_exprt(const typet &type)
typecast_exprt(const exprt &op, const typet &_type)
const exprt & old() const
const exprt & object() const
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast a generic exprt to a isnan_exprt.
unary_exprt(const irep_idt &_id, const typet &_type)
plus_exprt(const exprt &_lhs, const exprt &_rhs)
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Expression to hold a nondeterministic choice.
bitand_exprt(const exprt &_op0, const exprt &_op1)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
const and_exprt & to_and_expr(const exprt &expr)
Cast a generic exprt to a and_exprt.
shl_exprt(const exprt &_src, const exprt &_distance)
The popcount (counting the number of bits set to 1) expression.
const rem_exprt & to_rem_expr(const exprt &expr)
Cast a generic exprt to a rem_exprt.
Evaluates to true if the operand is finite.
concatenation_exprt(const typet &_type)
ashr_exprt(const exprt &_src, const exprt &_distance)
std::size_t get_bits_per_byte() const
xor_exprt(const exprt &_op0, const exprt &_op1)
binary_relation_exprt(const irep_idt &id)
semantic type conversion from/to floating-point formats
div_exprt(const exprt &_lhs, const exprt &_rhs)
object_descriptor_exprt()
shl_exprt(const exprt &_src, const std::size_t _distance)
Base class for all expressions.
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
const exprt & struct_op() const
const exprt & rounding_mode() const
isnormal_exprt(const exprt &op)
nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
dereference_exprt(const exprt &op)
const complex_exprt & to_complex_expr(const exprt &expr)
Cast a generic exprt to a complex_exprt.
dereference_exprt(const typet &type)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Operator to update elements in structs and arrays.
sign_exprt(const exprt &_op)
A base class for quantifier expressions.
lshr_exprt(const exprt &_src, const exprt &_distance)
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
irep_idt get_component_name() const
const exprt & offset() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
bool can_cast_expr< let_exprt >(const exprt &base)
rem_exprt(const exprt &_lhs, const exprt &_rhs)
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
const exprt & valid() const
bitor_exprt(const exprt &_op0, const exprt &_op1)
const exprt & true_case() const
void set_identifier(const irep_idt &identifier)
array_exprt(const array_typet &_type)
irep_idt get_component_name() const
bool can_cast_expr< unary_exprt >(const exprt &base)
void set_component_name(const irep_idt &component_name)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
bool is_static_lifetime() const
isinf_exprt(const exprt &op)
bool can_cast_expr< bswap_exprt >(const exprt &base)
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
isnan_exprt(const exprt &op)
Expression to hold a symbol (variable)
bool can_cast_expr< isinf_exprt >(const exprt &base)
bool can_cast_expr< power_exprt >(const exprt &base)
ashr_exprt(const exprt &_src, const std::size_t _distance)
bool can_cast_expr< isfinite_exprt >(const exprt &base)
bool can_cast_expr< struct_exprt >(const exprt &base)
replication_exprt(const exprt &_times, const exprt &_src)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
struct_exprt(const typet &_type)
bool can_cast_expr< index_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast a generic exprt to a bitnot_exprt.
void clear_static_lifetime()
#define DATA_INVARIANT(CONDITION, REASON)
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast a generic exprt to a isnormal_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast a generic exprt to a nondet_symbol_exprt.
A generic base class for multi-ary expressions.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
mult_exprt(const exprt &_lhs, const exprt &_rhs)
mod_exprt(const exprt &_lhs, const exprt &_rhs)
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Bit-wise negation of bit-vectors.
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
struct constructor from list of elements
bool can_cast_expr< if_exprt >(const exprt &base)
std::size_t get_size_t(const irep_namet &name) const
union_exprt(const typet &_type)
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
IEEE floating-point operations.
quantifier_exprt(const irep_idt &_id)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
array_list_exprt(const array_typet &_type)
A base class for shift operators.
const argumentst & arguments() const
array constructor from list of elements
complex constructor from a pair of numbers
bool can_cast_expr< array_exprt >(const exprt &base)
The byte swap expression.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
member_designatort(const irep_idt &_component_name)
bool can_cast_expr< popcount_exprt >(const exprt &base)
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
array_of_exprt(const exprt &_what, const array_typet &_type)
const member_designatort & to_member_designator(const exprt &expr)
Cast a generic exprt to an member_designatort.
A generic base class for expressions that are predicates, i.e., boolean-typed.
IEEE-floating-point equality.
bool can_cast_expr< equal_exprt >(const exprt &base)
address_of_exprt(const exprt &op, const pointer_typet &_type)
const exprt & new_value() const
function_application_exprt()