37 std::vector<mp_integer> bytes;
40 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
41 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
45 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
49 "bytes is not empty because we just pushed just as many elements on "
50 "top of it as we are popping now");
51 new_value+=bytes.back()<<bit;
73 type_id == ID_integer || type_id == ID_natural ||
74 type_id == ID_unsignedbv || type_id == ID_signedbv)
83 else if(type_id==ID_rational)
92 else if(type_id==ID_fixedbv)
99 else if(type_id==ID_floatbv)
122 type_id == ID_integer || type_id == ID_natural ||
123 type_id == ID_unsignedbv || type_id == ID_signedbv)
132 else if(type_id==ID_rational)
141 else if(type_id==ID_fixedbv)
148 else if(type_id==ID_floatbv)
169 bool no_change =
true;
172 exprt::operandst::iterator constant;
175 bool constant_found =
false;
180 for(exprt::operandst::iterator it = new_operands.begin();
181 it != new_operands.end();)
190 it->type().id()!=ID_floatbv)
196 bool do_erase =
false;
199 if(it->is_constant() && it->type()==expr.
type())
202 if(!c_sizeof_type.has_value())
204 const typet &sizeof_type =
205 static_cast<const typet &
>(it->find(ID_C_c_sizeof_type));
207 c_sizeof_type = sizeof_type;
220 constant_found =
true;
227 it = new_operands.erase(it);
234 if(c_sizeof_type.has_value())
238 "c_sizeof_type is only set to a non-nil value "
239 "if a constant has been found");
240 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
243 if(new_operands.size() == 1)
245 return new_operands.front();
250 if(constant_found && constant->is_one())
253 new_operands.erase(constant);
256 if(new_operands.size() == 1)
257 return new_operands.front();
266 tmp.
operands() = std::move(new_operands);
267 return std::move(tmp);
278 if(expr_type!=expr.
op0().
type() ||
284 if(expr_type.
id()==ID_signedbv ||
285 expr_type.
id()==ID_unsignedbv ||
286 expr_type.
id()==ID_natural ||
287 expr_type.
id()==ID_integer)
289 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
290 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
293 if(int_value1.has_value() && *int_value1 == 0)
297 if(int_value1.has_value() && *int_value1 == 1)
303 if(int_value0.has_value() && *int_value0 == 0)
308 if(int_value0.has_value() && int_value1.has_value())
310 mp_integer result = *int_value0 / *int_value1;
314 else if(expr_type.
id()==ID_rational)
322 if(ok1 && rat_value1.
is_zero())
325 if((ok1 && rat_value1.
is_one()) ||
337 return std::move(tmp);
340 else if(expr_type.
id()==ID_fixedbv)
370 if(expr.
type().
id()==ID_signedbv ||
371 expr.
type().
id()==ID_unsignedbv ||
372 expr.
type().
id()==ID_natural ||
373 expr.
type().
id()==ID_integer)
378 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
379 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
381 if(int_value1.has_value() && *int_value1 == 0)
385 (int_value1.has_value() && *int_value1 == 1) ||
386 (int_value0.has_value() && *int_value0 == 0))
391 if(int_value0.has_value() && int_value1.has_value())
393 mp_integer result = *int_value0 % *int_value1;
407 bool no_change =
true;
414 if(expr.
type().
id() == ID_floatbv)
419 const exprt::operandst::iterator next = std::next(it);
421 if(next != new_operands.end())
423 if(it->type()==next->type() &&
428 new_operands.erase(next);
439 expr.
op0().
id() == ID_plus && expr.
op0().
type().
id() == ID_pointer &&
444 if(op0.
op1().
id() == ID_plus)
459 if(
is_number(it->type()) && it->is_constant())
465 exprt::operandst::iterator const_sum;
466 bool const_sum_set=
false;
468 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
470 if(
is_number(it->type()) && it->is_constant())
492 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
496 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
497 if(it->id() == ID_unary_minus)
503 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
507 else if(it->id()==ID_unary_minus)
510 expr_mapt::iterator itm=expr_map.find(*it);
512 if(itm!=expr_map.end())
524 for(exprt::operandst::iterator it = new_operands.begin();
525 it != new_operands.end();
528 if(
is_number(it->type()) && it->is_zero())
530 it = new_operands.erase(it);
538 if(new_operands.empty())
542 else if(new_operands.size() == 1)
544 return new_operands.front();
552 tmp.
operands() = std::move(new_operands);
553 return std::move(tmp);
561 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
576 minus_expr.type().id() == ID_pointer &&
577 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
587 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
588 operands[1].type().id() == ID_pointer)
592 if(operands[0]==operands[1])
606 if(expr.
type().
id()!=ID_bool)
613 it->id() == ID_typecast &&
617 else if(it->is_zero() || it->is_one())
629 if(expr.
id()==ID_bitand)
631 else if(expr.
id()==ID_bitor)
633 else if(expr.
id()==ID_bitxor)
640 if(it->id()==ID_typecast)
642 else if(it->is_zero())
644 else if(it->is_one())
655 bool no_change =
true;
656 auto new_expr = expr;
662 while(new_expr.operands().size() >= 2)
664 if(!new_expr.op0().is_constant())
667 if(!new_expr.op1().is_constant())
670 if(new_expr.op0().type() != new_expr.type())
673 if(new_expr.op1().type() != new_expr.type())
679 std::function<bool(
bool,
bool)> f;
681 if(new_expr.id() == ID_bitand)
682 f = [](
bool a,
bool b) {
return a && b; };
683 else if(new_expr.id() == ID_bitor)
684 f = [](
bool a,
bool b) {
return a || b; };
685 else if(new_expr.id() == ID_bitxor)
686 f = [](
bool a,
bool b) {
return a != b; };
691 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
699 new_expr.operands().erase(new_expr.operands().begin());
700 new_expr.op0().swap(new_op);
707 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
709 for(exprt::operandst::iterator it = new_expr.operands().begin();
710 it != new_expr.operands().end();)
712 if(it->is_zero() && new_expr.operands().size() > 1)
714 it = new_expr.operands().erase(it);
718 it->is_constant() && it->type().id() == ID_bv &&
720 new_expr.operands().size() > 1)
722 it = new_expr.operands().erase(it);
732 if(new_expr.id() == ID_bitand)
734 const auto all_ones =
power(2, width) - 1;
735 for(exprt::operandst::iterator it = new_expr.operands().begin();
736 it != new_expr.operands().end();)
742 new_expr.operands().size() > 1)
744 it = new_expr.operands().erase(it);
754 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
756 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
758 return new_expr.op0();
760 else if(new_expr.id() == ID_bitxor)
766 if(new_expr.operands().size() == 1)
767 return new_expr.op0();
772 return std::move(new_expr);
785 const auto index_converted_to_int = numeric_cast<mp_integer>(expr.
index());
787 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
788 *index_converted_to_int >= src_bit_width)
799 numeric_cast_v<std::size_t>(*index_converted_to_int));
807 bool no_change =
true;
819 const bool value = op.
is_true();
828 while(i < new_expr.
operands().size() - 1)
843 const auto new_width = width_i + width_n;
846 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
861 else if(new_expr.
type().
id() == ID_verilog_unsignedbv)
866 while(i < new_expr.
operands().size() - 1)
873 (opi.
type().
id()==ID_verilog_unsignedbv ||
875 (opn.
type().
id()==ID_verilog_unsignedbv ||
879 const std::string new_value=
881 opi.
set(ID_value, new_value);
883 opi.
type().
id(ID_verilog_unsignedbv);
897 return new_expr.
op0();
903 return std::move(new_expr);
912 const auto distance = numeric_cast<mp_integer>(expr.
distance());
914 if(!distance.has_value())
920 auto value = numeric_cast<mp_integer>(expr.
op());
923 !value.has_value() && expr.
op().
type().
id() == ID_bv &&
924 expr.
op().
id() == ID_constant)
931 if(!value.has_value())
935 expr.
op().
type().
id() == ID_unsignedbv ||
940 if(expr.
id()==ID_lshr)
943 if(*distance >= width)
947 else if(*distance >= 0)
950 *value +=
power(2, width);
951 *value /=
power(2, *distance);
955 else if(expr.
id()==ID_ashr)
964 else if(expr.
id()==ID_shl)
967 if(*distance >= width)
971 else if(*distance >= 0)
973 *value *=
power(2, *distance);
981 if(expr.
id()==ID_lshr)
985 *value /=
power(2, *distance);
989 else if(expr.
id()==ID_ashr)
995 if(*value < 0 && new_value == 0)
1001 else if(expr.
id()==ID_shl)
1005 *value *=
power(2, *distance);
1020 const auto base = numeric_cast<mp_integer>(expr.
op0());
1021 const auto exponent = numeric_cast<mp_integer>(expr.
op1());
1023 if(!base.has_value())
1026 if(!exponent.has_value())
1046 const auto start = numeric_cast<mp_integer>(expr.
upper());
1047 const auto end = numeric_cast<mp_integer>(expr.
lower());
1049 if(!start.has_value())
1052 if(!end.has_value())
1057 if(!width.has_value())
1060 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1063 DATA_INVARIANT(*start >= *end,
"extractbits must have upper() >= lower()");
1069 if(!svalue.has_value() || svalue->size() != *width)
1072 std::string extracted_value = svalue->substr(
1073 numeric_cast_v<std::size_t>(*end),
1074 numeric_cast_v<std::size_t>(*start - *end + 1));
1077 if(!result.has_value())
1080 return std::move(*result);
1082 else if(expr.
src().
id() == ID_concatenation)
1092 if(!op_width.has_value() || *op_width <= 0)
1095 if(*start + 1 == offset && *end + *op_width == offset)
1101 return std::move(tmp);
1104 offset -= *op_width;
1124 const exprt &operand = expr.
op();
1129 if(operand.
id()==ID_unary_minus)
1137 else if(operand.
id()==ID_constant)
1142 if(type_id==ID_integer ||
1143 type_id==ID_signedbv ||
1144 type_id==ID_unsignedbv)
1146 const auto int_value = numeric_cast<mp_integer>(constant_expr);
1148 if(!int_value.has_value())
1153 else if(type_id==ID_rational)
1161 else if(type_id==ID_fixedbv)
1167 else if(type_id==ID_floatbv)
1183 const auto &type = expr.
type();
1186 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1187 type.id() == ID_signedbv)
1191 if(op.
type() == type)
1193 if(op.
id()==ID_constant)
1196 const auto new_value =
1197 make_bvrep(width, [&value, &width](std::size_t i) {
1212 if(expr.
type().
id()!=ID_bool)
1223 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1227 auto new_expr = expr;
1228 new_expr.
op0().
swap(new_expr.op1());
1232 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1246 (expr.
id() == ID_equal || expr.
id() == ID_notequal))
1251 if(tmp0.
id()==ID_pointer_object &&
1252 tmp1.
id()==ID_pointer_object &&
1253 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1258 if(tmp0.
type().
id()==ID_c_enum_tag)
1261 if(tmp1.
type().
id()==ID_c_enum_tag)
1268 if(tmp0_const && tmp1_const)
1278 if(expr.
id()==ID_ge)
1280 else if(expr.
id()==ID_le)
1282 else if(expr.
id()==ID_gt)
1284 else if(expr.
id()==ID_lt)
1312 if(tmp0.
type().
id() == ID_c_enum_tag)
1315 if(tmp1.
type().
id() == ID_c_enum_tag)
1321 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1325 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1327 !equal && tmp0_const.type().id() == ID_pointer &&
1328 tmp1_const.type().id() == ID_pointer)
1332 tmp1_const.get_value() == ID_NULL))
1338 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1343 if(tmp0.
type().
id() == ID_fixedbv)
1348 if(expr.
id() == ID_ge)
1350 else if(expr.
id() == ID_le)
1352 else if(expr.
id() == ID_gt)
1354 else if(expr.
id() == ID_lt)
1359 else if(tmp0.
type().
id() == ID_floatbv)
1364 if(expr.
id() == ID_ge)
1366 else if(expr.
id() == ID_le)
1368 else if(expr.
id() == ID_gt)
1370 else if(expr.
id() == ID_lt)
1375 else if(tmp0.
type().
id() == ID_rational)
1385 if(expr.
id() == ID_ge)
1387 else if(expr.
id() == ID_le)
1389 else if(expr.
id() == ID_gt)
1391 else if(expr.
id() == ID_lt)
1398 const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1403 const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1408 if(expr.
id() == ID_ge)
1410 else if(expr.
id() == ID_le)
1412 else if(expr.
id() == ID_gt)
1414 else if(expr.
id() == ID_lt)
1432 if(op0.
id()==ID_plus)
1434 bool no_change =
true;
1442 else if(op1.
id()==ID_plus)
1444 bool no_change =
true;
1455 op0.
type().
id()!=ID_complex)
1473 if(expr.
op0().
type().
id() == ID_floatbv)
1478 expr.
op0().
type().
id() == ID_pointer && expr.
id() != ID_equal &&
1479 expr.
id() != ID_notequal)
1485 if(expr.
id()==ID_notequal)
1487 auto new_rel_expr = expr;
1488 new_rel_expr.
id(ID_equal);
1492 else if(expr.
id()==ID_gt)
1494 auto new_rel_expr = expr;
1495 new_rel_expr.
id(ID_ge);
1497 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1501 else if(expr.
id()==ID_lt)
1503 auto new_rel_expr = expr;
1504 new_rel_expr.
id(ID_ge);
1508 else if(expr.
id()==ID_le)
1510 auto new_rel_expr = expr;
1511 new_rel_expr.
id(ID_ge);
1513 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1520 expr.
id() == ID_ge || expr.
id() == ID_equal,
1521 "we previously converted all other cases to >= or ==");
1525 if(expr.
op0() == expr.
op1())
1530 if(expr.
id()==ID_equal)
1566 if(expr.
id()==ID_notequal)
1568 auto new_rel_expr = expr;
1569 new_rel_expr.
id(ID_equal);
1575 if(expr.
id()==ID_equal &&
1577 expr.
op1().
get(ID_value)==ID_NULL)
1581 if(expr.
op0().
id() == ID_address_of)
1586 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1587 object.
id() == ID_member ||
object.
id() == ID_index ||
1588 object.
id() == ID_string_constant)
1594 expr.
op0().
id() == ID_typecast &&
1598 const auto &
object =
1602 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1603 object.
id() == ID_member ||
object.
id() == ID_index ||
1604 object.
id() == ID_string_constant)
1610 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_pointer)
1614 op.
type().
id() != ID_pointer &&
1616 op.
type().
id() == ID_complex))
1623 auto new_expr = expr;
1625 if(new_expr.op0().type().id() != ID_pointer)
1626 new_expr.op1() =
from_integer(0, new_expr.op0().type());
1628 new_expr.op1().type() = new_expr.op0().type();
1639 if(expr.
op0().
id()==ID_plus)
1643 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1646 bool op_changed =
false;
1647 auto new_expr = expr;
1651 if(it->is_constant())
1669 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1682 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_floatbv &&
1689 ieee_floatt const_val_converted_back=const_val_converted;
1692 if(const_val_converted_back==const_val)
1697 return std::move(result);
1706 if(expr.
id()==ID_ge &&
1713 auto new_expr = expr;
1716 if(expr.
id()==ID_equal)
1719 if(operand.
id()==ID_unary_minus)
1722 return std::move(new_expr);
1724 else if(operand.
id()==ID_plus)
1729 if(operand_plus_expr.operands().size() == 2)
1732 if(operand_plus_expr.op0().id() == ID_unary_minus)
1733 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1735 if(operand_plus_expr.op1().id() == ID_unary_minus)
1738 operand_plus_expr.op0(),
1750 expr.
op0().
id() == ID_typecast &&
1764 return lhs_typecast_op;
1768 #define NORMALISE_CONSTANT_TESTS
1769 #ifdef NORMALISE_CONSTANT_TESTS
1771 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1776 if(expr.
id()==ID_notequal)
1778 auto new_rel_expr = expr;
1779 new_rel_expr.
id(ID_equal);
1783 else if(expr.
id()==ID_gt)
1792 auto new_expr = expr;
1795 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1798 else if(expr.
id()==ID_lt)
1800 auto new_rel_expr = expr;
1801 new_rel_expr.
id(ID_ge);
1805 else if(expr.
id()==ID_le)
1814 auto new_rel_expr = expr;
1815 new_rel_expr.
id(ID_ge);
1817 new_rel_expr.op1() =
from_integer(i, new_rel_expr.op1().type());
1834 if(!const_bits_opt.has_value())
1837 std::reverse(const_bits_opt->begin(), const_bits_opt->end());
1844 if(!result.has_value())
1847 return std::move(*result);
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
void set_width(std::size_t width)
std::size_t get_width() const
The byte swap expression.
std::size_t get_bits_per_byte() const
Concatenation of bit-vector operands.
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
bool value_is_zero_string() const
void set_value(const irep_idt &value)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
constant_exprt to_expr() const
constant_exprt to_expr() const
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
mp_integer largest() const
Return the largest value that can be represented using this type.
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A base class for multi-ary expressions Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
The plus expression Associativity is not specified.
A base class for shift and rotate operators.
static bool is_bitvector_type(const typet &type)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_bitnot(const bitnot_exprt &)
static resultt changed(resultt<> result)
resultt simplify_if(const if_exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_mod(const mod_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_node(exprt)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
resultt simplify_unary_minus(const unary_minus_exprt &)
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
The unary plus expression.
Fixed-width bit-vector with unsigned binary interpretation.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
#define Forall_expr(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Deprecated expression utility functions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
static bool mul_expr(constant_exprt &dest, const constant_exprt &expr)
produce a product of two expressions of the same type
static bool sum_expr(constant_exprt &dest, const constant_exprt &expr)
produce a sum of two constant expressions of the same type
static bool eliminate_common_addends(exprt &op0, exprt &op1)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.