cprover
simplify_exprt Class Reference

#include <simplify_expr_class.h>

+ Collaboration diagram for simplify_exprt:

Classes

struct  resultt
 

Public Types

typedef std::set< mp_integervalue_listt
 

Public Member Functions

 simplify_exprt (const namespacet &_ns)
 
virtual ~simplify_exprt ()
 
resultt simplify_typecast (const typecast_exprt &)
 
resultt simplify_extractbit (const extractbit_exprt &)
 
resultt simplify_extractbits (const extractbits_exprt &)
 Simplifies extracting of bits from a constant. More...
 
resultt simplify_concatenation (const concatenation_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_typecast (const floatbv_typecast_exprt &)
 
resultt simplify_shifts (const shift_exprt &)
 
resultt simplify_power (const binary_exprt &)
 
resultt simplify_bitwise (const multi_ary_exprt &)
 
bool simplify_if_preorder (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_inequality (const binary_relation_exprt &)
 simplifies inequalities !=, <=, <, >=, >, and also == More...
 
resultt simplify_ieee_float_relation (const binary_relation_exprt &)
 
resultt simplify_lambda (const exprt &)
 
resultt simplify_with (const with_exprt &)
 
resultt simplify_update (const update_exprt &)
 
resultt simplify_index (const index_exprt &)
 
resultt simplify_member (const member_exprt &)
 
resultt simplify_byte_update (const byte_update_exprt &)
 
resultt simplify_byte_extract (const byte_extract_exprt &)
 
resultt simplify_pointer_object (const unary_exprt &)
 
resultt simplify_object_size (const unary_exprt &)
 
resultt simplify_dynamic_size (const unary_exprt &)
 
resultt simplify_is_dynamic_object (const unary_exprt &)
 
resultt simplify_is_invalid_pointer (const unary_exprt &)
 
resultt simplify_same_object (const unary_exprt &)
 
resultt simplify_good_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_address_of (const address_of_exprt &)
 
resultt simplify_pointer_offset (const unary_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_function_application (const function_application_exprt &)
 Attempt to simplify mathematical function applications if we have enough information to do so. More...
 
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)
 
bool eliminate_common_addends (exprt &op0, exprt &op1)
 
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 More...
 
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_inequality_pointer_object (const binary_relation_exprt &)
 
resultt simplify_node (exprt)
 
bool simplify_node_preorder (exprt &expr)
 
resultt simplify_rec (const exprt &)
 
virtual bool simplify (exprt &expr)
 
bool get_values (const exprt &expr, value_listt &value_list)
 
optionalt< exprtbits2expr (const std::string &bits, const typet &type, bool little_endian)
 
optionalt< std::string > expr2bits (const exprt &, bool little_endian)
 

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 namespacetns
 

Detailed Description

Definition at line 73 of file simplify_expr_class.h.

Member Typedef Documentation

◆ value_listt

Definition at line 229 of file simplify_expr_class.h.

Constructor & Destructor Documentation

◆ simplify_exprt()

simplify_exprt::simplify_exprt ( const namespacet _ns)
inlineexplicit

Definition at line 76 of file simplify_expr_class.h.

◆ ~simplify_exprt()

virtual simplify_exprt::~simplify_exprt ( )
inlinevirtual

Definition at line 89 of file simplify_expr_class.h.

Member Function Documentation

◆ bits2expr()

optionalt< exprt > simplify_exprt::bits2expr ( const std::string &  bits,
const typet type,
bool  little_endian 
)

Definition at line 1567 of file simplify_expr.cpp.

◆ changed()

static resultt simplify_exprt::changed ( resultt<>  result)
inlinestatic

Definition at line 135 of file simplify_expr_class.h.

◆ eliminate_common_addends()

bool simplify_exprt::eliminate_common_addends ( exprt op0,
exprt op1 
)

Definition at line 1417 of file simplify_expr_int.cpp.

◆ expr2bits()

optionalt< std::string > simplify_exprt::expr2bits ( const exprt expr,
bool  little_endian 
)

Definition at line 1764 of file simplify_expr.cpp.

◆ get_values()

bool simplify_exprt::get_values ( const exprt expr,
value_listt value_list 
)

Definition at line 1330 of file simplify_expr.cpp.

◆ is_bitvector_type()

static bool simplify_exprt::is_bitvector_type ( const typet type)
inlinestatic

Definition at line 232 of file simplify_expr_class.h.

◆ objects_equal()

tvt simplify_exprt::objects_equal ( const exprt a,
const exprt b 
)
static

Definition at line 663 of file simplify_expr_pointer.cpp.

◆ objects_equal_address_of()

tvt simplify_exprt::objects_equal_address_of ( const exprt a,
const exprt b 
)
static

Definition at line 689 of file simplify_expr_pointer.cpp.

◆ simplify()

bool simplify_exprt::simplify ( exprt expr)
virtual
Returns
returns true if expression unchanged; returns false if changed

Definition at line 2672 of file simplify_expr.cpp.

◆ simplify_abs()

simplify_exprt::resultt simplify_exprt::simplify_abs ( const abs_exprt expr)

Definition at line 67 of file simplify_expr.cpp.

◆ simplify_address_of()

simplify_exprt::resultt simplify_exprt::simplify_address_of ( const address_of_exprt expr)

Definition at line 212 of file simplify_expr_pointer.cpp.

◆ simplify_address_of_arg()

simplify_exprt::resultt simplify_exprt::simplify_address_of_arg ( const exprt expr)

Definition at line 59 of file simplify_expr_pointer.cpp.

◆ simplify_bitnot()

simplify_exprt::resultt simplify_exprt::simplify_bitnot ( const bitnot_exprt expr)

Definition at line 1171 of file simplify_expr_int.cpp.

◆ simplify_bitwise()

simplify_exprt::resultt simplify_exprt::simplify_bitwise ( const multi_ary_exprt expr)

Definition at line 599 of file simplify_expr_int.cpp.

◆ simplify_boolean()

simplify_exprt::resultt simplify_exprt::simplify_boolean ( const exprt expr)

Definition at line 20 of file simplify_expr_boolean.cpp.

◆ simplify_bswap()

simplify_exprt::resultt simplify_exprt::simplify_bswap ( const bswap_exprt expr)

Definition at line 28 of file simplify_expr_int.cpp.

◆ simplify_byte_extract()

simplify_exprt::resultt simplify_exprt::simplify_byte_extract ( const byte_extract_exprt expr)

Definition at line 1875 of file simplify_expr.cpp.

◆ simplify_byte_update()

simplify_exprt::resultt simplify_exprt::simplify_byte_update ( const byte_update_exprt expr)

Definition at line 2045 of file simplify_expr.cpp.

◆ simplify_complex()

simplify_exprt::resultt simplify_exprt::simplify_complex ( const unary_exprt expr)

Definition at line 2320 of file simplify_expr.cpp.

◆ simplify_concatenation()

simplify_exprt::resultt simplify_exprt::simplify_concatenation ( const concatenation_exprt expr)

Definition at line 797 of file simplify_expr_int.cpp.

◆ simplify_dereference()

simplify_exprt::resultt simplify_exprt::simplify_dereference ( const dereference_exprt expr)

Definition at line 1273 of file simplify_expr.cpp.

◆ simplify_div()

simplify_exprt::resultt simplify_exprt::simplify_div ( const div_exprt expr)

Definition at line 270 of file simplify_expr_int.cpp.

◆ simplify_dynamic_size()

resultt simplify_exprt::simplify_dynamic_size ( const unary_exprt )

◆ simplify_extractbit()

simplify_exprt::resultt simplify_exprt::simplify_extractbit ( const extractbit_exprt expr)

Definition at line 768 of file simplify_expr_int.cpp.

◆ simplify_extractbits()

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_floatbv_op()

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_floatbv_typecast()

simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast ( const floatbv_typecast_exprt expr)

Definition at line 134 of file simplify_expr_floatbv.cpp.

◆ simplify_function_application()

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_good_pointer()

simplify_exprt::resultt simplify_exprt::simplify_good_pointer ( const unary_exprt expr)

Definition at line 765 of file simplify_expr_pointer.cpp.

◆ simplify_ieee_float_relation()

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_if()

simplify_exprt::resultt simplify_exprt::simplify_if ( const if_exprt expr)

Definition at line 331 of file simplify_expr_if.cpp.

◆ simplify_if_branch()

bool simplify_exprt::simplify_if_branch ( exprt trueexpr,
exprt falseexpr,
const exprt cond 
)

Definition at line 145 of file simplify_expr_if.cpp.

◆ simplify_if_cond()

bool simplify_exprt::simplify_if_cond ( exprt expr)

Definition at line 177 of file simplify_expr_if.cpp.

◆ simplify_if_conj()

bool simplify_exprt::simplify_if_conj ( exprt expr,
const exprt cond 
)

Definition at line 107 of file simplify_expr_if.cpp.

◆ simplify_if_disj()

bool simplify_exprt::simplify_if_disj ( exprt expr,
const exprt cond 
)

Definition at line 126 of file simplify_expr_if.cpp.

◆ simplify_if_implies()

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.

◆ simplify_if_preorder()

bool simplify_exprt::simplify_if_preorder ( if_exprt expr)

Definition at line 215 of file simplify_expr_if.cpp.

◆ simplify_if_recursive()

bool simplify_exprt::simplify_if_recursive ( exprt expr,
const exprt cond,
bool  truth 
)

Definition at line 75 of file simplify_expr_if.cpp.

◆ simplify_index()

simplify_exprt::resultt simplify_exprt::simplify_index ( const index_exprt expr)

Definition at line 20 of file simplify_expr_array.cpp.

◆ simplify_inequality()

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_inequality_address_of()

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_inequality_both_constant()

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_inequality_no_constant()

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_inequality_pointer_object()

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_inequality_rhs_is_constant()

simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant ( const binary_relation_exprt expr)
expr: an inequality where the RHS is a constant
and the LHS is not

Definition at line 1587 of file simplify_expr_int.cpp.

◆ simplify_is_dynamic_object()

simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object ( const unary_exprt expr)

Definition at line 572 of file simplify_expr_pointer.cpp.

◆ simplify_is_invalid_pointer()

simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer ( const unary_exprt expr)

Definition at line 631 of file simplify_expr_pointer.cpp.

◆ simplify_isinf()

simplify_exprt::resultt simplify_exprt::simplify_isinf ( const unary_exprt expr)

Definition at line 21 of file simplify_expr_floatbv.cpp.

◆ simplify_isnan()

simplify_exprt::resultt simplify_exprt::simplify_isnan ( const unary_exprt expr)

Definition at line 36 of file simplify_expr_floatbv.cpp.

◆ simplify_isnormal()

simplify_exprt::resultt simplify_exprt::simplify_isnormal ( const unary_exprt expr)

Definition at line 48 of file simplify_expr_floatbv.cpp.

◆ simplify_lambda()

simplify_exprt::resultt simplify_exprt::simplify_lambda ( const exprt expr)

Definition at line 1355 of file simplify_expr.cpp.

◆ simplify_member()

simplify_exprt::resultt simplify_exprt::simplify_member ( const member_exprt expr)

Definition at line 19 of file simplify_expr_struct.cpp.

◆ simplify_minus()

simplify_exprt::resultt simplify_exprt::simplify_minus ( const minus_exprt expr)

Definition at line 557 of file simplify_expr_int.cpp.

◆ simplify_mod()

simplify_exprt::resultt simplify_exprt::simplify_mod ( const mod_exprt expr)

Definition at line 364 of file simplify_expr_int.cpp.

◆ simplify_mult()

simplify_exprt::resultt simplify_exprt::simplify_mult ( const mult_exprt expr)

Definition at line 158 of file simplify_expr_int.cpp.

◆ simplify_node()

simplify_exprt::resultt simplify_exprt::simplify_node ( exprt  node)

Definition at line 2371 of file simplify_expr.cpp.

◆ simplify_node_preorder()

bool simplify_exprt::simplify_node_preorder ( exprt expr)

Definition at line 2340 of file simplify_expr.cpp.

◆ simplify_not()

simplify_exprt::resultt simplify_exprt::simplify_not ( const not_exprt expr)

Definition at line 165 of file simplify_expr_boolean.cpp.

◆ simplify_object()

simplify_exprt::resultt simplify_exprt::simplify_object ( const exprt expr)

Definition at line 1488 of file simplify_expr.cpp.

◆ simplify_object_size()

simplify_exprt::resultt simplify_exprt::simplify_object_size ( const unary_exprt expr)

Definition at line 714 of file simplify_expr_pointer.cpp.

◆ simplify_plus()

simplify_exprt::resultt simplify_exprt::simplify_plus ( const plus_exprt expr)

Definition at line 401 of file simplify_expr_int.cpp.

◆ simplify_pointer_object()

simplify_exprt::resultt simplify_exprt::simplify_pointer_object ( const unary_exprt expr)

Definition at line 540 of file simplify_expr_pointer.cpp.

◆ simplify_pointer_offset()

simplify_exprt::resultt simplify_exprt::simplify_pointer_offset ( const unary_exprt expr)

Definition at line 250 of file simplify_expr_pointer.cpp.

◆ simplify_popcount()

simplify_exprt::resultt simplify_exprt::simplify_popcount ( const popcount_exprt expr)

Definition at line 127 of file simplify_expr.cpp.

◆ simplify_power()

simplify_exprt::resultt simplify_exprt::simplify_power ( const binary_exprt expr)

Definition at line 1007 of file simplify_expr_int.cpp.

◆ simplify_rec()

simplify_exprt::resultt simplify_exprt::simplify_rec ( const exprt expr)

Definition at line 2603 of file simplify_expr.cpp.

◆ simplify_same_object()

resultt simplify_exprt::simplify_same_object ( const unary_exprt )

◆ simplify_shifts()

simplify_exprt::resultt simplify_exprt::simplify_shifts ( const shift_exprt expr)

Definition at line 899 of file simplify_expr_int.cpp.

◆ simplify_sign()

simplify_exprt::resultt simplify_exprt::simplify_sign ( const sign_exprt expr)

Definition at line 101 of file simplify_expr.cpp.

◆ simplify_typecast()

simplify_exprt::resultt simplify_exprt::simplify_typecast ( const typecast_exprt expr)

Definition at line 678 of file simplify_expr.cpp.

◆ simplify_unary_minus()

simplify_exprt::resultt simplify_exprt::simplify_unary_minus ( const unary_minus_exprt expr)

Definition at line 1111 of file simplify_expr_int.cpp.

◆ simplify_unary_plus()

simplify_exprt::resultt simplify_exprt::simplify_unary_plus ( const unary_plus_exprt expr)

Definition at line 1104 of file simplify_expr_int.cpp.

◆ simplify_update()

simplify_exprt::resultt simplify_exprt::simplify_update ( const update_exprt expr)

Definition at line 1440 of file simplify_expr.cpp.

◆ simplify_with()

simplify_exprt::resultt simplify_exprt::simplify_with ( const with_exprt expr)

Definition at line 1360 of file simplify_expr.cpp.

◆ unchanged()

static resultt simplify_exprt::unchanged ( exprt  expr)
inlinestatic

Definition at line 130 of file simplify_expr_class.h.

Member Data Documentation

◆ do_simplify_if

bool simplify_exprt::do_simplify_if

Definition at line 93 of file simplify_expr_class.h.

◆ ns

const namespacet& simplify_exprt::ns
protected

Definition at line 246 of file simplify_expr_class.h.


The documentation for this class was generated from the following files: