cprover
simplify_exprt Class Reference

#include <simplify_expr_class.h>

+ Collaboration diagram for simplify_exprt:

Public Types

typedef std::set< mp_integervalue_listt
 

Public Member Functions

 simplify_exprt (const namespacet &_ns)
 
virtual ~simplify_exprt ()
 
bool simplify_typecast (exprt &expr)
 
bool simplify_extractbit (exprt &expr)
 
bool simplify_extractbits (extractbits_exprt &expr)
 Simplifies extracting of bits from a constant. More...
 
bool simplify_concatenation (exprt &expr)
 
bool simplify_mult (exprt &expr)
 
bool simplify_div (exprt &expr)
 
bool simplify_mod (exprt &expr)
 
bool simplify_plus (exprt &expr)
 
bool simplify_minus (exprt &expr)
 
bool simplify_floatbv_op (exprt &expr)
 
bool simplify_floatbv_typecast (exprt &expr)
 
bool simplify_shifts (exprt &expr)
 
bool simplify_power (exprt &expr)
 
bool simplify_bitwise (exprt &expr)
 
bool simplify_if_preorder (if_exprt &expr)
 
bool simplify_if (if_exprt &expr)
 
bool simplify_bitnot (exprt &expr)
 
bool simplify_not (exprt &expr)
 
bool simplify_boolean (exprt &expr)
 
bool simplify_inequality (exprt &expr)
 simplifies inequalities !=, <=, <, >=, >, and also == More...
 
bool simplify_ieee_float_relation (exprt &expr)
 
bool simplify_lambda (exprt &expr)
 
bool simplify_with (exprt &expr)
 
bool simplify_update (exprt &expr)
 
bool simplify_index (exprt &expr)
 
bool simplify_member (exprt &expr)
 
bool simplify_byte_update (byte_update_exprt &expr)
 
bool simplify_byte_extract (byte_extract_exprt &expr)
 
bool simplify_pointer_object (exprt &expr)
 
bool simplify_object_size (exprt &expr)
 
bool simplify_dynamic_size (exprt &expr)
 
bool simplify_dynamic_object (exprt &expr)
 
bool simplify_invalid_pointer (exprt &expr)
 
bool simplify_same_object (exprt &expr)
 
bool simplify_good_pointer (exprt &expr)
 
bool simplify_object (exprt &expr)
 
bool simplify_unary_minus (exprt &expr)
 
bool simplify_unary_plus (exprt &expr)
 
bool simplify_dereference (exprt &expr)
 
bool simplify_address_of (exprt &expr)
 
bool simplify_pointer_offset (exprt &expr)
 
bool simplify_bswap (bswap_exprt &expr)
 
bool simplify_isinf (exprt &expr)
 
bool simplify_isnan (exprt &expr)
 
bool simplify_isnormal (exprt &expr)
 
bool simplify_abs (exprt &expr)
 
bool simplify_sign (exprt &expr)
 
bool simplify_popcount (popcount_exprt &expr)
 
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)
 
bool simplify_address_of_arg (exprt &expr)
 
bool simplify_inequality_constant (exprt &expr)
 
bool simplify_inequality_not_constant (exprt &expr)
 
bool simplify_inequality_address_of (exprt &expr)
 
bool simplify_inequality_pointer_object (exprt &expr)
 
bool simplify_node (exprt &expr)
 
bool simplify_node_preorder (exprt &expr)
 
bool simplify_rec (exprt &expr)
 
virtual bool simplify (exprt &expr)
 
bool get_values (const exprt &expr, value_listt &value_list)
 
exprt bits2expr (const std::string &bits, const typet &type, bool little_endian)
 
optionalt< std::string > expr2bits (const exprt &, bool little_endian)
 

Static Public Member Functions

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 43 of file simplify_expr_class.h.

Member Typedef Documentation

◆ value_listt

Definition at line 141 of file simplify_expr_class.h.

Constructor & Destructor Documentation

◆ simplify_exprt()

simplify_exprt::simplify_exprt ( const namespacet _ns)
inlineexplicit

Definition at line 46 of file simplify_expr_class.h.

◆ ~simplify_exprt()

virtual simplify_exprt::~simplify_exprt ( )
inlinevirtual

Definition at line 59 of file simplify_expr_class.h.

Member Function Documentation

◆ bits2expr()

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

Definition at line 1431 of file simplify_expr.cpp.

◆ eliminate_common_addends()

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

Definition at line 1492 of file simplify_expr_int.cpp.

◆ expr2bits()

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

Definition at line 1547 of file simplify_expr.cpp.

◆ get_values()

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

Definition at line 1182 of file simplify_expr.cpp.

◆ is_bitvector_type()

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

Definition at line 144 of file simplify_expr_class.h.

◆ objects_equal()

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

Definition at line 600 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 624 of file simplify_expr_pointer.cpp.

◆ simplify()

bool simplify_exprt::simplify ( exprt expr)
virtual

Definition at line 2306 of file simplify_expr.cpp.

◆ simplify_abs()

