index_traits.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// 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)
//
 
// By putting this outside the definition of MCRL2_ATERMPP_INDEX_TRAITS_H a failing header test is avoided.
#include "mcrl2/atermpp/standard_containers/detail/unordered_map_implementation.h"
 
#ifndef MCRL2_ATERMPP_INDEX_TRAITS_H
#define MCRL2_ATERMPP_INDEX_TRAITS_H
#pragma once
 
#include "mcrl2/atermpp/detail/aterm_configuration.h"
#include "mcrl2/atermpp/standard_containers/unordered_map.h"
 
namespace atermpp {
 
namespace detail {
 
template <typename Variable, typename KeyType>
atermpp::unordered_map<KeyType, std::size_t>& variable_index_map()
{
  static atermpp::unordered_map<KeyType, std::size_t> m;
  return m;
}
 
template <typename Variable, typename KeyType>
std::stack<std::size_t>& variable_map_free_numbers()
{
  static std::stack<std::size_t> s;
  return s;
}
 
template <typename Variable, typename KeyType>
std::mutex& variable_mutex()
{
  static std::mutex m;
  return m;
}
 
 
template <typename Variable, typename KeyType>
std::size_t& variable_map_max_index()
{
  static std::size_t s;
  return s;
}
 
template <typename Variable, typename KeyType, const int N>
struct index_traits
{
 
public:
  static inline
  std::size_t index(const Variable& x)
  {
    const _aterm_int* i = reinterpret_cast<const _aterm_int*>(address(x[N]));
    return i->value();
  }
 
  static inline
  std::size_t max_index()
  {
    return variable_map_max_index<Variable, KeyType>();
  }
 
  static inline
  std::size_t insert(const KeyType& x)
  {
    if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().lock(); }
 
    auto& m = variable_index_map<Variable, KeyType>();
    auto i = m.find(x);
    std::size_t value;
    if (i == m.end())
    {
      auto& s = variable_map_free_numbers<Variable, KeyType>();
      if (s.empty())
      {
        value = m.size();
        variable_map_max_index<Variable, KeyType>() = value;
      }
      else
      {
        value = s.top();
        s.pop();
      }
      m[x] = value;
    }
    else 
    {
      value = i->second;
    }
    if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().unlock(); }
    return value;
  }
 
  static inline
  void erase(const KeyType& x)
  {
    if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().lock(); }
 
    auto& m = variable_index_map<Variable, KeyType>();
    auto& s = variable_map_free_numbers<Variable, KeyType>();
    auto i = m.find(x);
    assert(i != m.end());
    s.push(i->second);
    m.erase(i);
 
    if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) { variable_mutex<Variable, KeyType>().unlock(); }
  }
 
  static inline
  std::size_t size()
  {
    auto& m = variable_index_map<Variable, KeyType>();
    return m.size();
  }
};
 
} // namespace detail
 
} // namespace atermpp
 
#endif // MCRL2_ATERMPP_INDEX_TRAITS_H