CBMC
Classes | Public Types | Public Member Functions | Public Attributes | Protected Types | Protected Attributes | Private Member Functions | List of all members
cover_goalst Class Reference

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

#include <cover_goals.h>

+ Collaboration diagram for cover_goalst:

Classes

struct  goalt
 
class  observert
 

Public Types

typedef std::list< goalt > goalst
 

Public Member Functions

 cover_goalst (decision_proceduret &_decision_procedure)
 
virtual ~cover_goalst ()
 
decision_proceduret::resultt operator() (message_handlert &)
 Try to cover all goals. More...
 
std::size_t number_covered () const
 
unsigned iterations () const
 
goalst::size_type size () const
 
void add (exprt 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
 
decision_proceduret & decision_procedure
 
observerst observers
 

Private Member Functions

void mark ()
 Mark goals that are covered. More...
 
void constraint ()
 Build clause. More...
 

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 25 of file cover_goals.h.

Member Typedef Documentation

◆ goalst

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

Definition at line 53 of file cover_goals.h.

◆ observerst

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

Definition at line 100 of file cover_goals.h.

Constructor & Destructor Documentation

◆ cover_goalst()

cover_goalst::cover_goalst ( decision_proceduret &  _decision_procedure)
inlineexplicit

Definition at line 28 of file cover_goals.h.

◆ ~cover_goalst()

cover_goalst::~cover_goalst ( )
virtual

Definition at line 17 of file cover_goals.cpp.

Member Function Documentation

◆ add()

void cover_goalst::add ( exprt  condition)
inline

Definition at line 75 of file cover_goals.h.

◆ constraint()

void cover_goalst::constraint ( )
private

Build clause.

Definition at line 43 of file cover_goals.cpp.

◆ iterations()

unsigned cover_goalst::iterations ( ) const
inline

Definition at line 63 of file cover_goals.h.

◆ mark()

void cover_goalst::mark ( )
private

Mark goals that are covered.

Definition at line 22 of file cover_goals.cpp.

◆ number_covered()

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

Definition at line 58 of file cover_goals.h.

◆ operator()()

decision_proceduret::resultt cover_goalst::operator() ( message_handlert &  message_handler)

Try to cover all goals.

Definition at line 59 of file cover_goals.cpp.

◆ register_observer()

void cover_goalst::register_observer ( observert &  o)
inline

Definition at line 90 of file cover_goals.h.

◆ size()

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

Definition at line 68 of file cover_goals.h.

Member Data Documentation

◆ _iterations

unsigned cover_goalst::_iterations
protected

Definition at line 97 of file cover_goals.h.

◆ _number_covered

std::size_t cover_goalst::_number_covered
protected

Definition at line 96 of file cover_goals.h.

◆ decision_procedure

decision_proceduret& cover_goalst::decision_procedure
protected

Definition at line 98 of file cover_goals.h.

◆ goals

goalst cover_goalst::goals

Definition at line 54 of file cover_goals.h.

◆ observers

observerst cover_goalst::observers
protected

Definition at line 101 of file cover_goals.h.

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