18 typedef std::map<exprt, std::set<exprt> > used_bits_mapt;
19 used_bits_mapt used_bits_map;
23 if(it->id()==ID_extractbit && it->op1().is_constant())
25 used_bits_map[it->op0()].insert(it->op1());
27 else if(it->id()==ID_not &&
28 it->op0().id()==ID_extractbit && it->op0().op1().is_constant())
30 used_bits_map[it->op0().op0()].insert(it->op0().op1());
34 for(used_bits_mapt::const_iterator it=used_bits_map.begin();
35 it!=used_bits_map.end();
40 boolbv_get_width(it->first.type(), width);
42 std::string value_string;
43 value_string.resize(width,
'0');
45 if(it->second.size()==width)
47 const irep_idt &ident=it->first.get(ID_identifier);
51 for(exprt::operandst::const_iterator oit=old_operands.begin();
52 oit!=old_operands.end();
55 if(oit->id()==ID_extractbit &&
56 oit->op1().is_constant())
58 if(oit->op0().get(ID_identifier)==ident)
63 value_string[value.to_ulong()]=
'1';
66 std::cout <<
"[" << value <<
"]=1\n";
72 else if(oit->id()==ID_not &&
73 oit->op0().id()==ID_extractbit &&
74 oit->op0().op1().is_constant())
76 if(oit->op0().op0().get(ID_identifier)==ident)
83 new_operands.push_back(*oit);
86 exprt new_value(ID_constant, it->first.type());
87 new_value.
set(ID_value, value_string);
88 new_operands.push_back(equality_exprt(it->first, new_value));
91 std::cout <<
"FINAL: " << value_string <<
'\n';
void simplify_extractbits(exprt &expr) const
const irep_idt & id() const
API to expression classes.
#define forall_operands(it, expr)
std::vector< exprt > operandst
Base class for all expressions.
void set(const irep_namet &name, const irep_idt &value)