22 bool no_change =
true;
28 auto &index = new_expr.
index();
29 auto &array = new_expr.array();
33 if(index.id() == ID_div)
38 index_div_expr.dividend().id() == ID_mult &&
39 index_div_expr.dividend().operands().size() == 2 &&
40 to_mult_expr(index_div_expr.dividend()).
op1() == index_div_expr.divisor())
47 index_div_expr.dividend().id() == ID_mult &&
48 index_div_expr.dividend().operands().size() == 2 &&
49 to_mult_expr(index_div_expr.dividend()).
op0() == index_div_expr.divisor())
57 if(array.id() == ID_array_comprehension)
63 if(index.type() == comprehension.arg().type())
65 exprt tmp = comprehension.body();
70 else if(array.id()==ID_with)
74 if(array.operands().size() != 3)
79 if(with_expr.where() == index)
82 return with_expr.new_value();
88 const exprt rhs_casted =
94 index_exprt(with_expr.old(), index, new_expr.type()));
98 return with_expr.new_value();
102 return new_index_expr;
105 if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
110 array.id() == ID_constant || array.id() == ID_array ||
111 array.id() == ID_vector)
113 const auto i = numeric_cast<mp_integer>(index);
118 else if(*i < 0 || *i >= array.operands().size())
125 return array.operands()[numeric_cast_v<std::size_t>(*i)];
128 else if(array.id()==ID_string_constant)
130 const auto i = numeric_cast<mp_integer>(index);
137 else if(*i < 0 || *i > value.size())
145 (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
149 else if(array.id()==ID_array_of)
153 else if(array.id() == ID_array_list)
156 for(
size_t i=0; i<array.operands().size()/2; i++)
162 return array.operands()[i * 2 + 1];
166 else if(array.id()==ID_byte_extract_little_endian ||
167 array.id()==ID_byte_extract_big_endian)
171 if(array.type().id() == ID_array || array.type().id() == ID_vector)
174 if(array.type().id() == ID_array)
183 if(!sub_size.has_value())
188 from_integer(*sub_size, byte_extract_expr.offset().type()), index);
192 exprt result_expr(array.id(), expr.
type());
198 else if(array.id()==ID_if)
215 return std::move(new_expr);
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The trinary if-then-else operator.
Binary multiplication Associativity is not specified.
The plus expression Associativity is not specified.
static resultt changed(resultt<> result)
resultt simplify_if(const if_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_index(const index_exprt &)
static resultt unchanged(exprt expr)
virtual bool simplify(exprt &expr)
resultt simplify_node(exprt)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
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.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)