Generic substitution function. More...

#include <mutable_indexed_substitution.h>

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

Public Types
using	variable_type = VariableType
	Type of variables.

using	expression_type = ExpressionType
	Type of expressions.

using	argument_type = variable_type

using	result_type = expression_type

Public Member Functions
	mutable_indexed_substitution ()=default

	mutable_indexed_substitution (const substitution_type &substitution, const bool variables_in_rhs_set_is_defined, const std::multiset< variable_type > &variables_in_rhs)

template<class VARIABLES , class EXPRESSIONS >
	mutable_indexed_substitution (const VARIABLES &vars, const EXPRESSIONS &exps)

const expression_type &	operator() (const variable_type &v) const
	Application operator; applies substitution to v.

template<class ResultType >
void	apply (const variable_type &v, ResultType &target) const
	Application operator; applies substitution to v.

void	apply (const variable_type &v, expression_type &target, atermpp::detail::thread_aterm_pool &thread_aterm_pool)
	Application operator; applies substitution to v.

assignment	operator[] (variable_type const &v)
	Index operator.

void	clear ()
	Clear substitutions.

mutable_indexed_substitution< VariableType, ExpressionType >	clone ()
	Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.

template<IsSubstitution Substitution>
bool	operator== (const Substitution &) const
	Compare substitutions.

const std::multiset< variable_type > &	variables_occurring_in_right_hand_sides () const
	Provides a multiset containing the variables in the rhs.

bool	variable_occurs_in_a_rhs (const variable &v)
	Checks whether a variable v occurs in one of the rhs's of the current substitution.

bool	size ()
	Returns the number of assigned variables in the substitution.

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

std::string	to_string () const
	string representation of the substitution. N.B. This is an expensive operation!

Static Public Attributes
static constexpr bool	is_identity_substitution =false

Protected Types
using	substitution_type = atermpp::utilities::unordered_map< VariableType, ExpressionType >

Protected Attributes
substitution_type	m_substitution
	Internal storage for substitutions. Required to be a container with random access through [] operator. It is essential to store the variable also in the container, as it might be that this variable is not used anywhere although it has a valid assignment. This happens for instance when the assignment is already parsed, while the expression to which it needs to be applied must still be parsed.

bool	m_variables_in_rhs_set_is_defined =false

std::multiset< variable >	m_variables_in_rhs

Detailed Description

template<typename VariableType = data::variable, typename ExpressionType = data_expression>
class mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >

Generic substitution function.

This substitution assumes a function variable -> std::size_t, that, for each variable gives a unique index. The substitutions are stored internally as a vector, mapping std::size_t to expression. Provided that, given a variable, its index can be computed in O(1) time, insertion is O(1) amortized, and lookup is O(1). Memory required is O(n) where n is the largest index used. This substitution can maintain the variables occurring in the rhs of expressions. If it is requested that whether a variable occurs in a rhs, the substitution automatically maintains these variables. This requires time O(n log n) per rhs, where n is the size of the rhs.

Definition at line 43 of file mutable_indexed_substitution.h.

Member Typedef Documentation

◆ argument_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

using mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::argument_type = variable_type

Definition at line 66 of file mutable_indexed_substitution.h.

◆ expression_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

using mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::expression_type = ExpressionType

Type of expressions.

Definition at line 64 of file mutable_indexed_substitution.h.

◆ result_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

using mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::result_type = expression_type

Definition at line 67 of file mutable_indexed_substitution.h.

◆ substitution_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

using mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::substitution_type = atermpp::utilities::unordered_map<VariableType, ExpressionType>

protected

Definition at line 46 of file mutable_indexed_substitution.h.

◆ variable_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

using mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::variable_type = VariableType

Type of variables.

Definition at line 61 of file mutable_indexed_substitution.h.

Constructor & Destructor Documentation

◆ mutable_indexed_substitution() [1/3]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::mutable_indexed_substitution ( )

default

◆ mutable_indexed_substitution() [2/3]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::mutable_indexed_substitution	(	const substitution_type &	substitution,
		const bool	variables_in_rhs_set_is_defined,
		const std::multiset< variable_type > &	variables_in_rhs
	)

inline

Definition at line 71 of file mutable_indexed_substitution.h.

◆ mutable_indexed_substitution() [3/3]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

template<class VARIABLES , class EXPRESSIONS >

mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::mutable_indexed_substitution	(	const VARIABLES &	vars,
		const EXPRESSIONS &	exps
	)

inline

Definition at line 82 of file mutable_indexed_substitution.h.

Member Function Documentation

◆ apply() [1/2]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

void mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::apply	(	const variable_type &	v,
		expression_type &	target,
		atermpp::detail::thread_aterm_pool &	thread_aterm_pool
	)

inline

Application operator; applies substitution to v.

This must deliver an expression, and not a reference to an expression, as the expressions are stored in a vector that can be resized and moved.

Parameters

v	The variable to which the subsitution is applied.
target	The target into which the substitution is stored.

Definition at line 205 of file mutable_indexed_substitution.h.

◆ apply() [2/2]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

template<class ResultType >

void mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::apply	(	const variable_type &	v,
		ResultType &	target
	)		const

inline

Application operator; applies substitution to v.

This must deliver an expression, and not a reference to an expression, as the expressions are stored in a vector that can be resized and moved.

Parameters

v	The variable to which the subsitution is applied.
target	The target into which the substitution is stored.

Definition at line 186 of file mutable_indexed_substitution.h.

◆ clear()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

void mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::clear ( )

inline

Clear substitutions.

Definition at line 225 of file mutable_indexed_substitution.h.

◆ clone()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

mutable_indexed_substitution< VariableType, ExpressionType > mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::clone ( )

inline

Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.

This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially.

Returns: A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine.

Definition at line 237 of file mutable_indexed_substitution.h.

◆ empty()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::empty ( )

inline

Returns true if the substitution is empty.

Definition at line 281 of file mutable_indexed_substitution.h.

◆ operator()()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

const expression_type & mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::operator() ( const variable_type & v ) const

inline

Application operator; applies substitution to v.

Parameters

v	The variable to which the subsitution is applied.

Returns: The value to which v is mapped, or v itself if v is not mapped to a value.

Definition at line 167 of file mutable_indexed_substitution.h.

◆ operator==()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

template<IsSubstitution Substitution>

bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::operator== ( const Substitution & ) const

inline

Compare substitutions.

Definition at line 245 of file mutable_indexed_substitution.h.

◆ operator[]()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

assignment mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::operator[] ( variable_type const & v )

inline

Index operator.

Definition at line 219 of file mutable_indexed_substitution.h.

◆ size()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::size ( )

inline

Returns the number of assigned variables in the substitution.

Definition at line 275 of file mutable_indexed_substitution.h.

◆ to_string()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

std::string mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::to_string ( ) const

inline

string representation of the substitution. N.B. This is an expensive operation!

Definition at line 288 of file mutable_indexed_substitution.h.

◆ variable_occurs_in_a_rhs()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::variable_occurs_in_a_rhs ( const variable & v )

inline

Checks whether a variable v occurs in one of the rhs's of the current substitution.

Returns: A boolean indicating whether v occurs in sigma(x) for some variable x.

Definition at line 268 of file mutable_indexed_substitution.h.

◆ variables_occurring_in_right_hand_sides()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

const std::multiset< variable_type > & mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::variables_occurring_in_right_hand_sides ( ) const

inline

Provides a multiset containing the variables in the rhs.

Returns: A multiset with variables in the right hand side.

Definition at line 252 of file mutable_indexed_substitution.h.

Member Data Documentation

◆ is_identity_substitution

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

constexpr bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::is_identity_substitution =false

staticconstexpr

Definition at line 93 of file mutable_indexed_substitution.h.

◆ m_substitution

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

substitution_type mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::m_substitution

protected

Internal storage for substitutions. Required to be a container with random access through [] operator. It is essential to store the variable also in the container, as it might be that this variable is not used anywhere although it has a valid assignment. This happens for instance when the assignment is already parsed, while the expression to which it needs to be applied must still be parsed.

Definition at line 54 of file mutable_indexed_substitution.h.

◆ m_variables_in_rhs

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

std::multiset<variable> mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::m_variables_in_rhs

mutableprotected

Definition at line 56 of file mutable_indexed_substitution.h.

◆ m_variables_in_rhs_set_is_defined

template<typename VariableType = data::variable, typename ExpressionType = data_expression>

bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::m_variables_in_rhs_set_is_defined =false

mutableprotected

Definition at line 55 of file mutable_indexed_substitution.h.

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

data/include/mcrl2/data/substitutions/mutable_indexed_substitution.h

Classes

Public Types

Public Member Functions

Static Public Attributes

Protected Types

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ argument_type

◆ expression_type

◆ result_type

◆ substitution_type

◆ variable_type

Constructor & Destructor Documentation

◆ mutable_indexed_substitution() [1/3]

◆ mutable_indexed_substitution() [2/3]

◆ mutable_indexed_substitution() [3/3]

Member Function Documentation

◆ apply() [1/2]

◆ apply() [2/2]

◆ clear()

◆ clone()

◆ empty()

◆ operator()()

◆ operator==()

◆ operator[]()

◆ size()

◆ to_string()

◆ variable_occurs_in_a_rhs()

◆ variables_occurring_in_right_hand_sides()

Member Data Documentation

◆ is_identity_substitution

◆ m_substitution

◆ m_variables_in_rhs

◆ m_variables_in_rhs_set_is_defined