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();
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)
1633 std::string tmp=
expr2bits(*it, little_endian);
1640 else if(expr.
id()==ID_array)
1645 std::string tmp=
expr2bits(*it, little_endian);
1659 if(expr.
op().
id()==ID_if)
1673 if(expr.
op().
id()==expr.
id())
1688 if(((expr.
id()==ID_byte_extract_big_endian &&
1689 expr.
op().
id()==ID_byte_update_big_endian) ||
1690 (expr.
id()==ID_byte_extract_little_endian &&
1691 expr.
op().
id()==ID_byte_update_little_endian)) &&
1701 else if(el_size>=0 &&
1736 if(expr.
op().
id()==ID_array_of &&
1737 expr.
op().
op0().
id()==ID_constant)
1739 std::string const_bits=
1744 while(
mp_integer(const_bits.size())<offset*8+el_size)
1745 const_bits+=const_bits;
1747 std::string el_bits=
1757 expr.
id()==ID_byte_extract_little_endian);
1767 if(expr.
op().
id()==ID_array_of &&
1768 (offset*8)%el_size==0 &&
1780 expr2bits(expr.
op(), expr.
id()==ID_byte_extract_little_endian);
1783 if(
mp_integer(bits.size())==el_size+offset*8)
1785 std::string bits_cut=
1795 expr.
id()==ID_byte_extract_little_endian);
1806 if(expr.
id()!=ID_byte_extract_little_endian)
1812 if(op_type.
id()==ID_array)
1817 for(
const typet *op_type_ptr=&op_type;
1818 op_type_ptr->
id()==ID_array;
1824 assert(el_size%8==0);
1828 (expr.
type().
id()==ID_pointer &&
1829 op_type_ptr->subtype().id()==ID_pointer))
1831 if(offset%el_bytes==0)
1866 else if(op_type.
id()==ID_struct)
1874 for(
const auto &component : components)
1881 if(offset*8==m_offset_bits &&
1891 else if(offset*8>=m_offset_bits &&
1892 offset*8+el_size<=m_offset_bits+m_size &&
1905 m_offset_bits+=m_size;
1916 if(expr.
id()==expr.
op().
id() &&
1934 val_size>=root_size)
1937 expr.
id()==ID_byte_update_little_endian ?
1938 ID_byte_extract_little_endian :
1939 ID_byte_extract_big_endian,
1940 value, offset, expr.
type());
1956 if(expr.
id()!=ID_byte_update_little_endian)
1959 if(value.
id()==ID_with)
1963 if(with.
old().
id()==ID_byte_extract_little_endian)
1970 if(!(root==extract.
op()))
1972 if(!(offset==extract.
offset()))
1976 if(tp.
id()==ID_struct)
2004 else if(tp.
id()==ID_array)
2018 index_offset.
swap(tmp);
2035 if(
to_integer(offset, offset_int) || offset_int<0)
2046 if(op_type.
id()==ID_struct)
2057 struct_type.components();
2059 for(
const auto &component : components)
2076 else if(m_offset+m_size_bytes<=offset_int)
2079 else if(update_size>0 &&
2080 m_offset>=offset_int+update_size)
2084 result_expr=expr.
op();
2086 exprt member_name(ID_member_name);
2087 member_name.
set(ID_component_name, component.get_name());
2091 if(m_offset<offset_int ||
2092 (m_offset==offset_int &&
2094 m_size_bytes>update_size))
2097 ID_byte_update_little_endian,
2104 else if(update_size>0 &&
2105 m_offset+m_size_bytes>offset_int+update_size)
2114 ID_byte_extract_little_endian,
2126 expr.
swap(result_expr);
2134 expr.
swap(result_expr);
2142 if(root.
id()==ID_array)
2145 if(el_size<=0 || el_size%8!=0 || val_size%8!=0)
2153 if(offset_int*8+val_size<=m_offset_bits)
2156 if(offset_int*8<m_offset_bits+el_size)
2158 mp_integer bytes_req=(m_offset_bits+el_size)/8-offset_int;
2159 bytes_req-=val_offset;
2160 if(val_offset+bytes_req>val_size/8)
2161 bytes_req=val_size/8-val_offset;
2178 val_offset+=bytes_req;
2181 m_offset_bits+=el_size;
2198 if(expr.
id()==ID_address_of)
2202 else if(expr.
id()==ID_if)
2232 if(expr.
id()==ID_typecast)
2234 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2235 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2236 expr.
id()==ID_ge || expr.
id()==ID_le)
2238 else if(expr.
id()==ID_if)
2240 else if(expr.
id()==ID_lambda)
2242 else if(expr.
id()==ID_with)
2244 else if(expr.
id()==ID_update)
2246 else if(expr.
id()==ID_index)
2248 else if(expr.
id()==ID_member)
2250 else if(expr.
id()==ID_byte_update_little_endian ||
2251 expr.
id()==ID_byte_update_big_endian)
2253 else if(expr.
id()==ID_byte_extract_little_endian ||
2254 expr.
id()==ID_byte_extract_big_endian)
2256 else if(expr.
id()==ID_pointer_object)
2258 else if(expr.
id()==ID_dynamic_object)
2260 else if(expr.
id()==ID_invalid_pointer)
2262 else if(expr.
id()==ID_object_size)
2264 else if(expr.
id()==ID_good_pointer)
2266 else if(expr.
id()==ID_div)
2268 else if(expr.
id()==ID_mod)
2270 else if(expr.
id()==ID_bitnot)
2272 else if(expr.
id()==ID_bitand ||
2273 expr.
id()==ID_bitor ||
2274 expr.
id()==ID_bitxor)
2276 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2278 else if(expr.
id()==ID_power)
2280 else if(expr.
id()==ID_plus)
2282 else if(expr.
id()==ID_minus)
2284 else if(expr.
id()==ID_mult)
2286 else if(expr.
id()==ID_floatbv_plus ||
2287 expr.
id()==ID_floatbv_minus ||
2288 expr.
id()==ID_floatbv_mult ||
2289 expr.
id()==ID_floatbv_div)
2291 else if(expr.
id()==ID_floatbv_typecast)
2293 else if(expr.
id()==ID_unary_minus)
2295 else if(expr.
id()==ID_unary_plus)
2297 else if(expr.
id()==ID_not)
2299 else if(expr.
id()==ID_implies || expr.
id()==ID_iff ||
2300 expr.
id()==ID_or || expr.
id()==ID_xor ||
2303 else if(expr.
id()==ID_dereference)
2305 else if(expr.
id()==ID_address_of)
2307 else if(expr.
id()==ID_pointer_offset)
2309 else if(expr.
id()==ID_extractbit)
2311 else if(expr.
id()==ID_concatenation)
2313 else if(expr.
id()==ID_extractbits)
2315 else if(expr.
id()==ID_ieee_float_equal ||
2316 expr.
id()==ID_ieee_float_notequal)
2318 else if(expr.
id() == ID_bswap)
2320 else if(expr.
id()==ID_isinf)
2322 else if(expr.
id()==ID_isnan)
2324 else if(expr.
id()==ID_isnormal)
2326 else if(expr.
id()==ID_abs)
2328 else if(expr.
id()==ID_sign)
2330 else if(expr.
id() == ID_popcount)
2335 #ifdef DEBUG_ON_DEMAND
2340 std::cout <<
"===== " <<
format(old) <<
"\n ---> " <<
format(expr)
2354 std::pair<simplify_expr_cachet::containert::iterator, bool>
2355 cache_result=simplify_expr_cache.container().
2356 insert(std::pair<exprt, exprt>(expr,
exprt()));
2358 if(!cache_result.second)
2360 const exprt &new_expr=cache_result.first->second;
2379 #ifdef USE_LOCAL_REPLACE_MAP 2381 replace_mapt::const_iterator it=local_replace_map.find(tmp);
2382 if(it!=local_replace_map.end())
2388 if(!local_replace_map.empty() &&
2403 cache_result.first->second=expr;
2412 #ifdef DEBUG_ON_DEMAND 2414 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2417 #ifdef DEBUG_ON_DEMAND 2419 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.
std::string expr2bits(const exprt &expr, bool little_endian)
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.
bool simplify_address_of(exprt &expr)
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.
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()
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)
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.