mcrl2::data::enumerator_list_element_with_substitution
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/data/enumerator.h

.. cpp:class:: mcrl2::data::enumerator_list_element_with_substitution

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

  

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

.. cpp:type:: mcrl2::data::enumerator_list_element_with_substitution::expression_type

  typedef for :cpp:type:`Expression`
  
  

  

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

.. cpp:member:: data::data_expression_list mcrl2::data::enumerator_list_element_with_substitution::m_expressions
  
  

  

.. cpp:member:: data::variable_list mcrl2::data::enumerator_list_element_with_substitution::m_variables
  
  

  

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

.. cpp:function:: void add_assignments(const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const
  
  Adds the assignments that correspond with this element to the substitution result. 

  

.. cpp:function:: data::data_expression_list assign_expressions(const VariableList &v, const Rewriter &rewriter) const
  
  Returns the right hand sides corresponding to the variables v. 

  
      
  **Pre:** variables in v must be contained in variables()

.. cpp:function:: enumerator_list_element_with_substitution()=default
  
  Default constructor. 

  

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

  

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

  

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

  

.. cpp:function:: void remove_assignments(const VariableList &v, MutableSubstitution &result) const
  
  Removes the assignments corresponding with this element from the substitution result. 

  

.. cpp:function:: data::enumerator_substitution sigma() const