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/message.h>
15 #include <util/threeval.h>
16 
17 #include "literal_expr.h"
18 
20 {
21 }
22 
25 {
26  // notify observers
27  for(const auto &o : observers)
28  o->satisfying_assignment();
29 
30  for(auto &g : goals)
31  if(
32  g.status == goalt::statust::UNKNOWN &&
33  decision_procedure.get(g.condition).is_true())
34  {
35  g.status=goalt::statust::COVERED;
37 
38  // notify observers
39  for(const auto &o : observers)
40  o->goal_covered(g);
41  }
42 }
43 
46 {
47  exprt::operandst disjuncts;
48 
49  // cover at least one unknown goal
50 
51  for(const auto &g : goals)
52  if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false())
53  disjuncts.push_back(g.condition);
54 
55  // this is 'false' if there are no disjuncts
57 }
58 
61 operator()(message_handlert &message_handler)
62 {
64 
66 
67  do
68  {
69  // We want (at least) one of the remaining goals, please!
70  _iterations++;
71 
72  constraint();
73  dec_result = decision_procedure();
74 
75  switch(dec_result)
76  {
78  return dec_result;
79 
81  // mark the goals we got, and notify observers
82  mark();
83  break;
84 
86  {
87  messaget log(message_handler);
88  log.error() << "decision procedure has failed" << messaget::eom;
89  return dec_result;
90  }
91  }
92  }
94  number_covered()<size());
95 
97 }
observerst observers
Definition: cover_goals.h:101
virtual ~cover_goalst()
Definition: cover_goals.cpp:19
std::size_t _number_covered
Definition: cover_goals.h:96
unsigned _iterations
Definition: cover_goals.h:97
std::size_t number_covered() const
Definition: cover_goals.h:58
goalst::size_type size() const
Definition: cover_goals.h:68
decision_proceduret::resultt operator()(message_handlert &)
Try to cover all goals.
Definition: cover_goals.cpp:61
void constraint()
Build clause.
Definition: cover_goals.cpp:45
void mark()
Mark goals that are covered.
Definition: cover_goals.cpp:24
decision_proceduret & decision_procedure
Definition: cover_goals.h:98
goalst goals
Definition: cover_goals.h:54
resultt
Result of running the decision procedure.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
Cover a set of goals incrementally.
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:29