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 
78  return equation.SSA_steps.end();
79 }
80 
82  bv_cbmct &bv_cbmc,
83  const symex_target_equationt &equation)
84 {
85  // find failed property
86 
87  failed=get_failed_property(bv_cbmc, equation);
88 
89  // lock the failed assertion
90  bv_cbmc.set_to(literal_exprt(failed->cond_literal), false);
91 
92  {
93  bv_cbmc.status() << "Beautifying counterexample (guards)"
94  << messaget::eom;
95 
96  // compute weights for guards
97  typedef std::map<literalt, unsigned> guard_countt;
98  guard_countt guard_count;
99 
100  for(symex_target_equationt::SSA_stepst::const_iterator
101  it=equation.SSA_steps.begin();
102  it!=equation.SSA_steps.end(); it++)
103  {
104  if(it->is_assignment() &&
105  it->assignment_type!=symex_targett::assignment_typet::HIDDEN)
106  {
107  if(!it->guard_literal.is_constant())
108  guard_count[it->guard_literal]++;
109  }
110 
111  // reached failed assertion?
112  if(it==failed)
113  break;
114  }
115 
116  // give to propositional minimizer
117  prop_minimizet prop_minimize(bv_cbmc);
118  prop_minimize.set_message_handler(bv_cbmc.get_message_handler());
119 
120  for(const auto &g : guard_count)
121  prop_minimize.objective(g.first, g.second);
122 
123  // minimize
124  prop_minimize();
125  }
126 
127  {
128  bv_cbmc.status() << "Beautifying counterexample (values)"
129  << messaget::eom;
130 
131  // get symbols we care about
132  minimization_listt minimization_list;
133 
134  get_minimization_list(bv_cbmc, equation, minimization_list);
135 
136  // minimize
137  bv_minimizet bv_minimize(bv_cbmc);
138  bv_minimize.set_message_handler(bv_cbmc.get_message_handler());
139  bv_minimize(minimization_list);
140  }
141 }
The type of an expression.
Definition: type.h:22
bool is_false() const
Definition: threeval.h:26
Symbol table entry.
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:34
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
symex_target_equationt::SSA_stepst::const_iterator failed
const irep_idt & id() const
Definition: irep.h:259
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
void operator()(bv_cbmct &bv_cbmc, const symex_target_equationt &equation)
API to expression classes.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
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:153
mstreamt & status() const
Definition: message.h:317
absolute value
Definition: std_expr.h:388
#define UNREACHABLE
Definition: invariant.h:271
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:601
Counterexample Beautification.