Line data    Source code

       1             : // Author(s): Jeroen van der Wulp, Wieger Wesselink
       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/mutable_map_substitution.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
      13             : #define MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
      14             : 
      15             : #include "mcrl2/data/is_simple_substitution.h"
      16             : #include "mcrl2/data/undefined.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace data {
      21             : 
      22             : /// \brief Generic substitution function. The substitution is stored as a mapping
      23             : /// of variables to expressions. The substitution is mutable, meaning that substitutions
      24             : /// to variables can be added and removed as follows:
      25             : ///\verbatim
      26             : /// mutable_map_substitution sigma;
      27             : /// mutable_map_substitution::variable_type v;
      28             : /// mutable_map_substitution::expression_type e;
      29             : /// sigma[v] = e; // add the assignment of e to v
      30             : /// sigma[v] = v; // remove the assignment to v
      31             : ///\endverbatim
      32             : template <typename AssociativeContainer = std::map<variable,data_expression> >
      33             : class mutable_map_substitution
      34             : {
      35             : protected:
      36             :   AssociativeContainer m_map;
      37             : 
      38             : public:
      39             :   typedef typename AssociativeContainer::key_type variable_type;
      40             :   typedef typename AssociativeContainer::mapped_type expression_type;
      41             :   typedef typename AssociativeContainer::const_iterator const_iterator;
      42             :   typedef typename AssociativeContainer::iterator iterator;
      43             :   using argument_type = variable_type;
      44             :   using result_type = expression_type;
      45             : 
      46             :   /// \brief Wrapper class for internal storage and substitution updates using operator()
      47             :   struct assignment
      48             :   {
      49             :     typename AssociativeContainer::key_type m_variable;
      50             :     AssociativeContainer&                   m_map;
      51             : 
      52             :     /// \brief Constructor.
      53             :     ///
      54             :     /// \param[in] v a variable.
      55             :     /// \param[in] m a mapping of variables to expressions.
      56       31822 :     assignment(typename AssociativeContainer::key_type v, AssociativeContainer& m) :
      57       31822 :       m_variable(v), m_map(m)
      58       31822 :     { }
      59             : 
      60             :     template <typename AssignableToExpression>
      61       31822 :     assignment& operator=(AssignableToExpression const& e)
      62             :     {
      63       31822 :       mCRL2log(log::trace) << "Setting " << m_variable << " := " << e << std::endl;
      64       31822 :       if (e != m_variable)
      65             :       {
      66       22512 :         m_map[m_variable] = e;
      67             :       }
      68             :       else
      69             :       {
      70        9310 :         m_map.erase(m_variable);
      71             :       }
      72       31822 :       return *this;
      73             :     }
      74             :   };
      75             : 
      76       47257 :   mutable_map_substitution() = default;
      77             : 
      78           1 :   explicit mutable_map_substitution(const AssociativeContainer& m)
      79           1 :     : m_map(m)
      80           1 :   {}
      81             : 
      82             :   template <typename VariableContainer, typename ExpressionContainer>
      83           1 :   mutable_map_substitution(VariableContainer const& variables, ExpressionContainer const& expressions)
      84           1 :   {
      85           1 :     assert(variables.size() == expressions.size());
      86           1 :     auto j = expressions.begin();
      87           4 :     for (auto i = variables.begin(); i != variables.end(); ++i, ++j)
      88             :     {
      89           3 :       m_map[*i] = *j;
      90             :     }
      91           1 :   }
      92             : 
      93      163641 :   expression_type operator()(const variable_type& v) const
      94             :   {
      95      163641 :     auto i = m_map.find(v);
      96      163641 :     if (i == m_map.end())
      97             :     {
      98      128131 :       return v;
      99             :     }
     100             :     else
     101             :     {
     102       35510 :       return i->second;
     103             :     }
     104             :   }
     105             : 
     106       31822 :   assignment operator[](variable_type const& v)
     107             :   {
     108       31822 :     return assignment(v, this->m_map);
     109             :   }
     110             : 
     111             :   /// \brief Resets the substitution by letting every variable yield itself. Cf. clear() of a map.
     112             :   ///
     113         137 :   void clear()
     114             :   {
     115         137 :     m_map.clear();
     116         137 :   }
     117             : 
     118             :   template <typename Substitution>
     119             :   bool operator==(const Substitution&) const
     120             :   {
     121             :     return false;
     122             :   }
     123             : 
     124             :   /// \brief Returns an iterator pointing to the beginning of the sequence of assignments
     125             :   /// TODO: should become protected
     126        9361 :   const_iterator begin() const
     127             :   {
     128        9361 :     return m_map.begin();
     129             :   }
     130             : 
     131             :   /// \brief Returns an iterator pointing past the end of the sequence of assignments
     132             :   /// TODO: should become protected
     133       10436 :   const_iterator end() const
     134             :   {
     135       10436 :     return m_map.end();
     136             :   }
     137             : 
     138             :   /// \brief Returns an iterator pointing to the beginning of the sequence of assignments
     139             :   /// TODO: should become protected
     140        1609 :   iterator begin()
     141             :   {
     142        1609 :     return this->m_map.begin();
     143             :   }
     144             : 
     145             :   /// \brief Returns an iterator pointing past the end of the sequence of assignments
     146             :   /// TODO: should become protected
     147        1969 :   iterator end()
     148             :   {
     149        1969 :     return this->m_map.end();
     150             :   }
     151             : 
     152             :   /// \brief Returns true if the substitution is empty
     153         274 :   bool empty()
     154             :   {
     155         274 :     return m_map.empty();
     156             :   }
     157             : 
     158         113 :   std::string to_string() const
     159             :   {
     160         113 :     std::stringstream result;
     161         113 :     result << "[";
     162         223 :     for (auto i = begin(); i != end(); ++i)
     163             :     {
     164         110 :       result << (i == begin() ? "" : "; ") << i->first << ":" << i->first.sort() << " := " << i->second;
     165             :     }
     166         113 :     result << "]";
     167         226 :     return result.str();
     168         113 :   }
     169             : 
     170             :   /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end()
     171             :   iterator find(variable_type const& v)
     172             :   {
     173             :     return this->m_map.find(v);
     174             :   }
     175             : 
     176             :   /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end()
     177             :   const_iterator find(variable_type const& v) const
     178             :   {
     179             :     return m_map.find(v);
     180             :   }
     181             : };
     182             : 
     183             : /// \brief Utility function for creating a mutable_map_substitution.
     184             : template <typename VariableContainer, typename ExpressionContainer, typename MapContainer>
     185             : mutable_map_substitution<MapContainer>
     186             : make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
     187             : {
     188             :   return mutable_map_substitution<MapContainer>(vc, ec);
     189             : }
     190             : 
     191             : template <typename VariableContainer, typename ExpressionContainer>
     192             : mutable_map_substitution<std::map<typename VariableContainer::value_type, typename ExpressionContainer::value_type> >
     193           1 : make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
     194             : {
     195           1 :   return mutable_map_substitution<std::map<typename VariableContainer::value_type, typename ExpressionContainer::value_type> >(vc, ec);
     196             : }
     197             : 
     198             : template <typename AssociativeContainer>
     199         113 : std::ostream& operator<<(std::ostream& out, const mutable_map_substitution<AssociativeContainer>& sigma)
     200             : {
     201         113 :   return out << sigma.to_string();
     202             : }
     203             : 
     204             : std::set<data::variable> substitution_variables(const mutable_map_substitution<>& sigma);
     205             : 
     206             : template <typename AssociativeContainer>
     207         415 : bool is_simple_substitution(const mutable_map_substitution<AssociativeContainer>& sigma)
     208             : {
     209        1490 :   for (auto i = sigma.begin(); i != sigma.end(); ++i)
     210             :   {
     211        1075 :     if (!is_simple_substitution(i->first, i->second))
     212             :     {
     213           0 :       return false;
     214             :     }
     215             :   }
     216         415 :   return true;
     217             : }
     218             : 
     219             : } // namespace data
     220             : 
     221             : } // namespace mcrl2
     222             : 
     223             : #endif // MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H