29 for(symex_target_equationt::SSA_stepst::const_iterator
33 if(it->is_assignment() &&
38 const typet &type=it->ssa_lhs.type();
43 if(type.
id()==ID_signedbv ||
44 type.
id()==ID_fixedbv ||
45 type.
id()==ID_floatbv)
48 minimization_list.insert(abs_expr);
51 minimization_list.insert(it->ssa_lhs);
62 symex_target_equationt::SSA_stepst::const_iterator
69 for(symex_target_equationt::SSA_stepst::const_iterator
94 bv_cbmc.
status() <<
"Beautifying counterexample (guards)" 98 typedef std::map<literalt, unsigned> guard_countt;
99 guard_countt guard_count;
101 for(symex_target_equationt::SSA_stepst::const_iterator
105 if(it->is_assignment() &&
108 if(!it->guard_literal.is_constant())
109 guard_count[it->guard_literal]++;
121 for(
const auto &g : guard_count)
122 prop_minimize.
objective(g.first, g.second);
129 bv_cbmc.
status() <<
"Beautifying counterexample (values)" 140 bv_minimize(minimization_list);
The type of an expression.
void objective(const literalt condition, const weightt weight=1)
Add an objective.
static mstreamt & eom(mstreamt &m)
symex_target_equationt::SSA_stepst::const_iterator failed
const irep_idt & id() const
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
API to expression classes.
virtual void set_message_handler(message_handlert &_message_handler)
std::set< exprt > minimization_listt
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
void operator()(bv_cbmct &bv_cbmc, const symex_target_equationt &equation, const namespacet &ns)
void get_minimization_list(prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)
void set_to(const exprt &expr, bool value) override
Counterexample Beautification.