mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter > Class Template Reference

An enumerator algorithm that generates solutions of a condition. More...

#include <enumerator_with_iterator.h>

Inheritance diagram for mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >:

Classes
struct	always_false

Public Member Functions
	enumerator_algorithm_without_callback (const Rewriter &R, const data::data_specification &dataspec, const DataRewriter &r, enumerator_identifier_generator &id_generator, std::size_t max_count=(std::numeric_limits< std::size_t >::max)(), bool throw_exceptions=false)
	enumerator_algorithm_without_callback (const enumerator_algorithm< Rewriter, DataRewriter > &)=delete
template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter >
void	step (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, Filter accept) const
	Enumerates the front element of the todo list P.
template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter >
std::size_t	next (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, Filter accept) const
	Enumerates the front elements of the todo list P until a solution has been found, or until P is empty.
bool	throw_exceptions () const
Public Member Functions inherited from mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >
	enumerator_algorithm (const Rewriter &R_, const data::data_specification &dataspec_, const DataRewriter &datar_, enumerator_identifier_generator &id_generator_, bool accept_solutions_with_variables, std::size_t max_count=(std::numeric_limits< std::size_t >::max)())
	enumerator_algorithm (const enumerator_algorithm< Rewriter, DataRewriter > &)=delete
	~enumerator_algorithm ()
