LCOV - code coverage report
Current view: top level - atermpp/include/mcrl2/atermpp - function_symbol_generator.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 32 32 100.0 %
Date: 2024-03-08 02:52:28 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink, Jan Friso Groote
       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/atermpp/function_symbol_generator.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_ATERMPP_FUNCTION_SYMBOL_GENERATOR_H
      13             : #define MCRL2_ATERMPP_FUNCTION_SYMBOL_GENERATOR_H
      14             : 
      15             : #include "mcrl2/atermpp/detail/global_aterm_pool.h"
      16             : 
      17             : #include <cctype>
      18             : 
      19             : namespace atermpp {
      20             : 
      21       10286 : static inline std::mutex& function_symbol_generator_mutex()
      22             : {
      23             :   static std::mutex m_function_symbol_generator_mutex;
      24       10286 :   return m_function_symbol_generator_mutex;
      25             : }
      26             : 
      27        7453 : static inline std::size_t& generator_sequence_number()
      28             : {
      29             :   static size_t n=0;
      30        7453 :   return n;
      31             : }
      32             : 
      33             : 
      34             : /// \brief Generates unique function symbols with a given prefix.
      35             : class function_symbol_generator // : private mcrl2::utilities::noncopyable
      36             : {
      37             : protected:
      38             :   std::string m_prefix;
      39             : 
      40             :   /// \brief Cache the value that is set in the constructor
      41             :   std::size_t m_initial_index;
      42             : 
      43             :   /// \brief A local string cache to prevent allocating new strings for every function symbol generated.
      44             :   std::string m_string_buffer;
      45             : 
      46             :   /// \brief A reference to the index as present in the function symbol generator.
      47             :   std::size_t m_index;
      48             : 
      49             :   /// \brief The address of the central index for this prefix.
      50             :   std::shared_ptr<std::size_t> m_central_index;
      51             : 
      52             : public:
      53             :   /// \brief Constructor
      54             :   /// \param[in] prefix The prefix of the generated generated strings.
      55             :   /// \pre The prefix may not be empty, and it may not have trailing digits
      56        2505 :   function_symbol_generator(const std::string& prefix)
      57        2505 :   {
      58        2505 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) function_symbol_generator_mutex().lock();
      59             : 
      60        2505 :     m_prefix=prefix + (generator_sequence_number()>0?std::to_string(generator_sequence_number()) + "_":"");
      61        2505 :     generator_sequence_number()++;
      62        2505 :     m_string_buffer=m_prefix;
      63        2505 :     assert(!prefix.empty() && !(std::isdigit(*prefix.rbegin())));
      64             : 
      65             :     // Obtain a reference to the first index possible.
      66        2505 :     m_central_index = detail::g_term_pool().get_symbol_pool().register_prefix(m_prefix);
      67        2505 :     m_index = *m_central_index;
      68             : 
      69        2505 :     m_initial_index = m_index;
      70             : 
      71        2505 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) function_symbol_generator_mutex().unlock();
      72        2505 :   }
      73             : 
      74             :   /// \brief Restores the index back to the value that was initially assigned in the constructor.
      75             : 
      76       16620 :   void clear()
      77             :   {
      78       16620 :     m_index = m_initial_index;
      79       16620 :   } 
      80             : 
      81        2638 :   ~function_symbol_generator()
      82             :   {
      83        2638 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) function_symbol_generator_mutex().lock();
      84        2638 :     detail::g_term_pool().get_symbol_pool().deregister(m_prefix);
      85        2638 :     if constexpr (mcrl2::utilities::detail::GlobalThreadSafe) function_symbol_generator_mutex().unlock();
      86        2638 :   }
      87             : 
      88             :   /// \brief Generates a unique function symbol with the given prefix followed by a number.
      89       23644 :   function_symbol operator()(std::size_t arity = 0)
      90             :   {
      91             :     // Check whether in the meantime other variables have been used with the same prefix. 
      92             :     // if (m_index<=*detail::g_term_pool().get_symbol_pool().register_prefix(m_prefix))
      93       23644 :     if (m_index<=*m_central_index)
      94             :     {
      95             :       // m_index=*detail::g_term_pool().get_symbol_pool().register_prefix(m_prefix);
      96         147 :       m_index=*m_central_index;
      97         147 :       m_initial_index=m_index;
      98             :     } 
      99             :     // Put the number m_index after the prefix in the string buffer.
     100       23644 :     mcrl2::utilities::number2string(m_index, m_string_buffer, m_prefix.size());
     101             : 
     102             :     // Increase the index.
     103       23644 :     ++m_index;
     104             : 
     105             :     // Generate a new function symbol with prefix + index.
     106       23644 :     function_symbol f(m_string_buffer, arity, false);
     107       23644 :     return f;
     108             :   }
     109             : };
     110             : 
     111             : } // namespace atermpp
     112             : 
     113             : #endif // MCRL2_ATERMPP_FUNCTION_SYMBOL_GENERATOR_H

Generated by: LCOV version 1.14