Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
11 #define CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
14 #ifdef DEBUG_ON_DEMAND
25 #ifdef USE_LOCAL_REPLACE_MAP
69 #define forall_value_list(it, value_list) \
70 for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
71 it!=(value_list).end(); ++it)
79 #ifdef DEBUG_ON_DEMAND
83 #ifdef DEBUG_ON_DEMAND
85 debug_on=stat(
"SIMP_DEBUG", &f)==0;
95 template <
typename T = exprt>
201 exprt &expr,
const exprt &cond,
bool truth,
bool &new_truth);
234 return type.
id()==ID_unsignedbv ||
235 type.
id()==ID_signedbv ||
241 bits2expr(
const std::string &bits,
const typet &type,
bool little_endian);
247 #ifdef DEBUG_ON_DEMAND
250 #ifdef USE_LOCAL_REPLACE_MAP
256 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
Operator to update elements in structs and arrays.
virtual ~simplify_exprt()
resultt simplify_rec(const exprt &)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_isnormal(const unary_exprt &)
bool simplify_if_disj(exprt &expr, const exprt &cond)
A base class for multi-ary expressions Associativity is not specified.
resultt simplify_shifts(const shift_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
resultt simplify_address_of(const address_of_exprt &)
resultt
The result of goto verifying.
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_bitnot(const bitnot_exprt &)
The type of an expression, extends irept.
Operator to dereference a pointer.
simplify_exprt(const namespacet &_ns)
The trinary if-then-else operator.
resultt simplify_popcount(const popcount_exprt &)
resultt simplify_inequality_address_of(const binary_relation_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_is_dynamic_object(const unary_exprt &)
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool get_values(const exprt &expr, value_listt &value_list)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian)
resultt simplify_update(const update_exprt &)
The plus expression Associativity is not specified.
resultt simplify_boolean(const exprt &)
Base class for all expressions.
bool simplify_if_cond(exprt &expr)
Generic base class for unary expressions.
resultt simplify_extractbit(const extractbit_exprt &)
A base class for binary expressions.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Concatenation of bit-vector operands.
resultt simplify_complex(const unary_exprt &)
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_not(const not_exprt &)
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
static resultt unchanged(exprt expr)
resultt simplify_node(exprt)
Defines typet, type_with_subtypet and type_with_subtypest.
resultt simplify_if(const if_exprt &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
resultt simplify_minus(const minus_exprt &)
resultt simplify_dynamic_size(const unary_exprt &)
resultt simplify_same_object(const unary_exprt &)
resultt simplify_power(const binary_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_mod(const mod_exprt &)
Semantic type conversion from/to floating-point formats.
resultt simplify_isnan(const unary_exprt &)
static resultt changed(resultt<> result)
std::set< mp_integer > value_listt
static bool is_bitvector_type(const typet &type)
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
resultt simplify_bswap(const bswap_exprt &)
bool simplify_node_preorder(exprt &expr)
enum simplify_exprt::resultt::expr_changedt expr_changed
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
The unary minus expression.
resultt simplify_good_pointer(const unary_exprt &)
const irep_idt & id() const
The unary plus expression.
resultt simplify_mult(const mult_exprt &)
resultt simplify_with(const with_exprt &)
resultt(expr_changedt _expr_changed, T _expr)
resultt simplify_unary_minus(const unary_minus_exprt &)
nonstd::optional< T > optionalt
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_pointer_object(const unary_exprt &)
Operator to update elements in structs and arrays.
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
resultt simplify_index(const index_exprt &)
resultt(T _expr)
conversion from expression, thus not 'explicit' marks the expression as "CHANGED"
Bit-wise negation of bit-vectors.
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Extract member of struct or union.
resultt simplify_member(const member_exprt &)
A base class for shift operators.
resultt simplify_object(const exprt &)
static tvt objects_equal(const exprt &a, const exprt &b)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
resultt simplify_sign(const sign_exprt &)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
A base class for relations, i.e., binary predicates whose two operands have the same type.
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The byte swap expression.
resultt simplify_address_of_arg(const exprt &)
resultt simplify_byte_update(const byte_update_exprt &)
Operator to return the address of an object.
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
bool eliminate_common_addends(exprt &op0, exprt &op1)
resultt simplify_object_size(const unary_exprt &)
resultt simplify_abs(const abs_exprt &)
Array constructor from list of elements.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_lambda(const exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_isinf(const unary_exprt &)