An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi. More...

#include <enumerator.h>

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

Public Types
using	expression_type = Expression

Public Types inherited from mcrl2::data::enumerator_list_element< Expression >
using	expression_type = Expression

Public Member Functions
	enumerator_list_element_with_substitution ()=default
	Default constructor.

	enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi)
	Constructs the element (v, phi, [])

	enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
	Constructs the element (v, phi, e.sigma[v := x])

	enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
	Constructs the element (v, phi, e.sigma[v := x])

template<typename VariableList , IsSubstitution MutableSubstitution, typename Rewriter >
void	add_assignments (const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const
	Adds the assignments that correspond with this element to the substitution result.

template<typename VariableList , IsSubstitution MutableSubstitution>
void	remove_assignments (const VariableList &v, MutableSubstitution &result) const
	Removes the assignments corresponding with this element from the substitution result.

template<typename VariableList , typename Rewriter >
data::data_expression_list	assign_expressions (const VariableList &v, const Rewriter &rewriter) const
	Returns the right hand sides corresponding to the variables v.

data::enumerator_substitution	sigma () const

void	mark (std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &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, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
	Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

void	set (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
	Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Public Member Functions inherited from mcrl2::data::enumerator_list_element< Expression >
	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	m_variables

data::data_expression_list	m_expressions

Protected Attributes inherited from mcrl2::data::enumerator_list_element< Expression >
data::variable_list	v

Expression	phi

Detailed Description

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

An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi.

Definition at line 345 of file enumerator.h.

Member Typedef Documentation

◆ expression_type

template<typename Expression = data::data_expression>

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

Definition at line 352 of file enumerator.h.

Constructor & Destructor Documentation

◆ enumerator_list_element_with_substitution() [1/4]

template<typename Expression = data::data_expression>

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

default

Default constructor.

◆ enumerator_list_element_with_substitution() [2/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution	(	const data::variable_list &	v,
		const Expression &	phi
	)

inline

Constructs the element (v, phi, [])

Definition at line 358 of file enumerator.h.

◆ enumerator_list_element_with_substitution() [3/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution	(	const data::variable_list &	v,
		const Expression &	phi,
		const enumerator_list_element_with_substitution< Expression > &	elem
	)

inline

Constructs the element (v, phi, e.sigma[v := x])

Definition at line 363 of file enumerator.h.

◆ enumerator_list_element_with_substitution() [4/4]

template<typename Expression = data::data_expression>

mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution	(	const data::variable_list &	v,
		const Expression &	phi,
		const enumerator_list_element_with_substitution< Expression > &	elem,
		const data::variable &	d,
		const data::data_expression &	e
	)

inline

Constructs the element (v, phi, e.sigma[v := x])

Definition at line 374 of file enumerator.h.

Member Function Documentation

◆ add_assignments()

template<typename Expression = data::data_expression>

template<typename VariableList , IsSubstitution MutableSubstitution, typename Rewriter >

void mcrl2::data::enumerator_list_element_with_substitution< Expression >::add_assignments	(	const VariableList &	v,
		MutableSubstitution &	result,
		const Rewriter &	rewriter
	)		const

inline

Adds the assignments that correspond with this element to the substitution result.

Definition at line 391 of file enumerator.h.

◆ assign_expressions()

template<typename Expression = data::data_expression>

template<typename VariableList , typename Rewriter >

data::data_expression_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::assign_expressions	(	const VariableList &	v,
		const Rewriter &	rewriter
	)		const

inline

Returns the right hand sides corresponding to the variables v.

Precondition: variables in v must be contained in variables()

Definition at line 414 of file enumerator.h.

◆ mark()

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element_with_substitution< Expression >::mark ( std::stack< std::reference_wrapper< atermpp::detail::_aterm > > & 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 430 of file enumerator.h.

◆ remove_assignments()

template<typename Expression = data::data_expression>

template<typename VariableList , IsSubstitution MutableSubstitution>

void mcrl2::data::enumerator_list_element_with_substitution< Expression >::remove_assignments	(	const VariableList &	v,
		MutableSubstitution &	result
	)		const

inline

Removes the assignments corresponding with this element from the substitution result.

Definition at line 403 of file enumerator.h.

◆ set() [1/2]

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element_with_substitution< Expression >::set	(	const data::variable_list &	v,
		const Expression &	phi,
		const enumerator_list_element_with_substitution< Expression > &	elem
	)

inline

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

Definition at line 454 of file enumerator.h.

◆ set() [2/2]

template<typename Expression = data::data_expression>

void mcrl2::data::enumerator_list_element_with_substitution< Expression >::set	(	const data::variable_list &	v,
		const Expression &	phi,
		const enumerator_list_element_with_substitution< Expression > &	elem,
		const data::variable &	d,
		const data::data_expression &	e
	)

inline

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

Definition at line 439 of file enumerator.h.

◆ sigma()

template<typename Expression = data::data_expression>

data::enumerator_substitution mcrl2::data::enumerator_list_element_with_substitution< Expression >::sigma ( ) const

inline

Definition at line 421 of file enumerator.h.

Member Data Documentation

◆ m_expressions

template<typename Expression = data::data_expression>

data::data_expression_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::m_expressions

protected

Definition at line 349 of file enumerator.h.

◆ m_variables

template<typename Expression = data::data_expression>

data::variable_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::m_variables

protected

Definition at line 348 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_with_substitution() [1/4]

◆ enumerator_list_element_with_substitution() [2/4]

◆ enumerator_list_element_with_substitution() [3/4]

◆ enumerator_list_element_with_substitution() [4/4]

Member Function Documentation

◆ add_assignments()

◆ assign_expressions()

◆ mark()

◆ remove_assignments()

◆ set() [1/2]

◆ set() [2/2]

◆ sigma()

Member Data Documentation

◆ m_expressions

◆ m_variables