cprover
|
#include <simplify_expr_class.h>
Public Types | |
typedef std::set< mp_integer > | value_listt |
Static Public Member Functions | |
static tvt | objects_equal (const exprt &a, const exprt &b) |
static tvt | objects_equal_address_of (const exprt &a, const exprt &b) |
static bool | is_bitvector_type (const typet &type) |
Public Attributes | |
bool | do_simplify_if |
Protected Attributes | |
const namespacet & | ns |
replace_mapt | local_replace_map |
Definition at line 37 of file simplify_expr_class.h.
typedef std::set<mp_integer> simplify_exprt::value_listt |
Definition at line 135 of file simplify_expr_class.h.
|
inlineexplicit |
Definition at line 40 of file simplify_expr_class.h.
|
inlinevirtual |
Definition at line 53 of file simplify_expr_class.h.
exprt simplify_exprt::bits2expr | ( | const std::string & | bits, |
const typet & | type, | ||
bool | little_endian | ||
) |
Definition at line 1452 of file simplify_expr.cpp.
References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), integer2size_t(), irept::is_nil(), endianness_mapt::map_bit(), exprt::move_to_operands(), ns, pointer_offset_bits(), exprt::reserve_operands(), array_typet::size(), size_type(), typet::subtype(), to_array_type(), to_c_enum_tag_type(), to_integer(), to_struct_type(), to_union_type(), and exprt::type().
Referenced by simplify_byte_extract(), and simplify_member().
Definition at line 1384 of file simplify_expr_int.cpp.
References Forall_operands, from_integer(), constant_exprt::get_value(), irept::id(), exprt::is_constant(), exprt::is_zero(), to_constant_expr(), and exprt::type().
Referenced by simplify_inequality_not_constant().
std::string simplify_exprt::expr2bits | ( | const exprt & | expr, |
bool | little_endian | ||
) |
Definition at line 1566 of file simplify_expr.cpp.
References namespace_baset::follow(), forall_operands, irept::id(), id2string(), ns, size_type(), to_constant_expr(), to_union_expr(), and exprt::type().
Referenced by simplify_byte_extract(), and simplify_member().
bool simplify_exprt::get_values | ( | const exprt & | expr, |
value_listt & | value_list | ||
) |
Definition at line 1198 of file simplify_expr.cpp.
References irept::id(), exprt::is_constant(), exprt::op1(), exprt::operands(), and to_integer().
Referenced by simplify_inequality_not_constant().
|
inlinestatic |
Definition at line 138 of file simplify_expr_class.h.
References irept::id().
Referenced by simplify_bitwise(), simplify_concatenation(), simplify_extractbit(), and simplify_extractbits().
Definition at line 577 of file simplify_expr_pointer.cpp.
References irept::get(), irept::id(), objects_equal_address_of(), exprt::op0(), exprt::operands(), and tvt::unknown().
Definition at line 601 of file simplify_expr_pointer.cpp.
References irept::get(), irept::id(), exprt::op0(), exprt::operands(), and tvt::unknown().
Referenced by objects_equal().
|
virtual |
Definition at line 2370 of file simplify_expr.cpp.
References from_expr(), ns, and simplify_rec().
Referenced by simplify(), simplify_expr(), and simplify_index().
bool simplify_exprt::simplify_abs | ( | exprt & | expr | ) |
Definition at line 68 of file simplify_expr.cpp.
References namespace_baset::follow(), from_integer(), irept::id(), exprt::is_constant(), exprt::negate(), ns, exprt::op0(), exprt::operands(), ieee_floatt::set_sign(), to_constant_expr(), ieee_floatt::to_expr(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_address_of | ( | exprt & | expr | ) |
Definition at line 171 of file simplify_expr_pointer.cpp.
References namespace_baset::follow(), from_integer(), index_exprt::index(), exprt::is_zero(), exprt::move_to_operands(), ns, exprt::op0(), exprt::op1(), exprt::operands(), simplify_address_of_arg(), irept::swap(), to_index_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_address_of_arg | ( | exprt & | expr | ) |
Definition at line 54 of file simplify_expr_pointer.cpp.
References namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), index_type(), is_dereference_integer_object(), exprt::is_false(), exprt::is_true(), member_offset(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_size(), pointer_type(), simplify_rec(), typet::subtype(), irept::swap(), to_integer(), to_member_expr(), to_struct_type(), and exprt::type().
Referenced by simplify_address_of().
bool simplify_exprt::simplify_bitnot | ( | exprt & | expr | ) |
Definition at line 1131 of file simplify_expr_int.cpp.
References irept::get_string(), exprt::has_operands(), irept::id(), exprt::operands(), irept::set(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_bitwise | ( | exprt & | expr | ) |
Definition at line 548 of file simplify_expr_int.cpp.
References namespace_baset::follow(), forall_operands, Forall_operands, irept::get(), constant_exprt::get_value(), irept::id(), id2string(), integer2binary(), is_bitvector_type(), exprt::is_constant(), exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), constant_exprt::set_value(), simplify_node(), dstringt::size(), irept::swap(), to_bitvector_type(), to_constant_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_boolean | ( | exprt & | expr | ) |
Definition at line 18 of file simplify_expr_boolean.cpp.
References forall_operands, exprt::has_operands(), irept::id(), exprt::make_bool(), exprt::make_not(), exprt::op0(), exprt::operands(), simplify_node(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_bswap | ( | exprt & | expr | ) |
Definition at line 26 of file simplify_expr_int.cpp.
References from_integer(), irept::id(), exprt::is_constant(), exprt::op0(), exprt::operands(), to_bitvector_type(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_byte_extract | ( | byte_extract_exprt & | expr | ) |
Definition at line 1626 of file simplify_expr.cpp.
References base_type_eq(), bits2expr(), byte_extract_id(), struct_union_typet::components(), expr2bits(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::id(), integer2size_t(), irept::is_not_nil(), lift_if(), exprt::make_typecast(), ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), pointer_offset_bits(), pointer_offset_size(), simplify_if(), simplify_member(), simplify_plus(), simplify_rec(), typet::subtype(), irept::swap(), to_byte_extract_expr(), to_integer(), to_struct_type(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_byte_update(), and simplify_node().
bool simplify_exprt::simplify_byte_update | ( | byte_update_exprt & | expr | ) |
Definition at line 1881 of file simplify_expr.cpp.
References base_type_eq(), byte_extract_id(), namespace_baset::follow(), Forall_operands, from_integer(), irept::get(), struct_union_typet::get_component(), irept::id(), irept::is_nil(), irept::is_not_nil(), exprt::is_zero(), irept::make_nil(), member_offset(), with_exprt::new_value(), ns, byte_extract_exprt::offset(), byte_update_exprt::offset(), with_exprt::old(), byte_extract_exprt::op(), byte_update_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), pointer_offset_bits(), pointer_offset_size(), irept::set(), simplify_byte_extract(), simplify_node(), simplify_rec(), typet::subtype(), irept::swap(), to_byte_extract_expr(), to_integer(), to_struct_type(), to_with_expr(), exprt::type(), byte_update_exprt::value(), and with_exprt::where().
Referenced by simplify_node().
bool simplify_exprt::simplify_concatenation | ( | exprt & | expr | ) |
Definition at line 774 of file simplify_expr_int.cpp.
References Forall_operands, irept::get_string(), irept::id(), is_bitvector_type(), exprt::is_constant(), exprt::is_false(), exprt::is_true(), exprt::op0(), exprt::operands(), irept::set(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_dereference | ( | exprt & | expr | ) |
Definition at line 714 of file simplify_expr.cpp.
References index_exprt::array(), if_exprt::cond(), if_exprt::false_case(), namespace_baset::follow(), irept::id(), index_exprt::index(), ns, address_of_exprt::object(), exprt::op0(), exprt::op1(), exprt::operands(), dereference_exprt::pointer(), simplify_if(), simplify_rec(), irept::swap(), to_address_of_expr(), to_dereference_expr(), to_if_expr(), to_index_expr(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_div | ( | exprt & | expr | ) |
Definition at line 163 of file simplify_expr_int.cpp.
References from_integer(), from_rational(), irept::id(), exprt::is_constant(), irept::is_not_nil(), is_number(), rationalt::is_one(), exprt::is_one(), fixedbvt::is_zero(), rationalt::is_zero(), exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), to_constant_expr(), fixedbvt::to_expr(), to_integer(), to_rational(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_dynamic_object | ( | exprt & | expr | ) |
Definition at line 492 of file simplify_expr_pointer.cpp.
References if_exprt::false_case(), irept::get(), has_prefix(), irept::id(), id2string(), lift_if(), exprt::make_bool(), exprt::op0(), exprt::operands(), simplify_if(), simplify_object(), irept::swap(), to_symbol_expr(), and if_exprt::true_case().
Referenced by simplify_node().
bool simplify_exprt::simplify_dynamic_size | ( | exprt & | expr | ) |
bool simplify_exprt::simplify_extractbit | ( | exprt & | expr | ) |
Definition at line 740 of file simplify_expr_int.cpp.
References irept::get(), bitvector_typet::get_width(), id2string(), integer2size_t(), is_bitvector_type(), exprt::is_constant(), exprt::make_bool(), exprt::op0(), exprt::op1(), exprt::operands(), dstringt::size(), to_bitvector_type(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_extractbits | ( | exprt & | expr | ) |
Simplifies extracting of bits from a constant.
Definition at line 996 of file simplify_expr_int.cpp.
References irept::get(), bitvector_typet::get_width(), id2string(), integer2size_t(), is_bitvector_type(), exprt::is_constant(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::set(), dstringt::size(), irept::swap(), to_bitvector_type(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_floatbv_op | ( | exprt & | expr | ) |
Definition at line 270 of file simplify_expr_floatbv.cpp.
References namespace_baset::follow(), irept::id(), integer2size_t(), exprt::is_constant(), exprt::is_one(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), ieee_floatt::rounding_mode, irept::swap(), to_constant_expr(), ieee_floatt::to_expr(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_floatbv_typecast | ( | exprt & | expr | ) |
Definition at line 141 of file simplify_expr_floatbv.cpp.
References ieee_floatt::change_spec(), namespace_baset::follow(), from_integer(), ieee_floatt::from_integer(), irept::id(), integer2size_t(), exprt::is_constant(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), ieee_floatt::ROUND_TO_ZERO, ieee_floatt::rounding_mode, simplify_if(), simplify_node(), irept::swap(), to_constant_expr(), ieee_floatt::to_expr(), to_floatbv_type(), to_integer(), ieee_floatt::to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_good_pointer | ( | exprt & | expr | ) |
Definition at line 671 of file simplify_expr_pointer.cpp.
References good_pointer_def(), ns, exprt::op0(), exprt::operands(), simplify_node(), and irept::swap().
Referenced by simplify_node().
bool simplify_exprt::simplify_ieee_float_relation | ( | exprt & | expr | ) |
Definition at line 333 of file simplify_expr_floatbv.cpp.
References exprt::copy_to_operands(), irept::id(), ieee_floatt::ieee_equal(), ieee_floatt::ieee_not_equal(), exprt::is_constant(), exprt::make_bool(), exprt::make_not(), exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), to_constant_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_if | ( | if_exprt & | expr | ) |
Definition at line 1090 of file simplify_expr.cpp.
References if_exprt::cond(), do_simplify_if, if_exprt::false_case(), Forall_operands, irept::id(), exprt::is_false(), exprt::is_true(), exprt::make_not(), exprt::op0(), exprt::operands(), simplify_if_branch(), simplify_if_cond(), simplify_node(), irept::swap(), to_if_expr(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_byte_extract(), simplify_dereference(), simplify_dynamic_object(), simplify_floatbv_typecast(), simplify_index(), simplify_inequality(), simplify_inequality_constant(), simplify_node(), simplify_pointer_offset(), and simplify_typecast().
Definition at line 937 of file simplify_expr.cpp.
References irept::id(), simplify_if_conj(), simplify_if_disj(), simplify_if_recursive(), and simplify_rec().
Referenced by simplify_if().
bool simplify_exprt::simplify_if_cond | ( | exprt & | expr | ) |
Definition at line 969 of file simplify_expr.cpp.
References exprt::has_operands(), irept::id(), exprt::operands(), simplify_if_recursive(), and simplify_rec().
Referenced by simplify_if().
Definition at line 895 of file simplify_expr.cpp.
References forall_operands, and Forall_operands.
Referenced by simplify_if_branch().
Definition at line 916 of file simplify_expr.cpp.
References forall_operands, and Forall_operands.
Referenced by simplify_if_branch().
bool simplify_exprt::simplify_if_implies | ( | exprt & | expr, |
const exprt & | cond, | ||
bool | truth, | ||
bool & | new_truth | ||
) |
Definition at line 772 of file simplify_expr.cpp.
References binary2integer(), irept::get_string(), irept::id(), exprt::is_constant(), exprt::op0(), exprt::op1(), string2integer(), and exprt::type().
Referenced by simplify_if_recursive().
bool simplify_exprt::simplify_if_preorder | ( | if_exprt & | expr | ) |
Definition at line 1005 of file simplify_expr.cpp.
References if_exprt::cond(), do_simplify_if, if_exprt::false_case(), forall_operands, irept::id(), exprt::is_constant(), exprt::is_true(), local_replace_map, exprt::op0(), simplify_rec(), irept::swap(), and if_exprt::true_case().
Referenced by simplify_node_preorder().
Definition at line 863 of file simplify_expr.cpp.
References Forall_operands, irept::id(), simplify_if_implies(), and exprt::type().
Referenced by simplify_if_branch(), and simplify_if_cond().
bool simplify_exprt::simplify_index | ( | exprt & | expr | ) |
Definition at line 20 of file simplify_expr_array.cpp.
References index_exprt::array(), if_exprt::cond(), exprt::copy_to_operands(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::get(), irept::id(), index_exprt::index(), integer2size_t(), exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_size(), replace_expr(), binary_relation_exprt::rhs(), simplify(), simplify_if(), simplify_inequality(), simplify_node(), simplify_rec(), dstringt::size(), typet::subtype(), irept::swap(), to_if_expr(), to_index_expr(), to_integer(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_inequality | ( | exprt & | expr | ) |
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition at line 1168 of file simplify_expr_int.cpp.
References base_type_eq(), if_exprt::false_case(), namespace_baset::follow_symbol(), namespace_baset::follow_tag(), irept::id(), exprt::is_constant(), exprt::is_true(), lift_if(), exprt::make_bool(), ns, exprt::op0(), exprt::op1(), exprt::operands(), simplify_if(), simplify_inequality_address_of(), simplify_inequality_constant(), simplify_inequality_not_constant(), simplify_inequality_pointer_object(), irept::swap(), to_c_enum_tag_type(), to_constant_expr(), to_integer(), to_rational(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_index(), simplify_inequality_constant(), simplify_inequality_not_constant(), and simplify_node().
bool simplify_exprt::simplify_inequality_address_of | ( | exprt & | expr | ) |
Definition at line 391 of file simplify_expr_pointer.cpp.
References irept::get(), irept::id(), exprt::is_zero(), exprt::make_bool(), exprt::op0(), exprt::op1(), exprt::operands(), to_index_expr(), and exprt::type().
Referenced by simplify_inequality().
bool simplify_exprt::simplify_inequality_constant | ( | exprt & | expr | ) |
Definition at line 1559 of file simplify_expr_int.cpp.
References configt::ansi_c, ieee_floatt::change_spec(), config, if_exprt::false_case(), namespace_baset::follow(), Forall_operands, from_integer(), irept::get(), irept::id(), exprt::is_constant(), exprt::is_zero(), lift_if(), exprt::make_not(), ns, configt::ansi_ct::NULL_is_zero, exprt::op0(), exprt::op1(), exprt::operands(), simplify_if(), simplify_inequality(), simplify_node(), simplify_plus(), irept::swap(), to_constant_expr(), ieee_floatt::to_expr(), to_floatbv_type(), to_integer(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_inequality().
bool simplify_exprt::simplify_inequality_not_constant | ( | exprt & | expr | ) |
Definition at line 1432 of file simplify_expr_int.cpp.
References eliminate_common_addends(), namespace_baset::follow(), forall_value_list, get_values(), irept::id(), exprt::make_bool(), exprt::make_not(), ns, exprt::op0(), exprt::op1(), exprt::operands(), simplify_inequality(), simplify_node(), irept::swap(), and exprt::type().
Referenced by simplify_inequality().
bool simplify_exprt::simplify_inequality_pointer_object | ( | exprt & | expr | ) |
Definition at line 432 of file simplify_expr_pointer.cpp.
References forall_operands, irept::id(), exprt::make_bool(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by simplify_inequality().
bool simplify_exprt::simplify_invalid_pointer | ( | exprt & | expr | ) |
Definition at line 548 of file simplify_expr_pointer.cpp.
References irept::get(), irept::id(), exprt::op0(), exprt::operands(), and simplify_object().
Referenced by simplify_node().
bool simplify_exprt::simplify_isinf | ( | exprt & | expr | ) |
Definition at line 19 of file simplify_expr_floatbv.cpp.
References namespace_baset::follow(), exprt::is_constant(), ieee_floatt::is_infinity(), exprt::make_bool(), ns, exprt::op0(), exprt::operands(), to_constant_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_isnan | ( | exprt & | expr | ) |
Definition at line 37 of file simplify_expr_floatbv.cpp.
References exprt::is_constant(), ieee_floatt::is_NaN(), exprt::make_bool(), exprt::op0(), exprt::operands(), and to_constant_expr().
Referenced by simplify_node().
bool simplify_exprt::simplify_isnormal | ( | exprt & | expr | ) |
Definition at line 52 of file simplify_expr_floatbv.cpp.
References exprt::is_constant(), ieee_floatt::is_normal(), exprt::make_bool(), exprt::op0(), exprt::operands(), and to_constant_expr().
Referenced by simplify_node().
bool simplify_exprt::simplify_lambda | ( | exprt & | expr | ) |
Definition at line 1224 of file simplify_expr.cpp.
Referenced by simplify_node().
bool simplify_exprt::simplify_member | ( | exprt & | expr | ) |
Definition at line 19 of file simplify_expr_struct.cpp.
References bits2expr(), struct_union_typet::component_number(), member_exprt::compound(), if_exprt::cond(), exprt::copy_to_operands(), update_exprt::designator(), expr2bits(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::get(), struct_union_typet::get_component(), member_exprt::get_component_name(), struct_union_typet::has_component(), irept::id(), integer2size_t(), irept::is_nil(), irept::is_not_nil(), member_offset(), with_exprt::new_value(), update_exprt::new_value(), ns, update_exprt::old(), unary_exprt::op(), exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_size(), simplify_node(), simplify_rec(), irept::swap(), to_if_expr(), to_member_expr(), to_struct_type(), to_union_expr(), to_update_expr(), to_with_expr(), if_exprt::true_case(), exprt::type(), and with_exprt::where().
Referenced by simplify_byte_extract(), and simplify_node().
bool simplify_exprt::simplify_minus | ( | exprt & | expr | ) |
Definition at line 489 of file simplify_expr_int.cpp.
References from_integer(), irept::id(), irept::is_not_nil(), is_number(), exprt::operands(), simplify_node(), simplify_plus(), simplify_unary_minus(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_mod | ( | exprt & | expr | ) |
Definition at line 283 of file simplify_expr_int.cpp.
References from_integer(), irept::id(), irept::is_not_nil(), is_number(), exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_mult | ( | exprt & | expr | ) |
Definition at line 58 of file simplify_expr_int.cpp.
References from_integer(), irept::is_nil(), irept::is_not_nil(), is_number(), exprt::operands(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_node | ( | exprt & | expr | ) |
Definition at line 2178 of file simplify_expr.cpp.
References from_expr(), exprt::has_operands(), irept::id(), ns, simplify_abs(), simplify_address_of(), simplify_bitnot(), simplify_bitwise(), simplify_boolean(), simplify_bswap(), simplify_byte_extract(), simplify_byte_update(), simplify_concatenation(), simplify_dereference(), simplify_div(), simplify_dynamic_object(), simplify_extractbit(), simplify_extractbits(), simplify_floatbv_op(), simplify_floatbv_typecast(), simplify_good_pointer(), simplify_ieee_float_relation(), simplify_if(), simplify_index(), simplify_inequality(), simplify_invalid_pointer(), simplify_isinf(), simplify_isnan(), simplify_isnormal(), simplify_lambda(), simplify_member(), simplify_minus(), simplify_mod(), simplify_mult(), simplify_not(), simplify_object_size(), simplify_plus(), simplify_pointer_object(), simplify_pointer_offset(), simplify_popcount(), simplify_power(), simplify_shifts(), simplify_sign(), simplify_typecast(), simplify_unary_minus(), simplify_unary_plus(), simplify_update(), simplify_with(), sort_and_join(), to_byte_extract_expr(), to_byte_update_expr(), and to_if_expr().
Referenced by simplify_bitwise(), simplify_boolean(), simplify_byte_update(), simplify_floatbv_typecast(), simplify_good_pointer(), simplify_if(), simplify_index(), simplify_inequality_constant(), simplify_inequality_not_constant(), simplify_member(), simplify_minus(), simplify_not(), simplify_object_size(), simplify_pointer_offset(), simplify_rec(), and simplify_typecast().
bool simplify_exprt::simplify_node_preorder | ( | exprt & | expr | ) |
Definition at line 2153 of file simplify_expr.cpp.
References Forall_operands, exprt::has_operands(), irept::id(), simplify_if_preorder(), simplify_rec(), and to_if_expr().
Referenced by simplify_rec().
bool simplify_exprt::simplify_not | ( | exprt & | expr | ) |
Definition at line 191 of file simplify_expr_boolean.cpp.
References Forall_operands, irept::id(), exprt::is_false(), exprt::is_true(), exprt::make_not(), exprt::op0(), exprt::op1(), exprt::operands(), simplify_node(), irept::swap(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_object | ( | exprt & | expr | ) |
Definition at line 1361 of file simplify_expr.cpp.
References namespace_baset::follow(), Forall_operands, irept::id(), ns, exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), and exprt::type().
Referenced by simplify_dynamic_object(), simplify_invalid_pointer(), simplify_object_size(), and simplify_pointer_object().
bool simplify_exprt::simplify_object_size | ( | exprt & | expr | ) |
Definition at line 625 of file simplify_expr_pointer.cpp.
References namespace_baset::follow(), from_integer(), irept::get(), irept::id(), irept::is_not_nil(), exprt::make_typecast(), ns, exprt::op0(), exprt::operands(), simplify_node(), simplify_object(), dstringt::size(), size_of_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_plus | ( | exprt & | expr | ) |
Definition at line 332 of file simplify_expr_int.cpp.
References exprt::copy_to_operands(), namespace_baset::follow(), Forall_expr, forall_operands, Forall_operands, from_integer(), irept::id(), irept::is_not_nil(), is_number(), ns, exprt::op0(), exprt::op1(), exprt::operands(), irept::swap(), and exprt::type().
Referenced by simplify_byte_extract(), simplify_inequality_constant(), simplify_minus(), and simplify_node().
bool simplify_exprt::simplify_pointer_object | ( | exprt & | expr | ) |
Definition at line 464 of file simplify_expr_pointer.cpp.
References if_exprt::cond(), if_exprt::false_case(), irept::id(), exprt::op0(), exprt::operands(), simplify_object(), simplify_rec(), to_if_expr(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_pointer_offset | ( | exprt & | expr | ) |
Definition at line 213 of file simplify_expr_pointer.cpp.
References char_type(), compute_pointer_offset(), if_exprt::false_case(), namespace_baset::follow(), from_integer(), irept::get(), irept::id(), exprt::is_constant(), lift_if(), exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset(), pointer_offset_size(), simplify_if(), simplify_node(), typet::subtype(), irept::swap(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_popcount | ( | exprt & | expr | ) |
Definition at line 138 of file simplify_expr.cpp.
References namespace_baset::follow(), from_integer(), irept::id(), exprt::is_constant(), ns, exprt::op0(), exprt::operands(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_power | ( | exprt & | expr | ) |
Definition at line 973 of file simplify_expr_int.cpp.
References from_integer(), is_number(), exprt::op0(), exprt::op1(), exprt::operands(), power(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_rec | ( | exprt & | expr | ) |
Definition at line 2311 of file simplify_expr.cpp.
References dstringt::empty(), irept::id(), local_replace_map, replace_expr(), simplify_node(), simplify_node_preorder(), and irept::swap().
Referenced by simplify(), simplify_address_of_arg(), simplify_byte_extract(), simplify_byte_update(), simplify_dereference(), simplify_if_branch(), simplify_if_cond(), simplify_if_preorder(), simplify_index(), simplify_member(), simplify_node_preorder(), simplify_pointer_object(), and simplify_typecast().
bool simplify_exprt::simplify_same_object | ( | exprt & | expr | ) |
bool simplify_exprt::simplify_shifts | ( | exprt & | expr | ) |
Definition at line 861 of file simplify_expr_int.cpp.
References from_integer(), irept::get(), irept::id(), id2string(), is_number(), exprt::op0(), exprt::op1(), exprt::operands(), power(), string2integer(), irept::swap(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_sign | ( | exprt & | expr | ) |
Definition at line 108 of file simplify_expr.cpp.
References namespace_baset::follow(), ieee_floatt::get_sign(), irept::id(), exprt::is_constant(), exprt::make_bool(), ns, exprt::op0(), exprt::operands(), to_constant_expr(), to_integer(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_typecast | ( | exprt & | expr | ) |
Definition at line 169 of file simplify_expr.cpp.
References exprt::add_source_location(), configt::ansi_c, base_type(), base_type_eq(), binary2integer(), ieee_floatt::change_spec(), config, irept::find(), namespace_baset::follow(), namespace_baset::follow_tag(), Forall_operands, fixedbvt::from_integer(), from_integer(), ieee_floatt::from_integer(), from_rational(), fixedbv_spect::get_fraction_bits(), constant_exprt::get_value(), bitvector_typet::get_width(), irept::id(), id2string(), exprt::is_constant(), exprt::is_false(), irept::is_not_nil(), exprt::is_true(), exprt::is_zero(), binary_relation_exprt::lhs(), exprt::make_bool(), ns, configt::ansi_ct::NULL_is_zero, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_size(), configt::ansi_ct::pointer_width, power(), r, binary_relation_exprt::rhs(), fixedbvt::round(), irept::set(), fixedbvt::set_value(), constant_exprt::set_value(), simplify_if(), simplify_node(), simplify_rec(), size_type(), exprt::source_location(), fixedbvt::spec, ieee_floatt::spec, string2integer(), typet::subtype(), irept::swap(), to_bitvector_type(), to_c_enum_tag_type(), to_c_enum_type(), to_constant_expr(), fixedbvt::to_expr(), ieee_floatt::to_expr(), to_fixedbv_type(), to_floatbv_type(), to_if_expr(), to_integer(), fixedbvt::to_integer(), ieee_floatt::to_integer(), to_pointer_type(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_unary_minus | ( | exprt & | expr | ) |
Definition at line 1054 of file simplify_expr_int.cpp.
References from_integer(), from_rational(), irept::id(), irept::is_nil(), is_number(), fixedbvt::negate(), ieee_floatt::negate(), exprt::op0(), exprt::operands(), r, irept::swap(), to_constant_expr(), fixedbvt::to_expr(), ieee_floatt::to_expr(), to_integer(), to_rational(), and exprt::type().
Referenced by simplify_minus(), and simplify_node().
bool simplify_exprt::simplify_unary_plus | ( | exprt & | expr | ) |
Definition at line 1044 of file simplify_expr_int.cpp.
References exprt::op0(), and exprt::operands().
Referenced by simplify_node().
bool simplify_exprt::simplify_update | ( | exprt & | expr | ) |
Definition at line 1304 of file simplify_expr.cpp.
References update_exprt::designator(), namespace_baset::follow(), irept::id(), integer2size_t(), update_exprt::new_value(), ns, update_exprt::old(), exprt::operands(), irept::swap(), to_integer(), to_struct_type(), to_update_expr(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::simplify_with | ( | exprt & | expr | ) |
Definition at line 1231 of file simplify_expr.cpp.
References namespace_baset::follow(), irept::get(), irept::id(), integer2size_t(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::swap(), to_integer(), to_struct_type(), and exprt::type().
Referenced by simplify_node().
bool simplify_exprt::do_simplify_if |
Definition at line 57 of file simplify_expr_class.h.
Referenced by simplify_if(), and simplify_if_preorder().
|
protected |
Definition at line 155 of file simplify_expr_class.h.
Referenced by simplify_if_preorder(), and simplify_rec().
|
protected |
Definition at line 151 of file simplify_expr_class.h.
Referenced by bits2expr(), expr2bits(), simplify(), simplify_abs(), simplify_address_of(), simplify_address_of_arg(), simplify_bitwise(), simplify_byte_extract(), simplify_byte_update(), simplify_dereference(), simplify_floatbv_op(), simplify_floatbv_typecast(), simplify_good_pointer(), simplify_index(), simplify_inequality(), simplify_inequality_constant(), simplify_inequality_not_constant(), simplify_isinf(), simplify_member(), simplify_node(), simplify_object(), simplify_object_size(), simplify_plus(), simplify_pointer_offset(), simplify_popcount(), simplify_sign(), simplify_typecast(), simplify_update(), and simplify_with().