mcrl2::data::enumerator_algorithm =============================================================================== Include file: .. code-block:: c++ #include "mcrl2/data/enumerator.h .. cpp:class:: mcrl2::data::enumerator_algorithm An enumerator algorithm that generates solutions of a condition. Protected attributes ------------------------------------------------------------------------------- .. cpp:member:: const data::data_specification & mcrl2::data::enumerator_algorithm::dataspec A data specification. .. cpp:member:: enumerator_identifier_generator & mcrl2::data::enumerator_algorithm::id_generator .. cpp:member:: bool mcrl2::data::enumerator_algorithm::m_accept_solutions_with_variables If true, solutions with a non-empty list of variables may be reported. .. cpp:member:: std::size_t mcrl2::data::enumerator_algorithm::m_max_count max_count The enumeration is aborted after max_count iterations .. cpp:member:: const Rewriter & mcrl2::data::enumerator_algorithm::R .. cpp:member:: const DataRewriter & mcrl2::data::enumerator_algorithm::r Protected member functions ------------------------------------------------------------------------------- .. cpp:function:: std::string print(const data::variable &x) const .. cpp:function:: Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const Public member functions ------------------------------------------------------------------------------- .. cpp:function:: 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. **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 .. cpp:function:: 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. **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 .. cpp:function:: 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. **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 .. cpp:function:: 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)()) .. cpp:function:: enumerator_algorithm(const enumerator_algorithm< Rewriter, DataRewriter > &)=delete .. cpp:function:: std::size_t max_count() const .. cpp:function:: ~enumerator_algorithm()