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

#include <enumerator.h>

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

Classes
struct	always_false

Public Member Functions
	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 , IsSubstitution 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 , IsSubstitution 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 , IsSubstitution 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 , IsSubstitution 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 Member Functions
std::string	print (const data::variable &x) const

template<typename Expression , IsSubstitution MutableSubstitution>
Expression	rewrite (const Expression &phi, MutableSubstitution &sigma) const

template<typename Expression , IsSubstitution MutableSubstitution>
void	rewrite (Expression &result, const Expression &phi, MutableSubstitution &sigma) const

Protected Attributes
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< Rewriter, DataRewriter >

An enumerator algorithm that generates solutions of a condition.

Definition at line 598 of file enumerator.h.

Constructor & Destructor Documentation

◆ enumerator_algorithm() [1/2]

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

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)()`
	)

inline

Definition at line 651 of file enumerator.h.

◆ enumerator_algorithm() [2/2]

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

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

delete

◆ ~enumerator_algorithm()

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

mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::~enumerator_algorithm ( )

inline

Definition at line 668 of file enumerator.h.

Member Function Documentation

◆ enumerate() [1/2]

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

template<typename EnumeratorListElement , IsSubstitution MutableSubstitution, typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>

std::size_t mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::enumerate	(	const EnumeratorListElement &	p,
		MutableSubstitution &	sigma,
		ReportSolution	report_solution,
		Reject	reject = `Reject()`,
		Accept	accept = `Accept()`
	)		const

inline

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.

Parameters

p	An enumerator element, i.e. an expression with a list of variables.
sigma	A substitution.
report_solution	A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again.
reject	Elements p for which reject(p) is true are discarded.
accept	Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.

Returns: The number of elements that have been processed

Definition at line 972 of file enumerator.h.

◆ enumerate() [2/2]

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

template<typename EnumeratorListElement , IsSubstitution MutableSubstitution, typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>

std::size_t mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::enumerate	(	const variable_list &	vars,
		const typename EnumeratorListElement::expression_type &	cond,
		MutableSubstitution &	sigma,
		ReportSolution	report_solution,
		Reject	reject = `Reject()`,
		Accept	accept = `Accept()`
	)		const

inline

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.

Parameters

vars	The list of variables v to enumerate over.
cond	The condition to evaluate for each enumerated value.
sigma	A substitution.
report_solution	A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again.
reject	Elements p for which reject(p) is true are discarded.
accept	Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.

Returns: The number of elements that have been processed

Definition at line 1002 of file enumerator.h.

◆ enumerate_all()

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

template<typename EnumeratorListElement , IsSubstitution MutableSubstitution, typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>

std::size_t mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::enumerate_all	(	enumerator_queue< EnumeratorListElement > &	P,
		MutableSubstitution &	sigma,
		ReportSolution	report_solution,
		Reject	reject = `Reject()`,
		Accept	accept = `Accept()`
	)		const

inline

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.

Parameters

P	The todo list of the algorithm.
sigma	A substitution.
report_solution	A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again.
reject	Elements p for which reject(p) is true are discarded.
accept	Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.

Returns: The number of elements that have been processed

Definition at line 932 of file enumerator.h.

◆ enumerate_front()

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

template<typename EnumeratorListElement , IsSubstitution MutableSubstitution, typename ReportSolution , typename Reject = always_false<typename EnumeratorListElement::expression_type>, typename Accept = always_false<typename EnumeratorListElement::expression_type>>

bool mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::enumerate_front	(	enumerator_queue< EnumeratorListElement > &	P,
		MutableSubstitution &	sigma,
		ReportSolution	report_solution,
		Reject	reject = `Reject()`,
		Accept	accept = `Accept()`
	)		const

inline

Enumerates the front element of the todo list P. The enumeration is interrupted when report_solution returns true for the reported solution.

Parameters

P	The todo list of the algorithm.
sigma	A mutable substitution that is applied by the rewriter.
report_solution	A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again.
reject	Elements p for which reject(p) is true are discarded.
accept	Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty.

Precondition: !P.empty()

Returns: If the return value is true, enumeration will be interrupted

Definition at line 705 of file enumerator.h.

◆ max_count()

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

std::size_t mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::max_count ( ) const

inline

Definition at line 1015 of file enumerator.h.

◆ print()

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

std::string mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::print ( const data::variable & x ) const

inlineprotected

Definition at line 623 of file enumerator.h.

◆ reset_id_generator()

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

void mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::reset_id_generator ( )

inline

Definition at line 675 of file enumerator.h.

◆ rewrite() [1/2]

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

template<typename Expression , IsSubstitution MutableSubstitution>

Expression mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::rewrite	(	const Expression &	phi,
		MutableSubstitution &	sigma
	)		const

inlineprotected

Definition at line 632 of file enumerator.h.

◆ rewrite() [2/2]

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

template<typename Expression , IsSubstitution MutableSubstitution>

void mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::rewrite	(	Expression &	result,
		const Expression &	phi,
		MutableSubstitution &	sigma
	)		const

inlineprotected

Definition at line 642 of file enumerator.h.

Member Data Documentation

◆ dataspec

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

const data::data_specification& mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::dataspec

protected

A data specification.

Definition at line 605 of file enumerator.h.

◆ id_generator

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

enumerator_identifier_generator& mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::id_generator

protected

Definition at line 611 of file enumerator.h.

◆ m_accept_solutions_with_variables

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

bool mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::m_accept_solutions_with_variables

protected

If true, solutions with a non-empty list of variables may be reported.

Definition at line 617 of file enumerator.h.

◆ m_max_count

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

std::size_t mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::m_max_count

protected

max_count The enumeration is aborted after max_count iterations

Definition at line 614 of file enumerator.h.

◆ R

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

const Rewriter& mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::R

protected

Definition at line 602 of file enumerator.h.

◆ r

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

const DataRewriter& mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::r

protected

Definition at line 608 of file enumerator.h.

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

data/include/mcrl2/data/enumerator.h

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ enumerator_algorithm() [1/2]

◆ enumerator_algorithm() [2/2]

◆ ~enumerator_algorithm()

Member Function Documentation

◆ enumerate() [1/2]

◆ enumerate() [2/2]

◆ enumerate_all()

◆ enumerate_front()

◆ max_count()

◆ print()

◆ reset_id_generator()

◆ rewrite() [1/2]

◆ rewrite() [2/2]

Member Data Documentation

◆ dataspec

◆ id_generator

◆ m_accept_solutions_with_variables

◆ m_max_count

◆ R

◆ r