mcrl2::data::enumerator_queue< EnumeratorListElement > Class Template Reference

Contains the enumerator queue. More...

#include <enumerator.h>

Public Types
typedef EnumeratorListElement	value_type
typedef atermpp::deque< EnumeratorListElement >::size_type	size_type

Public Member Functions
	enumerator_queue ()=default
	Default constructor.
	enumerator_queue (const EnumeratorListElement &value)
	Initializes the enumerator queue with the given value.
void	push_back (const EnumeratorListElement &x)
template<class... Args>
void	emplace_back (Args &&... args)
bool	empty () const
void	clear ()
atermpp::deque< EnumeratorListElement >::size_type	size () const
const EnumeratorListElement &	front () const
EnumeratorListElement &	front ()
const EnumeratorListElement &	back () const
EnumeratorListElement &	back ()
void	pop_front ()
void	pop_back ()
template<class... Args>
const EnumeratorListElement &	enumerator_element_cache (const Args &... args)

Public Attributes
EnumeratorListElement::expression_type	scratch_expression
data_expression	scratch_data_expression
variable_list	scratch_variable_list

Protected Attributes
atermpp::deque< EnumeratorListElement >	P
EnumeratorListElement	m_enumerator_element_cache

Detailed Description

template<typename EnumeratorListElement>
class mcrl2::data::enumerator_queue< EnumeratorListElement >

Contains the enumerator queue.

Definition at line 500 of file enumerator.h.

Member Typedef Documentation

size_type

template<typename EnumeratorListElement >

typedef atermpp::deque<EnumeratorListElement>::size_type mcrl2::data::enumerator_queue< EnumeratorListElement >::size_type

Definition at line 518 of file enumerator.h.

value_type

template<typename EnumeratorListElement >

typedef EnumeratorListElement mcrl2::data::enumerator_queue< EnumeratorListElement >::value_type

Definition at line 517 of file enumerator.h.

Constructor & Destructor Documentation

enumerator_queue() [1/2]

template<typename EnumeratorListElement >

mcrl2::data::enumerator_queue< EnumeratorListElement >::enumerator_queue ( )

default

Default constructor.

enumerator_queue() [2/2]

template<typename EnumeratorListElement >

mcrl2::data::enumerator_queue< EnumeratorListElement >::enumerator_queue ( const EnumeratorListElement &  value )

inlineexplicit

Initializes the enumerator queue with the given value.

Definition at line 524 of file enumerator.h.

Member Function Documentation

back() [1/2]

template<typename EnumeratorListElement >

EnumeratorListElement & mcrl2::data::enumerator_queue< EnumeratorListElement >::back ( )

inline

Definition at line 575 of file enumerator.h.

back() [2/2]

template<typename EnumeratorListElement >

const EnumeratorListElement & mcrl2::data::enumerator_queue< EnumeratorListElement >::back ( ) const

inline

Definition at line 570 of file enumerator.h.

clear()

template<typename EnumeratorListElement >

void mcrl2::data::enumerator_queue< EnumeratorListElement >::clear ( )

inline

Definition at line 550 of file enumerator.h.

emplace_back()

template<typename EnumeratorListElement >

template<class... Args>

void mcrl2::data::enumerator_queue< EnumeratorListElement >::emplace_back ( Args &&...  args )

inline

Definition at line 537 of file enumerator.h.

empty()

template<typename EnumeratorListElement >

bool mcrl2::data::enumerator_queue< EnumeratorListElement >::empty ( ) const

inline

Definition at line 545 of file enumerator.h.

enumerator_element_cache()

template<typename EnumeratorListElement >

template<class... Args>

const EnumeratorListElement & mcrl2::data::enumerator_queue< EnumeratorListElement >::enumerator_element_cache ( const Args &...  args )

inline

Definition at line 591 of file enumerator.h.

front() [1/2]

template<typename EnumeratorListElement >

EnumeratorListElement & mcrl2::data::enumerator_queue< EnumeratorListElement >::front ( )

inline

Definition at line 565 of file enumerator.h.

front() [2/2]

template<typename EnumeratorListElement >

const EnumeratorListElement & mcrl2::data::enumerator_queue< EnumeratorListElement >::front ( ) const

inline

Definition at line 560 of file enumerator.h.

pop_back()

template<typename EnumeratorListElement >

void mcrl2::data::enumerator_queue< EnumeratorListElement >::pop_back ( )

inline

Definition at line 585 of file enumerator.h.

pop_front()

template<typename EnumeratorListElement >

void mcrl2::data::enumerator_queue< EnumeratorListElement >::pop_front ( )

inline

Definition at line 580 of file enumerator.h.

push_back()

template<typename EnumeratorListElement >

void mcrl2::data::enumerator_queue< EnumeratorListElement >::push_back ( const EnumeratorListElement &  x )

inline

Definition at line 528 of file enumerator.h.

size()

template<typename EnumeratorListElement >

atermpp::deque< EnumeratorListElement >::size_type mcrl2::data::enumerator_queue< EnumeratorListElement >::size ( ) const

inline

Definition at line 555 of file enumerator.h.

Member Data Documentation

m_enumerator_element_cache

template<typename EnumeratorListElement >

EnumeratorListElement mcrl2::data::enumerator_queue< EnumeratorListElement >::m_enumerator_element_cache

protected

Definition at line 504 of file enumerator.h.

P

template<typename EnumeratorListElement >

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

protected

Definition at line 503 of file enumerator.h.

scratch_data_expression

template<typename EnumeratorListElement >

data_expression mcrl2::data::enumerator_queue< EnumeratorListElement >::scratch_data_expression

Definition at line 514 of file enumerator.h.

scratch_expression

template<typename EnumeratorListElement >

EnumeratorListElement::expression_type mcrl2::data::enumerator_queue< EnumeratorListElement >::scratch_expression

Definition at line 513 of file enumerator.h.

scratch_variable_list

template<typename EnumeratorListElement >

variable_list mcrl2::data::enumerator_queue< EnumeratorListElement >::scratch_variable_list

Definition at line 515 of file enumerator.h.

---

The documentation for this class was generated from the following file:

• data/include/mcrl2/data/enumerator.h