cprover
cover_goals.h
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 #ifndef CPROVER_SOLVERS_PROP_COVER_GOALS_H
13 #define CPROVER_SOLVERS_PROP_COVER_GOALS_H
14 
15 #include <util/message.h>
16 
17 #include "prop_conv.h"
18 
21 class cover_goalst:public messaget
22 {
23 public:
24  explicit cover_goalst(prop_convt &_prop_conv):
25  _number_covered(0),
26  _iterations(0),
27  prop_conv(_prop_conv)
28  {
29  }
30 
31  virtual ~cover_goalst();
32 
33  // returns result of last run on success
35 
36  // the goals
37 
38  struct goalt
39  {
42 
44  {
45  }
46  };
47 
48  typedef std::list<goalt> goalst;
50 
51  // statistics
52 
53  std::size_t number_covered() const
54  {
55  return _number_covered;
56  }
57 
58  unsigned iterations() const
59  {
60  return _iterations;
61  }
62 
64  {
65  return goals.size();
66  }
67 
68  // managing the goals
69 
70  void add(const literalt condition)
71  {
72  goals.push_back(goalt());
73  goals.back().condition=condition;
74  }
75 
76  // register an observer if you want to be told
77  // about satisfying assignments
78 
79  class observert
80  {
81  public:
82  virtual void goal_covered(const goalt &) { }
83  virtual void satisfying_assignment() { }
84  };
85 
87  {
88  observers.push_back(&o);
89  }
90 
91 protected:
92  std::size_t _number_covered;
93  unsigned _iterations;
95 
96  typedef std::vector<observert *> observerst;
98 
99 private:
100  void mark();
101  void constraint();
102  void freeze_goal_variables();
103 };
104 
105 #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H
std::list< goalt > goalst
Definition: cover_goals.h:48
unsignedbv_typet size_type()
Definition: c_types.cpp:58
void mark()
Mark goals that are covered.
Definition: cover_goals.cpp:23
decision_proceduret::resultt operator()()
Try to cover all goals.
Definition: cover_goals.cpp:73
virtual void satisfying_assignment()
Definition: cover_goals.h:83
void constraint()
Build clause.
Definition: cover_goals.cpp:43
void freeze_goal_variables()
Build clause.
Definition: cover_goals.cpp:62
cover_goalst(prop_convt &_prop_conv)
Definition: cover_goals.h:24
std::size_t _number_covered
Definition: cover_goals.h:92
unsigned _iterations
Definition: cover_goals.h:93
std::size_t number_covered() const
Definition: cover_goals.h:53
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
void add(const literalt condition)
Definition: cover_goals.h:70
unsigned iterations() const
Definition: cover_goals.h:58
goalst goals
Definition: cover_goals.h:49
virtual ~cover_goalst()
Definition: cover_goals.cpp:18
observerst observers
Definition: cover_goals.h:97
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
std::vector< observert * > observerst
Definition: cover_goals.h:96
enum cover_goalst::goalt::statust status
prop_convt & prop_conv
Definition: cover_goals.h:94
void register_observer(observert &o)
Definition: cover_goals.h:86
goalst::size_type size() const
Definition: cover_goals.h:63
virtual void goal_covered(const goalt &)
Definition: cover_goals.h:82