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 : /// \file mcrl2/data/identifier_generator.h 10 : /// \brief The class identifier_generator. 11 : 12 : #ifndef MCRL2_DATA_IDENTIFIER_GENERATOR_H 13 : #define MCRL2_DATA_IDENTIFIER_GENERATOR_H 14 : 15 : #include "mcrl2/core/identifier_string.h" 16 : #include "mcrl2/utilities/number_postfix_generator.h" 17 : 18 : namespace mcrl2 19 : { 20 : 21 : namespace data 22 : { 23 : 24 : /// \brief Abstract base class for identifier generators. 25 : /// Identifier generators generate fresh names that do not appear in a 26 : /// given context. 27 : /// A context is maintained containing already used identifiers. 28 : /// Using the operator()() and operator()(std::string) fresh 29 : /// identifiers are generated that do not appear in the context. 30 : template <typename Generator = utilities::number_postfix_generator> 31 : class identifier_generator 32 : { 33 : protected: 34 : Generator m_generator; 35 : 36 : public: 37 : /// \brief Constructor. 38 29948 : identifier_generator() = default; 39 : 40 : /// \brief Destructor. 41 29948 : virtual ~identifier_generator() = default; 42 : 43 : /// \brief Clears the context. 44 : virtual void clear_context() = 0; 45 : 46 : /// \brief Adds the identifier s to the context. 47 : /// \param s An identifier. 48 : virtual void add_identifier(const core::identifier_string& s) = 0; 49 : 50 : /// \brief Removes the identifier s from the context. 51 : /// \param s An identifier. 52 : virtual void remove_identifier(const core::identifier_string& s) = 0; 53 : 54 : /// \brief Add a set of identifiers to the context. 55 15422 : void add_identifiers(const std::set<core::identifier_string>& ids) 56 : { 57 300715 : for (const core::identifier_string& id: ids) 58 : { 59 285293 : add_identifier(id); 60 : } 61 15422 : } 62 : 63 : /// \brief Remove a set of identifiers from the context. 64 : void remove_identifiers(const std::set<core::identifier_string>& ids) 65 : { 66 : for (const core::identifier_string& id: ids) 67 : { 68 : remove_identifier(id); 69 : } 70 : } 71 : 72 : /// \brief Returns true if the identifier s appears in the context. 73 : /// \param s An identifier. 74 : /// \return True if the identifier appears in the context. 75 : virtual bool has_identifier(const core::identifier_string& s) const = 0; 76 : 77 : /// \brief Returns a fresh identifier, with the given hint as prefix. 78 : /// The returned identifier is added to the context. 79 : /// \param hint A string 80 : /// \param add_to_context If true, the freshly generated identifier is added 81 : /// to the context to make sure no duplicates are generated. 82 : /// \return A fresh identifier. 83 24069 : virtual core::identifier_string operator()(const std::string& hint, bool add_to_context = true) 84 : { 85 48138 : core::identifier_string id(add_to_context?hint:m_generator(hint)); 86 41523 : while (has_identifier(id)) 87 : { 88 17454 : id = core::identifier_string(m_generator(hint)); 89 : } 90 24069 : if (add_to_context) 91 : { 92 24067 : add_identifier(id); 93 : } 94 24069 : return id; 95 0 : } 96 : }; 97 : 98 : } // namespace data 99 : 100 : } // namespace mcrl2 101 : 102 : #endif // MCRL2_DATA_IDENTIFIER_GENERATOR_H