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  bv_pointerst(*info.ns, *info.prop),
17  progress(false),
18  config_(info)
19 {
20  // check features we need
24 }
25 
27 {
28  // do the usual post-processing
29  status() << "BV-Refinement: post-processing" << eom;
30  post_process();
31 
32  debug() << "Solving with " << prop.solver_text() << eom;
33 
34  unsigned iteration=0;
35 
36  // now enter the loop
37  while(true)
38  {
39  iteration++;
40 
41  status() << "BV-Refinement: iteration " << iteration << eom;
42 
43  // output the very same information in a structured fashion
45  {
46  xmlt xml("refinement-iteration");
47  xml.data=std::to_string(iteration);
48  status() << xml << '\n';
49  }
50 
51  switch(prop_solve())
52  {
54  check_SAT();
55  if(!progress)
56  {
57  status() << "BV-Refinement: got SAT, and it simulates => SAT" << eom;
58  status() << "Total iterations: " << iteration << eom;
60  }
61  else
62  status() << "BV-Refinement: got SAT, and it is spurious, refining"
63  << eom;
64  break;
65 
67  check_UNSAT();
68  if(!progress)
69  {
70  status() << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
71  << eom;
72  status() << "Total iterations: " << iteration << eom;
74  }
75  else
76  status() << "BV-Refinement: got UNSAT, and the proof fails, refining"
77  << eom;
78  break;
79 
80  default:
81  return resultt::D_ERROR;
82  }
83  }
84 }
85 
87 {
88  // this puts the underapproximations into effect
89  bvt assumptions=parent_assumptions;
90 
91  for(const approximationt &approximation : approximations)
92  {
93  assumptions.insert(
94  assumptions.end(),
95  approximation.over_assumptions.begin(),
96  approximation.over_assumptions.end());
97  assumptions.insert(
98  assumptions.end(),
99  approximation.under_assumptions.begin(),
100  approximation.under_assumptions.end());
101  }
102 
103  prop.set_assumptions(assumptions);
106 
107  switch(result)
108  {
111  default: return resultt::D_ERROR;
112  }
113 }
114 
116 {
117  progress=false;
118 
120 
121  for(approximationt &approximation : this->approximations)
122  check_SAT(approximation);
123 }
124 
126 {
127  progress=false;
128 
129  for(approximationt &approximation : this->approximations)
130  check_UNSAT(approximation);
131 }
132 
133 void bv_refinementt::set_assumptions(const bvt &_assumptions)
134 {
135  parent_assumptions=_assumptions;
136  prop.set_assumptions(_assumptions);
137 }
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:327
std::list< approximationt > approximations
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
virtual bool has_set_assumptions() const
Definition: prop.h:86
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
Definition: xml.h:18
ui_message_handlert::uit ui
Definition: bv_refinement.h:26
resultt
Definition: prop.h:96
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop.h:85
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)
void post_process() override
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
virtual bool has_set_to() const
Definition: prop.h:78
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual resultt prop_solve()=0
Abstraction Refinement Loop.
mstreamt & debug() const
Definition: message.h:332
std::vector< literalt > bvt
Definition: literal.h:200