mcrl2::data::enumerator_queue

Include file:

#include "mcrl2/data/enumerator.h

class mcrl2::data::enumerator_queue

Contains the enumerator queue.

Public types

type mcrl2::data::enumerator_queue::size_type

typedef for atermpp::deque< EnumeratorListElement >::size_type

type mcrl2::data::enumerator_queue::value_type

typedef for EnumeratorListElement

Protected attributes

EnumeratorListElement mcrl2::data::enumerator_queue::m_enumerator_element_cache

atermpp::deque<EnumeratorListElement> mcrl2::data::enumerator_queue::P

Public attributes

data_expression mcrl2::data::enumerator_queue::scratch_data_expression

EnumeratorListElement::expression_type mcrl2::data::enumerator_queue::scratch_expression

variable_list mcrl2::data::enumerator_queue::scratch_variable_list

Public member functions

EnumeratorListElement &back()

const EnumeratorListElement &back() const

void clear()

void emplace_back(Args&&... args)

bool empty() const

const EnumeratorListElement &enumerator_element_cache(const Args&... args)

enumerator_queue() = default

Default constructor.

enumerator_queue(const EnumeratorListElement &value)

Initializes the enumerator queue with the given value.

EnumeratorListElement &front()

const EnumeratorListElement &front() const

void pop_back()

void pop_front()

void push_back(const EnumeratorListElement &x)

atermpp::deque<EnumeratorListElement>::size_type size() const