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