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/utilities/number_postfix_generator.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H
      13             : #define MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H
      14             : 
      15             : #include "mcrl2/utilities/text_utility.h"
      16             : #include <cassert>
      17             : #include <cctype>
      18             : #include <map>
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace utilities {
      23             : 
      24             : /// \brief Identifier generator that generates names consisting of a prefix followed by a number.
      25             : /// For each prefix an index is maintained, that is incremented after each call to operator()(prefix).
      26             : class number_postfix_generator
      27             : {
      28             :   protected:
      29             :     /// \brief A map that maintains the highest index for each prefix.
      30             :     mutable std::map<std::string, std::size_t> m_index;
      31             : 
      32             :     /// \brief The default hint.
      33             :     std::string m_hint;
      34             : 
      35             :   public:
      36             : 
      37             :     /// \brief Constructor.
      38       30106 :     number_postfix_generator(std::string hint = "FRESH_VAR")
      39       30106 :       : m_hint(hint)
      40       30106 :     {}
      41             : 
      42             :     /// \brief Adds the strings in the range [first, last) to the context.
      43             :     /// \param id A string
      44       10095 :     void add_identifier(const std::string& id)
      45             :     {
      46       10095 :       std::string::size_type i = id.find_last_not_of("0123456789");
      47       10095 :       std::size_t new_index = 0;
      48       10095 :       std::string name;
      49       10095 :       if (i == std::string::npos || id.size() == i + 1) // string does not end with a number
      50             :       {
      51        9224 :         name = id;
      52             :       }
      53             :       else
      54             :       {
      55         871 :         name = id.substr(0, i + 1);
      56         871 :         std::string num = id.substr(i + 1);
      57         871 :         new_index = atoi(num.c_str());
      58         871 :       }
      59       10095 :       std::size_t old_index = m_index.find(name) == m_index.end() ? 0 : m_index[name];
      60       10095 :       m_index[name] = (std::max)(old_index, new_index); // Windows requires brackets around std::max. 
      61       10095 :     }
      62             : 
      63             :     /// \brief Adds the strings in the range [first, last) to the context.
      64             :     /// \param first
      65             :     /// \param last
      66             :     /// [first, last) is a sequence of strings that is used as context.
      67             :     template <typename Iter>
      68           1 :     void add_identifiers(Iter first, Iter last)
      69             :     {
      70           3 :       for (Iter i = first; i != last; ++i)
      71             :       {
      72           2 :         add_identifier(*i);
      73             :       }
      74           1 :     }
      75             : 
      76             :     /// \brief Constructor.
      77             :     /// \param first
      78             :     /// \param last
      79             :     /// \param hint String hint to use as prefix for generated strings.
      80             :     /// [first, last) is a sequence of strings that is used as context.
      81             :     template <typename Iter>
      82             :     number_postfix_generator(Iter first, Iter last, std::string hint = "FRESH_VAR")
      83             :       : m_hint(hint)
      84             :     {
      85             :       add_identifiers(first, last);
      86             :     }
      87             : 
      88             :     /// \brief Generates a fresh identifier that doesn't appear in the context.
      89             :     /// \return A fresh identifier.
      90       17520 :     std::string operator()(std::string hint, bool add_to_context = true) const
      91             :     {
      92             :       // remove digits at the end of hint
      93       17520 :       if (std::isdigit(hint[hint.size() - 1]))
      94             :       {
      95         684 :         std::string::size_type i = hint.find_last_not_of("0123456789");
      96         684 :         hint = hint.substr(0, i + 1);
      97             :       }
      98             : 
      99       17520 :       auto j = m_index.find(hint);
     100       17520 :       if (j == m_index.end())
     101             :       {
     102        5736 :         if (add_to_context)
     103             :         {
     104        5734 :           m_index[hint] = 0;
     105             :         }
     106        5736 :         return hint;
     107             :       }
     108       23568 :       return hint + utilities::number2string(add_to_context ? ++(j->second) : j->second + 1);
     109             :     }
     110             : 
     111             :     /// \brief Generates a fresh identifier that doesn't appear in the context.
     112             :     /// \return A fresh identifier.
     113           2 :     std::string operator()() const
     114             :     {
     115           2 :       return (*this)(m_hint, true);
     116             :     }
     117             : 
     118             :     /// \brief Returns the default hint.
     119             :     const std::string& hint() const
     120             :     {
     121             :       return m_hint;
     122             :     }
     123             : 
     124             :     /// \brief Returns the default hint.
     125             :     std::string& hint()
     126             :     {
     127             :       return m_hint;
     128             :     }
     129             : 
     130             :     /// \brief Clear the context of the generator
     131         151 :     void clear()
     132             :     {
     133         151 :       m_index.clear();
     134         151 :     }
     135             : };
     136             : 
     137             : } // namespace utilities
     138             : 
     139             : } // namespace mcrl2
     140             : 
     141             : #endif // MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H