mcrl2::data::enumerator_algorithm

Include file:

#include "mcrl2/data/enumerator.h
class mcrl2::data::enumerator_algorithm

An enumerator algorithm that generates solutions of a condition.

Protected attributes

const data::data_specification &mcrl2::data::enumerator_algorithm::dataspec

A data specification.

enumerator_identifier_generator &mcrl2::data::enumerator_algorithm::id_generator
bool mcrl2::data::enumerator_algorithm::m_accept_solutions_with_variables

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

std::size_t mcrl2::data::enumerator_algorithm::m_max_count

max_count The enumeration is aborted after max_count iterations

const Rewriter &mcrl2::data::enumerator_algorithm::R
const DataRewriter &mcrl2::data::enumerator_algorithm::r

Protected member functions

std::string print(const data::variable &x) const
Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const
void rewrite(Expression &result, const Expression &phi, MutableSubstitution &sigma) const

Public member functions

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

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.

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

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

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

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)())
std::size_t max_count() const
void reset_id_generator()
~enumerator_algorithm()