44 struct simplify_expr_cachet
48 typedef std::unordered_map<
51 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
54 containert container_normal;
56 containert &container()
58 return container_normal;
62 simplify_expr_cachet simplify_expr_cache;
71 if(type.
id()==ID_floatbv)
77 else if(type.
id()==ID_signedbv ||
78 type.
id()==ID_unsignedbv)
80 auto value = numeric_cast<mp_integer>(
to_unary_expr(expr).op());
105 if(type.
id()==ID_floatbv)
110 else if(type.
id()==ID_signedbv ||
111 type.
id()==ID_unsignedbv)
113 const auto value = numeric_cast<mp_integer>(expr.
op());
114 if(value.has_value())
133 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
137 std::size_t result = 0;
139 for(std::size_t i = 0; i < width; i++)
158 if(!const_bits_opt.has_value())
162 std::size_t n_leading_zeros = const_bits_opt->rfind(
'1');
163 if(n_leading_zeros == std::string::npos)
168 n_leading_zeros = const_bits_opt->size();
171 n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
184 if(!const_bits_opt.has_value())
188 std::size_t n_trailing_zeros = const_bits_opt->find(
'1');
189 if(n_trailing_zeros == std::string::npos)
194 n_trailing_zeros = const_bits_opt->size();
242 const auto first_value_opt =
252 const auto second_value_opt =
255 if(!second_value_opt)
263 const bool includes =
289 const auto numeric_length =
326 const bool first_shorter = s1_size < s2_size;
331 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
333 if(it_pair.first == ops1.end())
342 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
354 const bool search_from_end)
356 std::size_t starting_index = 0;
361 auto &starting_index_expr = expr.
arguments().at(2);
363 if(starting_index_expr.id() != ID_constant)
374 starting_index = numeric_cast_v<std::size_t>(idx);
389 const auto search_string_size = s1_data.
operands().size();
390 if(starting_index >= search_string_size)
395 unsigned long starting_offset =
396 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
419 ? starting_index > 0 ? starting_index : search_string_size
425 auto end = std::prev(s1_data.
operands().end(), starting_offset);
426 auto it = std::find_end(
433 std::distance(s1_data.
operands().begin(), it), expr.
type());
437 auto it = std::search(
438 std::next(s1_data.
operands().begin(), starting_index),
445 std::distance(s1_data.
operands().begin(), it), expr.
type());
448 else if(expr.
arguments().at(1).id() == ID_constant)
453 const auto c1_val = numeric_cast_v<mp_integer>(c1);
455 auto pred = [&](
const exprt &c2) {
458 return c1_val == c2_val;
463 auto it = std::find_if(
464 std::next(s1_data.
operands().rbegin(), starting_offset),
469 std::distance(s1_data.
operands().begin(), it.base() - 1),
474 auto it = std::find_if(
475 std::next(s1_data.
operands().begin(), starting_index),
480 std::distance(s1_data.
operands().begin(), it), expr.
type());
500 if(expr.
arguments().at(1).id() != ID_constant)
518 const auto i_opt = numeric_cast<std::size_t>(index);
520 if(!i_opt || *i_opt >= char_seq.
operands().size())
527 if(c.type() != expr.
type())
538 auto &operands = string_data.
operands();
539 for(
auto &operand : operands)
542 auto character = numeric_cast_v<unsigned int>(constant_value);
548 if(isalpha(character))
550 if(isupper(character))
552 from_integer(tolower(character), constant_value.type());
574 const auto first_value_opt =
584 const auto second_value_opt =
587 if(!second_value_opt)
600 bool is_equal = first_value == second_value;
619 const auto first_value_opt =
629 const auto second_value_opt =
632 if(!second_value_opt)
643 if(offset.id() != ID_constant)
651 offset_int + second_value.
operands().size();
654 exprt::operandst::const_iterator second_it =
656 for(
const auto &first_op : first_value.
operands())
660 else if(second_it == second_value.
operands().end())
662 else if(first_op != *second_it)
691 if(func_id == ID_cprover_string_startswith_func)
695 else if(func_id == ID_cprover_string_endswith_func)
699 else if(func_id == ID_cprover_string_is_empty_func)
703 else if(func_id == ID_cprover_string_compare_to_func)
707 else if(func_id == ID_cprover_string_index_of_func)
711 else if(func_id == ID_cprover_string_char_at_func)
715 else if(func_id == ID_cprover_string_contains_func)
719 else if(func_id == ID_cprover_string_last_index_of_func)
723 else if(func_id == ID_cprover_string_equals_ignore_case_func)
738 if(expr.
op().
id() == ID_infinity)
743 return std::move(tmp);
750 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
760 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
761 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
765 auto new_expr = expr;
777 if(expr_type.
id()==ID_bool)
782 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
790 op_type.
id() == ID_bool &&
791 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
792 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
811 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
812 if(typecast.op().type()==expr_type)
814 return typecast.op();
820 if(expr_type.
id()==ID_c_bool &&
821 op_type.
id()!=ID_bool)
825 auto new_expr = expr;
839 return std::move(tmp);
845 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
846 op_type.
id() == ID_pointer)
848 auto new_expr = expr;
856 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
857 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
858 op_type.
id() == ID_pointer)
863 auto outer_cast = expr;
872 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
873 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
878 if(((op_plus_expr.op0().id() == ID_typecast &&
880 (op_plus_expr.op0().is_constant() &&
885 if(sub_size.has_value())
887 auto new_expr = expr;
892 if(*sub_size == 0 || *sub_size == 1)
893 new_expr.op() = offset_expr;
914 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
915 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
925 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
926 op_id==ID_unary_minus ||
927 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
946 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
956 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
957 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
961 if(step.has_value() && *step != 0)
964 auto new_expr = expr;
966 new_expr.
op().
type() = size_t_type;
968 for(
auto &op : new_expr.op().operands())
971 if(op.type().id() != ID_pointer && *step > 1)
976 op = std::move(new_op);
987 if(expr.
op().
id()==ID_if &&
994 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
996 return std::move(new_expr);
1001 const exprt &operand = expr.
op();
1009 typet c_sizeof_type=
1010 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
1012 if(op_type_id==ID_integer ||
1013 op_type_id==ID_natural)
1019 if(expr_type_id==ID_bool)
1024 if(expr_type_id==ID_unsignedbv ||
1025 expr_type_id==ID_signedbv ||
1026 expr_type_id==ID_c_enum ||
1027 expr_type_id==ID_c_bit_field ||
1028 expr_type_id==ID_integer)
1032 else if(expr_type_id == ID_c_enum_tag)
1035 if(!c_enum_type.is_incomplete())
1038 tmp.
type() = expr_type;
1039 return std::move(tmp);
1043 else if(op_type_id==ID_rational)
1046 else if(op_type_id==ID_real)
1049 else if(op_type_id==ID_bool)
1051 if(expr_type_id==ID_unsignedbv ||
1052 expr_type_id==ID_signedbv ||
1053 expr_type_id==ID_integer ||
1054 expr_type_id==ID_natural ||
1055 expr_type_id==ID_rational ||
1056 expr_type_id==ID_c_bool ||
1057 expr_type_id==ID_c_enum ||
1058 expr_type_id==ID_c_bit_field)
1069 else if(expr_type_id==ID_c_enum_tag)
1072 if(!c_enum_type.is_incomplete())
1074 unsigned int_value = operand.
is_true() ? 1u : 0u;
1076 tmp.
type()=expr_type;
1077 return std::move(tmp);
1080 else if(expr_type_id==ID_pointer &&
1087 else if(op_type_id==ID_unsignedbv ||
1088 op_type_id==ID_signedbv ||
1089 op_type_id==ID_c_bit_field ||
1090 op_type_id==ID_c_bool)
1097 if(expr_type_id==ID_bool)
1102 if(expr_type_id==ID_c_bool)
1107 if(expr_type_id==ID_integer)
1112 if(expr_type_id==ID_natural)
1120 if(expr_type_id==ID_unsignedbv ||
1121 expr_type_id==ID_signedbv ||
1122 expr_type_id==ID_bv ||
1123 expr_type_id==ID_c_bit_field)
1128 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1130 return std::move(result);
1133 if(expr_type_id==ID_c_enum_tag)
1136 if(!c_enum_type.is_incomplete())
1139 tmp.
type()=expr_type;
1140 return std::move(tmp);
1144 if(expr_type_id==ID_c_enum)
1149 if(expr_type_id==ID_fixedbv)
1161 if(expr_type_id==ID_floatbv)
1173 if(expr_type_id==ID_rational)
1179 else if(op_type_id==ID_fixedbv)
1181 if(expr_type_id==ID_unsignedbv ||
1182 expr_type_id==ID_signedbv)
1188 else if(expr_type_id==ID_fixedbv)
1195 else if(expr_type_id == ID_bv)
1201 else if(op_type_id==ID_floatbv)
1205 if(expr_type_id==ID_unsignedbv ||
1206 expr_type_id==ID_signedbv)
1211 else if(expr_type_id==ID_floatbv)
1217 else if(expr_type_id==ID_fixedbv)
1227 else if(expr_type_id == ID_bv)
1232 else if(op_type_id==ID_bv)
1235 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1236 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1237 expr_type_id == ID_c_bit_field)
1241 if(expr_type_id != ID_c_enum_tag)
1247 result.type() = tag_type;
1248 return std::move(result);
1251 else if(expr_type_id == ID_floatbv)
1256 ieee_float.unpack(int_value);
1257 return ieee_float.to_expr();
1259 else if(expr_type_id == ID_fixedbv)
1264 fixedbv.set_value(int_value);
1265 return fixedbv.to_expr();
1268 else if(op_type_id==ID_c_enum_tag)
1275 auto new_expr = expr;
1280 else if(op_type_id==ID_c_enum)
1286 auto new_expr = expr;
1292 else if(operand.
id()==ID_typecast)
1297 op_type_id == expr_type_id &&
1298 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1302 auto new_expr = expr;
1308 else if(operand.
id()==ID_address_of)
1314 o.
type().
id() == ID_array &&
1332 if(pointer.
type().
id()!=ID_pointer)
1335 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1339 auto tmp_op1 = expr;
1343 auto tmp_op2 = expr;
1347 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1352 if(pointer.
id()==ID_address_of)
1360 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1368 if(address_of.
object().
id()==ID_index)
1393 bool no_change =
true;
1399 auto with_expr = expr;
1401 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1405 if(old_type_followed.
id() == ID_struct)
1407 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1409 while(with_expr.operands().size() > 1)
1412 with_expr.where().get(ID_component_name);
1414 if(!
to_struct_type(old_type_followed).has_component(component_name))
1417 std::size_t number =
1420 if(number >= with_expr.old().operands().size())
1423 with_expr.old().operands()[number].swap(with_expr.new_value());
1425 with_expr.operands().erase(++with_expr.operands().begin());
1426 with_expr.operands().erase(++with_expr.operands().begin());
1433 with_expr.old().type().id() == ID_array ||
1434 with_expr.old().type().id() == ID_vector)
1437 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1438 with_expr.old().id() == ID_vector)
1440 while(with_expr.operands().size() > 1)
1442 const auto i = numeric_cast<mp_integer>(with_expr.where());
1447 if(*i < 0 || *i >= with_expr.old().operands().size())
1450 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1451 with_expr.new_value());
1453 with_expr.operands().erase(++with_expr.operands().begin());
1454 with_expr.operands().erase(++with_expr.operands().begin());
1461 if(with_expr.operands().size() == 1)
1462 return with_expr.old();
1467 return std::move(with_expr);
1478 exprt *value_ptr=&updated_value;
1480 for(
const auto &e : designator)
1484 if(e.id()==ID_index_designator &&
1485 value_ptr->
id()==ID_array)
1492 if(*i < 0 || *i >= value_ptr->
operands().size())
1495 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1497 else if(e.id()==ID_member_designator &&
1498 value_ptr->
id()==ID_struct)
1501 e.get(ID_component_name);
1507 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1516 return updated_value;
1521 if(expr.
id()==ID_plus)
1523 if(expr.
type().
id()==ID_pointer)
1527 if(op.type().id() == ID_pointer)
1531 else if(expr.
id()==ID_typecast)
1534 const typet &op_type = typecast_expr.op().type();
1536 if(op_type.
id()==ID_pointer)
1541 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1548 const exprt &casted_expr = typecast_expr.op();
1549 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1553 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1557 if(cand.
id() == ID_typecast)
1561 if(typecast_op.id() == ID_address_of)
1566 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1577 else if(expr.
id()==ID_address_of)
1581 if(
object.
id() == ID_index)
1587 else if(
object.
id() == ID_member)
1602 if(expr.
op().
id()==ID_if)
1613 if(el_size.has_value() && *el_size < 0)
1618 if(expr.
op().
id()==expr.
id())
1632 ((expr.
id() == ID_byte_extract_big_endian &&
1633 expr.
op().
id() == ID_byte_update_big_endian) ||
1634 (expr.
id() == ID_byte_extract_little_endian &&
1635 expr.
op().
id() == ID_byte_update_little_endian)) &&
1640 if(expr.
type() == op_byte_update.value().type())
1642 return op_byte_update.value();
1645 el_size.has_value() &&
1649 tmp.
op() = op_byte_update.value();
1657 auto offset = numeric_cast<mp_integer>(expr.
offset());
1658 if(!offset.has_value() || *offset < 0)
1664 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1667 (expr.
id() == ID_byte_extract_big_endian &&
1677 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1685 if(!el_size.has_value() || *el_size == 0)
1688 if(expr.
op().
id()==ID_array_of &&
1697 if(!const_bits_opt.has_value())
1700 std::string const_bits=const_bits_opt.value();
1702 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1705 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1706 const_bits+=const_bits;
1708 std::string el_bits = std::string(
1710 numeric_cast_v<std::size_t>(*offset * 8),
1711 numeric_cast_v<std::size_t>(*el_size));
1714 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1717 return std::move(*tmp);
1722 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1737 const bool struct_has_flexible_array_member =
has_subtype(
1739 [&](
const typet &type) {
1740 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1743 const struct_typet &st = to_struct_type(ns.follow(type));
1744 const auto &comps = st.components();
1745 if(comps.empty() || comps.back().type().id() != ID_array)
1749 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1750 return !size.has_value() || *size <= 1;
1754 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1755 !struct_has_flexible_array_member)
1757 std::string bits_cut = std::string(
1759 numeric_cast_v<std::size_t>(*offset * 8),
1760 numeric_cast_v<std::size_t>(*el_size));
1763 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1766 return std::move(*tmp);
1772 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1774 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1782 for(
const auto &comp : components)
1788 !component_bits.has_value() || *component_bits == 0 ||
1789 *component_bits % 8 != 0)
1795 auto member_offset_opt =
1798 if(!member_offset_opt.has_value())
1807 member_offset_opt.value(), expr.
offset().
type())});
1810 tmp.
type() = comp.type();
1811 tmp.offset() = new_offset;
1819 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1823 if(widest_member_opt.has_value())
1826 be.
type() = widest_member_opt->first.type();
1827 return union_exprt{widest_member_opt->first.get_name(),
1837 if(!subexpr.has_value() || subexpr.value() == expr)
1849 expr.
id() == expr.
op().
id() &&
1855 return std::move(tmp);
1858 const exprt &root = expr.
op();
1866 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1867 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1870 expr.
id()==ID_byte_update_little_endian ?
1871 ID_byte_extract_little_endian :
1872 ID_byte_extract_big_endian,
1873 value, offset, expr.
type());
1879 const auto offset_int = numeric_cast<mp_integer>(offset);
1881 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1882 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1883 *offset_int + *val_size <= *root_size)
1886 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1888 if(root_bits.has_value())
1890 const auto val_bits =
1891 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1893 if(val_bits.has_value())
1896 numeric_cast_v<std::size_t>(*offset_int * 8),
1897 numeric_cast_v<std::size_t>(*val_size),
1903 expr.
id() == ID_byte_update_little_endian,
1907 return std::move(*tmp);
1920 if(expr.
id()!=ID_byte_update_little_endian)
1923 if(value.
id()==ID_with)
1927 if(with.
old().
id()==ID_byte_extract_little_endian)
1934 if(!(root==extract.
op()))
1936 if(!(offset==extract.
offset()))
1940 if(tp.
id()==ID_struct)
1947 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1962 tmp.set_value(std::move(new_value));
1967 else if(tp.
id()==ID_array)
1973 exprt index_offset =
1987 tmp.set_value(std::move(new_value));
1995 if(!offset_int.has_value() || *offset_int < 0)
2001 if(!val_size.has_value() || *val_size == 0)
2006 if(op_type.
id()==ID_struct)
2025 if(!m_offset.has_value())
2032 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
2038 mp_integer m_size_bytes = (*m_size_bits) / 8;
2041 if(*m_offset + m_size_bytes <= *offset_int)
2045 update_size.has_value() && *update_size > 0 &&
2046 *m_offset >= *offset_int + *update_size)
2054 exprt member_name(ID_member_name);
2055 member_name.
set(ID_component_name,
component.get_name());
2060 *m_offset < *offset_int ||
2061 (*m_offset == *offset_int && update_size.has_value() &&
2062 *update_size > 0 && m_size_bytes > *update_size))
2065 ID_byte_update_little_endian,
2073 update_size.has_value() && *update_size > 0 &&
2074 *m_offset + m_size_bytes > *offset_int + *update_size)
2083 ID_byte_extract_little_endian,
2098 if(root.
id()==ID_array)
2102 if(!el_size.has_value() || *el_size == 0 ||
2103 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2113 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2116 if(*offset_int * 8 < m_offset_bits + *el_size)
2118 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2119 bytes_req-=val_offset;
2120 if(val_offset + bytes_req > (*val_size) / 8)
2121 bytes_req = (*val_size) / 8 - val_offset;
2124 ID_byte_extract_little_endian,
2134 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2139 val_offset+=bytes_req;
2142 m_offset_bits += *el_size;
2145 return std::move(result);
2154 if(expr.
id() == ID_complex_real)
2158 if(complex_real_expr.op().id() == ID_complex)
2161 else if(expr.
id() == ID_complex_imag)
2165 if(complex_imag_expr.op().id() == ID_complex)
2178 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2190 op_type_id == ID_integer || op_type_id == ID_rational ||
2191 op_type_id == ID_real)
2196 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2200 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2206 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2207 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2208 if(!op0_value.has_value() || !op1_value.has_value())
2212 if(expr.
id() == ID_overflow_plus)
2213 no_overflow_result = *op0_value + *op1_value;
2214 else if(expr.
id() == ID_overflow_minus)
2215 no_overflow_result = *op0_value - *op1_value;
2216 else if(expr.
id() == ID_overflow_mult)
2217 no_overflow_result = *op0_value * *op1_value;
2218 else if(expr.
id() == ID_overflow_shl)
2219 no_overflow_result = *op0_value << *op1_value;
2226 no_overflow_result < bv_type.smallest() ||
2227 no_overflow_result > bv_type.largest())
2245 op_type_id == ID_integer || op_type_id == ID_rational ||
2246 op_type_id == ID_real)
2251 if(op_type_id == ID_natural)
2255 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2261 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2262 if(!op_value.has_value())
2266 if(expr.
id() == ID_overflow_unary_minus)
2267 no_overflow_result = -*op_value;
2274 no_overflow_result < bv_type.smallest() ||
2275 no_overflow_result > bv_type.largest())
2289 if(expr.
id()==ID_address_of)
2293 else if(expr.
id()==ID_if)
2302 if(r_it.has_changed())
2330 if(expr.
id()==ID_typecast)
2334 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2335 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2336 expr.
id()==ID_ge || expr.
id()==ID_le)
2340 else if(expr.
id()==ID_if)
2344 else if(expr.
id()==ID_lambda)
2348 else if(expr.
id()==ID_with)
2352 else if(expr.
id()==ID_update)
2356 else if(expr.
id()==ID_index)
2360 else if(expr.
id()==ID_member)
2364 else if(expr.
id()==ID_byte_update_little_endian ||
2365 expr.
id()==ID_byte_update_big_endian)
2369 else if(expr.
id()==ID_byte_extract_little_endian ||
2370 expr.
id()==ID_byte_extract_big_endian)
2374 else if(expr.
id()==ID_pointer_object)
2378 else if(expr.
id() == ID_is_dynamic_object)
2382 else if(expr.
id() == ID_is_invalid_pointer)
2386 else if(expr.
id()==ID_object_size)
2390 else if(expr.
id()==ID_good_pointer)
2394 else if(expr.
id()==ID_div)
2398 else if(expr.
id()==ID_mod)
2402 else if(expr.
id()==ID_bitnot)
2406 else if(expr.
id()==ID_bitand ||
2407 expr.
id()==ID_bitor ||
2408 expr.
id()==ID_bitxor)
2412 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2416 else if(expr.
id()==ID_power)
2420 else if(expr.
id()==ID_plus)
2424 else if(expr.
id()==ID_minus)
2428 else if(expr.
id()==ID_mult)
2432 else if(expr.
id()==ID_floatbv_plus ||
2433 expr.
id()==ID_floatbv_minus ||
2434 expr.
id()==ID_floatbv_mult ||
2435 expr.
id()==ID_floatbv_div)
2439 else if(expr.
id()==ID_floatbv_typecast)
2443 else if(expr.
id()==ID_unary_minus)
2447 else if(expr.
id()==ID_unary_plus)
2451 else if(expr.
id()==ID_not)
2455 else if(expr.
id()==ID_implies ||
2456 expr.
id()==ID_or || expr.
id()==ID_xor ||
2461 else if(expr.
id()==ID_dereference)
2465 else if(expr.
id()==ID_address_of)
2469 else if(expr.
id()==ID_pointer_offset)
2473 else if(expr.
id()==ID_extractbit)
2477 else if(expr.
id()==ID_concatenation)
2481 else if(expr.
id()==ID_extractbits)
2485 else if(expr.
id()==ID_ieee_float_equal ||
2486 expr.
id()==ID_ieee_float_notequal)
2490 else if(expr.
id() == ID_bswap)
2494 else if(expr.
id()==ID_isinf)
2498 else if(expr.
id()==ID_isnan)
2502 else if(expr.
id()==ID_isnormal)
2506 else if(expr.
id()==ID_abs)
2510 else if(expr.
id()==ID_sign)
2514 else if(expr.
id() == ID_popcount)
2518 else if(expr.
id() == ID_count_leading_zeros)
2522 else if(expr.
id() == ID_count_trailing_zeros)
2526 else if(expr.
id() == ID_function_application)
2530 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2535 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2536 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2540 else if(expr.
id() == ID_overflow_unary_minus)
2545 if(!no_change_join_operands)
2551 # ifdef DEBUG_ON_DEMAND
2556 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2557 <<
" ---> " <<
format(
r.expr) <<
'\n';
2569 std::pair<simplify_expr_cachet::containert::iterator, bool>
2570 cache_result=simplify_expr_cache.container().
2571 insert(std::pair<exprt, exprt>(expr,
exprt()));
2573 if(!cache_result.second)
2575 const exprt &new_expr=cache_result.first->second;
2591 if(simplify_node_result.has_changed())
2594 tmp = simplify_node_result.expr;
2597 #ifdef USE_LOCAL_REPLACE_MAP
2599 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2600 if(it!=local_replace_map.end())
2606 if(!local_replace_map.empty() &&
2625 cache_result.first->second = tmp;
2628 return std::move(tmp);
2635 #ifdef DEBUG_ON_DEMAND
2637 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2640 #ifdef DEBUG_ON_DEMAND
2642 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2644 if(result.has_changed())