cprover
Loading...
Searching...
No Matches
bv_refinement_loop.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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, *info.message_handler),
15 progress(false),
16 config_(info)
17{
18 // check features we need
19 PRECONDITION(prop.has_assumptions());
20 PRECONDITION(prop.has_set_to());
21 PRECONDITION(prop.has_is_in_conflict());
22}
23
25{
26 // do the usual post-processing
27 log.progress() << "BV-Refinement: post-processing" << messaget::eom;
29
30 log.debug() << "Solving with " << prop.solver_text() << messaget::eom;
31
32 unsigned iteration=0;
33
34 // now enter the loop
35 while(true)
36 {
37 iteration++;
38
39 log.progress() << "BV-Refinement: iteration " << iteration << messaget::eom;
40
41 // output the very same information in a structured fashion
42 if(config_.output_xml)
43 {
44 xmlt xml("refinement-iteration");
45 xml.data=std::to_string(iteration);
46 log.status() << xml << '\n';
47 }
48
49 switch(prop_solve())
50 {
52 check_SAT();
53 if(!progress)
54 {
55 log.status() << "BV-Refinement: got SAT, and it simulates => SAT"
57 log.statistics() << "Total iterations: " << iteration << messaget::eom;
59 }
60 else
61 log.progress() << "BV-Refinement: got SAT, and it is spurious, refining"
63 break;
64
67 if(!progress)
68 {
69 log.status()
70 << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
72 log.statistics() << "Total iterations: " << iteration << messaget::eom;
74 }
75 else
76 log.progress()
77 << "BV-Refinement: got UNSAT, and the proof fails, refining"
79 break;
80
82 return resultt::D_ERROR;
83 }
84 }
85}
86
88{
89 // this puts the underapproximations into effect
90 std::vector<exprt> assumptions;
91
92 for(const approximationt &approximation : approximations)
93 {
94 assumptions.insert(
95 assumptions.end(),
96 approximation.over_assumptions.begin(),
97 approximation.over_assumptions.end());
98 assumptions.insert(
99 assumptions.end(),
100 approximation.under_assumptions.begin(),
101 approximation.under_assumptions.end());
102 }
103
104 push(assumptions);
105 propt::resultt result = prop.prop_solve(assumption_stack);
106 pop();
107
108 // clang-format off
109 switch(result)
110 {
114 }
115 // clang-format off
116
118}
119
121{
122 progress=false;
123
125
126 // get values before modifying the formula
127 for(approximationt &approximation : this->approximations)
128 get_values(approximation);
129
130 for(approximationt &approximation : this->approximations)
131 check_SAT(approximation);
132}
133
135{
136 progress=false;
137
138 for(approximationt &approximation : this->approximations)
139 check_UNSAT(approximation);
140}
Abstraction Refinement Loop.
const namespacet & ns
Definition arrays.h:56
message_handlert & message_handler
Definition arrays.h:58
messaget log
Definition arrays.h:57
void finish_eager_conversion() override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
decision_proceduret::resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
bv_refinementt(const infot &info)
void arrays_overapproximated()
check whether counterexample is spurious
void get_values(approximationt &approximation)
std::list< approximationt > approximations
resultt
Result of running the decision procedure.
Base class for all expressions.
Definition expr.h:56
static eomt eom
Definition message.h:289
void pop() override
Pop whatever is on top of the stack.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
bvt assumption_stack
Assumptions on the stack.
resultt
Definition prop.h:101
@ P_UNSATISFIABLE
Definition prop.h:101
@ P_SATISFIABLE
Definition prop.h:101
Definition xml.h:21
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463