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 attributes

const data::data_specification &mcrl2::data::enumerator_algorithm_without_callback::dataspec

A data specification.

enumerator_identifier_generator &mcrl2::data::enumerator_algorithm_without_callback::id_generator
std::size_t mcrl2::data::enumerator_algorithm_without_callback::m_max_count

max_count The enumeration is aborted after max_count iterations

bool mcrl2::data::enumerator_algorithm_without_callback::m_throw_exceptions

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

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

Protected member functions

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 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<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 cannot_enumerate(EnumeratorListElement &e, const std::string &msg) const
Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const
void rewrite(Expression &result, const Expression &phi, MutableSubstitution &sigma) const

Public member functions

enumerator_algorithm_without_callback(const enumerator_algorithm<Rewriter, DataRewriter>&) = delete
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)
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