The default element for the todo list of the enumerator. More...

#include <enumerator.h>

Inheritance diagram for mcrl2::data::enumerator_list_element< Expression >:

Public Types
using	expression_type = Expression

Public Member Functions
	enumerator_list_element ()=default
	Default constructor.

	enumerator_list_element (data::variable_list v_, const Expression &phi_)
	Constructs the element (v, phi)

	enumerator_list_element (data::variable_list v_, const Expression &phi_, const enumerator_list_element &)
	Constructs the element (v, phi)

	enumerator_list_element (data::variable_list v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
	Constructs the element (v, phi)

const data::variable_list &	variables () const

const Expression &	expression () const

Expression &	expression ()

bool	is_solution () const

void	invalidate ()
	Invalidates the element, by giving phi an undefined value.

bool	is_valid () const
	Returns true if the element is valid. If it becomes false, this is used to signal that the enumeration has been aborted.

void	mark (atermpp::term_mark_stack &todo) const
	The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

void	set (const data::variable_list &v_, const Expression &phi_)
	Set the variables and the condition explicitly.

void	set (const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &)
	Set the variables and the condition explicitly.

void	set (const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
	Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Protected Attributes
data::variable_list	v

Expression	phi

Detailed Description

template<typename Expression = data::data_expression>
class mcrl2::data::enumerator_list_element< Expression >

The default element for the todo list of the enumerator.

Definition at line 228 of file enumerator.h.

Member Typedef Documentation

◆ expression_type

template<typename Expression = data::data_expression>

using mcrl2::data::enumerator_list_element< Expression >::expression_type = Expression

Definition at line 235 of file enumerator.h.

Constructor & Destructor Documentation

◆ enumerator_list_element() [1/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element< Expression >::enumerator_list_element ( )

default

Default constructor.

◆ enumerator_list_element() [2/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element< Expression >::enumerator_list_element	(	data::variable_list	v_,
		const Expression &	phi_
	)

inline

Constructs the element (v, phi)

Definition at line 241 of file enumerator.h.

◆ enumerator_list_element() [3/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element< Expression >::enumerator_list_element	(	data::variable_list	v_,
		const Expression &	phi_,
		const enumerator_list_element< Expression > &
	)

inline

Constructs the element (v, phi)

Definition at line 246 of file enumerator.h.

◆ enumerator_list_element() [4/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element< Expression >::enumerator_list_element	(	data::variable_list	v_,
		const Expression &	phi_,
		const enumerator_list_element< Expression > &	,
		const data::variable &	,
		const data::data_expression &
	)

inline

Constructs the element (v, phi)

Definition at line 254 of file enumerator.h.

Member Function Documentation

◆ expression() [1/2]

template<typename Expression = data::data_expression>

Expression & mcrl2::data::enumerator_list_element< Expression >::expression ( )

inline

Definition at line 273 of file enumerator.h.

◆ expression() [2/2]

template<typename Expression = data::data_expression>

const Expression & mcrl2::data::enumerator_list_element< Expression >::expression ( ) const

inline

Definition at line 268 of file enumerator.h.

◆ invalidate()

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element< Expression >::invalidate ( )

inline

Invalidates the element, by giving phi an undefined value.

Definition at line 284 of file enumerator.h.

◆ is_solution()

template<typename Expression = data::data_expression>

bool mcrl2::data::enumerator_list_element< Expression >::is_solution ( ) const

inline

Definition at line 278 of file enumerator.h.

◆ is_valid()

template<typename Expression = data::data_expression>

bool mcrl2::data::enumerator_list_element< Expression >::is_valid ( ) const

inline

Returns true if the element is valid. If it becomes false, this is used to signal that the enumeration has been aborted.

Definition at line 291 of file enumerator.h.

◆ mark()

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element< Expression >::mark ( atermpp::term_mark_stack & todo ) const

inline

The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

Definition at line 300 of file enumerator.h.

◆ set() [1/3]

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element< Expression >::set	(	const data::variable_list &	v_,
		const Expression &	phi_
	)

inline

Set the variables and the condition explicitly.

Parameters

v_	The variable list.
phi_	The condition.

Definition at line 309 of file enumerator.h.

◆ set() [2/3]

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element< Expression >::set	(	const data::variable_list &	v_,
		const Expression &	phi_,
		const enumerator_list_element< Expression > &
	)

inline

Set the variables and the condition explicitly.

Parameters

v_	The variable list.
phi_	The condition.

Other arguments than the first two are ignored.

Definition at line 319 of file enumerator.h.

◆ set() [3/3]

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element< Expression >::set	(	const data::variable_list &	v_,
		const Expression &	phi_,
		const enumerator_list_element< Expression > &	,
		const data::variable &	,
		const data::data_expression &
	)

inline

Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Parameters

v_	The variable list.
phi_	The condition.

Other arguments than the first two are ignored.

Definition at line 330 of file enumerator.h.

◆ variables()

template<typename Expression = data::data_expression>

const data::variable_list & mcrl2::data::enumerator_list_element< Expression >::variables ( ) const

inline

Definition at line 263 of file enumerator.h.

Member Data Documentation

◆ phi

template<typename Expression = data::data_expression>

Expression mcrl2::data::enumerator_list_element< Expression >::phi

protected

Definition at line 232 of file enumerator.h.

◆ v

template<typename Expression = data::data_expression>

data::variable_list mcrl2::data::enumerator_list_element< Expression >::v

protected

Definition at line 231 of file enumerator.h.

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

data/include/mcrl2/data/enumerator.h

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ expression_type

Constructor & Destructor Documentation

◆ enumerator_list_element() [1/4]

◆ enumerator_list_element() [2/4]

◆ enumerator_list_element() [3/4]

◆ enumerator_list_element() [4/4]

Member Function Documentation

◆ expression() [1/2]

◆ expression() [2/2]

◆ invalidate()

◆ is_solution()

◆ is_valid()

◆ mark()

◆ set() [1/3]

◆ set() [2/3]

◆ set() [3/3]

◆ variables()

Member Data Documentation

◆ phi

◆ v