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
typedef Expression	expression_type

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 230 of file enumerator.h.

Member Typedef Documentation

◆ expression_type

template<typename Expression = data::data_expression>

typedef Expression mcrl2::data::enumerator_list_element< Expression >::expression_type

Definition at line 237 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 243 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 248 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 256 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 275 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 270 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 286 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 280 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 293 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 302 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 311 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 321 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 332 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 265 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 234 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 233 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