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¶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:
p An enumerator element, i.e. an expression with a list of variables.
sigma A substitution.
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.
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.
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:
P The todo list of the algorithm.
sigma A substitution.
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.
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.
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:
P The todo list of the algorithm.
sigma A mutable substitution that is applied by the rewriter.
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.
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.
Pre: !P.empty()
Returns: If the return value is true, enumeration will be interrupted
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¶max_count
() const¶~enumerator_algorithm
()¶