cprover
|
#include <simplify_expr_class.h>
Classes | |
struct | resultt |
Static Public Member Functions | |
static resultt | unchanged (exprt expr) |
static resultt | changed (resultt<> result) |
static bool | is_bitvector_type (const typet &type) |
Public Attributes | |
bool | do_simplify_if |
Protected Attributes | |
const namespacet & | ns |
Definition at line 69 of file simplify_expr_class.h.
|
inlineexplicit |
Definition at line 72 of file simplify_expr_class.h.
|
inlinevirtual |
Definition at line 85 of file simplify_expr_class.h.
Definition at line 131 of file simplify_expr_class.h.
|
inlinestatic |
Definition at line 230 of file simplify_expr_class.h.
|
virtual |
Definition at line 2503 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_abs | ( | const abs_exprt & | expr | ) |
Definition at line 66 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_address_of | ( | const address_of_exprt & | expr | ) |
Definition at line 210 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_address_of_arg | ( | const exprt & | expr | ) |
Definition at line 57 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bitnot | ( | const bitnot_exprt & | expr | ) |
Definition at line 1172 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bitwise | ( | const multi_ary_exprt & | expr | ) |
Definition at line 600 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_boolean | ( | const exprt & | expr | ) |
Definition at line 20 of file simplify_expr_boolean.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bswap | ( | const bswap_exprt & | expr | ) |
Definition at line 29 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_extract | ( | const byte_extract_exprt & | expr | ) |
Definition at line 1549 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_update | ( | const byte_update_exprt & | expr | ) |
Definition at line 1722 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_complex | ( | const unary_exprt & | expr | ) |
Definition at line 2030 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_concatenation | ( | const concatenation_exprt & | expr | ) |
Definition at line 798 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_dereference | ( | const dereference_exprt & | expr | ) |
Definition at line 1278 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_div | ( | const div_exprt & | expr | ) |
Definition at line 271 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_extractbit | ( | const extractbit_exprt & | expr | ) |
Definition at line 769 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_extractbits | ( | const extractbits_exprt & | expr | ) |
Simplifies extracting of bits from a constant.
Definition at line 1029 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_op | ( | const ieee_float_op_exprt & | expr | ) |
Definition at line 273 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast | ( | const floatbv_typecast_exprt & | expr | ) |
Definition at line 139 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_function_application | ( | const function_application_exprt & | expr | ) |
Attempt to simplify mathematical function applications if we have enough information to do so.
Currently focused on constant comparisons.
Definition at line 626 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_good_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 713 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_ieee_float_relation | ( | const binary_relation_exprt & | expr | ) |
Definition at line 338 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_if | ( | const if_exprt & | expr | ) |
Definition at line 331 of file simplify_expr_if.cpp.
Definition at line 145 of file simplify_expr_if.cpp.
bool simplify_exprt::simplify_if_cond | ( | exprt & | expr | ) |
Definition at line 177 of file simplify_expr_if.cpp.
Definition at line 107 of file simplify_expr_if.cpp.
Definition at line 126 of file simplify_expr_if.cpp.
bool simplify_exprt::simplify_if_implies | ( | exprt & | expr, |
const exprt & | cond, | ||
bool | truth, | ||
bool & | new_truth | ||
) |
Definition at line 16 of file simplify_expr_if.cpp.
bool simplify_exprt::simplify_if_preorder | ( | if_exprt & | expr | ) |
Definition at line 215 of file simplify_expr_if.cpp.
Definition at line 75 of file simplify_expr_if.cpp.
simplify_exprt::resultt simplify_exprt::simplify_index | ( | const index_exprt & | expr | ) |
Definition at line 20 of file simplify_expr_array.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality | ( | const binary_relation_exprt & | expr | ) |
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition at line 1203 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_address_of | ( | const binary_relation_exprt & | expr | ) |
Definition at line 420 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_both_constant | ( | const binary_relation_exprt & | expr | ) |
simplifies inequalities for the case in which both sides of the inequality are constants
Definition at line 1303 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_no_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1464 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_pointer_object | ( | const binary_relation_exprt & | expr | ) |
Definition at line 493 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1536 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object | ( | const unary_exprt & | expr | ) |
Definition at line 570 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 629 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isinf | ( | const unary_exprt & | expr | ) |
Definition at line 23 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnan | ( | const unary_exprt & | expr | ) |
Definition at line 37 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnormal | ( | const unary_exprt & | expr | ) |
Definition at line 51 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_lambda | ( | const lambda_exprt & | expr | ) |
Definition at line 1336 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_member | ( | const member_exprt & | expr | ) |
Definition at line 20 of file simplify_expr_struct.cpp.
simplify_exprt::resultt simplify_exprt::simplify_minus | ( | const minus_exprt & | expr | ) |
Definition at line 558 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mod | ( | const mod_exprt & | expr | ) |
Definition at line 365 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mult | ( | const mult_exprt & | expr | ) |
Definition at line 159 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_node | ( | exprt | node | ) |
Definition at line 2192 of file simplify_expr.cpp.
bool simplify_exprt::simplify_node_preorder | ( | exprt & | expr | ) |
Definition at line 2161 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_not | ( | const not_exprt & | expr | ) |
Definition at line 165 of file simplify_expr_boolean.cpp.
simplify_exprt::resultt simplify_exprt::simplify_object | ( | const exprt & | expr | ) |
Definition at line 1469 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_object_size | ( | const unary_exprt & | expr | ) |
Definition at line 662 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_overflow_binary | ( | const binary_exprt & | expr | ) |
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Simplification will be possible when the operands are constants or the types of the operands have infinite domains.
Definition at line 2051 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_overflow_unary | ( | const unary_exprt & | expr | ) |
Try to simplify overflow-unary-.
Simplification will be possible when the operand is constants or the type of the operand has an infinite domain.
Definition at line 2114 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_plus | ( | const plus_exprt & | expr | ) |
Definition at line 402 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_pointer_object | ( | const unary_exprt & | expr | ) |
Definition at line 538 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_pointer_offset | ( | const unary_exprt & | expr | ) |
Definition at line 248 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_popcount | ( | const popcount_exprt & | expr | ) |
Definition at line 126 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_power | ( | const binary_exprt & | expr | ) |
Definition at line 1008 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_rec | ( | const exprt & | expr | ) |
Definition at line 2434 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_shifts | ( | const shift_exprt & | expr | ) |
Definition at line 900 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_sign | ( | const sign_exprt & | expr | ) |
Definition at line 100 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_typecast | ( | const typecast_exprt & | expr | ) |
Definition at line 683 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_minus | ( | const unary_minus_exprt & | expr | ) |
Definition at line 1112 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_plus | ( | const unary_plus_exprt & | expr | ) |
Definition at line 1105 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_update | ( | const update_exprt & | expr | ) |
Definition at line 1421 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_with | ( | const with_exprt & | expr | ) |
Definition at line 1341 of file simplify_expr.cpp.
Definition at line 126 of file simplify_expr_class.h.
bool simplify_exprt::do_simplify_if |
Definition at line 89 of file simplify_expr_class.h.
|
protected |
Definition at line 238 of file simplify_expr_class.h.