mcrl2::data::enumerator_algorithm_without_callback

Include file:

#include "mcrl2/data/enumerator_with_iterator.h
class mcrl2::data::enumerator_algorithm_without_callback

An enumerator algorithm that generates solutions of a condition.

Protected types

type super

typedef for enumerator_algorithm< Rewriter, DataRewriter >

Protected attributes

bool m_throw_exceptions

throw_exceptions If true, an exception is thrown when the enumeration is aborted.

Protected member functions

void add_element(enumerator_queue<EnumeratorListElement> &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const Expression &phi, const EnumeratorListElement &p, const data::variable &v, const data::data_expression &e) const
void add_element(enumerator_queue<EnumeratorListElement> &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const data::variable_list &added_variables, const Expression &phi, const EnumeratorListElement &p, const data::variable &v, const data::data_expression &e) const
void add_element(enumerator_queue<enumerator_list_element<Expression>> &P, MutableSubstitution &sigma, Filter accept, const data::variable_list &variables, const data::variable_list &added_variables, const Expression &phi, const enumerator_list_element<Expression> &p, const data::variable &v, const data::data_expression &e) const
void cannot_enumerate(EnumeratorListElement &e, const std::string &msg) const

Public member functions

enumerator_algorithm_without_callback(const Rewriter &R, const data::data_specification &dataspec, const DataRewriter &r, enumerator_identifier_generator &id_generator, std::size_t max_count = (std::numeric_limits< std::size_t >::max)(), bool throw_exceptions = false)
enumerator_algorithm_without_callback(const enumerator_algorithm<Rewriter, DataRewriter>&) = delete
std::size_t next(enumerator_queue<EnumeratorListElement> &P, MutableSubstitution &sigma, Filter accept) const

Enumerates the front elements of the todo list P until a solution has been found, or until P is empty.

Parameters:

  • P The todo list of the algorithm.
  • sigma A substitution.
  • accept Elements p for which accept(p) is false are discarded.

Returns: The number of elements that have been processed

Post: Either P.empty() or P.front().is_solution()

void step(enumerator_queue<EnumeratorListElement> &P, MutableSubstitution &sigma, Filter accept) const

Enumerates the front element of the todo list P.

Parameters:

  • P The todo list of the algorithm.
  • sigma A mutable substitution that is applied by the rewriter.
  • accept Elements p for which accept(p) is false are discarded.

Pre: !P.empty()

bool throw_exceptions() const