mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution > Class Template Reference

An enumerator algorithm with an iterator interface. More...

#include <enumerator_with_iterator.h>

Inheritance diagram for mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >:

Classes
class	iterator
	A class to enumerate solutions for terms. More...

Public Types
typedef enumerator_algorithm_without_callback< Rewriter, DataRewriter >	super

Public Member Functions
	enumerator_algorithm_with_iterator (const Rewriter &R, const data::data_specification &dataspec, const DataRewriter &datar, enumerator_identifier_generator &id_generator, std::size_t max_count=(std::numeric_limits< std::size_t >::max)(), bool throw_exceptions=false, const Filter &f=Filter())
iterator	begin (MutableSubstitution &sigma, enumerator_queue< EnumeratorListElement > &P)
	Returns an iterator that enumerates solutions for variables that satisfy a condition.
const iterator &	end ()
Public Member Functions inherited from 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)
	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 Attributes
Filter	m_accept
Protected Attributes inherited from mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >
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.

Additional Inherited Members
Protected Types inherited from mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >
typedef enumerator_algorithm< Rewriter, DataRewriter >	super
Protected Member Functions inherited from mcrl2::data::enumerator_algorithm_without_callback< Rewriter, DataRewriter >
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

Detailed Description

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>
class mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >

An enumerator algorithm with an iterator interface.

Definition at line 324 of file enumerator_with_iterator.h.

Member Typedef Documentation

super

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>

typedef enumerator_algorithm_without_callback<Rewriter, DataRewriter> mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >::super

Definition at line 330 of file enumerator_with_iterator.h.

Constructor & Destructor Documentation

enumerator_algorithm_with_iterator()

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>

mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >::enumerator_algorithm_with_iterator ( const Rewriter &  R, const data::data_specification &  dataspec, const DataRewriter &  datar, enumerator_identifier_generator &  id_generator, std::size_t  max_count = (std::numeric_limits<std::size_t>::max)(), bool  throw_exceptions = false, const Filter &  f = Filter()  )

inline

Definition at line 409 of file enumerator_with_iterator.h.

Member Function Documentation

begin()

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>

iterator mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >::begin ( MutableSubstitution &  sigma, enumerator_queue< EnumeratorListElement > &  P  )

inline

Returns an iterator that enumerates solutions for variables that satisfy a condition.

Parameters

sigma	A mutable substitution that is applied by the rewriter contained in E
P	The condition that is solved, together with the list of variables Otherwise an invalidated enumerator element is returned when it is dereferenced.

Definition at line 425 of file enumerator_with_iterator.h.

end()

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>

const iterator & mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >::end ( )

inline

Definition at line 440 of file enumerator_with_iterator.h.

Member Data Documentation

m_accept

template<typename Rewriter = data::rewriter, typename EnumeratorListElement = enumerator_list_element_with_substitution<>, typename Filter = data::is_not_false, typename DataRewriter = data::rewriter, typename MutableSubstitution = data::mutable_indexed_substitution<>>

Filter mcrl2::data::enumerator_algorithm_with_iterator< Rewriter, EnumeratorListElement, Filter, DataRewriter, MutableSubstitution >::m_accept

protected

Definition at line 327 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