Go to the documentation of this file.
25 if(index.
id()==ID_div &&
28 if(index.
op0().
id()==ID_mult &&
36 else if(index.
op0().
id()==ID_mult &&
46 if(array.
id()==ID_lambda)
50 const exprt &lambda_expr=array;
63 else if(array.
id()==ID_with)
67 const exprt &with_expr=array;
72 if(with_expr.
op1()==expr.
op1())
85 if(equality_expr.lhs().type()!=equality_expr.rhs().type())
92 new_index_expr.
array()=with_expr.
op0();
97 if(equality_expr.is_true())
102 else if(equality_expr.is_false())
104 expr.
swap(new_index_expr);
108 if_exprt if_expr(equality_expr, with_expr.
op2(), new_index_expr);
116 else if(array.
id()==ID_constant ||
117 array.
id()==ID_array)
119 const auto i = numeric_cast<mp_integer>(expr.
op1());
124 else if(*i < 0 || *i >= array.
operands().size())
131 exprt tmp = array.
operands()[numeric_cast_v<std::size_t>(*i)];
136 else if(array.
id()==ID_string_constant)
138 const auto i = numeric_cast<mp_integer>(expr.
op1());
145 else if(*i < 0 || *i > value.size())
153 (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
159 else if(array.
id()==ID_array_of)
168 else if(array.
id() == ID_array_list)
171 for(
size_t i=0; i<array.
operands().size()/2; i++)
184 else if(array.
id()==ID_byte_extract_little_endian ||
185 array.
id()==ID_byte_extract_big_endian)
187 if(array.
type().
id() == ID_array)
195 if(!sub_size.has_value())
205 expr.
swap(result_expr);
212 else if(array.
id()==ID_if)
bool simplify_node(exprt &expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool simplify_index(exprt &expr)
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The trinary if-then-else operator.
virtual bool simplify(exprt &expr)
The plus expression Associativity is not specified.
Base class for all expressions.
typet & type()
Return the type of the expression.
Binary multiplication Associativity is not specified.
const irep_idt & id() const
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const irep_idt & get(const irep_namet &name) const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify_rec(exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
bool simplify_if(if_exprt &expr)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.