41 struct simplify_expr_cachet
45 typedef std::unordered_map<
48 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
51 containert container_normal;
53 containert &container()
55 return container_normal;
59 simplify_expr_cachet simplify_expr_cache;
71 if(type.
id()==ID_floatbv)
78 else if(type.
id()==ID_signedbv ||
79 type.
id()==ID_unsignedbv)
111 if(type.
id()==ID_floatbv)
117 else if(type.
id()==ID_signedbv ||
118 type.
id()==ID_unsignedbv)
140 if(type.
id()==ID_signedbv ||
141 type.
id()==ID_unsignedbv)
148 for(result=0; value!=0; value=value>>1)
153 expr.
swap(simp_result);
172 if(expr.
op0().
id()==ID_infinity)
183 if(op_type.
id()==ID_pointer &&
186 (expr_type.
id()==ID_unsignedbv || expr_type.
id()==ID_signedbv) &&
197 if(expr_type.
id()==ID_pointer &&
198 expr.
op0().
id()==ID_typecast &&
200 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv) &&
220 if(expr_type.
id()==ID_bool)
224 inequality.
id(op_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
226 inequality.
lhs()=expr.
op0();
230 expr.
swap(inequality);
236 expr.
op0().
id()==ID_typecast)
245 if(typecast.op().type()==expr_type)
254 if(expr_type.
id()==ID_c_bool &&
255 op_type.
id()!=ID_bool)
259 inequality.
id(op_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
261 inequality.
lhs()=expr.
op0();
265 expr.
op0()=inequality;
271 if(expr_type.
id()==ID_pointer &&
285 if(expr_type.
id()==ID_pointer &&
286 expr.
op0().
id()==ID_typecast &&
287 op_type.
id()==ID_pointer &&
300 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
301 expr.
op0().
id()==ID_typecast &&
303 op_type.
id()==ID_pointer)
314 (expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
315 op_type.
id()==ID_pointer &&
316 expr.
op0().
id()==ID_plus &&
318 ((expr.
op0().
op0().
id()==ID_typecast &&
328 if(sub_size==0 || sub_size==1)
349 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
350 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
360 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
361 op_id==ID_unary_minus ||
362 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
373 it->make_typecast(expr.
type());
382 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
391 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
392 op_type.
id()==ID_pointer &&
393 expr.
op0().
id()==ID_plus)
404 if(op.type().id()==ID_pointer)
406 op.make_typecast(size_t_type);
410 op.make_typecast(size_t_type);
423 if(expr.
op0().
id()==ID_if &&
446 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
448 if(op_type_id==ID_integer ||
449 op_type_id==ID_natural)
455 if(expr_type_id==ID_bool)
461 if(expr_type_id==ID_unsignedbv ||
462 expr_type_id==ID_signedbv ||
463 expr_type_id==ID_c_enum ||
464 expr_type_id==ID_c_bit_field ||
465 expr_type_id==ID_integer)
471 else if(op_type_id==ID_rational)
474 else if(op_type_id==ID_real)
477 else if(op_type_id==ID_bool)
479 if(expr_type_id==ID_unsignedbv ||
480 expr_type_id==ID_signedbv ||
481 expr_type_id==ID_integer ||
482 expr_type_id==ID_natural ||
483 expr_type_id==ID_rational ||
484 expr_type_id==ID_c_bool ||
485 expr_type_id==ID_c_enum ||
486 expr_type_id==ID_c_bit_field)
501 else if(expr_type_id==ID_c_enum_tag)
504 if(c_enum_type.
id()==ID_c_enum)
506 unsigned int_value = operand.
is_true() ? 1u : 0u;
508 tmp.
type()=expr_type;
513 else if(expr_type_id==ID_pointer &&
521 else if(op_type_id==ID_unsignedbv ||
522 op_type_id==ID_signedbv ||
523 op_type_id==ID_c_bit_field ||
524 op_type_id==ID_c_bool)
531 if(expr_type_id==ID_bool)
537 if(expr_type_id==ID_c_bool)
543 if(expr_type_id==ID_integer)
549 if(expr_type_id==ID_natural)
558 if(expr_type_id==ID_unsignedbv ||
559 expr_type_id==ID_signedbv ||
560 expr_type_id==ID_bv ||
561 expr_type_id==ID_c_bit_field)
566 expr.
set(ID_C_c_sizeof_type, c_sizeof_type);
571 if(expr_type_id==ID_c_enum_tag)
574 if(c_enum_type.
id()==ID_c_enum)
577 tmp.
type()=expr_type;
583 if(expr_type_id==ID_c_enum)
589 if(expr_type_id==ID_fixedbv)
603 if(expr_type_id==ID_floatbv)
616 if(expr_type_id==ID_rational)
623 else if(op_type_id==ID_fixedbv)
625 if(expr_type_id==ID_unsignedbv ||
626 expr_type_id==ID_signedbv)
633 else if(expr_type_id==ID_fixedbv)
642 else if(op_type_id==ID_floatbv)
646 if(expr_type_id==ID_unsignedbv ||
647 expr_type_id==ID_signedbv)
653 else if(expr_type_id==ID_floatbv)
661 else if(expr_type_id==ID_fixedbv)
673 else if(op_type_id==ID_bv)
675 if(expr_type_id==ID_unsignedbv ||
676 expr_type_id==ID_signedbv ||
677 expr_type_id==ID_floatbv)
684 else if(op_type_id==ID_c_enum_tag)
696 else if(op_type_id==ID_c_enum)
708 else if(operand.
id()==ID_typecast)
713 op_type_id==expr_type_id &&
714 (expr_type_id==ID_unsignedbv || expr_type_id==ID_signedbv) &&
726 else if(operand.
id()==ID_address_of)
731 if(o.
type().
id()==ID_array &&
748 if(pointer.
type().
id()!=ID_pointer)
751 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
769 if(pointer.
id()==ID_address_of)
778 else if(pointer.
id()==ID_plus &&
780 pointer.
op0().
id()==ID_address_of)
784 if(address_of.
object().
id()==ID_index)
814 if(truth && cond.
id()==ID_lt && expr.
id()==ID_lt)
816 if(cond.
op0()==expr.
op0() &&
822 if(type_id==ID_integer || type_id==ID_natural)
831 else if(type_id==ID_unsignedbv)
841 else if(type_id==ID_signedbv)
852 if(cond.
op1()==expr.
op1() &&
858 if(type_id==ID_integer || type_id==ID_natural)
867 else if(type_id==ID_unsignedbv)
877 else if(type_id==ID_signedbv)
898 if(expr.
type().
id()==ID_bool)
975 if(cond.
id()==ID_and)
980 else if(cond.
id()==ID_or)
996 return tresult && fresult;
1008 if(expr.
id()==ID_and)
1013 for(exprt::operandst::iterator it1=operands.begin();
1014 it1!=operands.end(); it1++)
1016 for(exprt::operandst::iterator it2=operands.begin();
1017 it2!=operands.end(); it2++)
1029 result=tmp && result;
1055 if(cond.
id()==ID_not)
1060 truevalue.
swap(falsevalue);
1064 #ifdef USE_LOCAL_REPLACE_MAP 1068 if(cond.
id()==ID_and)
1072 if(it->id()==ID_not)
1073 local_replace_map.insert(
1076 local_replace_map.insert(
1081 local_replace_map.insert(std::make_pair(cond,
true_exprt()));
1085 local_replace_map=map_before;
1088 if(cond.
id()==ID_or)
1092 if(it->id()==ID_not)
1093 local_replace_map.insert(
1096 local_replace_map.insert(
1101 local_replace_map.insert(std::make_pair(cond,
false_exprt()));
1105 local_replace_map.swap(map_before);
1196 if(truevalue==falsevalue)
1199 tmp.
swap(truevalue);
1204 if(((truevalue.
id()==ID_struct && falsevalue.
id()==ID_struct) ||
1205 (truevalue.
id()==ID_array && falsevalue.
id()==ID_array)) &&
1208 exprt cond_copy=cond;
1209 exprt falsevalue_copy=falsevalue;
1210 expr.
swap(truevalue);
1212 exprt::operandst::const_iterator f_it=
1213 falsevalue_copy.
operands().begin();
1216 if_exprt if_expr(cond_copy, *it, *f_it);
1238 value_list.insert(int_value);
1242 else if(expr.
id()==ID_if)
1272 if(op0_type.
id()==ID_struct)
1274 if(expr.
op0().
id()==ID_struct ||
1275 expr.
op0().
id()==ID_constant)
1280 expr.
op1().
get(ID_component_name);
1283 has_component(component_name))
1287 component_number(component_name);
1298 else if(expr.
op0().
type().
id()==ID_array)
1300 if(expr.
op0().
id()==ID_array ||
1301 expr.
op0().
id()==ID_constant)
1344 exprt *value_ptr=&updated_value;
1346 for(
const auto &e : designator)
1350 if(e.id()==ID_index_designator &&
1351 value_ptr->
id()==ID_array)
1358 if(i<0 || i>=value_ptr->
operands().size())
1363 else if(e.id()==ID_member_designator &&
1364 value_ptr->
id()==ID_struct)
1367 e.get(ID_component_name);
1370 has_component(component_name))
1374 component_number(component_name);
1376 assert(number<value_ptr->operands().size());
1378 value_ptr=&value_ptr->
operands()[number];
1386 expr.
swap(updated_value);
1393 if(expr.
id()==ID_plus)
1395 if(expr.
type().
id()==ID_pointer)
1399 if(
ns.
follow(it->type()).
id()==ID_pointer)
1408 else if(expr.
id()==ID_typecast)
1414 if(op_type.
id()==ID_pointer)
1423 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1431 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
1435 if(cand.
id()==ID_typecast &&
1437 cand.
op0().
id()==ID_address_of)
1442 else if(cand.
id()==ID_typecast &&
1444 cand.
op0().
id()==ID_plus &&
1446 cand.
op0().
op0().
id()==ID_typecast &&
1456 else if(expr.
id()==ID_address_of)
1464 expr.
swap(new_expr);
1472 expr.
swap(new_expr);
1483 const std::string &bits,
1493 if(type.
id()==ID_unsignedbv ||
1494 type.
id()==ID_signedbv ||
1495 type.
id()==ID_floatbv ||
1496 type.
id()==ID_fixedbv)
1500 std::string tmp=bits;
1504 std::reverse(tmp.begin(), tmp.end());
1507 else if(type.
id()==ID_c_enum)
1513 else if(type.
id()==ID_c_enum_tag)
1519 else if(type.
id()==ID_union)
1526 for(
const auto &component : components)
1532 return union_exprt(component.get_name(), val, type);
1535 else if(type.
id()==ID_struct)
1545 for(
const auto &component : components)
1550 std::string comp_bits=
1555 exprt comp=
bits2expr(comp_bits, component.type(), little_endian);
1560 m_offset_bits+=m_size;
1565 else if(type.
id()==ID_array)
1574 std::size_t el_size=
1581 for(std::size_t i=0; i<n_el; ++i)
1583 std::string el_bits=std::string(bits, i*el_size, el_size);
1603 if(expr.
id()==ID_constant)
1605 if(type.
id()==ID_unsignedbv ||
1606 type.
id()==ID_signedbv ||
1607 type.
id()==ID_c_enum ||
1608 type.
id()==ID_c_enum_tag ||
1609 type.
id()==ID_floatbv ||
1610 type.
id()==ID_fixedbv)
1613 std::reverse(nat.begin(), nat.end());
1617 std::string result=nat;
1619 result[map.map_bit(i)]=nat[i];
1624 else if(expr.
id()==ID_union)
1628 else if(expr.
id()==ID_struct)
1634 if(!tmp.has_value())
1636 result+=tmp.value();
1641 else if(expr.
id()==ID_array)
1647 if(!tmp.has_value())
1649 result+=tmp.value();
1661 if(expr.
op().
id()==ID_if)
1675 if(expr.
op().
id()==expr.
id())
1690 if(((expr.
id()==ID_byte_extract_big_endian &&
1691 expr.
op().
id()==ID_byte_update_big_endian) ||
1692 (expr.
id()==ID_byte_extract_little_endian &&
1693 expr.
op().
id()==ID_byte_update_little_endian)) &&
1703 else if(el_size>=0 &&
1738 if(expr.
op().
id()==ID_array_of &&
1741 const auto const_bits_opt=
1745 if(!const_bits_opt.has_value())
1748 std::string const_bits=const_bits_opt.value();
1750 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1753 while(
mp_integer(const_bits.size())<offset*8+el_size)
1754 const_bits+=const_bits;
1756 std::string el_bits=
1766 expr.
id()==ID_byte_extract_little_endian);
1776 if(expr.
op().
id()==ID_array_of &&
1777 (offset*8)%el_size==0 &&
1789 expr2bits(expr.
op(), expr.
id()==ID_byte_extract_little_endian);
1793 if(bits.has_value() &&
1796 std::string bits_cut=
1806 expr.
id()==ID_byte_extract_little_endian);
1808 if(tmp.is_not_nil())
1817 if(expr.
id()!=ID_byte_extract_little_endian)
1823 if(op_type.
id()==ID_array)
1828 for(
const typet *op_type_ptr=&op_type;
1829 op_type_ptr->
id()==ID_array;
1835 assert(el_size%8==0);
1839 (expr.
type().
id()==ID_pointer &&
1840 op_type_ptr->subtype().id()==ID_pointer))
1842 if(offset%el_bytes==0)
1877 else if(op_type.
id()==ID_struct)
1885 for(
const auto &component : components)
1892 if(offset*8==m_offset_bits &&
1902 else if(offset*8>=m_offset_bits &&
1903 offset*8+el_size<=m_offset_bits+m_size &&
1916 m_offset_bits+=m_size;
1927 if(expr.
id()==expr.
op().
id() &&
1945 val_size>=root_size)
1948 expr.
id()==ID_byte_update_little_endian ?
1949 ID_byte_extract_little_endian :
1950 ID_byte_extract_big_endian,
1951 value, offset, expr.
type());
1967 if(expr.
id()!=ID_byte_update_little_endian)
1970 if(value.
id()==ID_with)
1974 if(with.
old().
id()==ID_byte_extract_little_endian)
1981 if(!(root==extract.
op()))
1983 if(!(offset==extract.
offset()))
1987 if(tp.
id()==ID_struct)
2015 else if(tp.
id()==ID_array)
2029 index_offset.
swap(tmp);
2046 if(
to_integer(offset, offset_int) || offset_int<0)
2057 if(op_type.
id()==ID_struct)
2068 struct_type.components();
2070 for(
const auto &component : components)
2087 else if(m_offset+m_size_bytes<=offset_int)
2090 else if(update_size>0 &&
2091 m_offset>=offset_int+update_size)
2095 result_expr=expr.
op();
2097 exprt member_name(ID_member_name);
2098 member_name.
set(ID_component_name, component.get_name());
2102 if(m_offset<offset_int ||
2103 (m_offset==offset_int &&
2105 m_size_bytes>update_size))
2108 ID_byte_update_little_endian,
2115 else if(update_size>0 &&
2116 m_offset+m_size_bytes>offset_int+update_size)
2125 ID_byte_extract_little_endian,
2137 expr.
swap(result_expr);
2145 expr.
swap(result_expr);
2153 if(root.
id()==ID_array)
2156 if(el_size<=0 || el_size%8!=0 || val_size%8!=0)
2164 if(offset_int*8+val_size<=m_offset_bits)
2167 if(offset_int*8<m_offset_bits+el_size)
2169 mp_integer bytes_req=(m_offset_bits+el_size)/8-offset_int;
2170 bytes_req-=val_offset;
2171 if(val_offset+bytes_req>val_size/8)
2172 bytes_req=val_size/8-val_offset;
2189 val_offset+=bytes_req;
2192 m_offset_bits+=el_size;
2209 if(expr.
id()==ID_address_of)
2213 else if(expr.
id()==ID_if)
2243 if(expr.
id()==ID_typecast)
2245 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2246 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2247 expr.
id()==ID_ge || expr.
id()==ID_le)
2249 else if(expr.
id()==ID_if)
2251 else if(expr.
id()==ID_lambda)
2253 else if(expr.
id()==ID_with)
2255 else if(expr.
id()==ID_update)
2257 else if(expr.
id()==ID_index)
2259 else if(expr.
id()==ID_member)
2261 else if(expr.
id()==ID_byte_update_little_endian ||
2262 expr.
id()==ID_byte_update_big_endian)
2264 else if(expr.
id()==ID_byte_extract_little_endian ||
2265 expr.
id()==ID_byte_extract_big_endian)
2267 else if(expr.
id()==ID_pointer_object)
2269 else if(expr.
id()==ID_dynamic_object)
2271 else if(expr.
id()==ID_invalid_pointer)
2273 else if(expr.
id()==ID_object_size)
2275 else if(expr.
id()==ID_good_pointer)
2277 else if(expr.
id()==ID_div)
2279 else if(expr.
id()==ID_mod)
2281 else if(expr.
id()==ID_bitnot)
2283 else if(expr.
id()==ID_bitand ||
2284 expr.
id()==ID_bitor ||
2285 expr.
id()==ID_bitxor)
2287 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2289 else if(expr.
id()==ID_power)
2291 else if(expr.
id()==ID_plus)
2293 else if(expr.
id()==ID_minus)
2295 else if(expr.
id()==ID_mult)
2297 else if(expr.
id()==ID_floatbv_plus ||
2298 expr.
id()==ID_floatbv_minus ||
2299 expr.
id()==ID_floatbv_mult ||
2300 expr.
id()==ID_floatbv_div)
2302 else if(expr.
id()==ID_floatbv_typecast)
2304 else if(expr.
id()==ID_unary_minus)
2306 else if(expr.
id()==ID_unary_plus)
2308 else if(expr.
id()==ID_not)
2310 else if(expr.
id()==ID_implies || expr.
id()==ID_iff ||
2311 expr.
id()==ID_or || expr.
id()==ID_xor ||
2314 else if(expr.
id()==ID_dereference)
2316 else if(expr.
id()==ID_address_of)
2318 else if(expr.
id()==ID_pointer_offset)
2320 else if(expr.
id()==ID_extractbit)
2322 else if(expr.
id()==ID_concatenation)
2324 else if(expr.
id()==ID_extractbits)
2326 else if(expr.
id()==ID_ieee_float_equal ||
2327 expr.
id()==ID_ieee_float_notequal)
2329 else if(expr.
id() == ID_bswap)
2331 else if(expr.
id()==ID_isinf)
2333 else if(expr.
id()==ID_isnan)
2335 else if(expr.
id()==ID_isnormal)
2337 else if(expr.
id()==ID_abs)
2339 else if(expr.
id()==ID_sign)
2341 else if(expr.
id() == ID_popcount)
2346 #ifdef DEBUG_ON_DEMAND
2351 std::cout <<
"===== " <<
format(old) <<
"\n ---> " <<
format(expr)
2365 std::pair<simplify_expr_cachet::containert::iterator, bool>
2366 cache_result=simplify_expr_cache.container().
2367 insert(std::pair<exprt, exprt>(expr,
exprt()));
2369 if(!cache_result.second)
2371 const exprt &new_expr=cache_result.first->second;
2390 #ifdef USE_LOCAL_REPLACE_MAP 2392 replace_mapt::const_iterator it=local_replace_map.find(tmp);
2393 if(it!=local_replace_map.end())
2399 if(!local_replace_map.empty() &&
2414 cache_result.first->second=expr;
2423 #ifdef DEBUG_ON_DEMAND 2425 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2428 #ifdef DEBUG_ON_DEMAND 2430 std::cout <<
"FULLSIMP " <<
format(expr) <<
"\n";
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
The type of an expression.
bool simplify_abs(exprt &expr)
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
bool simplify_member(exprt &expr)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast a generic exprt to a bswap_exprt.
std::size_t get_fraction_bits() const
bool simplify_sign(exprt &expr)
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
Maps a big-endian offset to a little-endian offset.
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
bool simplify_pointer_object(exprt &expr)
void set_value(const mp_integer &_v)
const mp_integer string2integer(const std::string &n, unsigned base)
bool simplify_popcount(popcount_exprt &expr)
bool simplify_node(exprt &expr)
bool simplify_if_cond(exprt &expr)
constant_exprt to_expr() const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Fixed-width bit-vector with IEEE floating-point interpretation.
bool simplify_shifts(exprt &expr)
bool simplify_index(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Deprecated expression utility functions.
bool simplify_concatenation(exprt &expr)
bool simplify_dynamic_object(exprt &expr)
exprt::operandst & designator()
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
The null pointer constant.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bool simplify_lambda(exprt &expr)
const componentst & components() const
void set_sign(bool _sign)
The trinary if-then-else operator.
bool simplify_mult(exprt &expr)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
A constant literal expression.
void make_bool(bool value)
bool simplify_mod(exprt &expr)
bool simplify_with(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
void round(const fixedbv_spect &dest_spec)
const typet & follow_tag(const union_tag_typet &) const
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
bool simplify_node_preorder(exprt &expr)
Extract member of struct or union.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
void change_spec(const ieee_float_spect &dest_spec)
bool simplify_bswap(bswap_exprt &expr)
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void set_value(const irep_idt &value)
mp_integer to_integer() const
bool simplify_good_pointer(exprt &expr)
Expression classes for byte-level operators.
The boolean constant true.
bool simplify_object(exprt &expr)
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
bool simplify_floatbv_op(exprt &expr)
bool simplify_div(exprt &expr)
bool simplify_boolean(exprt &expr)
void from_integer(const mp_integer &i)
bool simplify_if_disj(exprt &expr, const exprt &cond)
Fixed-width bit-vector with two's complement interpretation.
nonstd::optional< T > optionalt
bool simplify_address_of(exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
union constructor from single element
API to expression classes.
bool simplify_pointer_offset(exprt &expr)
bool simplify_isinf(exprt &expr)
const irep_idt & get(const irep_namet &name) const
irep_idt byte_extract_id()
bool simplify_byte_extract(byte_extract_exprt &expr)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
const exprt & size() const
#define forall_operands(it, expr)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
constant_exprt to_expr() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Fixed-width bit-vector with signed fixed-point interpretation.
bool has_operands() const
The boolean constant false.
bool simplify_unary_plus(exprt &expr)
std::size_t get_width() const
bool get_values(const exprt &expr, value_listt &value_list)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
std::vector< exprt > operandst
mp_integer to_integer() const
bool simplify_floatbv_typecast(exprt &expr)
bool simplify_if_preorder(if_exprt &expr)
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
bool simplify_typecast(exprt &expr)
bool simplify_rec(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
The popcount (counting the number of bits set to 1) expression.
bool simplify_unary_minus(exprt &expr)
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
bool simplify_ieee_float_relation(exprt &expr)
Operator to update elements in structs and arrays.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const source_locationt & source_location() const
void base_type(typet &type, const namespacet &ns)
const std::string & get_string(const irep_namet &name) const
bool simplify_update(exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
void from_integer(const mp_integer &i)
virtual bool simplify(exprt &expr)
#define Forall_operands(it, expr)
source_locationt & add_source_location()
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
bool simplify_dereference(exprt &expr)
size_t map_bit(size_t bit) const
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
bool simplify_not(exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
const typet & subtype() const
bool simplify_invalid_pointer(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
struct constructor from list of elements
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool simplify_isnormal(exprt &expr)
bool simplify_object_size(exprt &expr)
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
array constructor from list of elements
bool simplify_plus(exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
const componentt & get_component(const irep_idt &component_name) const
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify_bitnot(exprt &expr)
bool simplify_isnan(exprt &expr)
bool simplify(exprt &expr, const namespacet &ns)
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.