Line data    Source code

       1             : // Author(s): Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/substitutions/maintain_variables_in_rhs.h
      10             : /// \brief This class extends a substitution to recall the variables that occur in its right hand side. 
      11             : ///        It assumes the presence of an operation sigma[x]=v to set values of a variable. 
      12             : ///        If sigma[x]=x, this is seen as clearing the variable, and x is not recalled. 
      13             : ///        The variables recalled are an overapproximation. By regular garbage collection the 
      14             : 
      15             : 
      16             : #ifndef MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H
      17             : #define MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H
      18             : 
      19             : #include "mcrl2/data/is_simple_substitution.h"
      20             : #include "mcrl2/data/undefined.h"
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace data {
      25             : 
      26             : 
      27             : /// \brief Wrapper that extends any substitution to a substitution maintaining the vars in its rhs. 
      28             : /// \details This substitution assumes a function variable -> std::size_t, that, for
      29             : ///          each variable gives a unique index. The substitutions are stored
      30             : ///          internally as a vector, mapping std::size_t to expression.
      31             : ///          Provided that, given a variable, its index can be computed in O(1)
      32             : ///          time, insertion is O(1) amortized, and lookup is O(1).
      33             : ///          Memory required is O(n) where n is the largest index used.
      34             : template <typename Substitution>
      35             : class maintain_variables_in_rhs: public Substitution
      36             : {
      37             :   public:
      38             :     typedef Substitution super;
      39             :     typedef typename super::variable_type variable_type;
      40             :     typedef typename super::expression_type expression_type;
      41             :   
      42             :   protected:
      43             :     std::multiset<variable_type> m_variables_in_rhs;
      44             :     std::set<variable_type> m_scratch_set;
      45             :   
      46             :   public:
      47             :     /// \brief Default constructor
      48       21773 :     maintain_variables_in_rhs() 
      49       21773 :     {
      50       21773 :     }
      51             :   
      52             :     /// \brief Wrapper class for internal storage and substitution updates using operator()
      53             :     class assignment
      54             :     {
      55             :       protected: 
      56             :         const variable_type& m_variable;
      57             :         Substitution& m_sigma; 
      58             :         std::multiset<variable_type>& m_variables_in_rhs;
      59             :         std::set<variable_type>& m_scratch_set;
      60             :   
      61             :       public:
      62             :         /// \brief Constructor.
      63             :         /// \param[in] v A reference to the variable.
      64             :         /// \param[in] sigma A reference to the substitution.
      65             :         /// \param[in] variables_in_rhs Variables in the rhs of the assignments.
      66             :         /// \param[in] scratch_set A set used for locally for computations.
      67        8604 :         assignment(const variable_type& v,
      68             :                    Substitution& sigma,
      69             :                    std::multiset<variable_type>& variables_in_rhs,
      70             :                    std::set<variable_type>& scratch_set) :
      71        8604 :           m_variable(v),
      72        8604 :           m_sigma(sigma),
      73        8604 :           m_variables_in_rhs(variables_in_rhs),
      74        8604 :           m_scratch_set(scratch_set)
      75        8604 :         { }
      76             :   
      77             :         /// \brief Actual assignment
      78        8604 :         void operator=(const expression_type& e)
      79             :         {
      80        8604 :           assert(e.defined());
      81             : 
      82        8604 :           const expression_type& e_old=m_sigma(m_variable);
      83        8604 :           if (e_old!=m_variable)
      84             :           {
      85             :             // Remove the free variables in the old rhs.
      86         100 :             m_scratch_set=find_free_variables(e_old);
      87         200 :             for(const variable_type& v: m_scratch_set) 
      88             :             {
      89         100 :               m_variables_in_rhs.erase(v);
      90             :             }
      91         100 :             m_scratch_set.clear();
      92             :           }
      93        8604 :           if (e != m_variable)
      94             :           {
      95             :             // Add the free variables in the new rhs.
      96        7411 :             m_scratch_set=find_free_variables(e);
      97        7411 :             m_variables_in_rhs.insert(m_scratch_set.begin(),m_scratch_set.end());
      98        7411 :             m_scratch_set.clear();
      99             :           }
     100             :           // Set the new variable;
     101        8604 :           m_sigma.operator[](m_variable)=e; 
     102        8604 :         }
     103             :     };
     104             :   
     105             :     /// \brief Assigment operator.
     106             :     /// \param v The variable to which the assignment is carried out. 
     107        8604 :     assignment operator[](variable_type const& v)
     108             :     {
     109        8604 :       return assignment(v, *this, m_variables_in_rhs, m_scratch_set);
     110             :     }
     111             :   
     112             :     /// \brief Clear substitutions.
     113             :     void clear()
     114             :     {
     115             :       m_variables_in_rhs().clear();
     116             :       super::clear();
     117             :     }
     118             :   
     119             :     /// \brief Provides a set of variables that occur in the right hand sides of the assignments.
     120             :     const std::multiset<variable>& variables_in_rhs()
     121             :     {
     122             :       return m_variables_in_rhs;
     123             :     }
     124             : 
     125             :     /// \brief Indicates whether a variable occurs in some rhs of this substitution. 
     126             :     /// \param v The variable for which occurrence in a rhs is checked.
     127         100 :     bool variable_occurs_in_a_rhs(const variable_type& v)
     128             :     {
     129         100 :       return m_variables_in_rhs.find(v)!=m_variables_in_rhs.end();
     130             :     }
     131             : 
     132             : };
     133             : 
     134             : } // namespace data
     135             : 
     136             : } // namespace mcrl2
     137             : 
     138             : #endif // MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H