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 }
bv_refinementt::configt::output_xml
bool output_xml
Definition: bv_refinement.h:24
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
propt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: prop.h:108
propt::set_assumptions
virtual void set_assumptions(const bvt &)
Definition: prop.h:85
propt::solver_text
virtual const std::string solver_text()=0
bvt
std::vector< literalt > bvt
Definition: literal.h:200
messaget::status
mstreamt & status() const
Definition: message.h:401
bv_refinementt::arrays_overapproximated
void arrays_overapproximated()
check whether counterexample is spurious
Definition: refine_arrays.cpp:37
propt::resultt::P_UNSATISFIABLE
@ P_UNSATISFIABLE
bv_refinementt::infot
Definition: bv_refinement.h:33
bv_refinement.h
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
bv_refinementt::check_SAT
void check_SAT()
Definition: bv_refinement_loop.cpp:113
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
bv_refinementt::parent_assumptions
bvt parent_assumptions
Definition: bv_refinement.h:110
bv_refinementt::bv_refinementt
bv_refinementt(const infot &info)
Definition: bv_refinement_loop.cpp:13
propt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop.h:86
xml.h
bv_refinementt::approximations
std::list< approximationt > approximations
Definition: bv_refinement.h:109
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
bv_refinementt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: bv_refinement_loop.cpp:131
bv_refinementt::dec_solve
decision_proceduret::resultt dec_solve() override
Definition: bv_refinement_loop.cpp:24
messaget::result
mstreamt & result() const
Definition: message.h:396
bv_refinementt::approximationt
Definition: bv_refinement.h:63
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
bv_pointerst
Definition: bv_pointers.h:17
decision_proceduret::resultt::D_ERROR
@ D_ERROR
bv_refinementt::check_UNSAT
void check_UNSAT()
Definition: bv_refinement_loop.cpp:123
propt::resultt
resultt
Definition: prop.h:96
bv_refinementt::progress
bool progress
Definition: bv_refinement.h:108
xmlt
Definition: xml.h:18
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
bv_refinementt::prop_solve
resultt prop_solve()
Definition: bv_refinement_loop.cpp:84
bv_refinementt::config_
configt config_
Definition: bv_refinement.h:113
propt::prop_solve
virtual resultt prop_solve()=0
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:78
messaget::debug
mstreamt & debug() const
Definition: message.h:416
xmlt::data
std::string data
Definition: xml.h:30
bv_pointerst::post_process
void post_process() override
Definition: bv_pointers.cpp:827
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152