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 72 of file simplify_expr_class.h.
|
inlineexplicit |
Definition at line 75 of file simplify_expr_class.h.
|
inlinevirtual |
Definition at line 88 of file simplify_expr_class.h.
Definition at line 134 of file simplify_expr_class.h.
|
inlinestatic |
Definition at line 236 of file simplify_expr_class.h.
|
virtual |
Definition at line 2531 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 1181 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bitwise | ( | const multi_ary_exprt & | expr | ) |
Definition at line 601 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 30 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_extract | ( | const byte_extract_exprt & | expr | ) |
Definition at line 1573 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_update | ( | const byte_update_exprt & | expr | ) |
Definition at line 1746 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_clz | ( | const count_leading_zeros_exprt & | expr | ) |
Try to simplify count-leading-zeros to a constant expression.
Definition at line 152 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_complex | ( | const unary_exprt & | expr | ) |
Definition at line 2054 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_concatenation | ( | const concatenation_exprt & | expr | ) |
Definition at line 807 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_dereference | ( | const dereference_exprt & | expr | ) |
Definition at line 1302 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_div | ( | const div_exprt & | expr | ) |
Definition at line 272 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_extractbit | ( | const extractbit_exprt & | expr | ) |
Definition at line 778 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 1038 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_op | ( | const ieee_float_op_exprt & | expr | ) |
Definition at line 274 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast | ( | const floatbv_typecast_exprt & | expr | ) |
Definition at line 140 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 650 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_good_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 705 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_ieee_float_relation | ( | const binary_relation_exprt & | expr | ) |
Definition at line 339 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 1212 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 1307 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_no_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1468 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_pointer_object | ( | const binary_relation_exprt & | expr | ) |
Definition at line 485 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1540 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object | ( | const unary_exprt & | expr | ) |
Definition at line 562 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 621 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isinf | ( | const unary_exprt & | expr | ) |
Definition at line 24 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnan | ( | const unary_exprt & | expr | ) |
Definition at line 38 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnormal | ( | const unary_exprt & | expr | ) |
Definition at line 52 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_lambda | ( | const lambda_exprt & | expr | ) |
Definition at line 1360 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_member | ( | const member_exprt & | expr | ) |
Definition at line 21 of file simplify_expr_struct.cpp.
simplify_exprt::resultt simplify_exprt::simplify_minus | ( | const minus_exprt & | expr | ) |
Definition at line 559 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mod | ( | const mod_exprt & | expr | ) |
Definition at line 366 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mult | ( | const mult_exprt & | expr | ) |
Definition at line 160 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_node | ( | exprt | node | ) |
Definition at line 2216 of file simplify_expr.cpp.
bool simplify_exprt::simplify_node_preorder | ( | exprt & | expr | ) |
Definition at line 2185 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 1493 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_object_size | ( | const unary_exprt & | expr | ) |
Definition at line 654 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_overflow_binary | ( | const binary_overflow_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 2075 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_overflow_unary | ( | const unary_overflow_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 2138 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_plus | ( | const plus_exprt & | expr | ) |
Definition at line 403 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_pointer_object | ( | const unary_exprt & | expr | ) |
Definition at line 530 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 1017 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_rec | ( | const exprt & | expr | ) |
Definition at line 2462 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_shifts | ( | const shift_exprt & | expr | ) |
Definition at line 909 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 707 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_minus | ( | const unary_minus_exprt & | expr | ) |
Definition at line 1121 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_plus | ( | const unary_plus_exprt & | expr | ) |
Definition at line 1114 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_update | ( | const update_exprt & | expr | ) |
Definition at line 1445 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_with | ( | const with_exprt & | expr | ) |
Definition at line 1365 of file simplify_expr.cpp.
Definition at line 129 of file simplify_expr_class.h.
bool simplify_exprt::do_simplify_if |
Definition at line 92 of file simplify_expr_class.h.
|
protected |
Definition at line 244 of file simplify_expr_class.h.