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 }
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