28 if(index.
id()==ID_div &&
31 if(index.
op0().
id()==ID_mult &&
39 else if(index.
op0().
id()==ID_mult &&
49 if(array.
id()==ID_lambda)
53 const exprt &lambda_expr=array;
66 else if(array.
id()==ID_with)
70 const exprt &with_expr=array;
75 if(with_expr.
op1()==expr.
op1())
88 if(equality_expr.lhs().type()!=equality_expr.rhs().type())
95 new_index_expr.
array()=with_expr.
op0();
100 if(equality_expr.is_true())
102 expr=with_expr.
op2();
105 else if(equality_expr.is_false())
107 expr.
swap(new_index_expr);
111 if_exprt if_expr(equality_expr, with_expr.
op2(), new_index_expr);
119 else if(array.
id()==ID_constant ||
120 array.
id()==ID_array)
127 else if(i<0 || i>=array.
operands().size())
139 else if(array.
id()==ID_string_constant)
148 else if(i<0 || i>value.
size())
161 else if(array.
id()==ID_array_of)
170 else if(array.
id()==
"array-list")
173 for(
size_t i=0; i<array.
operands().size()/2; i++)
186 else if(array.
id()==ID_byte_extract_little_endian ||
187 array.
id()==ID_byte_extract_big_endian)
191 if(array_type.
id()==ID_array)
214 else if(array.
id()==ID_if)
The type of an expression.
const typet & follow(const typet &src) const
bool simplify_node(exprt &expr)
bool simplify_index(exprt &expr)
void copy_to_operands(const exprt &expr)
The trinary if-then-else operator.
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
bool simplify_rec(exprt &expr)
Base class for all expressions.
virtual bool simplify(exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
void make_typecast(const typet &_type)
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==