|
| | simplify_expr_with_value_sett (const value_sett &_vs, const irep_idt &_mode, const namespacet &_ns) |
| |
| resultt | simplify_inequality (const binary_relation_exprt &) override |
| | simplifies inequalities !=, <=, <, >=, >, and also ==
|
| |
| resultt | simplify_inequality_pointer_object (const binary_relation_exprt &) override |
| | When all candidates in the value set have the same offset we can replace a pointer_offset expression by the offset value found in the value set.
|
| |
| resultt | simplify_pointer_offset (const pointer_offset_exprt &) override |
| |
| | simplify_exprt (const namespacet &_ns) |
| |
| virtual | ~simplify_exprt () |
| |
| resultt | simplify_typecast (const typecast_exprt &) |
| |
| resultt | simplify_typecast_preorder (const typecast_exprt &) |
| |
| resultt | simplify_extractbit (const extractbit_exprt &) |
| |
| resultt | simplify_extractbits (const extractbits_exprt &) |
| | Simplifies extracting of bits from a constant.
|
| |
| resultt | simplify_concatenation (const concatenation_exprt &) |
| |
| resultt | simplify_zero_extend (const zero_extend_exprt &) |
| |
| resultt | simplify_mult (const mult_exprt &) |
| |
| resultt | simplify_div (const div_exprt &) |
| |
| resultt | simplify_mod (const mod_exprt &) |
| |
| resultt | simplify_plus (const plus_exprt &) |
| |
| resultt | simplify_minus (const minus_exprt &) |
| |
| resultt | simplify_floatbv_op (const ieee_float_op_exprt &) |
| |
| resultt | simplify_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &) |
| |
| resultt | simplify_floatbv_typecast (const floatbv_typecast_exprt &) |
| |
| resultt | simplify_shifts (const shift_exprt &) |
| |
| resultt | simplify_power (const power_exprt &) |
| |
| resultt | simplify_bitwise (const multi_ary_exprt &) |
| |
| resultt | simplify_if_preorder (const if_exprt &expr) |
| |
| resultt | simplify_if (const if_exprt &) |
| |
| resultt | simplify_bitnot (const bitnot_exprt &) |
| |
| resultt | simplify_not (const not_exprt &) |
| |
| resultt | simplify_boolean (const exprt &) |
| |
| resultt | simplify_ieee_float_relation (const binary_relation_exprt &) |
| |
| resultt | simplify_lambda (const lambda_exprt &) |
| |
| resultt | simplify_with (const with_exprt &) |
| |
| resultt | simplify_update (const update_exprt &) |
| |
| resultt | simplify_index (const index_exprt &) |
| |
| resultt | simplify_index_preorder (const index_exprt &) |
| |
| resultt | simplify_member (const member_exprt &) |
| |
| resultt | simplify_member_preorder (const member_exprt &) |
| |
| resultt | simplify_byte_update (const byte_update_exprt &) |
| |
| resultt | simplify_byte_extract (const byte_extract_exprt &) |
| |
| resultt | simplify_byte_extract_preorder (const byte_extract_exprt &) |
| |
| resultt | simplify_pointer_object (const pointer_object_exprt &) |
| |
| resultt | simplify_unary_pointer_predicate_preorder (const unary_exprt &) |
| |
| resultt | simplify_object_size (const object_size_exprt &) |
| |
| resultt | simplify_is_dynamic_object (const unary_exprt &) |
| |
| resultt | simplify_is_invalid_pointer (const unary_exprt &) |
| |
| resultt | simplify_object (const exprt &) |
| |
| resultt | simplify_unary_minus (const unary_minus_exprt &) |
| |
| resultt | simplify_unary_plus (const unary_plus_exprt &) |
| |
| resultt | simplify_dereference (const dereference_exprt &) |
| |
| resultt | simplify_dereference_preorder (const dereference_exprt &) |
| |
| resultt | simplify_address_of (const address_of_exprt &) |
| |
| resultt | simplify_bswap (const bswap_exprt &) |
| |
| resultt | simplify_isinf (const unary_exprt &) |
| |
| resultt | simplify_isnan (const unary_exprt &) |
| |
| resultt | simplify_isnormal (const unary_exprt &) |
| |
| resultt | simplify_abs (const abs_exprt &) |
| |
| resultt | simplify_sign (const sign_exprt &) |
| |
| resultt | simplify_popcount (const popcount_exprt &) |
| |
| resultt | simplify_complex (const unary_exprt &) |
| |
| resultt | simplify_overflow_binary (const binary_overflow_exprt &) |
| | Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
|
| |
| resultt | simplify_overflow_unary (const unary_overflow_exprt &) |
| | Try to simplify overflow-unary-.
|
| |
| resultt | simplify_overflow_result (const overflow_result_exprt &) |
| | Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl, overflow_result-unary–.
|
| |
| resultt | simplify_function_application (const function_application_exprt &) |
| | Attempt to simplify mathematical function applications if we have enough information to do so.
|
| |
| resultt | simplify_clz (const count_leading_zeros_exprt &) |
| | Try to simplify count-leading-zeros to a constant expression.
|
| |
| resultt | simplify_ctz (const count_trailing_zeros_exprt &) |
| | Try to simplify count-trailing-zeros to a constant expression.
|
| |
| resultt | simplify_bitreverse (const bitreverse_exprt &) |
| | Try to simplify bit-reversing to a constant expression.
|
| |
| resultt | simplify_ffs (const find_first_set_exprt &) |
| | Try to simplify find-first-set to a constant expression.
|
| |
| resultt | simplify_prophecy_r_or_w_ok (const prophecy_r_or_w_ok_exprt &) |
| | Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
|
| |
| resultt | simplify_prophecy_pointer_in_range (const prophecy_pointer_in_range_exprt &) |
| | Try to simplify prophecy_pointer_in_range to a constant expression.
|
| |
| resultt | simplify_quantifier_expr (const quantifier_exprt &) |
| | Try to simplify exists/forall to a constant expression.
|
| |
| bool | simplify_if_implies (exprt &expr, const exprt &cond, bool truth, bool &new_truth) |
| |
| bool | simplify_if_recursive (exprt &expr, const exprt &cond, bool truth) |
| |
| bool | simplify_if_conj (exprt &expr, const exprt &cond) |
| |
| bool | simplify_if_disj (exprt &expr, const exprt &cond) |
| |
| bool | simplify_if_branch (exprt &trueexpr, exprt &falseexpr, const exprt &cond) |
| |
| bool | simplify_if_cond (exprt &expr) |
| |
| resultt | simplify_address_of_arg (const exprt &) |
| |
| resultt | simplify_inequality_both_constant (const binary_relation_exprt &) |
| | simplifies inequalities for the case in which both sides of the inequality are constants
|
| |
| resultt | simplify_inequality_no_constant (const binary_relation_exprt &) |
| |
| resultt | simplify_inequality_rhs_is_constant (const binary_relation_exprt &) |
| |
| resultt | simplify_inequality_address_of (const binary_relation_exprt &) |
| |
| resultt | simplify_node (const exprt &) |
| |
| resultt | simplify_node_preorder (const exprt &) |
| |
| resultt | simplify_rec (const exprt &) |
| |
| virtual bool | simplify (exprt &expr) |
| |
Inheritance diagram for simplify_expr_with_value_sett: