mCRL2
Loading...
Searching...
No Matches
mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType > Class Template Reference

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

typedef VariableType variable_type
 Type of variables.
 
typedef ExpressionType expression_type
 Type of expressions.
 
using argument_type = variable_type
 
using result_type = expression_type
 

Public Member Functions

 mutable_indexed_substitution ()
 Default constructor.
 
 mutable_indexed_substitution (const substitution_type &substitution, const bool variables_in_rhs_set_is_defined, const std::multiset< variable_type > &variables_in_rhs)
 
const expression_typeoperator() (const variable_type &v) const
 Application operator; applies substitution to v.
 
template<class ResultType >
void apply (const variable_type &v, ResultType &target)
 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<typename 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!
 

Protected Types

typedef atermpp::utilities::unordered_map< VariableType, ExpressionType > substitution_type
 

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
 
std::multiset< variablem_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 44 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 67 of file mutable_indexed_substitution.h.

◆ expression_type

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

Type of expressions.

Definition at line 65 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 68 of file mutable_indexed_substitution.h.

◆ substitution_type

template<typename VariableType = data::variable, typename ExpressionType = data_expression>
typedef atermpp::utilities::unordered_map< VariableType, ExpressionType > mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::substitution_type
protected

Definition at line 47 of file mutable_indexed_substitution.h.

◆ variable_type

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

Type of variables.

Definition at line 62 of file mutable_indexed_substitution.h.

Constructor & Destructor Documentation

◆ mutable_indexed_substitution() [1/2]

template<typename VariableType = data::variable, typename ExpressionType = data_expression>
mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::mutable_indexed_substitution ( )
inline

Default constructor.

Definition at line 71 of file mutable_indexed_substitution.h.

◆ mutable_indexed_substitution() [2/2]

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 76 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
vThe variable to which the subsitution is applied.
targetThe target into which the substitution is stored.

Definition at line 194 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 
)
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
vThe variable to which the subsitution is applied.
targetThe target into which the substitution is stored.

Definition at line 175 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 214 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 226 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 270 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
vThe 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 156 of file mutable_indexed_substitution.h.

◆ operator==()

template<typename VariableType = data::variable, typename ExpressionType = data_expression>
template<typename Substitution >
bool mcrl2::data::mutable_indexed_substitution< VariableType, ExpressionType >::operator== ( const Substitution &  ) const
inline

Compare substitutions.

Definition at line 234 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 208 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 264 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 277 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 257 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 241 of file mutable_indexed_substitution.h.

Member Data Documentation

◆ 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 55 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 57 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
mutableprotected

Definition at line 56 of file mutable_indexed_substitution.h.


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