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             : 
      10             : // By putting this outside the definition of MCRL2_ATERMPP_INDEX_TRAITS_H a failing header test is avoided.
      11             : #include "mcrl2/atermpp/standard_containers/detail/unordered_map_implementation.h"
      12             : 
      13             : #ifndef MCRL2_ATERMPP_INDEX_TRAITS_H
      14             : #define MCRL2_ATERMPP_INDEX_TRAITS_H
      15             : #pragma once
      16             : 
      17             : #include "mcrl2/atermpp/detail/aterm_configuration.h"
      18             : #include "mcrl2/atermpp/standard_containers/unordered_map.h"
      19             : 
      20             : namespace atermpp {
      21             : 
      22             : namespace detail {
      23             : 
      24             : template <typename Variable, typename KeyType>
      25    19721037 : atermpp::unordered_map<KeyType, std::size_t>& variable_index_map()
      26             : {
      27    19721037 :   static atermpp::unordered_map<KeyType, std::size_t> m;
      28    19721037 :   return m;
      29             : }
      30             : 
      31             : template <typename Variable, typename KeyType>
      32       42853 : std::stack<std::size_t>& variable_map_free_numbers()
      33             : {
      34       42853 :   static std::stack<std::size_t> s;
      35       42853 :   return s;
      36             : }
      37             : 
      38             : template <typename Variable, typename KeyType>
      39    39442074 : std::mutex& variable_mutex()
      40             : {
      41             :   static std::mutex m;
      42    39442074 :   return m;
      43             : }
      44             : 
      45             : 
      46             : template <typename Variable, typename KeyType>
      47       42858 : std::size_t& variable_map_max_index()
      48             : {
      49             :   static std::size_t s;
      50       42858 :   return s;
      51             : }
      52             : 
      53             : /// \brief For several variable types in mCRL2 an implicit mapping of these variables
      54             : /// to integers is available. This is done for efficiency reasons. Examples are:
      55             : ///
      56             : /// data::variable, process::process_identifier
      57             : ///
      58             : /// The class index_traits is used to implement this mapping. A traits class was chosen to
      59             : /// prevent pollution of the public interface of the classes that represent these variables.
      60             : ///
      61             : /// N is the position of the index in the aterm_appl.
      62             : template <typename Variable, typename KeyType, const int N>
      63             : struct index_traits
      64             : {
      65             : 
      66             : public:
      67             :   /// \brief Returns the index of the variable.
      68             :   static inline
      69     2154856 :   std::size_t index(const Variable& x)
      70             :   {
      71     2154856 :     const _aterm_int* i = reinterpret_cast<const _aterm_int*>(address(x[N]));
      72     2154856 :     return i->value();
      73             :   }
      74             : 
      75             :   /// \brief Returns an upper bound for the largest index of a variable that is currently in use.
      76             :   static inline
      77           5 :   std::size_t max_index()
      78             :   {
      79           5 :     return variable_map_max_index<Variable, KeyType>();
      80             :   }
      81             : 
      82             :   /// \brief Note: intended for internal use only!
      83             :   /// Returns the index of the variable. If the variable was not already in the map, it is added.
      84             :   static inline
      85    19721037 :   std::size_t insert(const KeyType& x)
      86             :   {
      87    19721037 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().lock(); }
      88             : 
      89    19721037 :     auto& m = variable_index_map<Variable, KeyType>();
      90    19721037 :     auto i = m.find(x);
      91             :     std::size_t value;
      92    19721037 :     if (i == m.end())
      93             :     {
      94       42853 :       auto& s = variable_map_free_numbers<Variable, KeyType>();
      95       42853 :       if (s.empty())
      96             :       {
      97       42853 :         value = m.size();
      98       42853 :         variable_map_max_index<Variable, KeyType>() = value;
      99             :       }
     100             :       else
     101             :       {
     102           0 :         value = s.top();
     103           0 :         s.pop();
     104             :       }
     105       42853 :       m[x] = value;
     106             :     }
     107             :     else 
     108             :     {
     109    19678184 :       value = i->second;
     110             :     }
     111    19721037 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().unlock(); }
     112    19721037 :     return value;
     113             :   }
     114             : 
     115             :   /// \brief Note: intended for internal use only!
     116             :   /// Removes the variable from the index map.
     117             :   static inline
     118             :   void erase(const KeyType& x)
     119             :   {
     120             :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().lock(); }
     121             : 
     122             :     auto& m = variable_index_map<Variable, KeyType>();
     123             :     auto& s = variable_map_free_numbers<Variable, KeyType>();
     124             :     auto i = m.find(x);
     125             :     assert(i != m.end());
     126             :     s.push(i->second);
     127             :     m.erase(i);
     128             : 
     129             :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().unlock(); }
     130             :   }
     131             : 
     132             :   /// \brief Note: intended for internal use only!
     133             :   /// Provides the size of the variable index map.
     134             :   static inline
     135             :   std::size_t size()
     136             :   {
     137             :     auto& m = variable_index_map<Variable, KeyType>();
     138             :     return m.size();
     139             :   }
     140             : };
     141             : 
     142             : } // namespace detail
     143             : 
     144             : } // namespace atermpp
     145             : 
     146             : #endif // MCRL2_ATERMPP_INDEX_TRAITS_H