mcrl2::data::enumerator_algorithm_with_iterator

Include file:

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

An enumerator algorithm with an iterator interface.

Protected attributes

Filter mcrl2::data::enumerator_algorithm_with_iterator::m_accept

Public member functions

iterator begin(MutableSubstitution &sigma, enumerator_queue<EnumeratorListElement> &P)

Returns an iterator that enumerates solutions for variables that satisfy a condition.

Parameters:

  • sigma A mutable substitution that is applied by the rewriter contained in E
  • P The condition that is solved, together with the list of variables Otherwise an invalidated enumerator element is returned when it is dereferenced.
const iterator &end()
enumerator_algorithm_with_iterator(const Rewriter &R, const data::data_specification &dataspec, const DataRewriter &datar, enumerator_identifier_generator &id_generator, std::size_t max_count = (std::numeric_limits<std::size_t>::max)(), bool throw_exceptions = false, const Filter &f = Filter())
Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const
void rewrite(Expression &result, const Expression &phi, MutableSubstitution &sigma) const