maintain_variables_in_rhs.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
 
#ifndef MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H
#define MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H
 
#include "mcrl2/data/is_simple_substitution.h"
#include "mcrl2/data/undefined.h"
 
namespace mcrl2 {
 
namespace data {
 
 
template <typename Substitution>
class maintain_variables_in_rhs: public Substitution
{
  public:
    typedef Substitution super;
    typedef typename super::variable_type variable_type;
    typedef typename super::expression_type expression_type;
  
  protected:
    std::multiset<variable_type> m_variables_in_rhs;
    std::set<variable_type> m_scratch_set;
  
  public:
    maintain_variables_in_rhs() 
    {
    }
  
    class assignment
    {
      protected: 
        const variable_type& m_variable;
        Substitution& m_sigma; 
        std::multiset<variable_type>& m_variables_in_rhs;
        std::set<variable_type>& m_scratch_set;
  
      public:
        assignment(const variable_type& v,
                   Substitution& sigma,
                   std::multiset<variable_type>& variables_in_rhs,
                   std::set<variable_type>& scratch_set) :
          m_variable(v),
          m_sigma(sigma),
          m_variables_in_rhs(variables_in_rhs),
          m_scratch_set(scratch_set)
        { }
  
        void operator=(const expression_type& e)
        {
          assert(e.defined());
 
          const expression_type& e_old=m_sigma(m_variable);
          if (e_old!=m_variable)
          {
            // Remove the free variables in the old rhs.
            m_scratch_set=find_free_variables(e_old);
            for(const variable_type& v: m_scratch_set) 
            {
              m_variables_in_rhs.erase(v);
            }
            m_scratch_set.clear();
          }
          if (e != m_variable)
          {
            // Add the free variables in the new rhs.
            m_scratch_set=find_free_variables(e);
            m_variables_in_rhs.insert(m_scratch_set.begin(),m_scratch_set.end());
            m_scratch_set.clear();
          }
          // Set the new variable;
          m_sigma.operator[](m_variable)=e; 
        }
    };
  
    assignment operator[](variable_type const& v)
    {
      return assignment(v, *this, m_variables_in_rhs, m_scratch_set);
    }
  
    void clear()
    {
      m_variables_in_rhs().clear();
      super::clear();
    }
  
    const std::multiset<variable>& variables_in_rhs()
    {
      return m_variables_in_rhs;
    }
 
    bool variable_occurs_in_a_rhs(const variable_type& v)
    {
      return m_variables_in_rhs.find(v)!=m_variables_in_rhs.end();
    }
 
};
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_SUBSTITUTIONS_MAINTAIN_VARIABLES_IN_RHS_H