cprover
cover_goalst Class Reference

Try to cover some given set of goals incrementally. More...

#include <cover_goals.h>

Inheritance diagram for cover_goalst:
[legend]
Collaboration diagram for cover_goalst:
[legend]

Classes

struct  goalt
 
class  observert
 

Public Types

typedef std::list< goaltgoalst
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

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 Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Public Attributes

goalst goals
 

Protected Types

typedef std::vector< observert * > observerst
 

Protected Attributes

std::size_t _number_covered
 
unsigned _iterations
 
prop_convtprop_conv
 
observerst observers
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

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.

Member Typedef Documentation

§ goalst

typedef std::list<goalt> cover_goalst::goalst

Definition at line 46 of file cover_goals.h.

§ observerst

typedef std::vector<observert *> cover_goalst::observerst
protected

Definition at line 94 of file cover_goals.h.

Constructor & Destructor Documentation

§ cover_goalst()

cover_goalst::cover_goalst ( prop_convt _prop_conv)
inlineexplicit

Definition at line 24 of file cover_goals.h.

References operator()(), and ~cover_goalst().

§ ~cover_goalst()

cover_goalst::~cover_goalst ( )
virtual

Definition at line 18 of file cover_goals.cpp.

Referenced by cover_goalst().

Member Function Documentation

§ add()

void cover_goalst::add ( const literalt  condition)
inline

§ constraint()

void cover_goalst::constraint ( )
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()().

§ freeze_goal_variables()

void cover_goalst::freeze_goal_variables ( )
private

Build clause.

Definition at line 62 of file cover_goals.cpp.

References goals, prop_conv, and prop_convt::set_frozen().

Referenced by operator()().

§ iterations()

unsigned cover_goalst::iterations ( ) const
inline

Definition at line 56 of file cover_goals.h.

References _iterations.

Referenced by bmc_covert::operator()(), and bmc_all_propertiest::report().

§ mark()

void cover_goalst::mark ( )
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()().

§ number_covered()

std::size_t cover_goalst::number_covered ( ) const
inline

§ operator()()

§ register_observer()

void cover_goalst::register_observer ( observert o)
inline

Definition at line 84 of file cover_goals.h.

References observers.

Referenced by bmc_all_propertiest::operator()(), and bmc_covert::operator()().

§ size()

goalst::size_type cover_goalst::size ( ) const
inline

Definition at line 61 of file cover_goals.h.

Referenced by operator()(), bmc_covert::operator()(), and bmc_all_propertiest::report().

Member Data Documentation

§ _iterations

unsigned cover_goalst::_iterations
protected

Definition at line 91 of file cover_goals.h.

Referenced by iterations(), and operator()().

§ _number_covered

std::size_t cover_goalst::_number_covered
protected

Definition at line 90 of file cover_goals.h.

Referenced by mark(), number_covered(), and operator()().

§ goals

goalst cover_goalst::goals

Definition at line 47 of file cover_goals.h.

Referenced by constraint(), freeze_goal_variables(), and mark().

§ observers

observerst cover_goalst::observers
protected

Definition at line 95 of file cover_goals.h.

Referenced by mark(), and register_observer().

§ prop_conv

prop_convt& cover_goalst::prop_conv
protected

Definition at line 92 of file cover_goals.h.

Referenced by constraint(), freeze_goal_variables(), mark(), and operator()().


The documentation for this class was generated from the following files: