cprover
bv_refinement_loop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_refinement.h"
10 
11 #include <iostream>
12 
13 #include <util/xml.h>
14 
16  const namespacet &_ns, propt &_prop):
17  bv_pointerst(_ns, _prop),
18  max_node_refinement(5),
19  do_array_refinement(true),
20  do_arithmetic_refinement(true)
21 {
22  // check features we need
23  assert(prop.has_set_assumptions());
24  assert(prop.has_set_to());
25  assert(prop.has_is_in_conflict());
26 }
27 
29 {
30 }
31 
33 {
34  // do the usual post-processing
35  status() << "BV-Refinement: post-processing" << eom;
36  post_process();
37 
38  debug() << "Solving with " << prop.solver_text() << eom;
39 
40  unsigned iteration=0;
41 
42  // now enter the loop
43  while(true)
44  {
45  iteration++;
46 
47  status() << "BV-Refinement: iteration " << iteration << eom;
48 
49  // output the very same information in a structured fashion
51  {
52  xmlt xml("refinement-iteration");
53  xml.data=std::to_string(iteration);
54  std::cout << xml << '\n';
55  }
56 
57  switch(prop_solve())
58  {
60  check_SAT();
61  if(!progress)
62  {
63  status() << "BV-Refinement: got SAT, and it simulates => SAT" << eom;
64  status() << "Total iterations: " << iteration << eom;
66  }
67  else
68  status() << "BV-Refinement: got SAT, and it is spurious, refining"
69  << eom;
70  break;
71 
73  check_UNSAT();
74  if(!progress)
75  {
76  status() << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
77  << eom;
78  status() << "Total iterations: " << iteration << eom;
80  }
81  else
82  status() << "BV-Refinement: got UNSAT, and the proof fails, refining"
83  << eom;
84  break;
85 
86  default:
87  return resultt::D_ERROR;
88  }
89  }
90 }
91 
93 {
94  // this puts the underapproximations into effect
95  bvt assumptions=parent_assumptions;
96 
97  for(approximationst::const_iterator
98  a_it=approximations.begin();
99  a_it!=approximations.end();
100  a_it++)
101  {
102  assumptions.insert(
103  assumptions.end(),
104  a_it->over_assumptions.begin(), a_it->over_assumptions.end());
105  assumptions.insert(
106  assumptions.end(),
107  a_it->under_assumptions.begin(), a_it->under_assumptions.end());
108  }
109 
110  prop.set_assumptions(assumptions);
113 
114  switch(result)
115  {
118  default: return resultt::D_ERROR;
119  }
120 }
121 
123 {
124  progress=false;
125 
127 
128  for(approximationst::iterator
129  a_it=approximations.begin();
130  a_it!=approximations.end();
131  a_it++)
132  check_SAT(*a_it);
133 }
134 
136 {
137  progress=false;
138 
139  for(approximationst::iterator
140  a_it=approximations.begin();
141  a_it!=approximations.end();
142  a_it++)
143  check_UNSAT(*a_it);
144 }
145 
146 void bv_refinementt::set_to(const exprt &expr, bool value)
147 {
148  #if 0
149  unsigned prev=prop.no_variables();
150  SUB::set_to(expr, value);
151  unsigned n=prop.no_variables()-prev;
152  std::cout << n << " EEE " << expr.id() << "@" << expr.type().id();
153  forall_operands(it, expr)
154  std::cout << " " << it->id() << "@" << it->type().id();
155  if(expr.id()=="=" && expr.operands().size()==2)
156  forall_operands(it, expr.op1())
157  std::cout << " " << it->id() << "@" << it->type().id();
158  std::cout << '\n';
159  #else
160  SUB::set_to(expr, value);
161  #endif
162 }
163 
164 void bv_refinementt::set_assumptions(const bvt &_assumptions)
165 {
166  parent_assumptions=_assumptions;
167  prop.set_assumptions(_assumptions);
168 }
virtual decision_proceduret::resultt dec_solve()
mstreamt & result()
Definition: message.h:233
virtual bool has_is_in_conflict() const
Definition: prop.h:106
virtual const std::string solver_text()=0
mstreamt & status()
Definition: message.h:238
virtual void set_assumptions(const bvt &_assumptions)
virtual void set_to(const exprt &expr, bool value)
approximationst approximations
Definition: bv_refinement.h:83
typet & type()
Definition: expr.h:60
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
virtual bool has_set_assumptions() const
Definition: prop.h:84
const irep_idt & id() const
Definition: irep.h:189
virtual size_t no_variables() const =0
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
language_uit::uit ui
Definition: xml.h:18
#define forall_operands(it, expr)
Definition: expr.h:17
resultt
Definition: prop.h:94
bv_refinementt(const namespacet &_ns, propt &_prop)
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop.h:83
std::string data
Definition: xml.h:30
TO_BE_DOCUMENTED.
Definition: prop.h:22
void arrays_overapproximated()
check whether counterexample is spurious
void post_process() override
mstreamt & debug()
Definition: message.h:253
virtual void check_SAT()
Base class for all expressions.
Definition: expr.h:46
virtual bool has_set_to() const
Definition: prop.h:76
virtual resultt prop_solve()=0
mstreamt & progress()
Definition: message.h:248
Abstraction Refinement Loop.
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:621
operandst & operands()
Definition: expr.h:70
virtual void check_UNSAT()
std::vector< literalt > bvt
Definition: literal.h:197