46 struct simplify_expr_cachet
50 typedef std::unordered_map<
53 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
56 containert container_normal;
58 containert &container()
60 return container_normal;
64 simplify_expr_cachet simplify_expr_cache;
73 if(type.
id()==ID_floatbv)
79 else if(type.
id()==ID_signedbv ||
80 type.
id()==ID_unsignedbv)
82 auto value = numeric_cast<mp_integer>(
to_unary_expr(expr).op());
107 if(type.
id()==ID_floatbv)
112 else if(type.
id()==ID_signedbv ||
113 type.
id()==ID_unsignedbv)
115 const auto value = numeric_cast<mp_integer>(expr.
op());
116 if(value.has_value())
135 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
139 std::size_t result = 0;
141 for(std::size_t i = 0; i < width; i++)
194 const auto first_value_opt =
204 const auto second_value_opt =
207 if(!second_value_opt)
215 const bool includes =
241 const auto numeric_length =
278 const bool first_shorter = s1_size < s2_size;
283 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
285 if(it_pair.first == ops1.end())
294 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
306 const bool search_from_end)
308 std::size_t starting_index = 0;
313 auto &starting_index_expr = expr.
arguments().at(2);
315 if(starting_index_expr.id() != ID_constant)
326 starting_index = numeric_cast_v<std::size_t>(idx);
341 const auto search_string_size = s1_data.
operands().size();
342 if(starting_index >= search_string_size)
347 unsigned long starting_offset =
348 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
371 ? starting_index > 0 ? starting_index : search_string_size
377 auto end = std::prev(s1_data.
operands().end(), starting_offset);
378 auto it = std::find_end(
385 std::distance(s1_data.
operands().begin(), it), expr.
type());
389 auto it = std::search(
390 std::next(s1_data.
operands().begin(), starting_index),
397 std::distance(s1_data.
operands().begin(), it), expr.
type());
400 else if(expr.
arguments().at(1).id() == ID_constant)
405 const auto c1_val = numeric_cast_v<mp_integer>(c1);
407 auto pred = [&](
const exprt &c2) {
410 return c1_val == c2_val;
415 auto it = std::find_if(
416 std::next(s1_data.
operands().rbegin(), starting_offset),
421 std::distance(s1_data.
operands().begin(), it.base() - 1),
426 auto it = std::find_if(
427 std::next(s1_data.
operands().begin(), starting_index),
432 std::distance(s1_data.
operands().begin(), it), expr.
type());
452 if(expr.
arguments().at(1).id() != ID_constant)
470 const auto i_opt = numeric_cast<std::size_t>(index);
472 if(!i_opt || *i_opt >= char_seq.
operands().size())
479 if(c.type() != expr.
type())
490 auto &operands = string_data.
operands();
491 for(
auto &operand : operands)
494 auto character = numeric_cast_v<unsigned int>(constant_value);
500 if(isalpha(character))
502 if(isupper(character))
504 from_integer(tolower(character), constant_value.type());
526 const auto first_value_opt =
536 const auto second_value_opt =
539 if(!second_value_opt)
552 bool is_equal = first_value == second_value;
571 const auto first_value_opt =
581 const auto second_value_opt =
584 if(!second_value_opt)
595 if(offset.id() != ID_constant)
603 offset_int + second_value.
operands().size();
606 exprt::operandst::const_iterator second_it =
608 for(
const auto &first_op : first_value.
operands())
612 else if(second_it == second_value.
operands().end())
614 else if(first_op != *second_it)
637 if(func_id == ID_cprover_string_startswith_func)
641 else if(func_id == ID_cprover_string_endswith_func)
645 else if(func_id == ID_cprover_string_is_empty_func)
649 else if(func_id == ID_cprover_string_compare_to_func)
653 else if(func_id == ID_cprover_string_index_of_func)
657 else if(func_id == ID_cprover_string_char_at_func)
661 else if(func_id == ID_cprover_string_contains_func)
665 else if(func_id == ID_cprover_string_last_index_of_func)
669 else if(func_id == ID_cprover_string_equals_ignore_case_func)
684 if(expr.
op().
id() == ID_infinity)
689 return std::move(tmp);
696 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
706 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
707 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
711 auto new_expr = expr;
723 if(expr_type.
id()==ID_bool)
728 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
736 op_type.
id() == ID_bool &&
737 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
738 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
756 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
757 if(typecast.op().type()==expr_type)
759 return typecast.op();
765 if(expr_type.
id()==ID_c_bool &&
766 op_type.
id()!=ID_bool)
770 auto new_expr = expr;
784 return std::move(tmp);
790 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
791 op_type.
id() == ID_pointer)
793 auto new_expr = expr;
801 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
802 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
803 op_type.
id() == ID_pointer)
808 auto outer_cast = expr;
817 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
818 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
823 if(((op_plus_expr.op0().id() == ID_typecast &&
825 (op_plus_expr.op0().is_constant() &&
830 if(sub_size.has_value())
832 auto new_expr = expr;
835 if(*sub_size == 0 || *sub_size == 1)
858 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
859 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
869 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
870 op_id==ID_unary_minus ||
871 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
890 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
900 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
901 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
905 if(step.has_value() && *step != 0)
908 auto new_expr = expr;
910 new_expr.
op().
type() = size_t_type;
912 for(
auto &op : new_expr.op().operands())
914 if(op.type().id()==ID_pointer)
932 if(expr.
op().
id()==ID_if &&
939 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
941 return std::move(new_expr);
946 const exprt &operand = expr.
op();
955 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
957 if(op_type_id==ID_integer ||
958 op_type_id==ID_natural)
964 if(expr_type_id==ID_bool)
969 if(expr_type_id==ID_unsignedbv ||
970 expr_type_id==ID_signedbv ||
971 expr_type_id==ID_c_enum ||
972 expr_type_id==ID_c_bit_field ||
973 expr_type_id==ID_integer)
977 else if(expr_type_id == ID_c_enum_tag)
980 if(!c_enum_type.is_incomplete())
983 tmp.
type() = expr_type;
984 return std::move(tmp);
988 else if(op_type_id==ID_rational)
991 else if(op_type_id==ID_real)
994 else if(op_type_id==ID_bool)
996 if(expr_type_id==ID_unsignedbv ||
997 expr_type_id==ID_signedbv ||
998 expr_type_id==ID_integer ||
999 expr_type_id==ID_natural ||
1000 expr_type_id==ID_rational ||
1001 expr_type_id==ID_c_bool ||
1002 expr_type_id==ID_c_enum ||
1003 expr_type_id==ID_c_bit_field)
1014 else if(expr_type_id==ID_c_enum_tag)
1017 if(!c_enum_type.is_incomplete())
1019 unsigned int_value = operand.
is_true() ? 1u : 0u;
1021 tmp.
type()=expr_type;
1022 return std::move(tmp);
1025 else if(expr_type_id==ID_pointer &&
1032 else if(op_type_id==ID_unsignedbv ||
1033 op_type_id==ID_signedbv ||
1034 op_type_id==ID_c_bit_field ||
1035 op_type_id==ID_c_bool)
1042 if(expr_type_id==ID_bool)
1047 if(expr_type_id==ID_c_bool)
1052 if(expr_type_id==ID_integer)
1057 if(expr_type_id==ID_natural)
1065 if(expr_type_id==ID_unsignedbv ||
1066 expr_type_id==ID_signedbv ||
1067 expr_type_id==ID_bv ||
1068 expr_type_id==ID_c_bit_field)
1073 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1075 return std::move(result);
1078 if(expr_type_id==ID_c_enum_tag)
1081 if(!c_enum_type.is_incomplete())
1084 tmp.
type()=expr_type;
1085 return std::move(tmp);
1089 if(expr_type_id==ID_c_enum)
1094 if(expr_type_id==ID_fixedbv)
1106 if(expr_type_id==ID_floatbv)
1118 if(expr_type_id==ID_rational)
1124 else if(op_type_id==ID_fixedbv)
1126 if(expr_type_id==ID_unsignedbv ||
1127 expr_type_id==ID_signedbv)
1133 else if(expr_type_id==ID_fixedbv)
1140 else if(expr_type_id == ID_bv)
1146 else if(op_type_id==ID_floatbv)
1150 if(expr_type_id==ID_unsignedbv ||
1151 expr_type_id==ID_signedbv)
1156 else if(expr_type_id==ID_floatbv)
1162 else if(expr_type_id==ID_fixedbv)
1172 else if(expr_type_id == ID_bv)
1177 else if(op_type_id==ID_bv)
1180 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1181 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1182 expr_type_id == ID_c_bit_field)
1186 if(expr_type_id != ID_c_enum_tag)
1192 result.type() = tag_type;
1193 return std::move(result);
1196 else if(expr_type_id == ID_floatbv)
1201 ieee_float.unpack(int_value);
1202 return ieee_float.to_expr();
1204 else if(expr_type_id == ID_fixedbv)
1209 fixedbv.set_value(int_value);
1210 return fixedbv.to_expr();
1213 else if(op_type_id==ID_c_enum_tag)
1220 auto new_expr = expr;
1225 else if(op_type_id==ID_c_enum)
1231 auto new_expr = expr;
1237 else if(operand.
id()==ID_typecast)
1242 op_type_id == expr_type_id &&
1243 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1247 auto new_expr = expr;
1253 else if(operand.
id()==ID_address_of)
1259 o.
type().
id() == ID_array &&
1277 if(pointer.
type().
id()!=ID_pointer)
1280 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1284 auto tmp_op1 = expr;
1288 auto tmp_op2 = expr;
1292 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1297 if(pointer.
id()==ID_address_of)
1305 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1313 if(address_of.
object().
id()==ID_index)
1340 value_list.insert(int_value);
1344 else if(expr.
id()==ID_if)
1348 return get_values(if_expr.true_case(), value_list) ||
1349 get_values(if_expr.false_case(), value_list);
1362 bool no_change =
true;
1368 auto with_expr = expr;
1370 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1374 if(old_type_followed.
id() == ID_struct)
1376 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1378 while(with_expr.operands().size() > 1)
1381 with_expr.where().get(ID_component_name);
1383 if(!
to_struct_type(old_type_followed).has_component(component_name))
1386 std::size_t number =
1389 if(number >= with_expr.old().operands().size())
1392 with_expr.old().operands()[number].swap(with_expr.new_value());
1394 with_expr.operands().erase(++with_expr.operands().begin());
1395 with_expr.operands().erase(++with_expr.operands().begin());
1402 with_expr.old().type().id() == ID_array ||
1403 with_expr.old().type().id() == ID_vector)
1406 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1407 with_expr.old().id() == ID_vector)
1409 while(with_expr.operands().size() > 1)
1411 const auto i = numeric_cast<mp_integer>(with_expr.where());
1416 if(*i < 0 || *i >= with_expr.old().operands().size())
1419 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1420 with_expr.new_value());
1422 with_expr.operands().erase(++with_expr.operands().begin());
1423 with_expr.operands().erase(++with_expr.operands().begin());
1430 if(with_expr.operands().size() == 1)
1431 return with_expr.old();
1436 return std::move(with_expr);
1447 exprt *value_ptr=&updated_value;
1449 for(
const auto &e : designator)
1453 if(e.id()==ID_index_designator &&
1454 value_ptr->
id()==ID_array)
1461 if(*i < 0 || *i >= value_ptr->
operands().size())
1464 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1466 else if(e.id()==ID_member_designator &&
1467 value_ptr->
id()==ID_struct)
1470 e.get(ID_component_name);
1476 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1485 return updated_value;
1490 if(expr.
id()==ID_plus)
1492 if(expr.
type().
id()==ID_pointer)
1496 if(op.type().id() == ID_pointer)
1500 else if(expr.
id()==ID_typecast)
1503 const typet &op_type = typecast_expr.op().type();
1505 if(op_type.
id()==ID_pointer)
1510 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1517 const exprt &casted_expr = typecast_expr.op();
1518 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1522 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1526 if(cand.
id() == ID_typecast)
1530 if(typecast_op.id() == ID_address_of)
1535 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1546 else if(expr.
id()==ID_address_of)
1550 if(
object.
id() == ID_index)
1556 else if(
object.
id() == ID_member)
1568 const std::string &bits,
1575 if(!type_bits.has_value() || *type_bits != bits.size())
1579 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1580 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
1581 type.
id() == ID_c_bit_field || type.
id() == ID_pointer ||
1586 std::string tmp=bits;
1590 std::reverse(tmp.begin(), tmp.end());
1595 else if(type.
id()==ID_c_enum)
1606 else if(type.
id()==ID_c_enum_tag)
1618 else if(type.
id()==ID_union)
1628 if(!val.has_value())
1634 else if(type.
id() == ID_union_tag)
1646 else if(type.
id()==ID_struct)
1661 std::string comp_bits = std::string(
1663 numeric_cast_v<std::size_t>(m_offset_bits),
1664 numeric_cast_v<std::size_t>(*m_size));
1667 if(!comp.has_value())
1669 result.add_to_operands(std::move(*comp));
1671 m_offset_bits += *m_size;
1674 return std::move(result);
1676 else if(type.
id() == ID_struct_tag)
1688 else if(type.
id()==ID_array)
1691 const auto &size_expr = array_type.
size();
1695 const std::size_t number_of_elements =
1699 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
1701 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
1706 for(std::size_t i = 0; i < number_of_elements; ++i)
1708 std::string el_bits=std::string(bits, i*el_size, el_size);
1712 result.add_to_operands(std::move(*el));
1715 return std::move(result);
1717 else if(type.
id() == ID_vector)
1721 const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.
size());
1724 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
1726 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
1731 for(std::size_t i = 0; i < n_el; ++i)
1733 std::string el_bits = std::string(bits, i * el_size, el_size);
1737 result.add_to_operands(std::move(*el));
1740 return std::move(result);
1742 else if(type.
id() == ID_complex)
1747 CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
1749 const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
1752 bits.substr(0, sub_size), complex_type.
subtype(), little_endian);
1755 if(!real.has_value() || !imag.has_value())
1771 if(expr.
id()==ID_constant)
1776 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
1777 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
1778 type.
id() == ID_c_bit_field || type.
id() == ID_bv)
1784 std::string result(width,
' ');
1791 else if(type.
id() == ID_pointer)
1798 else if(type.
id() == ID_c_enum_tag)
1803 else if(type.
id() == ID_c_enum)
1809 else if(expr.
id() == ID_string_constant)
1813 else if(expr.
id()==ID_union)
1818 expr.
id() == ID_struct || expr.
id() == ID_array || expr.
id() == ID_vector ||
1819 expr.
id() == ID_complex)
1825 if(!tmp.has_value())
1827 result+=tmp.value();
1839 if(content.
id() != ID_address_of)
1846 if(array_pointer.object().id() != ID_index)
1851 const auto &array_start =
to_index_expr(array_pointer.object());
1853 if(array_start.array().id() != ID_symbol ||
1854 array_start.array().type().id() != ID_array)
1861 const symbolt *symbol_ptr =
nullptr;
1863 if(ns.
lookup(array.get_identifier(), symbol_ptr) ||
1864 symbol_ptr->
value.
id() != ID_array)
1878 if(expr.
op().
id()==ID_if)
1892 if(expr.
op().
id()==expr.
id())
1906 ((expr.
id() == ID_byte_extract_big_endian &&
1907 expr.
op().
id() == ID_byte_update_big_endian) ||
1908 (expr.
id() == ID_byte_extract_little_endian &&
1909 expr.
op().
id() == ID_byte_update_little_endian)) &&
1914 if(expr.
type() == op_byte_update.value().type())
1916 return op_byte_update.value();
1919 el_size.has_value() &&
1923 tmp.
op() = op_byte_update.value();
1931 auto offset = numeric_cast<mp_integer>(expr.
offset());
1932 if(!offset.has_value() || *offset < 0)
1945 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1953 if(!el_size.has_value() || *el_size == 0)
1956 if(expr.
op().
id()==ID_array_of &&
1959 const auto const_bits_opt=
1963 if(!const_bits_opt.has_value())
1966 std::string const_bits=const_bits_opt.value();
1968 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1971 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1972 const_bits+=const_bits;
1974 std::string el_bits = std::string(
1976 numeric_cast_v<std::size_t>(*offset * 8),
1977 numeric_cast_v<std::size_t>(*el_size));
1980 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian);
1983 return std::move(*tmp);
1988 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
2000 expr2bits(expr.
op(), expr.
id()==ID_byte_extract_little_endian);
2003 const bool struct_has_flexible_array_member =
has_subtype(
2005 [&](
const typet &type) {
2006 if(type.id() != ID_struct && type.id() != ID_struct_tag)
2009 const struct_typet &st = to_struct_type(ns.follow(type));
2010 const auto &comps = st.components();
2011 if(comps.empty() || comps.back().type().id() != ID_array)
2015 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
2016 return !size.has_value() || *size <= 1;
2020 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
2021 !struct_has_flexible_array_member)
2023 std::string bits_cut = std::string(
2025 numeric_cast_v<std::size_t>(*offset * 8),
2026 numeric_cast_v<std::size_t>(*el_size));
2029 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian);
2032 return std::move(*tmp);
2038 if(!subexpr.has_value() || subexpr.value() == expr)
2050 expr.
id() == expr.
op().
id() &&
2056 return std::move(tmp);
2059 const exprt &root = expr.
op();
2067 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2068 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2071 expr.
id()==ID_byte_update_little_endian ?
2072 ID_byte_extract_little_endian :
2073 ID_byte_extract_big_endian,
2074 value, offset, expr.
type());
2087 if(expr.
id()!=ID_byte_update_little_endian)
2090 if(value.
id()==ID_with)
2094 if(with.
old().
id()==ID_byte_extract_little_endian)
2101 if(!(root==extract.
op()))
2103 if(!(offset==extract.
offset()))
2107 if(tp.
id()==ID_struct)
2114 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2129 tmp.set_value(std::move(new_value));
2134 else if(tp.
id()==ID_array)
2140 exprt index_offset =
2154 tmp.set_value(std::move(new_value));
2162 const auto offset_int = numeric_cast<mp_integer>(offset);
2163 if(!offset_int.has_value() || *offset_int < 0)
2169 if(!val_size.has_value() || *val_size == 0)
2174 if(op_type.
id()==ID_struct)
2193 if(!m_offset.has_value())
2200 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
2206 mp_integer m_size_bytes = (*m_size_bits) / 8;
2209 if(*m_offset + m_size_bytes <= *offset_int)
2213 update_size.has_value() && *update_size > 0 &&
2214 *m_offset >= *offset_int + *update_size)
2222 exprt member_name(ID_member_name);
2223 member_name.
set(ID_component_name,
component.get_name());
2228 *m_offset < *offset_int ||
2229 (*m_offset == *offset_int && update_size.has_value() &&
2230 *update_size > 0 && m_size_bytes > *update_size))
2233 ID_byte_update_little_endian,
2241 update_size.has_value() && *update_size > 0 &&
2242 *m_offset + m_size_bytes > *offset_int + *update_size)
2251 ID_byte_extract_little_endian,
2266 if(root.
id()==ID_array)
2270 if(!el_size.has_value() || *el_size == 0 ||
2271 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2281 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2284 if(*offset_int * 8 < m_offset_bits + *el_size)
2286 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2287 bytes_req-=val_offset;
2288 if(val_offset + bytes_req > (*val_size) / 8)
2289 bytes_req = (*val_size) / 8 - val_offset;
2302 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2307 val_offset+=bytes_req;
2310 m_offset_bits += *el_size;
2313 return std::move(result);
2322 if(expr.
id() == ID_complex_real)
2326 if(complex_real_expr.op().id() == ID_complex)
2329 else if(expr.
id() == ID_complex_imag)
2333 if(complex_imag_expr.op().id() == ID_complex)
2346 if(expr.
id()==ID_address_of)
2350 else if(expr.
id()==ID_if)
2359 if(r_it.has_changed())
2387 if(expr.
id()==ID_typecast)
2391 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2392 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2393 expr.
id()==ID_ge || expr.
id()==ID_le)
2397 else if(expr.
id()==ID_if)
2401 else if(expr.
id()==ID_lambda)
2405 else if(expr.
id()==ID_with)
2409 else if(expr.
id()==ID_update)
2413 else if(expr.
id()==ID_index)
2417 else if(expr.
id()==ID_member)
2421 else if(expr.
id()==ID_byte_update_little_endian ||
2422 expr.
id()==ID_byte_update_big_endian)
2426 else if(expr.
id()==ID_byte_extract_little_endian ||
2427 expr.
id()==ID_byte_extract_big_endian)
2431 else if(expr.
id()==ID_pointer_object)
2435 else if(expr.
id() == ID_is_dynamic_object)
2439 else if(expr.
id() == ID_is_invalid_pointer)
2443 else if(expr.
id()==ID_object_size)
2447 else if(expr.
id()==ID_good_pointer)
2451 else if(expr.
id()==ID_div)
2455 else if(expr.
id()==ID_mod)
2459 else if(expr.
id()==ID_bitnot)
2463 else if(expr.
id()==ID_bitand ||
2464 expr.
id()==ID_bitor ||
2465 expr.
id()==ID_bitxor)
2469 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2473 else if(expr.
id()==ID_power)
2477 else if(expr.
id()==ID_plus)
2481 else if(expr.
id()==ID_minus)
2485 else if(expr.
id()==ID_mult)
2489 else if(expr.
id()==ID_floatbv_plus ||
2490 expr.
id()==ID_floatbv_minus ||
2491 expr.
id()==ID_floatbv_mult ||
2492 expr.
id()==ID_floatbv_div)
2496 else if(expr.
id()==ID_floatbv_typecast)
2500 else if(expr.
id()==ID_unary_minus)
2504 else if(expr.
id()==ID_unary_plus)
2508 else if(expr.
id()==ID_not)
2512 else if(expr.
id()==ID_implies ||
2513 expr.
id()==ID_or || expr.
id()==ID_xor ||
2518 else if(expr.
id()==ID_dereference)
2522 else if(expr.
id()==ID_address_of)
2526 else if(expr.
id()==ID_pointer_offset)
2530 else if(expr.
id()==ID_extractbit)
2534 else if(expr.
id()==ID_concatenation)
2538 else if(expr.
id()==ID_extractbits)
2542 else if(expr.
id()==ID_ieee_float_equal ||
2543 expr.
id()==ID_ieee_float_notequal)
2547 else if(expr.
id() == ID_bswap)
2551 else if(expr.
id()==ID_isinf)
2555 else if(expr.
id()==ID_isnan)
2559 else if(expr.
id()==ID_isnormal)
2563 else if(expr.
id()==ID_abs)
2567 else if(expr.
id()==ID_sign)
2571 else if(expr.
id() == ID_popcount)
2575 else if(expr.
id() == ID_function_application)
2579 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2584 if(!no_change_sort_and_join)
2590 # ifdef DEBUG_ON_DEMAND
2595 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2596 <<
" ---> " <<
format(
r.expr) <<
'\n';
2608 std::pair<simplify_expr_cachet::containert::iterator, bool>
2609 cache_result=simplify_expr_cache.container().
2610 insert(std::pair<exprt, exprt>(expr,
exprt()));
2612 if(!cache_result.second)
2614 const exprt &new_expr=cache_result.first->second;
2630 if(simplify_node_result.has_changed())
2633 tmp = simplify_node_result.expr;
2636 #ifdef USE_LOCAL_REPLACE_MAP
2638 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2639 if(it!=local_replace_map.end())
2645 if(!local_replace_map.empty() &&
2664 cache_result.first->second = tmp;
2667 return std::move(tmp);
2674 #ifdef DEBUG_ON_DEMAND
2676 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2679 #ifdef DEBUG_ON_DEMAND
2681 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2683 if(result.has_changed())