bool simplify_exprt::simplify_abs ( exprt expr)

Definition at line 62 of file simplify_expr.cpp.

◆ simplify_address_of()

bool simplify_exprt::simplify_address_of ( exprt expr)

Definition at line 173 of file simplify_expr_pointer.cpp.

◆ simplify_address_of_arg()

bool simplify_exprt::simplify_address_of_arg ( exprt expr)

Definition at line 52 of file simplify_expr_pointer.cpp.

◆ simplify_bitnot()

bool simplify_exprt::simplify_bitnot ( exprt expr)

Definition at line 1266 of file simplify_expr_int.cpp.

◆ simplify_bitwise()

bool simplify_exprt::simplify_bitwise ( exprt expr)

Definition at line 649 of file simplify_expr_int.cpp.

◆ simplify_boolean()

bool simplify_exprt::simplify_boolean ( exprt expr)

Definition at line 19 of file simplify_expr_boolean.cpp.

◆ simplify_bswap()

bool simplify_exprt::simplify_bswap ( bswap_exprt expr)

Definition at line 29 of file simplify_expr_int.cpp.

◆ simplify_byte_extract()

bool simplify_exprt::simplify_byte_extract ( byte_extract_exprt expr)

Definition at line 1619 of file simplify_expr.cpp.

◆ simplify_byte_update()

bool simplify_exprt::simplify_byte_update ( byte_update_exprt expr)

Definition at line 1795 of file simplify_expr.cpp.

◆ simplify_concatenation()

bool simplify_exprt::simplify_concatenation ( exprt expr)

Definition at line 869 of file simplify_expr_int.cpp.

◆ simplify_dereference()

bool simplify_exprt::simplify_dereference ( exprt expr)

Definition at line 737 of file simplify_expr.cpp.

◆ simplify_div()

bool simplify_exprt::simplify_div ( exprt expr)

Definition at line 268 of file simplify_expr_int.cpp.

◆ simplify_dynamic_object()

bool simplify_exprt::simplify_dynamic_object ( exprt expr)

Definition at line 515 of file simplify_expr_pointer.cpp.

◆ simplify_dynamic_size()

bool simplify_exprt::simplify_dynamic_size ( exprt expr)

◆ simplify_extractbit()

bool simplify_exprt::simplify_extractbit ( exprt expr)

Definition at line 835 of file simplify_expr_int.cpp.

◆ simplify_extractbits()

bool simplify_exprt::simplify_extractbits ( extractbits_exprt expr)

Simplifies extracting of bits from a constant.

Definition at line 1102 of file simplify_expr_int.cpp.

◆ simplify_floatbv_op()

bool simplify_exprt::simplify_floatbv_op ( exprt expr)

Definition at line 283 of file simplify_expr_floatbv.cpp.

◆ simplify_floatbv_typecast()

bool simplify_exprt::simplify_floatbv_typecast ( exprt expr)

Definition at line 141 of file simplify_expr_floatbv.cpp.

◆ simplify_good_pointer()

bool simplify_exprt::simplify_good_pointer ( exprt expr)

Definition at line 694 of file simplify_expr_pointer.cpp.

◆ simplify_ieee_float_relation()

bool simplify_exprt::simplify_ieee_float_relation ( exprt expr)

Definition at line 354 of file simplify_expr_floatbv.cpp.

◆ simplify_if()

bool simplify_exprt::simplify_if ( if_exprt expr)

Definition at line 1078 of file simplify_expr.cpp.

◆ simplify_if_branch()

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

Definition at line 925 of file simplify_expr.cpp.

◆ simplify_if_cond()

bool simplify_exprt::simplify_if_cond ( exprt expr)

Definition at line 957 of file simplify_expr.cpp.

◆ simplify_if_conj()

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

Definition at line 883 of file simplify_expr.cpp.

◆ simplify_if_disj()

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

Definition at line 904 of file simplify_expr.cpp.

◆ simplify_if_implies()

bool simplify_exprt::simplify_if_implies ( exprt expr,
const exprt cond,
bool  truth,
bool &  new_truth 
)

Definition at line 795 of file simplify_expr.cpp.

◆ simplify_if_preorder()

bool simplify_exprt::simplify_if_preorder ( if_exprt expr)

Definition at line 993 of file simplify_expr.cpp.

◆ simplify_if_recursive()

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

Definition at line 851 of file simplify_expr.cpp.

◆ simplify_index()

bool simplify_exprt::simplify_index ( exprt expr)

Definition at line 17 of file simplify_expr_array.cpp.

◆ simplify_inequality()

bool simplify_exprt::simplify_inequality ( exprt expr)

simplifies inequalities !=, <=, <, >=, >, and also ==

Definition at line 1305 of file simplify_expr_int.cpp.

◆ simplify_inequality_address_of()

bool simplify_exprt::simplify_inequality_address_of ( exprt expr)

Definition at line 413 of file simplify_expr_pointer.cpp.

◆ simplify_inequality_constant()

bool simplify_exprt::simplify_inequality_constant ( exprt expr)
parameters: an inequality with a constant on the RHS

