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/enumerator_identifier_generator.h
      10             : /// \brief The class enumerator_identifier_genierator 
      11             : ///        contains a generator of fresh identifier strings that
      12             : ///        works intimately together with the atermpp function_symbols
      13             : ///        to make it as efficient to generate fresh strings. Construction of a
      14             : ///        enumerator identifier generator is less efficient, as it sets up
      15             : ///        internal data structures and searches through all existing
      16             : ///        function symbols in the aterm library. 
      17             : 
      18             : #ifndef MCRL2_DATA_DETAIL_ENUMERATOR_IDENTIFIER_GENERATOR_H
      19             : #define MCRL2_DATA_DETAIL_ENUMERATOR_IDENTIFIER_GENERATOR_H
      20             : 
      21             : #include "mcrl2/atermpp/function_symbol_generator.h"
      22             : #include "mcrl2/core/identifier_string.h"
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : 
      27             : namespace data
      28             : {
      29             : 
      30             : class enumerator_identifier_generator
      31             : {
      32             :   protected:
      33             :     atermpp::function_symbol_generator f;
      34             : 
      35             :   public:
      36             :     /// \brief Constructor
      37             :     /// \param prefix The prefix of the generated generated strings
      38             :     /// \pre The prefix may not be empty, and it may not have trailing digits
      39        2540 :     explicit enumerator_identifier_generator(const std::string& prefix = "x_")
      40        2540 :       : f(prefix)
      41        2540 :     { }
      42             :     
      43             :     /// \brief Generates a unique function symbol with the given prefix followed by a number.
      44       23637 :     core::identifier_string operator()()
      45             :     {
      46       47274 :       return core::identifier_string(f());
      47             :     }
      48             :     
      49       16713 :     void clear()
      50             :     {
      51       16713 :       f.clear();
      52       16713 :     }
      53             : };
      54             : 
      55             : 
      56             : } // namespace data
      57             : 
      58             : } // namespace mcrl2
      59             : 
      60             : 
      61             : #endif // MCRL2_DATA_DETAIL_ENUMERATOR_IDENTIFIER_GENERATOR_H