cprover
|
Try to cover some given set of goals incrementally. More...
#include <cover_goals.h>
Classes | |
struct | goalt |
class | observert |
Public Types | |
typedef std::list< goalt > | goalst |
Public Member Functions | |
cover_goalst (prop_convt &_prop_conv) | |
virtual | ~cover_goalst () |
decision_proceduret::resultt | operator() () |
Try to cover all goals. More... | |
std::size_t | number_covered () const |
unsigned | iterations () const |
goalst::size_type | size () const |
void | add (const literalt condition) |
void | register_observer (observert &o) |
Public Attributes | |
goalst | goals |
Protected Types | |
typedef std::vector< observert * > | observerst |
Protected Attributes | |
std::size_t | _number_covered |
unsigned | _iterations |
prop_convt & | prop_conv |
observerst | observers |
Private Member Functions | |
void | mark () |
Mark goals that are covered. More... | |
void | constraint () |
Build clause. More... | |
void | freeze_goal_variables () |
Build clause. More... | |
Additional Inherited Members |
Try to cover some given set of goals incrementally.
This can be seen as a heuristic variant of SAT-based set-cover. No minimality guarantee.
Definition at line 21 of file cover_goals.h.
typedef std::list<goalt> cover_goalst::goalst |
Definition at line 48 of file cover_goals.h.
|
protected |
Definition at line 96 of file cover_goals.h.
|
inlineexplicit |
Definition at line 24 of file cover_goals.h.
|
virtual |
Definition at line 18 of file cover_goals.cpp.
|
inline |
Definition at line 70 of file cover_goals.h.
|
private |
Build clause.
Definition at line 43 of file cover_goals.cpp.
|
private |
Build clause.
Definition at line 62 of file cover_goals.cpp.
|
inline |
Definition at line 58 of file cover_goals.h.
|
private |
Mark goals that are covered.
Definition at line 23 of file cover_goals.cpp.
|
inline |
Definition at line 53 of file cover_goals.h.
decision_proceduret::resultt cover_goalst::operator() | ( | ) |
Try to cover all goals.
Definition at line 73 of file cover_goals.cpp.
|
inline |
Definition at line 86 of file cover_goals.h.
|
inline |
Definition at line 63 of file cover_goals.h.
|
protected |
Definition at line 93 of file cover_goals.h.
|
protected |
Definition at line 92 of file cover_goals.h.
goalst cover_goalst::goals |
Definition at line 49 of file cover_goals.h.
|
protected |
Definition at line 97 of file cover_goals.h.
|
protected |
Definition at line 94 of file cover_goals.h.