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
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);
159 #ifdef DEBUG_ON_DEMAND
162 #ifdef USE_LOCAL_REPLACE_MAP
167 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H
bool simplify_node(exprt &expr)
virtual ~simplify_exprt()
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
bool simplify_if_disj(exprt &expr, const exprt &cond)
bool simplify_pointer_object(exprt &expr)
bool simplify_extractbit(exprt &expr)
bool simplify_index(exprt &expr)
bool simplify_minus(exprt &expr)
bool simplify_mult(exprt &expr)
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
bool simplify_inequality_pointer_object(exprt &expr)
bool simplify_dynamic_size(exprt &expr)
bool simplify_isnormal(exprt &expr)
bool simplify_if_preorder(if_exprt &expr)
The type of an expression, extends irept.
simplify_exprt(const namespacet &_ns)
The trinary if-then-else operator.
virtual bool simplify(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool get_values(const exprt &expr, value_listt &value_list)
Base class for all expressions.
bool simplify_if_cond(exprt &expr)
bool simplify_bitwise(exprt &expr)
bool simplify_inequality_not_constant(exprt &expr)
bool simplify_lambda(exprt &expr)
bool simplify_boolean(exprt &expr)
bool simplify_popcount(popcount_exprt &expr)
bool simplify_abs(exprt &expr)
bool simplify_dynamic_object(exprt &expr)
bool simplify_typecast(exprt &expr)
bool simplify_member(exprt &expr)
bool simplify_good_pointer(exprt &expr)
bool simplify_concatenation(exprt &expr)
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool simplify_inequality_address_of(exprt &expr)
bool simplify_shifts(exprt &expr)
bool simplify_not(exprt &expr)
bool simplify_update(exprt &expr)
std::set< mp_integer > value_listt
static bool is_bitvector_type(const typet &type)
bool simplify_unary_minus(exprt &expr)
bool simplify_invalid_pointer(exprt &expr)
bool simplify_node_preorder(exprt &expr)
bool simplify_object_size(exprt &expr)
bool simplify_bswap(bswap_exprt &expr)
bool simplify_sign(exprt &expr)
bool simplify_bitnot(exprt &expr)
bool simplify_same_object(exprt &expr)
const irep_idt & id() const
bool simplify_unary_plus(exprt &expr)
bool simplify_pointer_offset(exprt &expr)
nonstd::optional< T > optionalt
bool simplify_floatbv_op(exprt &expr)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Extract member of struct or union.
bool simplify_power(exprt &expr)
bool simplify_ieee_float_relation(exprt &expr)
static tvt objects_equal(const exprt &a, const exprt &b)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
bool simplify_isinf(exprt &expr)
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify_address_of(exprt &expr)
bool simplify_rec(exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
bool simplify_isnan(exprt &expr)
bool simplify_object(exprt &expr)
bool simplify_mod(exprt &expr)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
bool simplify_inequality_constant(exprt &expr)
bool simplify_if(if_exprt &expr)
The byte swap expression.
bool simplify_plus(exprt &expr)
The popcount (counting the number of bits set to 1) expression.
bool simplify_address_of_arg(exprt &expr)
bool eliminate_common_addends(exprt &op0, exprt &op1)
bool simplify_with(exprt &expr)
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.
bool simplify_dereference(exprt &expr)
bool simplify_byte_extract(byte_extract_exprt &expr)
bool simplify_div(exprt &expr)
bool simplify_floatbv_typecast(exprt &expr)