mcrl2::data::mutable_indexed_substitution
===============================================================================


Include file:

.. code-block:: c++

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

.. cpp:class:: mcrl2::data::mutable_indexed_substitution

  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. 

Protected types
-------------------------------------------------------------------------------

.. cpp:type:: mcrl2::data::mutable_indexed_substitution::substitution_type

  typedef for :cpp:type:`std::pair\< VariableType, ExpressionType >`
  
  

  

Public types
-------------------------------------------------------------------------------

.. cpp:type:: mcrl2::data::mutable_indexed_substitution::argument_type

  typedef for :cpp:type:`variable_type`
  
  

  

.. cpp:type:: mcrl2::data::mutable_indexed_substitution::expression_type

  typedef for :cpp:type:`ExpressionType`
  
  Type of expressions. 

  

.. cpp:type:: mcrl2::data::mutable_indexed_substitution::variable_type

  typedef for :cpp:type:`VariableType`
  
  Type of variables. 

  

Protected attributes
-------------------------------------------------------------------------------

.. cpp:member:: std::vector< substitution_type > mcrl2::data::mutable_indexed_substitution::m_container
  
  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. 

  

.. cpp:member:: std::stack< std::size_t > mcrl2::data::mutable_indexed_substitution::m_free_positions
  
  

  

.. cpp:member:: std::vector< std::size_t > mcrl2::data::mutable_indexed_substitution::m_index_table
  
  

  

.. cpp:member:: std::multiset< variable > mcrl2::data::mutable_indexed_substitution::m_variables_in_rhs
  
  

  

.. cpp:member:: bool mcrl2::data::mutable_indexed_substitution::m_variables_in_rhs_set_is_defined
  
  

  

Public member functions
-------------------------------------------------------------------------------

.. cpp:function:: void clear()
  
  Clear substitutions. 

  

.. cpp:function:: bool empty()
  
  Returns true if the substitution is empty. 

  

.. cpp:function:: mutable_indexed_substitution()
  
  Default constructor. 

  

.. cpp:function:: const expression_type operator()(const variable_type &v) const
  
  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. 

.. cpp:function:: bool operator==(const Substitution &) const
  
  Compare substitutions. 

  

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

  

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

  

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

  

.. cpp:function:: 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. 

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

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

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