cprover
counterexample_beautification.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Counterexample Beautification using Incremental SAT
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/threeval.h>
15 #include <util/arith_tools.h>
16 #include <util/symbol.h>
17 #include <util/std_expr.h>
18 
19 #include <solvers/prop/minimize.h>
21 
23  prop_convt &prop_conv,
24  const symex_target_equationt &equation,
25  minimization_listt &minimization_list)
26 {
27  // ignore the ones that are assigned under false guards
28 
29  for(symex_target_equationt::SSA_stepst::const_iterator
30  it=equation.SSA_steps.begin();
31  it!=equation.SSA_steps.end(); it++)
32  {
33  if(it->is_assignment() &&
34  it->assignment_type==symex_targett::assignment_typet::STATE)
35  {
36  if(!prop_conv.l_get(it->guard_literal).is_false())
37  {
38  const typet &type=it->ssa_lhs.type();
39 
40  if(type!=bool_typet())
41  {
42  // we minimize the absolute value, if applicable
43  if(type.id()==ID_signedbv ||
44  type.id()==ID_fixedbv ||
45  type.id()==ID_floatbv)
46  {
47  abs_exprt abs_expr(it->ssa_lhs);
48  minimization_list.insert(abs_expr);
49  }
50  else
51  minimization_list.insert(it->ssa_lhs);
52  }
53  }
54  }
55 
56  // reached failed assertion?
57  if(it==failed)
58  break;
59  }
60 }
61 
62 symex_target_equationt::SSA_stepst::const_iterator
64  const prop_convt &prop_conv,
65  const symex_target_equationt &equation)
66 {
67  // find failed property
68 
69  for(symex_target_equationt::SSA_stepst::const_iterator
70  it=equation.SSA_steps.begin();
71  it!=equation.SSA_steps.end(); it++)
72  if(it->is_assert() &&
73  prop_conv.l_get(it->guard_literal).is_true() &&
74  prop_conv.l_get(it->cond_literal).is_false())
75  return it;
76 
77  assert(false);
78  return equation.SSA_steps.end();
79 }
80 
82  bv_cbmct &bv_cbmc,
83  const symex_target_equationt &equation,
84  const namespacet &ns)
85 {
86  // find failed property
87 
88  failed=get_failed_property(bv_cbmc, equation);
89 
90  // lock the failed assertion
91  bv_cbmc.set_to(literal_exprt(failed->cond_literal), false);
92 
93  {
94  bv_cbmc.status() << "Beautifying counterexample (guards)"
95  << messaget::eom;
96 
97  // compute weights for guards
98  typedef std::map<literalt, unsigned> guard_countt;
99  guard_countt guard_count;
100 
101  for(symex_target_equationt::SSA_stepst::const_iterator
102  it=equation.SSA_steps.begin();
103  it!=equation.SSA_steps.end(); it++)
104  {
105  if(it->is_assignment() &&
106  it->assignment_type!=symex_targett::assignment_typet::HIDDEN)
107  {
108  if(!it->guard_literal.is_constant())
109  guard_count[it->guard_literal]++;
110  }
111 
112  // reached failed assertion?
113  if(it==failed)
114  break;
115  }
116 
117  // give to propositional minimizer
118  prop_minimizet prop_minimize(bv_cbmc);
119  prop_minimize.set_message_handler(bv_cbmc.get_message_handler());
120 
121  for(const auto &g : guard_count)
122  prop_minimize.objective(g.first, g.second);
123 
124  // minimize
125  prop_minimize();
126  }
127 
128  {
129  bv_cbmc.status() << "Beautifying counterexample (values)"
130  << messaget::eom;
131 
132  // get symbols we care about
133  minimization_listt minimization_list;
134 
135  get_minimization_list(bv_cbmc, equation, minimization_list);
136 
137  // minimize
138  bv_minimizet bv_minimize(bv_cbmc);
139  bv_minimize.set_message_handler(bv_cbmc.get_message_handler());
140  bv_minimize(minimization_list);
141  }
142 }
The type of an expression.
Definition: type.h:20
bool is_false() const
Definition: threeval.h:26
Symbol table entry.
mstreamt & status()
Definition: message.h:238
void objective(const literalt condition, const weightt weight=1)
Add an objective.
Definition: minimize.cpp:19
SAT Minimizer.
The proper Booleans.
Definition: std_types.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
symex_target_equationt::SSA_stepst::const_iterator failed
const irep_idt & id() const
Definition: irep.h:189
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
bool is_true() const
Definition: threeval.h:25
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Definition: message.h:127
absolute value
Definition: std_expr.h:300
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
Definition: boolbv.cpp:621
Counterexample Beautification.