Line data    Source code

       1             : // Author(s): 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/map_substitution.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_SUBSTITUTIONS_MAP_SUBSTITUTION_H
      13             : #define MCRL2_DATA_SUBSTITUTIONS_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.
      24             : template <typename AssociativeContainer>
      25             : struct map_substitution
      26             : {
      27             :   typedef typename AssociativeContainer::key_type variable_type;
      28             :   typedef typename AssociativeContainer::mapped_type expression_type;
      29             :   using argument_type = variable_type;
      30             :   using result_type = expression_type;
      31             : 
      32             :   const AssociativeContainer& m_map;
      33             : 
      34          54 :   map_substitution(const AssociativeContainer& m)
      35          54 :     : m_map(m)
      36          54 :   { }
      37             : 
      38          88 :   const expression_type operator()(const variable_type& v) const
      39             :   {
      40          88 :     typename AssociativeContainer::const_iterator i = m_map.find(v);
      41          88 :     if (i == m_map.end())
      42             :     {
      43           2 :       return v;
      44             :     }
      45             :     else
      46             :     {
      47          86 :       return i->second;
      48             :     }
      49             :     // N.B. This does not work!
      50             :     // return i == m_map.end() ? v : i->second;
      51             :   }
      52             : 
      53             :   std::string to_string() const
      54             :   {
      55             :     std::ostringstream out;
      56             :     out << "[";
      57             :     for (typename AssociativeContainer::const_iterator i = m_map.begin(); i != m_map.end(); ++i)
      58             :     {
      59             :       out << (i == m_map.begin() ? "" : "; ") << i->first << ":" << i->first.sort() << " := " << i->second;
      60             :     }
      61             :     out << "]";
      62             :     return out.str();
      63             :   }
      64             : };
      65             : 
      66             : /// \brief Utility function for creating a map_substitution.
      67             : template <typename AssociativeContainer>
      68             : map_substitution<AssociativeContainer>
      69          54 : make_map_substitution(const AssociativeContainer& m)
      70             : {
      71          54 :   return map_substitution<AssociativeContainer>(m);
      72             : }
      73             : 
      74             : template <typename AssociativeContainer>
      75           0 : std::set<data::variable> substitution_variables(const map_substitution<AssociativeContainer>& sigma)
      76             : {
      77           0 :   std::set<data::variable> result;
      78           0 :   for (const auto& [key, value]: sigma.m_map)
      79             :   {
      80           0 :     data::find_free_variables(value, std::inserter(result, result.end()));
      81             :   }
      82           0 :   return result;
      83           0 : }
      84             : 
      85             : template <typename AssociativeContainer>
      86             : bool is_simple_substitution(const map_substitution<AssociativeContainer>& sigma)
      87             : {
      88             :   for (auto i = sigma.m_map.begin(); i != sigma.m_map.end(); ++i)
      89             :   {
      90             :     if (!is_simple_substitution(i->first, i->second))
      91             :     {
      92             :       return false;
      93             :     }
      94             :   }
      95             :   return true;
      96             : }
      97             : 
      98             : } // namespace data
      99             : 
     100             : } // namespace mcrl2
     101             : 
     102             : #endif // MCRL2_DATA_SUBSTITUTIONS_MAP_SUBSTITUTION_H