45 struct simplify_expr_cachet
49 typedef std::unordered_map<
52 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
55 containert container_normal;
57 containert &container()
59 return container_normal;
63 simplify_expr_cachet simplify_expr_cache;
72 if(type.
id()==ID_floatbv)
78 else if(type.
id()==ID_signedbv ||
79 type.
id()==ID_unsignedbv)
81 auto value = numeric_cast<mp_integer>(
to_unary_expr(expr).op());
106 if(type.
id()==ID_floatbv)
111 else if(type.
id()==ID_signedbv ||
112 type.
id()==ID_unsignedbv)
114 const auto value = numeric_cast<mp_integer>(expr.
op());
115 if(value.has_value())
134 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
138 std::size_t result = 0;
140 for(std::size_t i = 0; i < width; i++)
157 if(!const_bits_opt.has_value())
161 std::size_t n_leading_zeros = const_bits_opt->rfind(
'1');
162 if(n_leading_zeros == std::string::npos)
167 n_leading_zeros = const_bits_opt->size();
170 n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
217 const auto first_value_opt =
227 const auto second_value_opt =
230 if(!second_value_opt)
238 const bool includes =
264 const auto numeric_length =
301 const bool first_shorter = s1_size < s2_size;
306 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
308 if(it_pair.first == ops1.end())
317 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
329 const bool search_from_end)
331 std::size_t starting_index = 0;
336 auto &starting_index_expr = expr.
arguments().at(2);
338 if(starting_index_expr.id() != ID_constant)
349 starting_index = numeric_cast_v<std::size_t>(idx);
364 const auto search_string_size = s1_data.
operands().size();
365 if(starting_index >= search_string_size)
370 unsigned long starting_offset =
371 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
394 ? starting_index > 0 ? starting_index : search_string_size
400 auto end = std::prev(s1_data.
operands().end(), starting_offset);
401 auto it = std::find_end(
408 std::distance(s1_data.
operands().begin(), it), expr.
type());
412 auto it = std::search(
413 std::next(s1_data.
operands().begin(), starting_index),
420 std::distance(s1_data.
operands().begin(), it), expr.
type());
423 else if(expr.
arguments().at(1).id() == ID_constant)
428 const auto c1_val = numeric_cast_v<mp_integer>(c1);
430 auto pred = [&](
const exprt &c2) {
433 return c1_val == c2_val;
438 auto it = std::find_if(
439 std::next(s1_data.
operands().rbegin(), starting_offset),
444 std::distance(s1_data.
operands().begin(), it.base() - 1),
449 auto it = std::find_if(
450 std::next(s1_data.
operands().begin(), starting_index),
455 std::distance(s1_data.
operands().begin(), it), expr.
type());
475 if(expr.
arguments().at(1).id() != ID_constant)
493 const auto i_opt = numeric_cast<std::size_t>(index);
495 if(!i_opt || *i_opt >= char_seq.
operands().size())
502 if(c.type() != expr.
type())
513 auto &operands = string_data.
operands();
514 for(
auto &operand : operands)
517 auto character = numeric_cast_v<unsigned int>(constant_value);
523 if(isalpha(character))
525 if(isupper(character))
527 from_integer(tolower(character), constant_value.type());
549 const auto first_value_opt =
559 const auto second_value_opt =
562 if(!second_value_opt)
575 bool is_equal = first_value == second_value;
594 const auto first_value_opt =
604 const auto second_value_opt =
607 if(!second_value_opt)
618 if(offset.id() != ID_constant)
626 offset_int + second_value.
operands().size();
629 exprt::operandst::const_iterator second_it =
631 for(
const auto &first_op : first_value.
operands())
635 else if(second_it == second_value.
operands().end())
637 else if(first_op != *second_it)
666 if(func_id == ID_cprover_string_startswith_func)
670 else if(func_id == ID_cprover_string_endswith_func)
674 else if(func_id == ID_cprover_string_is_empty_func)
678 else if(func_id == ID_cprover_string_compare_to_func)
682 else if(func_id == ID_cprover_string_index_of_func)
686 else if(func_id == ID_cprover_string_char_at_func)
690 else if(func_id == ID_cprover_string_contains_func)
694 else if(func_id == ID_cprover_string_last_index_of_func)
698 else if(func_id == ID_cprover_string_equals_ignore_case_func)
713 if(expr.
op().
id() == ID_infinity)
718 return std::move(tmp);
725 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
735 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
736 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
740 auto new_expr = expr;
752 if(expr_type.
id()==ID_bool)
757 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
765 op_type.
id() == ID_bool &&
766 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
767 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
785 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
786 if(typecast.op().type()==expr_type)
788 return typecast.op();
794 if(expr_type.
id()==ID_c_bool &&
795 op_type.
id()!=ID_bool)
799 auto new_expr = expr;
813 return std::move(tmp);
819 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
820 op_type.
id() == ID_pointer)
822 auto new_expr = expr;
830 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
831 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
832 op_type.
id() == ID_pointer)
837 auto outer_cast = expr;
846 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
847 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
852 if(((op_plus_expr.op0().id() == ID_typecast &&
854 (op_plus_expr.op0().is_constant() &&
859 if(sub_size.has_value())
861 auto new_expr = expr;
864 if(*sub_size == 0 || *sub_size == 1)
887 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
888 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
898 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
899 op_id==ID_unary_minus ||
900 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
919 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
929 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
930 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
934 if(step.has_value() && *step != 0)
937 auto new_expr = expr;
939 new_expr.
op().
type() = size_t_type;
941 for(
auto &op : new_expr.op().operands())
943 if(op.type().id()==ID_pointer)
961 if(expr.
op().
id()==ID_if &&
968 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
970 return std::move(new_expr);
975 const exprt &operand = expr.
op();
984 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
986 if(op_type_id==ID_integer ||
987 op_type_id==ID_natural)
993 if(expr_type_id==ID_bool)
998 if(expr_type_id==ID_unsignedbv ||
999 expr_type_id==ID_signedbv ||
1000 expr_type_id==ID_c_enum ||
1001 expr_type_id==ID_c_bit_field ||
1002 expr_type_id==ID_integer)
1006 else if(expr_type_id == ID_c_enum_tag)
1009 if(!c_enum_type.is_incomplete())
1012 tmp.
type() = expr_type;
1013 return std::move(tmp);
1017 else if(op_type_id==ID_rational)
1020 else if(op_type_id==ID_real)
1023 else if(op_type_id==ID_bool)
1025 if(expr_type_id==ID_unsignedbv ||
1026 expr_type_id==ID_signedbv ||
1027 expr_type_id==ID_integer ||
1028 expr_type_id==ID_natural ||
1029 expr_type_id==ID_rational ||
1030 expr_type_id==ID_c_bool ||
1031 expr_type_id==ID_c_enum ||
1032 expr_type_id==ID_c_bit_field)
1043 else if(expr_type_id==ID_c_enum_tag)
1046 if(!c_enum_type.is_incomplete())
1048 unsigned int_value = operand.
is_true() ? 1u : 0u;
1050 tmp.
type()=expr_type;
1051 return std::move(tmp);
1054 else if(expr_type_id==ID_pointer &&
1061 else if(op_type_id==ID_unsignedbv ||
1062 op_type_id==ID_signedbv ||
1063 op_type_id==ID_c_bit_field ||
1064 op_type_id==ID_c_bool)
1071 if(expr_type_id==ID_bool)
1076 if(expr_type_id==ID_c_bool)
1081 if(expr_type_id==ID_integer)
1086 if(expr_type_id==ID_natural)
1094 if(expr_type_id==ID_unsignedbv ||
1095 expr_type_id==ID_signedbv ||
1096 expr_type_id==ID_bv ||
1097 expr_type_id==ID_c_bit_field)
1102 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1104 return std::move(result);
1107 if(expr_type_id==ID_c_enum_tag)
1110 if(!c_enum_type.is_incomplete())
1113 tmp.
type()=expr_type;
1114 return std::move(tmp);
1118 if(expr_type_id==ID_c_enum)
1123 if(expr_type_id==ID_fixedbv)
1135 if(expr_type_id==ID_floatbv)
1147 if(expr_type_id==ID_rational)
1153 else if(op_type_id==ID_fixedbv)
1155 if(expr_type_id==ID_unsignedbv ||
1156 expr_type_id==ID_signedbv)
1162 else if(expr_type_id==ID_fixedbv)
1169 else if(expr_type_id == ID_bv)
1175 else if(op_type_id==ID_floatbv)
1179 if(expr_type_id==ID_unsignedbv ||
1180 expr_type_id==ID_signedbv)
1185 else if(expr_type_id==ID_floatbv)
1191 else if(expr_type_id==ID_fixedbv)
1201 else if(expr_type_id == ID_bv)
1206 else if(op_type_id==ID_bv)
1209 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1210 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1211 expr_type_id == ID_c_bit_field)
1215 if(expr_type_id != ID_c_enum_tag)
1221 result.type() = tag_type;
1222 return std::move(result);
1225 else if(expr_type_id == ID_floatbv)
1230 ieee_float.unpack(int_value);
1231 return ieee_float.to_expr();
1233 else if(expr_type_id == ID_fixedbv)
1238 fixedbv.set_value(int_value);
1239 return fixedbv.to_expr();
1242 else if(op_type_id==ID_c_enum_tag)
1249 auto new_expr = expr;
1254 else if(op_type_id==ID_c_enum)
1260 auto new_expr = expr;
1266 else if(operand.
id()==ID_typecast)
1271 op_type_id == expr_type_id &&
1272 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1276 auto new_expr = expr;
1282 else if(operand.
id()==ID_address_of)
1288 o.
type().
id() == ID_array &&
1306 if(pointer.
type().
id()!=ID_pointer)
1309 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1313 auto tmp_op1 = expr;
1317 auto tmp_op2 = expr;
1321 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1326 if(pointer.
id()==ID_address_of)
1334 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1342 if(address_of.
object().
id()==ID_index)
1367 bool no_change =
true;
1373 auto with_expr = expr;
1375 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1379 if(old_type_followed.
id() == ID_struct)
1381 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1383 while(with_expr.operands().size() > 1)
1386 with_expr.where().get(ID_component_name);
1388 if(!
to_struct_type(old_type_followed).has_component(component_name))
1391 std::size_t number =
1394 if(number >= with_expr.old().operands().size())
1397 with_expr.old().operands()[number].swap(with_expr.new_value());
1399 with_expr.operands().erase(++with_expr.operands().begin());
1400 with_expr.operands().erase(++with_expr.operands().begin());
1407 with_expr.old().type().id() == ID_array ||
1408 with_expr.old().type().id() == ID_vector)
1411 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1412 with_expr.old().id() == ID_vector)
1414 while(with_expr.operands().size() > 1)
1416 const auto i = numeric_cast<mp_integer>(with_expr.where());
1421 if(*i < 0 || *i >= with_expr.old().operands().size())
1424 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1425 with_expr.new_value());
1427 with_expr.operands().erase(++with_expr.operands().begin());
1428 with_expr.operands().erase(++with_expr.operands().begin());
1435 if(with_expr.operands().size() == 1)
1436 return with_expr.old();
1441 return std::move(with_expr);
1452 exprt *value_ptr=&updated_value;
1454 for(
const auto &e : designator)
1458 if(e.id()==ID_index_designator &&
1459 value_ptr->
id()==ID_array)
1466 if(*i < 0 || *i >= value_ptr->
operands().size())
1469 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1471 else if(e.id()==ID_member_designator &&
1472 value_ptr->
id()==ID_struct)
1475 e.get(ID_component_name);
1481 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1490 return updated_value;
1495 if(expr.
id()==ID_plus)
1497 if(expr.
type().
id()==ID_pointer)
1501 if(op.type().id() == ID_pointer)
1505 else if(expr.
id()==ID_typecast)
1508 const typet &op_type = typecast_expr.op().type();
1510 if(op_type.
id()==ID_pointer)
1515 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1522 const exprt &casted_expr = typecast_expr.op();
1523 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1527 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1531 if(cand.
id() == ID_typecast)
1535 if(typecast_op.id() == ID_address_of)
1540 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1551 else if(expr.
id()==ID_address_of)
1555 if(
object.
id() == ID_index)
1561 else if(
object.
id() == ID_member)
1576 if(expr.
op().
id()==ID_if)
1587 if(el_size.has_value() && *el_size < 0)
1592 if(expr.
op().
id()==expr.
id())
1606 ((expr.
id() == ID_byte_extract_big_endian &&
1607 expr.
op().
id() == ID_byte_update_big_endian) ||
1608 (expr.
id() == ID_byte_extract_little_endian &&
1609 expr.
op().
id() == ID_byte_update_little_endian)) &&
1614 if(expr.
type() == op_byte_update.value().type())
1616 return op_byte_update.value();
1619 el_size.has_value() &&
1623 tmp.
op() = op_byte_update.value();
1631 auto offset = numeric_cast<mp_integer>(expr.
offset());
1632 if(!offset.has_value() || *offset < 0)
1645 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1653 if(!el_size.has_value() || *el_size == 0)
1656 if(expr.
op().
id()==ID_array_of &&
1664 if(!const_bits_opt.has_value())
1667 std::string const_bits=const_bits_opt.value();
1669 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1672 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1673 const_bits+=const_bits;
1675 std::string el_bits = std::string(
1677 numeric_cast_v<std::size_t>(*offset * 8),
1678 numeric_cast_v<std::size_t>(*el_size));
1681 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1684 return std::move(*tmp);
1689 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1704 const bool struct_has_flexible_array_member =
has_subtype(
1706 [&](
const typet &type) {
1707 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1710 const struct_typet &st = to_struct_type(ns.follow(type));
1711 const auto &comps = st.components();
1712 if(comps.empty() || comps.back().type().id() != ID_array)
1716 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1717 return !size.has_value() || *size <= 1;
1721 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1722 !struct_has_flexible_array_member)
1724 std::string bits_cut = std::string(
1726 numeric_cast_v<std::size_t>(*offset * 8),
1727 numeric_cast_v<std::size_t>(*el_size));
1730 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1733 return std::move(*tmp);
1739 if(!subexpr.has_value() || subexpr.value() == expr)
1751 expr.
id() == expr.
op().
id() &&
1757 return std::move(tmp);
1760 const exprt &root = expr.
op();
1768 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1769 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1772 expr.
id()==ID_byte_update_little_endian ?
1773 ID_byte_extract_little_endian :
1774 ID_byte_extract_big_endian,
1775 value, offset, expr.
type());
1781 const auto offset_int = numeric_cast<mp_integer>(offset);
1783 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1784 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1785 *offset_int + *val_size <= *root_size)
1788 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1790 if(root_bits.has_value())
1792 const auto val_bits =
1793 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1795 if(val_bits.has_value())
1798 numeric_cast_v<std::size_t>(*offset_int * 8),
1799 numeric_cast_v<std::size_t>(*val_size),
1805 expr.
id() == ID_byte_update_little_endian,
1809 return std::move(*tmp);
1822 if(expr.
id()!=ID_byte_update_little_endian)
1825 if(value.
id()==ID_with)
1829 if(with.
old().
id()==ID_byte_extract_little_endian)
1836 if(!(root==extract.
op()))
1838 if(!(offset==extract.
offset()))
1842 if(tp.
id()==ID_struct)
1849 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1864 tmp.set_value(std::move(new_value));
1869 else if(tp.
id()==ID_array)
1875 exprt index_offset =
1889 tmp.set_value(std::move(new_value));
1897 if(!offset_int.has_value() || *offset_int < 0)
1903 if(!val_size.has_value() || *val_size == 0)
1908 if(op_type.
id()==ID_struct)
1927 if(!m_offset.has_value())
1934 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1940 mp_integer m_size_bytes = (*m_size_bits) / 8;
1943 if(*m_offset + m_size_bytes <= *offset_int)
1947 update_size.has_value() && *update_size > 0 &&
1948 *m_offset >= *offset_int + *update_size)
1956 exprt member_name(ID_member_name);
1957 member_name.
set(ID_component_name,
component.get_name());
1962 *m_offset < *offset_int ||
1963 (*m_offset == *offset_int && update_size.has_value() &&
1964 *update_size > 0 && m_size_bytes > *update_size))
1967 ID_byte_update_little_endian,
1975 update_size.has_value() && *update_size > 0 &&
1976 *m_offset + m_size_bytes > *offset_int + *update_size)
1985 ID_byte_extract_little_endian,
2000 if(root.
id()==ID_array)
2004 if(!el_size.has_value() || *el_size == 0 ||
2005 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2015 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2018 if(*offset_int * 8 < m_offset_bits + *el_size)
2020 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2021 bytes_req-=val_offset;
2022 if(val_offset + bytes_req > (*val_size) / 8)
2023 bytes_req = (*val_size) / 8 - val_offset;
2036 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2041 val_offset+=bytes_req;
2044 m_offset_bits += *el_size;
2047 return std::move(result);
2056 if(expr.
id() == ID_complex_real)
2060 if(complex_real_expr.op().id() == ID_complex)
2063 else if(expr.
id() == ID_complex_imag)
2067 if(complex_imag_expr.op().id() == ID_complex)
2080 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2092 op_type_id == ID_integer || op_type_id == ID_rational ||
2093 op_type_id == ID_real)
2098 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2102 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2108 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2109 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2110 if(!op0_value.has_value() || !op1_value.has_value())
2114 if(expr.
id() == ID_overflow_plus)
2115 no_overflow_result = *op0_value + *op1_value;
2116 else if(expr.
id() == ID_overflow_minus)
2117 no_overflow_result = *op0_value - *op1_value;
2118 else if(expr.
id() == ID_overflow_mult)
2119 no_overflow_result = *op0_value * *op1_value;
2120 else if(expr.
id() == ID_overflow_shl)
2121 no_overflow_result = *op0_value << *op1_value;
2128 no_overflow_result < bv_type.smallest() ||
2129 no_overflow_result > bv_type.largest())
2147 op_type_id == ID_integer || op_type_id == ID_rational ||
2148 op_type_id == ID_real)
2153 if(op_type_id == ID_natural)
2157 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2163 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2164 if(!op_value.has_value())
2168 if(expr.
id() == ID_overflow_unary_minus)
2169 no_overflow_result = -*op_value;
2176 no_overflow_result < bv_type.smallest() ||
2177 no_overflow_result > bv_type.largest())
2191 if(expr.
id()==ID_address_of)
2195 else if(expr.
id()==ID_if)
2204 if(r_it.has_changed())
2232 if(expr.
id()==ID_typecast)
2236 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2237 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2238 expr.
id()==ID_ge || expr.
id()==ID_le)
2242 else if(expr.
id()==ID_if)
2246 else if(expr.
id()==ID_lambda)
2250 else if(expr.
id()==ID_with)
2254 else if(expr.
id()==ID_update)
2258 else if(expr.
id()==ID_index)
2262 else if(expr.
id()==ID_member)
2266 else if(expr.
id()==ID_byte_update_little_endian ||
2267 expr.
id()==ID_byte_update_big_endian)
2271 else if(expr.
id()==ID_byte_extract_little_endian ||
2272 expr.
id()==ID_byte_extract_big_endian)
2276 else if(expr.
id()==ID_pointer_object)
2280 else if(expr.
id() == ID_is_dynamic_object)
2284 else if(expr.
id() == ID_is_invalid_pointer)
2288 else if(expr.
id()==ID_object_size)
2292 else if(expr.
id()==ID_good_pointer)
2296 else if(expr.
id()==ID_div)
2300 else if(expr.
id()==ID_mod)
2304 else if(expr.
id()==ID_bitnot)
2308 else if(expr.
id()==ID_bitand ||
2309 expr.
id()==ID_bitor ||
2310 expr.
id()==ID_bitxor)
2314 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2318 else if(expr.
id()==ID_power)
2322 else if(expr.
id()==ID_plus)
2326 else if(expr.
id()==ID_minus)
2330 else if(expr.
id()==ID_mult)
2334 else if(expr.
id()==ID_floatbv_plus ||
2335 expr.
id()==ID_floatbv_minus ||
2336 expr.
id()==ID_floatbv_mult ||
2337 expr.
id()==ID_floatbv_div)
2341 else if(expr.
id()==ID_floatbv_typecast)
2345 else if(expr.
id()==ID_unary_minus)
2349 else if(expr.
id()==ID_unary_plus)
2353 else if(expr.
id()==ID_not)
2357 else if(expr.
id()==ID_implies ||
2358 expr.
id()==ID_or || expr.
id()==ID_xor ||
2363 else if(expr.
id()==ID_dereference)
2367 else if(expr.
id()==ID_address_of)
2371 else if(expr.
id()==ID_pointer_offset)
2375 else if(expr.
id()==ID_extractbit)
2379 else if(expr.
id()==ID_concatenation)
2383 else if(expr.
id()==ID_extractbits)
2387 else if(expr.
id()==ID_ieee_float_equal ||
2388 expr.
id()==ID_ieee_float_notequal)
2392 else if(expr.
id() == ID_bswap)
2396 else if(expr.
id()==ID_isinf)
2400 else if(expr.
id()==ID_isnan)
2404 else if(expr.
id()==ID_isnormal)
2408 else if(expr.
id()==ID_abs)
2412 else if(expr.
id()==ID_sign)
2416 else if(expr.
id() == ID_popcount)
2420 else if(expr.
id() == ID_count_leading_zeros)
2424 else if(expr.
id() == ID_function_application)
2428 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2433 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2434 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2438 else if(expr.
id() == ID_overflow_unary_minus)
2443 if(!no_change_join_operands)
2449 # ifdef DEBUG_ON_DEMAND
2454 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2455 <<
" ---> " <<
format(
r.expr) <<
'\n';
2467 std::pair<simplify_expr_cachet::containert::iterator, bool>
2468 cache_result=simplify_expr_cache.container().
2469 insert(std::pair<exprt, exprt>(expr,
exprt()));
2471 if(!cache_result.second)
2473 const exprt &new_expr=cache_result.first->second;
2489 if(simplify_node_result.has_changed())
2492 tmp = simplify_node_result.expr;
2495 #ifdef USE_LOCAL_REPLACE_MAP
2497 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2498 if(it!=local_replace_map.end())
2504 if(!local_replace_map.empty() &&
2523 cache_result.first->second = tmp;
2526 return std::move(tmp);
2533 #ifdef DEBUG_ON_DEMAND
2535 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2538 #ifdef DEBUG_ON_DEMAND
2540 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2542 if(result.has_changed())