19 typedef std::map<exprt, std::set<exprt> > used_bits_mapt;
20 used_bits_mapt used_bits_map;
24 if(it->id() == ID_extractbit)
27 if(extractbit_expr.op1().is_constant())
28 used_bits_map[extractbit_expr.src()].insert(extractbit_expr.index());
30 else if(it->id() == ID_not &&
to_not_expr(*it).
op().
id() == ID_extractbit)
33 if(extractbit_expr.op1().is_constant())
34 used_bits_map[extractbit_expr.src()].insert(extractbit_expr.index());
40 for(used_bits_mapt::const_iterator it=used_bits_map.begin();
41 it!=used_bits_map.end();
46 boolbv_get_width(it->first.type(), width);
48 std::string value_string;
49 value_string.resize(width,
'0');
51 if(it->second.size()==width)
53 const irep_idt &ident=it->first.get(ID_identifier);
57 for(exprt::operandst::const_iterator oit=old_operands.begin();
58 oit!=old_operands.end();
61 if(oit->id()==ID_extractbit &&
62 oit->op1().is_constant())
64 if(oit->op0().get(ID_identifier)==ident)
67 const std::size_t value = numeric_cast_v<std::size_t>(val_expr);
68 value_string[value]=
'1';
71 std::cout <<
"[" << value <<
"]=1\n";
77 else if(oit->id()==ID_not &&
78 oit->op0().id()==ID_extractbit &&
79 oit->op0().op1().is_constant())
81 if(oit->op0().op0().get(ID_identifier)==ident)
88 new_operands.push_back(*oit);
92 new_operands.push_back(equality_exprt(it->first, new_value));
95 std::cout <<
"FINAL: " << value_string <<
'\n';