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 
19 {
20 }
21 
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;
35 
36  // notify observers
37  for(const auto &o : observers)
38  o->goal_covered(g);
39  }
40 }
41 
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 
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 
74 {
76 
78 
79  // We use incremental solving, so need to freeze some variables
80  // to prevent them from being eliminated.
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  {
94  return dec_result;
95 
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  }
107  number_covered()<size());
108 
110 }
void mark()
Mark goals that are covered.
Definition: cover_goals.cpp:23
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
decision_proceduret::resultt operator()()
Try to cover all goals.
Definition: cover_goals.cpp:73
void constraint()
Build clause.
Definition: cover_goals.cpp:43
virtual resultt dec_solve()=0
void freeze_goal_variables()
Build clause.
Definition: cover_goals.cpp:62
std::size_t _number_covered
Definition: cover_goals.h:92
mstreamt & error() const
Definition: message.h:302
unsigned _iterations
Definition: cover_goals.h:93
std::size_t number_covered() const
Definition: cover_goals.h:53
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
bool is_true() const
Definition: threeval.h:25
std::vector< exprt > operandst
Definition: expr.h:45
virtual tvt l_get(literalt a) const =0
goalst goals
Definition: cover_goals.h:49
virtual ~cover_goalst()
Definition: cover_goals.cpp:18
void set_to_true(const exprt &expr)
Cover a set of goals incrementally.
observerst observers
Definition: cover_goals.h:97
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:24
prop_convt & prop_conv
Definition: cover_goals.h:94
goalst::size_type size() const
Definition: cover_goals.h:63