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