cprover
|
#include <simplify_expr_class.h>
Classes | |
struct | resultt |
Public Types | |
typedef std::set< mp_integer > | value_listt |
Static Public Member Functions | |
static resultt | unchanged (exprt expr) |
static resultt | changed (resultt<> result) |
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 |
Definition at line 73 of file simplify_expr_class.h.
typedef std::set<mp_integer> simplify_exprt::value_listt |
Definition at line 229 of file simplify_expr_class.h.
|
inlineexplicit |
Definition at line 76 of file simplify_expr_class.h.
|
inlinevirtual |
Definition at line 89 of file simplify_expr_class.h.
optionalt< exprt > simplify_exprt::bits2expr | ( | const std::string & | bits, |
const typet & | type, | ||
bool | little_endian | ||
) |
Definition at line 1567 of file simplify_expr.cpp.
Definition at line 135 of file simplify_expr_class.h.
Definition at line 1417 of file simplify_expr_int.cpp.
Definition at line 1764 of file simplify_expr.cpp.
bool simplify_exprt::get_values | ( | const exprt & | expr, |
value_listt & | value_list | ||
) |
Definition at line 1330 of file simplify_expr.cpp.
|
inlinestatic |
Definition at line 232 of file simplify_expr_class.h.
Definition at line 663 of file simplify_expr_pointer.cpp.
Definition at line 689 of file simplify_expr_pointer.cpp.
|
virtual |
Definition at line 2672 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_abs | ( | const abs_exprt & | expr | ) |
Definition at line 67 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_address_of | ( | const address_of_exprt & | expr | ) |
Definition at line 212 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_address_of_arg | ( | const exprt & | expr | ) |
Definition at line 59 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bitnot | ( | const bitnot_exprt & | expr | ) |
Definition at line 1171 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_bitwise | ( | const multi_ary_exprt & | expr | ) |
Definition at line 599 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 28 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_extract | ( | const byte_extract_exprt & | expr | ) |
Definition at line 1875 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_byte_update | ( | const byte_update_exprt & | expr | ) |
Definition at line 2045 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_complex | ( | const unary_exprt & | expr | ) |
Definition at line 2320 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_concatenation | ( | const concatenation_exprt & | expr | ) |
Definition at line 797 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_dereference | ( | const dereference_exprt & | expr | ) |
Definition at line 1273 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_div | ( | const div_exprt & | expr | ) |
Definition at line 270 of file simplify_expr_int.cpp.
resultt simplify_exprt::simplify_dynamic_size | ( | const unary_exprt & | ) |
simplify_exprt::resultt simplify_exprt::simplify_extractbit | ( | const extractbit_exprt & | expr | ) |
Definition at line 768 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 1028 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_op | ( | const ieee_float_op_exprt & | expr | ) |
Definition at line 268 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast | ( | const floatbv_typecast_exprt & | expr | ) |
Definition at line 134 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 627 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_good_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 765 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_ieee_float_relation | ( | const binary_relation_exprt & | expr | ) |
Definition at line 333 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 1202 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_address_of | ( | const binary_relation_exprt & | expr | ) |
Definition at line 422 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 1302 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_no_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1465 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_pointer_object | ( | const binary_relation_exprt & | expr | ) |
Definition at line 495 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1587 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object | ( | const unary_exprt & | expr | ) |
Definition at line 572 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 631 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isinf | ( | const unary_exprt & | expr | ) |
Definition at line 21 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnan | ( | const unary_exprt & | expr | ) |
Definition at line 36 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_isnormal | ( | const unary_exprt & | expr | ) |
Definition at line 48 of file simplify_expr_floatbv.cpp.
simplify_exprt::resultt simplify_exprt::simplify_lambda | ( | const exprt & | expr | ) |
Definition at line 1355 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_member | ( | const member_exprt & | expr | ) |
Definition at line 19 of file simplify_expr_struct.cpp.
simplify_exprt::resultt simplify_exprt::simplify_minus | ( | const minus_exprt & | expr | ) |
Definition at line 557 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mod | ( | const mod_exprt & | expr | ) |
Definition at line 364 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_mult | ( | const mult_exprt & | expr | ) |
Definition at line 158 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_node | ( | exprt | node | ) |
Definition at line 2371 of file simplify_expr.cpp.
bool simplify_exprt::simplify_node_preorder | ( | exprt & | expr | ) |
Definition at line 2340 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 1488 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_object_size | ( | const unary_exprt & | expr | ) |
Definition at line 714 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_plus | ( | const plus_exprt & | expr | ) |
Definition at line 401 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_pointer_object | ( | const unary_exprt & | expr | ) |
Definition at line 540 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_pointer_offset | ( | const unary_exprt & | expr | ) |
Definition at line 250 of file simplify_expr_pointer.cpp.
simplify_exprt::resultt simplify_exprt::simplify_popcount | ( | const popcount_exprt & | expr | ) |
Definition at line 127 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_power | ( | const binary_exprt & | expr | ) |
Definition at line 1007 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_rec | ( | const exprt & | expr | ) |
Definition at line 2603 of file simplify_expr.cpp.
resultt simplify_exprt::simplify_same_object | ( | const unary_exprt & | ) |
simplify_exprt::resultt simplify_exprt::simplify_shifts | ( | const shift_exprt & | expr | ) |
Definition at line 899 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_sign | ( | const sign_exprt & | expr | ) |
Definition at line 101 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_typecast | ( | const typecast_exprt & | expr | ) |
Definition at line 678 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_minus | ( | const unary_minus_exprt & | expr | ) |
Definition at line 1111 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_unary_plus | ( | const unary_plus_exprt & | expr | ) |
Definition at line 1104 of file simplify_expr_int.cpp.
simplify_exprt::resultt simplify_exprt::simplify_update | ( | const update_exprt & | expr | ) |
Definition at line 1440 of file simplify_expr.cpp.
simplify_exprt::resultt simplify_exprt::simplify_with | ( | const with_exprt & | expr | ) |
Definition at line 1360 of file simplify_expr.cpp.
Definition at line 130 of file simplify_expr_class.h.
bool simplify_exprt::do_simplify_if |
Definition at line 93 of file simplify_expr_class.h.
|
protected |
Definition at line 246 of file simplify_expr_class.h.