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 46 of file cover_goals.h.
|
protected |
Definition at line 94 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 68 of file cover_goals.h.
References goals.
Referenced by bmc_all_propertiest::operator()(), and bmc_covert::operator()().
|
private |
Build clause.
Definition at line 43 of file cover_goals.cpp.
References disjunction(), goals, prop_conv, decision_proceduret::set_to_true(), and cover_goalst::goalt::UNKNOWN.
Referenced by operator()().
|
private |
Build clause.
Definition at line 62 of file cover_goals.cpp.
References goals, prop_conv, and prop_convt::set_frozen().
Referenced by operator()().
|
inline |
Definition at line 56 of file cover_goals.h.
References _iterations.
Referenced by bmc_covert::operator()(), and bmc_all_propertiest::report().
|
private |
Mark goals that are covered.
Definition at line 23 of file cover_goals.cpp.
References _number_covered, cover_goalst::goalt::COVERED, goals, tvt::is_true(), prop_convt::l_get(), observers, prop_conv, and cover_goalst::goalt::UNKNOWN.
Referenced by operator()().
|
inline |
Definition at line 51 of file cover_goals.h.
References _number_covered.
Referenced by bmc_all_propertiest::operator()(), operator()(), bmc_all_propertiest::report(), and fault_localizationt::report().
decision_proceduret::resultt cover_goalst::operator() | ( | void | ) |
Try to cover all goals.
Definition at line 73 of file cover_goals.cpp.
References _iterations, _number_covered, constraint(), decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, decision_proceduret::dec_solve(), messaget::eom(), messaget::error(), freeze_goal_variables(), mark(), number_covered(), prop_conv, and size().
|
inline |
Definition at line 84 of file cover_goals.h.
References observers.
Referenced by bmc_all_propertiest::operator()(), and bmc_covert::operator()().
|
inline |
Definition at line 61 of file cover_goals.h.
References goals.
Referenced by operator()(), bmc_covert::operator()(), and bmc_all_propertiest::report().
|
protected |
Definition at line 91 of file cover_goals.h.
Referenced by iterations(), and operator()().
|
protected |
Definition at line 90 of file cover_goals.h.
Referenced by mark(), number_covered(), and operator()().
goalst cover_goalst::goals |
Definition at line 47 of file cover_goals.h.
Referenced by add(), constraint(), freeze_goal_variables(), mark(), and size().
|
protected |
Definition at line 95 of file cover_goals.h.
Referenced by mark(), and register_observer().
|
protected |
Definition at line 92 of file cover_goals.h.
Referenced by constraint(), freeze_goal_variables(), mark(), and operator()().