cprover
cover_goals.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Cover a set of goals incrementally
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
cover_goals.h
"
13
14
#include <
util/threeval.h
>
15
16
#include "
literal_expr.h
"
17
18
cover_goalst::~cover_goalst
()
19
{
20
}
21
23
void
cover_goalst::mark
()
24
{
25
// notify observers
26
for
(
const
auto
&o :
observers
)
27
o->satisfying_assignment();
28
29
for
(
auto
&g :
goals
)
30
if
(g.status==
goalt::statust::UNKNOWN
&&
31
prop_conv
.
l_get
(g.condition).
is_true
())
32
{
33
g.status=
goalt::statust::COVERED
;
34
_number_covered
++;
35
36
// notify observers
37
for
(
const
auto
&o :
observers
)
38
o->goal_covered(g);
39
}
40
}
41
43
void
cover_goalst::constraint
()
44
{
45
exprt::operandst
disjuncts;
46
47
// cover at least one unknown goal
48
49
for
(std::list<goalt>::const_iterator
50
g_it=
goals
.begin();
51
g_it!=
goals
.end();
52
g_it++)
53
if
(g_it->status==
goalt::statust::UNKNOWN
&&
54
!g_it->condition.is_false())
55
disjuncts.push_back(
literal_exprt
(g_it->condition));
56
57
// this is 'false' if there are no disjuncts
58
prop_conv
.
set_to_true
(
disjunction
(disjuncts));
59
}
60
62
void
cover_goalst::freeze_goal_variables
()
63
{
64
for
(std::list<goalt>::const_iterator
65
g_it=
goals
.begin();
66
g_it!=
goals
.end();
67
g_it++)
68
if
(!g_it->condition.is_constant())
69
prop_conv
.
set_frozen
(g_it->condition);
70
}
71
73
decision_proceduret::resultt
cover_goalst::operator()
()
74
{
75
_iterations
=
_number_covered
=0;
76
77
decision_proceduret::resultt
dec_result;
78
79
// We use incremental solving, so need to freeze some variables
80
// to prevent them from being eliminated.
81
freeze_goal_variables
();
82
83
do
84
{
85
// We want (at least) one of the remaining goals, please!
86
_iterations
++;
87
88
constraint
();
89
dec_result=
prop_conv
.
dec_solve
();
90
91
switch
(dec_result)
92
{
93
case
decision_proceduret::resultt::D_UNSATISFIABLE
:
// DONE
94
return
dec_result;
95
96
case
decision_proceduret::resultt::D_SATISFIABLE
:
97
// mark the goals we got, and notify observers
98
mark
();
99
break
;
100
101
default
:
102
error
() <<
"decision procedure has failed"
<<
eom
;
103
return
dec_result;
104
}
105
}
106
while
(dec_result==
decision_proceduret::resultt::D_SATISFIABLE
&&
107
number_covered
()<
size
());
108
109
return
decision_proceduret::resultt::D_SATISFIABLE
;
110
}
cover_goalst::~cover_goalst
virtual ~cover_goalst()
Definition:
cover_goals.cpp:18
cover_goalst::goals
goalst goals
Definition:
cover_goals.h:49
threeval.h
decision_proceduret::resultt::D_UNSATISFIABLE
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
Definition:
decision_procedure.h:40
cover_goalst::_number_covered
std::size_t _number_covered
Definition:
cover_goals.h:92
messaget::eom
static eomt eom
Definition:
message.h:284
cover_goalst::number_covered
std::size_t number_covered() const
Definition:
cover_goals.h:53
cover_goalst::operator()
decision_proceduret::resultt operator()()
Try to cover all goals.
Definition:
cover_goals.cpp:73
decision_proceduret::resultt::D_SATISFIABLE
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition:
std_expr.cpp:26
messaget::error
mstreamt & error() const
Definition:
message.h:386
cover_goalst::mark
void mark()
Mark goals that are covered.
Definition:
cover_goals.cpp:23
cover_goalst::constraint
void constraint()
Build clause.
Definition:
cover_goals.cpp:43
cover_goalst::observers
observerst observers
Definition:
cover_goals.h:97
cover_goalst::_iterations
unsigned _iterations
Definition:
cover_goals.h:93
literal_exprt
Definition:
literal_expr.h:17
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
cover_goalst::size
goalst::size_type size() const
Definition:
cover_goals.h:63
exprt::operandst
std::vector< exprt > operandst
Definition:
expr.h:57
cover_goalst::prop_conv
prop_convt & prop_conv
Definition:
cover_goals.h:94
cover_goalst::goalt::statust::UNKNOWN
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
decision_proceduret::resultt
resultt
Definition:
decision_procedure.h:47
cover_goalst::goalt::statust::COVERED
prop_convt::set_frozen
virtual void set_frozen(literalt a)
Definition:
prop_conv.cpp:24
cover_goalst::freeze_goal_variables
void freeze_goal_variables()
Build clause.
Definition:
cover_goals.cpp:62
cover_goals.h
literal_expr.h
tvt::is_true
bool is_true() const
Definition:
threeval.h:25
solvers
prop
cover_goals.cpp
Generated by
1.8.16