Generic substitution function. The substitution is stored as a mapping of variables to expressions. The substitution is mutable, meaning that substitutions to variables can be added and removed as follows: More...

#include <mutable_map_substitution.h>

Classes
struct	assignment
	Wrapper class for internal storage and substitution updates using operator() More...

Public Types
typedef AssociativeContainer::key_type	variable_type

typedef AssociativeContainer::mapped_type	expression_type

typedef AssociativeContainer::const_iterator	const_iterator

typedef AssociativeContainer::iterator	iterator

using	argument_type = variable_type

using	result_type = expression_type

Public Member Functions
	mutable_map_substitution ()=default

	mutable_map_substitution (const AssociativeContainer &m)

template<typename VariableContainer , typename ExpressionContainer >
	mutable_map_substitution (VariableContainer const &variables, ExpressionContainer const &expressions)

expression_type	operator() (const variable_type &v) const

assignment	operator[] (variable_type const &v)

void	clear ()
	Resets the substitution by letting every variable yield itself. Cf. clear() of a map.

template<typename Substitution >
bool	operator== (const Substitution &) const

const_iterator	begin () const
	Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

const_iterator	end () const
	Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

iterator	begin ()
	Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

iterator	end ()
	Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

bool	empty () const
	Returns true if the substitution is empty.

std::string	to_string () const

iterator	find (variable_type const &v)
	Returns an iterator that references the expression associated with v or is equal to m_map.end()

const_iterator	find (variable_type const &v) const
	Returns an iterator that references the expression associated with v or is equal to m_map.end()

Protected Attributes
AssociativeContainer	m_map

Detailed Description

template<typename AssociativeContainer = std::map<variable,data_expression>>
class mcrl2::data::mutable_map_substitution< AssociativeContainer >

Generic substitution function. The substitution is stored as a mapping of variables to expressions. The substitution is mutable, meaning that substitutions to variables can be added and removed as follows:

*  mutable_map_substitution sigma;
*  mutable_map_substitution::variable_type v;
*  mutable_map_substitution::expression_type e;
*  sigma[v] = e; // add the assignment of e to v
*  sigma[v] = v; // remove the assignment to v
*

Definition at line 33 of file mutable_map_substitution.h.

Member Typedef Documentation

◆ argument_type

template<typename AssociativeContainer = std::map<variable,data_expression>>

using mcrl2::data::mutable_map_substitution< AssociativeContainer >::argument_type = variable_type

Definition at line 43 of file mutable_map_substitution.h.

◆ const_iterator

template<typename AssociativeContainer = std::map<variable,data_expression>>

typedef AssociativeContainer::const_iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::const_iterator

Definition at line 41 of file mutable_map_substitution.h.

◆ expression_type

template<typename AssociativeContainer = std::map<variable,data_expression>>

typedef AssociativeContainer::mapped_type mcrl2::data::mutable_map_substitution< AssociativeContainer >::expression_type

Definition at line 40 of file mutable_map_substitution.h.

◆ iterator

template<typename AssociativeContainer = std::map<variable,data_expression>>

typedef AssociativeContainer::iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::iterator

Definition at line 42 of file mutable_map_substitution.h.

◆ result_type

template<typename AssociativeContainer = std::map<variable,data_expression>>

using mcrl2::data::mutable_map_substitution< AssociativeContainer >::result_type = expression_type

Definition at line 44 of file mutable_map_substitution.h.

◆ variable_type

template<typename AssociativeContainer = std::map<variable,data_expression>>

typedef AssociativeContainer::key_type mcrl2::data::mutable_map_substitution< AssociativeContainer >::variable_type

Definition at line 39 of file mutable_map_substitution.h.

Constructor & Destructor Documentation

◆ mutable_map_substitution() [1/3]

template<typename AssociativeContainer = std::map<variable,data_expression>>

mcrl2::data::mutable_map_substitution< AssociativeContainer >::mutable_map_substitution ( )

default

◆ mutable_map_substitution() [2/3]

template<typename AssociativeContainer = std::map<variable,data_expression>>

mcrl2::data::mutable_map_substitution< AssociativeContainer >::mutable_map_substitution ( const AssociativeContainer & m )

inlineexplicit

Definition at line 78 of file mutable_map_substitution.h.

◆ mutable_map_substitution() [3/3]