Definition at line 1669 of file simplify_expr_int.cpp.

◆ simplify_inequality_not_constant()

bool simplify_exprt::simplify_inequality_not_constant ( exprt expr)

Definition at line 1540 of file simplify_expr_int.cpp.

◆ simplify_inequality_pointer_object()

bool simplify_exprt::simplify_inequality_pointer_object ( exprt expr)

Definition at line 454 of file simplify_expr_pointer.cpp.

◆ simplify_invalid_pointer()

bool simplify_exprt::simplify_invalid_pointer ( exprt expr)

Definition at line 571 of file simplify_expr_pointer.cpp.

◆ simplify_isinf()

bool simplify_exprt::simplify_isinf ( exprt expr)

Definition at line 19 of file simplify_expr_floatbv.cpp.

◆ simplify_isnan()

bool simplify_exprt::simplify_isnan ( exprt expr)

Definition at line 37 of file simplify_expr_floatbv.cpp.

◆ simplify_isnormal()

bool simplify_exprt::simplify_isnormal ( exprt expr)

Definition at line 52 of file simplify_expr_floatbv.cpp.

◆ simplify_lambda()

bool simplify_exprt::simplify_lambda ( exprt expr)

Definition at line 1208 of file simplify_expr.cpp.

◆ simplify_member()

bool simplify_exprt::simplify_member ( exprt expr)

Definition at line 19 of file simplify_expr_struct.cpp.

◆ simplify_minus()

bool simplify_exprt::simplify_minus ( exprt expr)

Definition at line 592 of file simplify_expr_int.cpp.

◆ simplify_mod()

bool simplify_exprt::simplify_mod ( exprt expr)

Definition at line 388 of file simplify_expr_int.cpp.

◆ simplify_mult()

bool simplify_exprt::simplify_mult ( exprt expr)

Definition at line 160 of file simplify_expr_int.cpp.

◆ simplify_node()

bool simplify_exprt::simplify_node ( exprt expr)

Definition at line 2113 of file simplify_expr.cpp.

◆ simplify_node_preorder()

bool simplify_exprt::simplify_node_preorder ( exprt expr)

Definition at line 2088 of file simplify_expr.cpp.

◆ simplify_not()

bool simplify_exprt::simplify_not ( exprt expr)

Definition at line 159 of file simplify_expr_boolean.cpp.

◆ simplify_object()

bool simplify_exprt::simplify_object ( exprt expr)

Definition at line 1341 of file simplify_expr.cpp.

◆ simplify_object_size()

bool simplify_exprt::simplify_object_size ( exprt expr)

Definition at line 648 of file simplify_expr_pointer.cpp.

◆ simplify_plus()

bool simplify_exprt::simplify_plus ( exprt expr)

Definition at line 437 of file simplify_expr_int.cpp.

◆ simplify_pointer_object()

bool simplify_exprt::simplify_pointer_object ( exprt expr)

Definition at line 487 of file simplify_expr_pointer.cpp.

◆ simplify_pointer_offset()

bool simplify_exprt::simplify_pointer_offset ( exprt expr)

Definition at line 211 of file simplify_expr_pointer.cpp.

◆ simplify_popcount()

bool simplify_exprt::simplify_popcount ( popcount_exprt expr)

Definition at line 132 of file simplify_expr.cpp.

◆ simplify_power()

bool simplify_exprt::simplify_power ( exprt expr)

Definition at line 1079 of file simplify_expr_int.cpp.

◆ simplify_rec()

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

Definition at line 2245 of file simplify_expr.cpp.

◆ simplify_same_object()

bool simplify_exprt::simplify_same_object ( exprt expr)

◆ simplify_shifts()

bool simplify_exprt::simplify_shifts ( exprt expr)

Definition at line 967 of file simplify_expr_int.cpp.

◆ simplify_sign()

bool simplify_exprt::simplify_sign ( exprt expr)

Definition at line 102 of file simplify_expr.cpp.

◆ simplify_typecast()

bool simplify_exprt::simplify_typecast ( exprt expr)

Definition at line 160 of file simplify_expr.cpp.

◆ simplify_unary_minus()

bool simplify_exprt::simplify_unary_minus ( exprt expr)

Definition at line 1189 of file simplify_expr_int.cpp.

◆ simplify_unary_plus()

bool simplify_exprt::simplify_unary_plus ( exprt expr)

Definition at line 1179 of file simplify_expr_int.cpp.

◆ simplify_update()

bool simplify_exprt::simplify_update ( exprt expr)

Definition at line 1288 of file simplify_expr.cpp.

◆ simplify_with()

bool simplify_exprt::simplify_with ( exprt expr)

Definition at line 1215 of file simplify_expr.cpp.

Member Data Documentation

◆ do_simplify_if

bool simplify_exprt::do_simplify_if

Definition at line 63 of file simplify_expr_class.h.

◆ ns

const namespacet& simplify_exprt::ns
protected

Definition at line 158 of file simplify_expr_class.h.


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