Line data    Source code

       1             : // Author(s): Maurice Laveaux.
       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             : #ifndef DETAIL_FUNCTION_SYMBOL_POOL_H
      11             : #define DETAIL_FUNCTION_SYMBOL_POOL_H
      12             : 
      13             : #include "mcrl2/atermpp/detail/function_symbol_hash.h"
      14             : #include "mcrl2/utilities/cache_metric.h"
      15             : #include "mcrl2/utilities/unordered_set.h"
      16             : #include "mcrl2/utilities/mutex.h"
      17             : 
      18             : namespace atermpp
      19             : {
      20             : namespace detail
      21             : {
      22             : 
      23             : /// \brief This class stores a set of function symbols.
      24             : class function_symbol_pool : private mcrl2::utilities::noncopyable
      25             : {
      26             : public:
      27             :   function_symbol_pool();
      28             : 
      29             :   /// \brief Creates a function symbol pair (name, arity), returns a pointer to an existing element
      30             :   ///        if this pair is already defined.
      31             :   /// \param check_for_registered_functions Check whether there is a registered prefix p such that
      32             :   ///           name equal pn where n is a number. In that case prevent that pn will be generated
      33             :   ///           as a fresh function name.
      34             :   /// \threadsafe
      35             :   function_symbol create(const std::string& name, const std::size_t arity, const bool check_for_registered_functions = false);
      36             :   function_symbol create(std::string&& name, const std::size_t arity, const bool check_for_registered_functions = false);
      37             : 
      38             :   /// \brief Restore the index back to index before registering this prefix.
      39             :   /// \threadsafe
      40             :   void deregister(const std::string& prefix);
      41             : 
      42             :   /// \returns An index that is always a safe index for the given prefix.
      43             :   /// \todo These functions are all used by the function_symbol_generator and should probably not
      44             :   ///       be public.
      45             :   /// \threadsafe
      46             :   std::shared_ptr<std::size_t> register_prefix(const std::string& prefix);
      47             : 
      48             :   /// \brief Resize the function symbol pool if necessary.
      49             :   void resize_if_needed();
      50             : 
      51             :   /// \brief Get an index such that no function symbol with name prefix + returned value
      52             :   ///        and any value above it already exists.
      53             :   std::size_t get_sufficiently_large_postfix_index(const std::string& prefix) const;
      54             : 
      55             :   /// \brief Collect all garbage function symbols.
      56             :   void sweep();
      57             : 
      58             :   /// \returns The function symbol used by integral terms.
      59         143 :   const function_symbol& as_int() noexcept { return m_as_int; }
      60             : 
      61             :   /// \returns The function symbol used by the list constructor.
      62  6923269673 :   const function_symbol& as_list() noexcept { return m_as_list; }
      63             : 
      64             :   /// \returns The function symbol used by the term indicating the empty list.
      65  2378655287 :   const function_symbol& as_empty_list() noexcept { return m_as_empty_list; }
      66             : 
      67             :   /// \returns The number of function symbols stored in this pool.
      68        1015 :   std::size_t size() const noexcept { return m_symbol_set.size(); }
      69             :   
      70             :   /// \returns The maximum number of function symbols stored in this pool.
      71          38 :   std::size_t capacity() const noexcept { return m_symbol_set.capacity(); }
      72             : 
      73             : private:
      74             :   using unordered_set = mcrl2::utilities::unordered_set<
      75             :     _function_symbol,
      76             :     function_symbol_hasher,
      77             :     function_symbol_equals,
      78             :     typename std::conditional_t<EnableBlockAllocator, 
      79             :       mcrl2::utilities::block_allocator<_function_symbol, 1024, mcrl2::utilities::detail::GlobalThreadSafe>, 
      80             :       std::allocator<_function_symbol>>,
      81             :     mcrl2::utilities::detail::GlobalThreadSafe,
      82             :     false>;
      83             : 
      84             :   /// \brief Stores the underlying function symbols.
      85             :   unordered_set m_symbol_set;
      86             : 
      87             :   /// \brief A map that records a function for each prefix that must be called to set the
      88             :   ///        postfix number to a sufficiently high number if a function symbol with the same
      89             :   ///        prefix string is registered.
      90             :   std::map<std::string, std::shared_ptr<std::size_t>> m_prefix_to_register_function_map;
      91             : 
      92             :   mutable mcrl2::utilities::mutex m_mutex; // Mutex for m_prefix_to_register_function_map.
      93             : 
      94             :   // Default function symbols.
      95             :   function_symbol m_as_int;
      96             :   function_symbol m_as_list;
      97             :   function_symbol m_as_empty_list;
      98             : 
      99             :   // Various performance metrics.
     100             :   mcrl2::utilities::cache_metric m_function_symbol_metrics; ///< Track the number of function symbols found in or added to the set.
     101             : 
     102             :   // Create helper function. 
     103             :   void create_helper(const std::string& name);
     104             : };
     105             : 
     106             : 
     107             : } // namespace detail
     108             : } // namespace atermpp
     109             : 
     110             : #endif // DETAIL_FUNCTION_SYMBOL_POOL_H
     111             :