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++)
193 const auto first_value_opt =
203 const auto second_value_opt =
206 if(!second_value_opt)
214 const bool includes =
240 const auto numeric_length =
277 const bool first_shorter = s1_size < s2_size;
282 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
284 if(it_pair.first == ops1.end())
293 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
305 const bool search_from_end)
307 std::size_t starting_index = 0;
312 auto &starting_index_expr = expr.
arguments().at(2);
314 if(starting_index_expr.id() != ID_constant)
325 starting_index = numeric_cast_v<std::size_t>(idx);
340 const auto search_string_size = s1_data.
operands().size();
341 if(starting_index >= search_string_size)
346 unsigned long starting_offset =
347 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
370 ? starting_index > 0 ? starting_index : search_string_size
376 auto end = std::prev(s1_data.
operands().end(), starting_offset);
377 auto it = std::find_end(
384 std::distance(s1_data.
operands().begin(), it), expr.
type());
388 auto it = std::search(
389 std::next(s1_data.
operands().begin(), starting_index),
396 std::distance(s1_data.
operands().begin(), it), expr.
type());
399 else if(expr.
arguments().at(1).id() == ID_constant)
404 const auto c1_val = numeric_cast_v<mp_integer>(c1);
406 auto pred = [&](
const exprt &c2) {
409 return c1_val == c2_val;
414 auto it = std::find_if(
415 std::next(s1_data.
operands().rbegin(), starting_offset),
420 std::distance(s1_data.
operands().begin(), it.base() - 1),
425 auto it = std::find_if(
426 std::next(s1_data.
operands().begin(), starting_index),
431 std::distance(s1_data.
operands().begin(), it), expr.
type());
451 if(expr.
arguments().at(1).id() != ID_constant)
469 const auto i_opt = numeric_cast<std::size_t>(index);
471 if(!i_opt || *i_opt >= char_seq.
operands().size())
478 if(c.type() != expr.
type())
489 auto &operands = string_data.
operands();
490 for(
auto &operand : operands)
493 auto character = numeric_cast_v<unsigned int>(constant_value);
499 if(isalpha(character))
501 if(isupper(character))
503 from_integer(tolower(character), constant_value.type());
525 const auto first_value_opt =
535 const auto second_value_opt =
538 if(!second_value_opt)
551 bool is_equal = first_value == second_value;
570 const auto first_value_opt =
580 const auto second_value_opt =
583 if(!second_value_opt)
594 if(offset.id() != ID_constant)
602 offset_int + second_value.
operands().size();
605 exprt::operandst::const_iterator second_it =
607 for(
const auto &first_op : first_value.
operands())
611 else if(second_it == second_value.
operands().end())
613 else if(first_op != *second_it)
642 if(func_id == ID_cprover_string_startswith_func)
646 else if(func_id == ID_cprover_string_endswith_func)
650 else if(func_id == ID_cprover_string_is_empty_func)
654 else if(func_id == ID_cprover_string_compare_to_func)
658 else if(func_id == ID_cprover_string_index_of_func)
662 else if(func_id == ID_cprover_string_char_at_func)
666 else if(func_id == ID_cprover_string_contains_func)
670 else if(func_id == ID_cprover_string_last_index_of_func)
674 else if(func_id == ID_cprover_string_equals_ignore_case_func)
689 if(expr.
op().
id() == ID_infinity)
694 return std::move(tmp);
701 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
711 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
712 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
716 auto new_expr = expr;
728 if(expr_type.
id()==ID_bool)
733 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
741 op_type.
id() == ID_bool &&
742 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
743 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
761 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
762 if(typecast.op().type()==expr_type)
764 return typecast.op();
770 if(expr_type.
id()==ID_c_bool &&
771 op_type.
id()!=ID_bool)
775 auto new_expr = expr;
789 return std::move(tmp);
795 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
796 op_type.
id() == ID_pointer)
798 auto new_expr = expr;
806 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
807 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
808 op_type.
id() == ID_pointer)
813 auto outer_cast = expr;
822 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
823 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
828 if(((op_plus_expr.op0().id() == ID_typecast &&
830 (op_plus_expr.op0().is_constant() &&
835 if(sub_size.has_value())
837 auto new_expr = expr;
840 if(*sub_size == 0 || *sub_size == 1)
863 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
864 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
874 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
875 op_id==ID_unary_minus ||
876 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
895 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
905 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
906 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
910 if(step.has_value() && *step != 0)
913 auto new_expr = expr;
915 new_expr.
op().
type() = size_t_type;
917 for(
auto &op : new_expr.op().operands())
919 if(op.type().id()==ID_pointer)
937 if(expr.
op().
id()==ID_if &&
944 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
946 return std::move(new_expr);
951 const exprt &operand = expr.
op();
960 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
962 if(op_type_id==ID_integer ||
963 op_type_id==ID_natural)
969 if(expr_type_id==ID_bool)
974 if(expr_type_id==ID_unsignedbv ||
975 expr_type_id==ID_signedbv ||
976 expr_type_id==ID_c_enum ||
977 expr_type_id==ID_c_bit_field ||
978 expr_type_id==ID_integer)
982 else if(expr_type_id == ID_c_enum_tag)
985 if(!c_enum_type.is_incomplete())
988 tmp.
type() = expr_type;
989 return std::move(tmp);
993 else if(op_type_id==ID_rational)
996 else if(op_type_id==ID_real)
999 else if(op_type_id==ID_bool)
1001 if(expr_type_id==ID_unsignedbv ||
1002 expr_type_id==ID_signedbv ||
1003 expr_type_id==ID_integer ||
1004 expr_type_id==ID_natural ||
1005 expr_type_id==ID_rational ||
1006 expr_type_id==ID_c_bool ||
1007 expr_type_id==ID_c_enum ||
1008 expr_type_id==ID_c_bit_field)
1019 else if(expr_type_id==ID_c_enum_tag)
1022 if(!c_enum_type.is_incomplete())
1024 unsigned int_value = operand.
is_true() ? 1u : 0u;
1026 tmp.
type()=expr_type;
1027 return std::move(tmp);
1030 else if(expr_type_id==ID_pointer &&
1037 else if(op_type_id==ID_unsignedbv ||
1038 op_type_id==ID_signedbv ||
1039 op_type_id==ID_c_bit_field ||
1040 op_type_id==ID_c_bool)
1047 if(expr_type_id==ID_bool)
1052 if(expr_type_id==ID_c_bool)
1057 if(expr_type_id==ID_integer)
1062 if(expr_type_id==ID_natural)
1070 if(expr_type_id==ID_unsignedbv ||
1071 expr_type_id==ID_signedbv ||
1072 expr_type_id==ID_bv ||
1073 expr_type_id==ID_c_bit_field)
1078 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1080 return std::move(result);
1083 if(expr_type_id==ID_c_enum_tag)
1086 if(!c_enum_type.is_incomplete())
1089 tmp.
type()=expr_type;
1090 return std::move(tmp);
1094 if(expr_type_id==ID_c_enum)
1099 if(expr_type_id==ID_fixedbv)
1111 if(expr_type_id==ID_floatbv)
1123 if(expr_type_id==ID_rational)
1129 else if(op_type_id==ID_fixedbv)
1131 if(expr_type_id==ID_unsignedbv ||
1132 expr_type_id==ID_signedbv)
1138 else if(expr_type_id==ID_fixedbv)
1145 else if(expr_type_id == ID_bv)
1151 else if(op_type_id==ID_floatbv)
1155 if(expr_type_id==ID_unsignedbv ||
1156 expr_type_id==ID_signedbv)
1161 else if(expr_type_id==ID_floatbv)
1167 else if(expr_type_id==ID_fixedbv)
1177 else if(expr_type_id == ID_bv)
1182 else if(op_type_id==ID_bv)
1185 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1186 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1187 expr_type_id == ID_c_bit_field)
1191 if(expr_type_id != ID_c_enum_tag)
1197 result.type() = tag_type;
1198 return std::move(result);
1201 else if(expr_type_id == ID_floatbv)
1206 ieee_float.unpack(int_value);
1207 return ieee_float.to_expr();
1209 else if(expr_type_id == ID_fixedbv)
1214 fixedbv.set_value(int_value);
1215 return fixedbv.to_expr();
1218 else if(op_type_id==ID_c_enum_tag)
1225 auto new_expr = expr;
1230 else if(op_type_id==ID_c_enum)
1236 auto new_expr = expr;
1242 else if(operand.
id()==ID_typecast)
1247 op_type_id == expr_type_id &&
1248 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1252 auto new_expr = expr;
1258 else if(operand.
id()==ID_address_of)
1264 o.
type().
id() == ID_array &&
1282 if(pointer.
type().
id()!=ID_pointer)
1285 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1289 auto tmp_op1 = expr;
1293 auto tmp_op2 = expr;
1297 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1302 if(pointer.
id()==ID_address_of)
1310 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1318 if(address_of.
object().
id()==ID_index)
1343 bool no_change =
true;
1349 auto with_expr = expr;
1351 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1355 if(old_type_followed.
id() == ID_struct)
1357 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1359 while(with_expr.operands().size() > 1)
1362 with_expr.where().get(ID_component_name);
1364 if(!
to_struct_type(old_type_followed).has_component(component_name))
1367 std::size_t number =
1370 if(number >= with_expr.old().operands().size())
1373 with_expr.old().operands()[number].swap(with_expr.new_value());
1375 with_expr.operands().erase(++with_expr.operands().begin());
1376 with_expr.operands().erase(++with_expr.operands().begin());
1383 with_expr.old().type().id() == ID_array ||
1384 with_expr.old().type().id() == ID_vector)
1387 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1388 with_expr.old().id() == ID_vector)
1390 while(with_expr.operands().size() > 1)
1392 const auto i = numeric_cast<mp_integer>(with_expr.where());
1397 if(*i < 0 || *i >= with_expr.old().operands().size())
1400 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1401 with_expr.new_value());
1403 with_expr.operands().erase(++with_expr.operands().begin());
1404 with_expr.operands().erase(++with_expr.operands().begin());
1411 if(with_expr.operands().size() == 1)
1412 return with_expr.old();
1417 return std::move(with_expr);
1428 exprt *value_ptr=&updated_value;
1430 for(
const auto &e : designator)
1434 if(e.id()==ID_index_designator &&
1435 value_ptr->
id()==ID_array)
1442 if(*i < 0 || *i >= value_ptr->
operands().size())
1445 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1447 else if(e.id()==ID_member_designator &&
1448 value_ptr->
id()==ID_struct)
1451 e.get(ID_component_name);
1457 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1466 return updated_value;
1471 if(expr.
id()==ID_plus)
1473 if(expr.
type().
id()==ID_pointer)
1477 if(op.type().id() == ID_pointer)
1481 else if(expr.
id()==ID_typecast)
1484 const typet &op_type = typecast_expr.op().type();
1486 if(op_type.
id()==ID_pointer)
1491 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1498 const exprt &casted_expr = typecast_expr.op();
1499 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1503 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1507 if(cand.
id() == ID_typecast)
1511 if(typecast_op.id() == ID_address_of)
1516 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1527 else if(expr.
id()==ID_address_of)
1531 if(
object.
id() == ID_index)
1537 else if(
object.
id() == ID_member)
1552 if(expr.
op().
id()==ID_if)
1563 if(el_size.has_value() && *el_size < 0)
1568 if(expr.
op().
id()==expr.
id())
1582 ((expr.
id() == ID_byte_extract_big_endian &&
1583 expr.
op().
id() == ID_byte_update_big_endian) ||
1584 (expr.
id() == ID_byte_extract_little_endian &&
1585 expr.
op().
id() == ID_byte_update_little_endian)) &&
1590 if(expr.
type() == op_byte_update.value().type())
1592 return op_byte_update.value();
1595 el_size.has_value() &&
1599 tmp.
op() = op_byte_update.value();
1607 auto offset = numeric_cast<mp_integer>(expr.
offset());
1608 if(!offset.has_value() || *offset < 0)
1621 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1629 if(!el_size.has_value() || *el_size == 0)
1632 if(expr.
op().
id()==ID_array_of &&
1640 if(!const_bits_opt.has_value())
1643 std::string const_bits=const_bits_opt.value();
1645 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1648 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1649 const_bits+=const_bits;
1651 std::string el_bits = std::string(
1653 numeric_cast_v<std::size_t>(*offset * 8),
1654 numeric_cast_v<std::size_t>(*el_size));
1657 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1660 return std::move(*tmp);
1665 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1680 const bool struct_has_flexible_array_member =
has_subtype(
1682 [&](
const typet &type) {
1683 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1686 const struct_typet &st = to_struct_type(ns.follow(type));
1687 const auto &comps = st.components();
1688 if(comps.empty() || comps.back().type().id() != ID_array)
1692 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1693 return !size.has_value() || *size <= 1;
1697 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1698 !struct_has_flexible_array_member)
1700 std::string bits_cut = std::string(
1702 numeric_cast_v<std::size_t>(*offset * 8),
1703 numeric_cast_v<std::size_t>(*el_size));
1706 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1709 return std::move(*tmp);
1715 if(!subexpr.has_value() || subexpr.value() == expr)
1727 expr.
id() == expr.
op().
id() &&
1733 return std::move(tmp);
1736 const exprt &root = expr.
op();
1744 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1745 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1748 expr.
id()==ID_byte_update_little_endian ?
1749 ID_byte_extract_little_endian :
1750 ID_byte_extract_big_endian,
1751 value, offset, expr.
type());
1757 const auto offset_int = numeric_cast<mp_integer>(offset);
1759 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1760 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1761 *offset_int + *val_size <= *root_size)
1764 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1766 if(root_bits.has_value())
1768 const auto val_bits =
1769 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1771 if(val_bits.has_value())
1774 numeric_cast_v<std::size_t>(*offset_int * 8),
1775 numeric_cast_v<std::size_t>(*val_size),
1781 expr.
id() == ID_byte_update_little_endian,
1785 return std::move(*tmp);
1798 if(expr.
id()!=ID_byte_update_little_endian)
1801 if(value.
id()==ID_with)
1805 if(with.
old().
id()==ID_byte_extract_little_endian)
1812 if(!(root==extract.
op()))
1814 if(!(offset==extract.
offset()))
1818 if(tp.
id()==ID_struct)
1825 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1840 tmp.set_value(std::move(new_value));
1845 else if(tp.
id()==ID_array)
1851 exprt index_offset =
1865 tmp.set_value(std::move(new_value));
1873 if(!offset_int.has_value() || *offset_int < 0)
1879 if(!val_size.has_value() || *val_size == 0)
1884 if(op_type.
id()==ID_struct)
1903 if(!m_offset.has_value())
1910 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1916 mp_integer m_size_bytes = (*m_size_bits) / 8;
1919 if(*m_offset + m_size_bytes <= *offset_int)
1923 update_size.has_value() && *update_size > 0 &&
1924 *m_offset >= *offset_int + *update_size)
1932 exprt member_name(ID_member_name);
1933 member_name.
set(ID_component_name,
component.get_name());
1938 *m_offset < *offset_int ||
1939 (*m_offset == *offset_int && update_size.has_value() &&
1940 *update_size > 0 && m_size_bytes > *update_size))
1943 ID_byte_update_little_endian,
1951 update_size.has_value() && *update_size > 0 &&
1952 *m_offset + m_size_bytes > *offset_int + *update_size)
1961 ID_byte_extract_little_endian,
1976 if(root.
id()==ID_array)
1980 if(!el_size.has_value() || *el_size == 0 ||
1981 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
1991 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
1994 if(*offset_int * 8 < m_offset_bits + *el_size)
1996 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
1997 bytes_req-=val_offset;
1998 if(val_offset + bytes_req > (*val_size) / 8)
1999 bytes_req = (*val_size) / 8 - val_offset;
2012 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2017 val_offset+=bytes_req;
2020 m_offset_bits += *el_size;
2023 return std::move(result);
2032 if(expr.
id() == ID_complex_real)
2036 if(complex_real_expr.op().id() == ID_complex)
2039 else if(expr.
id() == ID_complex_imag)
2043 if(complex_imag_expr.op().id() == ID_complex)
2056 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2068 op_type_id == ID_integer || op_type_id == ID_rational ||
2069 op_type_id == ID_real)
2074 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2078 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2084 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2085 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2086 if(!op0_value.has_value() || !op1_value.has_value())
2090 if(expr.
id() == ID_overflow_plus)
2091 no_overflow_result = *op0_value + *op1_value;
2092 else if(expr.
id() == ID_overflow_minus)
2093 no_overflow_result = *op0_value - *op1_value;
2094 else if(expr.
id() == ID_overflow_mult)
2095 no_overflow_result = *op0_value * *op1_value;
2096 else if(expr.
id() == ID_overflow_shl)
2097 no_overflow_result = *op0_value << *op1_value;
2104 no_overflow_result < bv_type.smallest() ||
2105 no_overflow_result > bv_type.largest())
2123 op_type_id == ID_integer || op_type_id == ID_rational ||
2124 op_type_id == ID_real)
2129 if(op_type_id == ID_natural)
2133 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2139 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2140 if(!op_value.has_value())
2144 if(expr.
id() == ID_overflow_unary_minus)
2145 no_overflow_result = -*op_value;
2152 no_overflow_result < bv_type.smallest() ||
2153 no_overflow_result > bv_type.largest())
2167 if(expr.
id()==ID_address_of)
2171 else if(expr.
id()==ID_if)
2180 if(r_it.has_changed())
2208 if(expr.
id()==ID_typecast)
2212 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2213 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2214 expr.
id()==ID_ge || expr.
id()==ID_le)
2218 else if(expr.
id()==ID_if)
2222 else if(expr.
id()==ID_lambda)
2226 else if(expr.
id()==ID_with)
2230 else if(expr.
id()==ID_update)
2234 else if(expr.
id()==ID_index)
2238 else if(expr.
id()==ID_member)
2242 else if(expr.
id()==ID_byte_update_little_endian ||
2243 expr.
id()==ID_byte_update_big_endian)
2247 else if(expr.
id()==ID_byte_extract_little_endian ||
2248 expr.
id()==ID_byte_extract_big_endian)
2252 else if(expr.
id()==ID_pointer_object)
2256 else if(expr.
id() == ID_is_dynamic_object)
2260 else if(expr.
id() == ID_is_invalid_pointer)
2264 else if(expr.
id()==ID_object_size)
2268 else if(expr.
id()==ID_good_pointer)
2272 else if(expr.
id()==ID_div)
2276 else if(expr.
id()==ID_mod)
2280 else if(expr.
id()==ID_bitnot)
2284 else if(expr.
id()==ID_bitand ||
2285 expr.
id()==ID_bitor ||
2286 expr.
id()==ID_bitxor)
2290 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2294 else if(expr.
id()==ID_power)
2298 else if(expr.
id()==ID_plus)
2302 else if(expr.
id()==ID_minus)
2306 else if(expr.
id()==ID_mult)
2310 else if(expr.
id()==ID_floatbv_plus ||
2311 expr.
id()==ID_floatbv_minus ||
2312 expr.
id()==ID_floatbv_mult ||
2313 expr.
id()==ID_floatbv_div)
2317 else if(expr.
id()==ID_floatbv_typecast)
2321 else if(expr.
id()==ID_unary_minus)
2325 else if(expr.
id()==ID_unary_plus)
2329 else if(expr.
id()==ID_not)
2333 else if(expr.
id()==ID_implies ||
2334 expr.
id()==ID_or || expr.
id()==ID_xor ||
2339 else if(expr.
id()==ID_dereference)
2343 else if(expr.
id()==ID_address_of)
2347 else if(expr.
id()==ID_pointer_offset)
2351 else if(expr.
id()==ID_extractbit)
2355 else if(expr.
id()==ID_concatenation)
2359 else if(expr.
id()==ID_extractbits)
2363 else if(expr.
id()==ID_ieee_float_equal ||
2364 expr.
id()==ID_ieee_float_notequal)
2368 else if(expr.
id() == ID_bswap)
2372 else if(expr.
id()==ID_isinf)
2376 else if(expr.
id()==ID_isnan)
2380 else if(expr.
id()==ID_isnormal)
2384 else if(expr.
id()==ID_abs)
2388 else if(expr.
id()==ID_sign)
2392 else if(expr.
id() == ID_popcount)
2396 else if(expr.
id() == ID_function_application)
2400 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2405 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2406 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2410 else if(expr.
id() == ID_overflow_unary_minus)
2415 if(!no_change_join_operands)
2421 # ifdef DEBUG_ON_DEMAND
2426 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2427 <<
" ---> " <<
format(
r.expr) <<
'\n';
2439 std::pair<simplify_expr_cachet::containert::iterator, bool>
2440 cache_result=simplify_expr_cache.container().
2441 insert(std::pair<exprt, exprt>(expr,
exprt()));
2443 if(!cache_result.second)
2445 const exprt &new_expr=cache_result.first->second;
2461 if(simplify_node_result.has_changed())
2464 tmp = simplify_node_result.expr;
2467 #ifdef USE_LOCAL_REPLACE_MAP
2469 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2470 if(it!=local_replace_map.end())
2476 if(!local_replace_map.empty() &&
2495 cache_result.first->second = tmp;
2498 return std::move(tmp);
2505 #ifdef DEBUG_ON_DEMAND
2507 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2510 #ifdef DEBUG_ON_DEMAND
2512 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2514 if(result.has_changed())