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
92 boolbv.
status() <<
"Beautifying counterexample (guards)" 96 typedef std::map<literalt, unsigned> guard_countt;
97 guard_countt guard_count;
99 for(symex_target_equationt::SSA_stepst::const_iterator
103 if(it->is_assignment() &&
106 if(!it->guard_literal.is_constant())
107 guard_count[it->guard_literal]++;
119 for(
const auto &g : guard_count)
120 prop_minimize.
objective(g.first, g.second);
127 boolbv.
status() <<
"Beautifying counterexample (values)" 138 bv_minimize(minimization_list);
The type of an expression, extends irept.
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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()
mstreamt & status() const
void operator()(boolbvt &boolbv, const symex_target_equationt &equation)
#define UNREACHABLE
This should be used to mark dead code.
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.