template<typename AssociativeContainer = std::map<variable,data_expression>>

template<typename VariableContainer , typename ExpressionContainer >

mcrl2::data::mutable_map_substitution< AssociativeContainer >::mutable_map_substitution	(	VariableContainer const &	variables,
		ExpressionContainer const &	expressions
	)

inline

Definition at line 83 of file mutable_map_substitution.h.

Member Function Documentation

◆ begin() [1/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::begin ( )

inline

Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

Definition at line 140 of file mutable_map_substitution.h.

◆ begin() [2/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

const_iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::begin ( ) const

inline

Returns an iterator pointing to the beginning of the sequence of assignments TODO: should become protected.

Definition at line 126 of file mutable_map_substitution.h.

◆ clear()

template<typename AssociativeContainer = std::map<variable,data_expression>>

void mcrl2::data::mutable_map_substitution< AssociativeContainer >::clear ( )

inline

Resets the substitution by letting every variable yield itself. Cf. clear() of a map.

Definition at line 113 of file mutable_map_substitution.h.

◆ empty()

template<typename AssociativeContainer = std::map<variable,data_expression>>

bool mcrl2::data::mutable_map_substitution< AssociativeContainer >::empty ( ) const

inline

Returns true if the substitution is empty.

Definition at line 153 of file mutable_map_substitution.h.

◆ end() [1/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::end ( )

inline

Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

Definition at line 147 of file mutable_map_substitution.h.

◆ end() [2/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

const_iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::end ( ) const

inline

Returns an iterator pointing past the end of the sequence of assignments TODO: should become protected.

Definition at line 133 of file mutable_map_substitution.h.

◆ find() [1/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::find ( variable_type const & v )

inline

Returns an iterator that references the expression associated with v or is equal to m_map.end()

Definition at line 171 of file mutable_map_substitution.h.

◆ find() [2/2]

template<typename AssociativeContainer = std::map<variable,data_expression>>

const_iterator mcrl2::data::mutable_map_substitution< AssociativeContainer >::find ( variable_type const & v ) const

inline

Returns an iterator that references the expression associated with v or is equal to m_map.end()

Definition at line 177 of file mutable_map_substitution.h.

◆ operator()()

template<typename AssociativeContainer = std::map<variable,data_expression>>

expression_type mcrl2::data::mutable_map_substitution< AssociativeContainer >::operator() ( const variable_type & v ) const

inline

Definition at line 93 of file mutable_map_substitution.h.

◆ operator==()

template<typename AssociativeContainer = std::map<variable,data_expression>>

template<typename Substitution >

bool mcrl2::data::mutable_map_substitution< AssociativeContainer >::operator== ( const Substitution & ) const

inline

Definition at line 119 of file mutable_map_substitution.h.

◆ operator[]()

template<typename AssociativeContainer = std::map<variable,data_expression>>

assignment mcrl2::data::mutable_map_substitution< AssociativeContainer >::operator[] ( variable_type const & v )

inline

Definition at line 106 of file mutable_map_substitution.h.

◆ to_string()

template<typename AssociativeContainer = std::map<variable,data_expression>>

std::string mcrl2::data::mutable_map_substitution< AssociativeContainer >::to_string ( ) const

inline

Definition at line 158 of file mutable_map_substitution.h.

Member Data Documentation

◆ m_map

template<typename AssociativeContainer = std::map<variable,data_expression>>

AssociativeContainer mcrl2::data::mutable_map_substitution< AssociativeContainer >::m_map

protected

Definition at line 36 of file mutable_map_substitution.h.

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

data/include/mcrl2/data/substitutions/mutable_map_substitution.h

Classes

Public Types

Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ argument_type

◆ const_iterator

◆ expression_type

◆ iterator

◆ result_type

◆ variable_type

Constructor & Destructor Documentation

◆ mutable_map_substitution() [1/3]

◆ mutable_map_substitution() [2/3]

◆ mutable_map_substitution() [3/3]

Member Function Documentation

◆ begin() [1/2]

◆ begin() [2/2]

◆ clear()

◆ empty()

◆ end() [1/2]

◆ end() [2/2]

◆ find() [1/2]

◆ find() [2/2]

◆ operator()()

◆ operator==()

◆ operator[]()

◆ to_string()

Member Data Documentation

◆ m_map