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 <util/xml.h>
12 
14  bv_pointerst(*info.ns, *info.prop),
15  progress(false),
16  config_(info)
17 {
18  // check features we need
22 }
23 
25 {
26  // do the usual post-processing
27  status() << "BV-Refinement: post-processing" << eom;
28  post_process();
29 
30  debug() << "Solving with " << prop.solver_text() << eom;
31 
32  unsigned iteration=0;
33 
34  // now enter the loop
35  while(true)
36  {
37  iteration++;
38 
39  status() << "BV-Refinement: iteration " << iteration << eom;
40 
41  // output the very same information in a structured fashion
43  {
44  xmlt xml("refinement-iteration");
45  xml.data=std::to_string(iteration);
46  status() << xml << '\n';
47  }
48 
49  switch(prop_solve())
50  {
52  check_SAT();
53  if(!progress)
54  {
55  status() << "BV-Refinement: got SAT, and it simulates => SAT" << eom;
56  status() << "Total iterations: " << iteration << eom;
58  }
59  else
60  status() << "BV-Refinement: got SAT, and it is spurious, refining"
61  << eom;
62  break;
63 
65  check_UNSAT();
66  if(!progress)
67  {
68  status() << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
69  << eom;
70  status() << "Total iterations: " << iteration << eom;
72  }
73  else
74  status() << "BV-Refinement: got UNSAT, and the proof fails, refining"
75  << eom;
76  break;
77 
78  default:
79  return resultt::D_ERROR;
80  }
81  }
82 }
83 
85 {
86  // this puts the underapproximations into effect
87  bvt assumptions=parent_assumptions;
88 
89  for(const approximationt &approximation : approximations)
90  {
91  assumptions.insert(
92  assumptions.end(),
93  approximation.over_assumptions.begin(),
94  approximation.over_assumptions.end());
95  assumptions.insert(
96  assumptions.end(),
97  approximation.under_assumptions.begin(),
98  approximation.under_assumptions.end());
99  }
100 
101  prop.set_assumptions(assumptions);
104 
105  switch(result)
106  {
109  default: return resultt::D_ERROR;
110  }
111 }
112 
114 {
115  progress=false;
116 
118 
119  for(approximationt &approximation : this->approximations)
120  check_SAT(approximation);
121 }
122 
124 {
125  progress=false;
126 
127  for(approximationt &approximation : this->approximations)
128  check_UNSAT(approximation);
129 }
130 
131 void bv_refinementt::set_assumptions(const bvt &_assumptions)
132 {
133  parent_assumptions=_assumptions;
134  prop.set_assumptions(_assumptions);
135 }
void set_assumptions(const bvt &_assumptions) override
virtual bool has_is_in_conflict() const
Definition: prop.h:108
virtual const std::string solver_text()=0
mstreamt & progress() const
Definition: message.h:411
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::list< approximationt > approximations
virtual void set_assumptions(const bvt &)
Definition: prop.h:85
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
virtual bool has_set_assumptions() const
Definition: prop.h:86
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Definition: xml.h:18
resultt
Definition: prop.h:96
std::string data
Definition: xml.h:30
decision_proceduret::resultt dec_solve() override
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
static eomt eom
Definition: message.h:284
void post_process() override
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
virtual bool has_set_to() const
Definition: prop.h:78
virtual resultt prop_solve()=0
Abstraction Refinement Loop.
mstreamt & debug() const
Definition: message.h:416
std::vector< literalt > bvt
Definition: literal.h:200