void	reset_id_generator ()
template<typename EnumeratorListElement , typename MutableSubstitution , typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>
bool	enumerate_front (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
	Enumerates the front element of the todo list P. The enumeration is interrupted when report_solution returns true for the reported solution.
template<typename EnumeratorListElement , typename MutableSubstitution , typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>
std::size_t	enumerate_all (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
	Enumerates until P is empty. Solutions are reported using the callback function report_solution. The enumeration is interrupted when report_solution returns true for the reported solution.
template<typename EnumeratorListElement , typename MutableSubstitution , typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>
std::size_t	enumerate (const EnumeratorListElement &p, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
	Enumerates the element p. Solutions are reported using the callback function report_solution. The enumeration is interrupted when report_solution returns true for the reported solution.
template<typename EnumeratorListElement , typename MutableSubstitution , typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>
std::size_t	enumerate (const variable_list &vars, const typename EnumeratorListElement::expression_type &cond, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
	Enumerates the variables v for condition c. Solutions are reported using the callback function report_solution. The enumeration is interrupted when report_solution returns true for the reported solution.
std::size_t	max_count () const

Protected Types
typedef enumerator_algorithm< Rewriter, DataRewriter >	super

Protected Member Functions
template<typename EnumeratorListElement >
void	cannot_enumerate (EnumeratorListElement &e, const std::string &msg) const
template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter , typename Expression >
void	add_element (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const Expression &phi, const EnumeratorListElement &p, const data::variable &v, const data::data_expression &e) const
template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter , typename Expression >
void	add_element (enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const data::variable_list &added_variables, const Expression &phi, const EnumeratorListElement &p, const data::variable &v, const data::data_expression &e) const
template<typename MutableSubstitution , typename Filter , typename Expression >
void	add_element (enumerator_queue< enumerator_list_element< Expression > > &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const data::variable_list &added_variables, const Expression &phi, const enumerator_list_element< Expression > &p, const data::variable &v, const data::data_expression &e) const
Protected Member Functions inherited from mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >
std::string	print (const data::variable &x) const
template<typename Expression , typename MutableSubstitution >
Expression	rewrite (const Expression &phi, MutableSubstitution &sigma) const
template<typename Expression , typename MutableSubstitution >
void	rewrite (Expression &result, const Expression &phi, MutableSubstitution &sigma) const

Protected Attributes
bool	m_throw_exceptions
	throw_exceptions If true, an exception is thrown when the enumeration is aborted.
Protected Attributes inherited from mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >
const Rewriter &	R
const data::data_specification &	dataspec
	A data specification.
const DataRewriter &	r
enumerator_identifier_generator &	id_generator
std::size_t	m_max_count
	max_count The enumeration is aborted after max_count iterations
bool	m_accept_solutions_with_variables
	If true, solutions with a non-empty list of variables may be reported.

Detailed Description

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>
class mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >

An enumerator algorithm that generates solutions of a condition.

Definition at line 40 of file enumerator_with_iterator.h.

Member Typedef Documentation

super

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

typedef enumerator_algorithm<Rewriter, DataRewriter> mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::super

protected

Definition at line 43 of file enumerator_with_iterator.h.

Constructor & Destructor Documentation

enumerator_algorithm_without_callback() [1/2]

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::enumerator_algorithm_without_callback ( const Rewriter &  R, const data::data_specification &  dataspec, const DataRewriter &  r, enumerator_identifier_generator &  id_generator, std::size_t  max_count = (std::numeric_limits<std::size_t>::max)(), bool  throw_exceptions = false  )

inline

Definition at line 133 of file enumerator_with_iterator.h.

enumerator_algorithm_without_callback() [2/2]

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::enumerator_algorithm_without_callback ( const enumerator_algorithm< Rewriter, DataRewriter > &  )

delete

Member Function Documentation

add_element() [1/3]

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename MutableSubstitution , typename Filter , typename Expression >

void mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::add_element ( enumerator_queue< enumerator_list_element< Expression > > &  P, MutableSubstitution &  sigma, Filter  accept, const data::variable_list &  variables, const data::variable_list &  added_variables, const Expression &  phi, const enumerator_list_element< Expression > &  p, const data::variable &  v, const data::data_expression &  e  ) const

inlineprotected

Definition at line 105 of file enumerator_with_iterator.h.

add_element() [2/3]

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter , typename Expression >

void mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::add_element ( enumerator_queue< EnumeratorListElement > &  P, MutableSubstitution &  sigma, Filter  accept, const data::variable_list &  variables, const data::variable_list &  added_variables, const Expression &  phi, const EnumeratorListElement &  p, const data::variable &  v, const data::data_expression &  e  ) const

inlineprotected

Definition at line 84 of file enumerator_with_iterator.h.

add_element() [3/3]

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter , typename Expression >

void mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::add_element ( enumerator_queue< EnumeratorListElement > &  P, MutableSubstitution &  sigma, Filter  accept, const data::variable_list &  variables, const Expression &  phi, const EnumeratorListElement &  p, const data::variable &  v, const data::data_expression &  e  ) const

inlineprotected

Definition at line 66 of file enumerator_with_iterator.h.

cannot_enumerate()

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename EnumeratorListElement >

void mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::cannot_enumerate ( EnumeratorListElement &  e, const std::string &  msg  ) const

inlineprotected

Definition at line 55 of file enumerator_with_iterator.h.

next()

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter >

std::size_t mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::next ( enumerator_queue< EnumeratorListElement > &  P, MutableSubstitution &  sigma, Filter  accept  ) const

inline

Enumerates the front elements of the todo list P until a solution has been found, or until P is empty.

Parameters

P	The todo list of the algorithm.
sigma	A substitution.
accept	Elements p for which accept(p) is false are discarded.

Returns

The number of elements that have been processed

Postcondition

Either P.empty() or P.front().is_solution()

Definition at line 295 of file enumerator_with_iterator.h.

step()

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

template<typename EnumeratorListElement , typename MutableSubstitution , typename Filter >

void mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::step ( enumerator_queue< EnumeratorListElement > &  P, MutableSubstitution &  sigma, Filter  accept  ) const

inline

Enumerates the front element of the todo list P.

Parameters

P	The todo list of the algorithm.
sigma	A mutable substitution that is applied by the rewriter.
accept	Elements p for which accept(p) is false are discarded.

Precondition

!P.empty()

Definition at line 157 of file enumerator_with_iterator.h.

throw_exceptions()

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

bool mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::throw_exceptions ( ) const

inline

Definition at line 316 of file enumerator_with_iterator.h.

Member Data Documentation

m_throw_exceptions

template<typename Rewriter = data::rewriter, typename DataRewriter = data::rewriter>

bool mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >::m_throw_exceptions

protected

throw_exceptions If true, an exception is thrown when the enumeration is aborted.

Definition at line 52 of file enumerator_with_iterator.h.

---

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

• data/include/mcrl2/data/enumerator_with_iterator.h