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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
cover_goalst::~cover_goalst
virtual ~cover_goalst()
Definition: cover_goals.cpp:19
cover_goalst::goals
goalst goals
Definition: cover_goals.h:54
cover_goalst::operator()
decision_proceduret::resultt operator()(message_handlert &)
Try to cover all goals.
Definition: cover_goals.cpp:61
threeval.h
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Definition: decision_procedure.cpp:23
cover_goalst::_number_covered
std::size_t _number_covered
Definition: cover_goals.h:96
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
cover_goalst::number_covered
std::size_t number_covered() const
Definition: cover_goals.h:58
decision_proceduret::resultt::D_SATISFIABLE
@ 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:29
messaget::error
mstreamt & error() const
Definition: message.h:399
cover_goalst::mark
void mark()
Mark goals that are covered.
Definition: cover_goals.cpp:24
cover_goalst::constraint
void constraint()
Build clause.
Definition: cover_goals.cpp:45
cover_goalst::observers
observerst observers
Definition: cover_goals.h:101
cover_goalst::_iterations
unsigned _iterations
Definition: cover_goals.h:97
cover_goalst::size
goalst::size_type size() const
Definition: cover_goals.h:68
decision_proceduret::resultt::D_ERROR
@ D_ERROR
cover_goalst::decision_procedure
decision_proceduret & decision_procedure
Definition: cover_goals.h:98
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
cover_goalst::goalt::statust::UNKNOWN
@ UNKNOWN
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
cover_goalst::goalt::statust::COVERED
@ COVERED
message.h
cover_goals.h
Cover a set of goals incrementally.
literal_expr.h