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  prop_conv(_prop_conv)
26  {
27  }
28 
29  virtual ~cover_goalst();
30 
31  // returns result of last run on success
33 
34  // the goals
35 
36  struct goalt
37  {
40 
41  goalt():status(statust::UNKNOWN)
42  {
43  }
44  };
45 
46  typedef std::list<goalt> goalst;
48 
49  // statistics
50 
51  std::size_t number_covered() const
52  {
53  return _number_covered;
54  }
55 
56  unsigned iterations() const
57  {
58  return _iterations;
59  }
60 
62  {
63  return goals.size();
64  }
65 
66  // managing the goals
67 
68  void add(const literalt condition)
69  {
70  goals.push_back(goalt());
71  goals.back().condition=condition;
72  }
73 
74  // register an observer if you want to be told
75  // about satisfying assignments
76 
77  class observert
78  {
79  public:
80  virtual void goal_covered(const goalt &) { }
81  virtual void satisfying_assignment() { }
82  };
83 
85  {
86  observers.push_back(&o);
87  }
88 
89 protected:
90  std::size_t _number_covered;
91  unsigned _iterations;
93 
94  typedef std::vector<observert *> observerst;
96 
97 private:
98  void mark();
99  void constraint();
100  void freeze_goal_variables();
101 };
102 
103 #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H
std::list< goalt > goalst
Definition: cover_goals.h:46
unsignedbv_typet size_type()
Definition: c_types.cpp:57
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:81
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:90
unsigned _iterations
Definition: cover_goals.h:91
std::size_t number_covered() const
Definition: cover_goals.h:51
void add(const literalt condition)
Definition: cover_goals.h:68
unsigned iterations() const
Definition: cover_goals.h:56
goalst goals
Definition: cover_goals.h:47
virtual ~cover_goalst()
Definition: cover_goals.cpp:18
observerst observers
Definition: cover_goals.h:95
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
std::vector< observert * > observerst
Definition: cover_goals.h:94
enum cover_goalst::goalt::statust status
prop_convt & prop_conv
Definition: cover_goals.h:92
void register_observer(observert &o)
Definition: cover_goals.h:84
goalst::size_type size() const
Definition: cover_goals.h:61
virtual void goal_covered(const goalt &)
Definition: cover_goals.h:80