10 #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H 11 #define CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H 14 #ifdef DEBUG_ON_DEMAND 23 #ifdef USE_LOCAL_REPLACE_MAP 39 #define forall_value_list(it, value_list) \ 40 for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \ 41 it!=(value_list).end(); ++it) 49 #ifdef DEBUG_ON_DEMAND
53 #ifdef DEBUG_ON_DEMAND 55 debug_on=stat(
"SIMP_DEBUG", &f)==0;
119 exprt &expr,
const exprt &cond,
bool truth,
bool &new_truth);
146 return type.
id()==ID_unsignedbv ||
147 type.
id()==ID_signedbv ||
153 const std::string &bits,
const typet &type,
bool little_endian);
158 #ifdef DEBUG_ON_DEMAND 161 #ifdef USE_LOCAL_REPLACE_MAP 166 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H The type of an expression.
bool simplify_abs(exprt &expr)
bool simplify_member(exprt &expr)
bool simplify_same_object(exprt &expr)
bool simplify_sign(exprt &expr)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
bool simplify_pointer_object(exprt &expr)
bool simplify_popcount(popcount_exprt &expr)
bool simplify_node(exprt &expr)
bool simplify_if_cond(exprt &expr)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
bool simplify_shifts(exprt &expr)
bool simplify_index(exprt &expr)
bool simplify_concatenation(exprt &expr)
bool simplify_dynamic_object(exprt &expr)
std::string expr2bits(const exprt &expr, bool little_endian)
bool simplify_lambda(exprt &expr)
bool simplify_inequality_pointer_object(exprt &expr)
The trinary if-then-else operator.
bool simplify_mult(exprt &expr)
bool simplify_address_of_arg(exprt &expr)
bool simplify_mod(exprt &expr)
bool simplify_with(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool simplify_node_preorder(exprt &expr)
Extract member of struct or union.
bool simplify_bswap(bswap_exprt &expr)
virtual ~simplify_exprt()
bool simplify_if(if_exprt &expr)
bool simplify_inequality_constant(exprt &expr)
simplify_exprt(const namespacet &_ns)
const irep_idt & id() const
bool simplify_good_pointer(exprt &expr)
bool simplify_object(exprt &expr)
bool simplify_floatbv_op(exprt &expr)
bool simplify_div(exprt &expr)
bool simplify_boolean(exprt &expr)
bool simplify_if_disj(exprt &expr, const exprt &cond)
bool simplify_address_of(exprt &expr)
bool simplify_pointer_offset(exprt &expr)
bool simplify_isinf(exprt &expr)
bool simplify_byte_extract(byte_extract_exprt &expr)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
bool simplify_dynamic_size(exprt &expr)
bool simplify_unary_plus(exprt &expr)
bool get_values(const exprt &expr, value_listt &value_list)
bool simplify_floatbv_typecast(exprt &expr)
static tvt objects_equal(const exprt &a, const exprt &b)
bool simplify_if_preorder(if_exprt &expr)
bool simplify_typecast(exprt &expr)
bool simplify_rec(exprt &expr)
bool eliminate_common_addends(exprt &op0, exprt &op1)
The popcount (counting the number of bits set to 1) expression.
bool simplify_unary_minus(exprt &expr)
Base class for all expressions.
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
bool simplify_ieee_float_relation(exprt &expr)
bool simplify_update(exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
virtual bool simplify(exprt &expr)
bool simplify_inequality_not_constant(exprt &expr)
bool simplify_dereference(exprt &expr)
bool simplify_not(exprt &expr)
bool simplify_inequality_address_of(exprt &expr)
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
bool simplify_invalid_pointer(exprt &expr)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
bool simplify_isnormal(exprt &expr)
bool simplify_object_size(exprt &expr)
The byte swap expression.
bool simplify_plus(exprt &expr)
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
static bool is_bitvector_type(const typet &type)
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify_bitnot(exprt &expr)
bool simplify_isnan(exprt &expr)
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.