Include file:
#include "mcrl2/data/enumerator.h
mcrl2::data::
enumerator_algorithm
¶An enumerator algorithm that generates solutions of a condition.
mcrl2::data::enumerator_algorithm::
dataspec
¶A data specification.
mcrl2::data::enumerator_algorithm::
id_generator
¶mcrl2::data::enumerator_algorithm::
m_accept_solutions_with_variables
¶If true, solutions with a non-empty list of variables may be reported.
mcrl2::data::enumerator_algorithm::
m_max_count
¶max_count The enumeration is aborted after max_count iterations
mcrl2::data::enumerator_algorithm::
R
¶mcrl2::data::enumerator_algorithm::
r
¶rewrite
(const Expression &phi, MutableSubstitution &sigma) const¶rewrite
(Expression &result, const Expression &phi, MutableSubstitution &sigma) const¶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.
Parameters:
Returns: The number of elements that have been processed
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.
Parameters:
Returns: The number of elements that have been processed
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.
Parameters:
Returns: The number of elements that have been processed
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.
Parameters:
Pre: !P.empty()
Returns: If the return value is true, enumeration will be interrupted
enumerator_algorithm
(const enumerator_algorithm<Rewriter, DataRewriter>&) = delete¶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)())¶max_count
() const¶reset_id_generator
()¶~enumerator_algorithm
()¶