number_postfix_generator.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H
#define MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H
 
#include "mcrl2/utilities/text_utility.h"
#include <cassert>
#include <cctype>
#include <map>
 
namespace mcrl2 {
 
namespace utilities {
 
class number_postfix_generator
{
  protected:
    mutable std::map<std::string, std::size_t> m_index;
 
    std::string m_hint;
 
  public:
 
    number_postfix_generator(std::string hint = "FRESH_VAR")
      : m_hint(hint)
    {}
 
    void add_identifier(const std::string& id)
    {
      std::string::size_type i = id.find_last_not_of("0123456789");
      std::size_t new_index = 0;
      std::string name;
      if (i == std::string::npos || id.size() == i + 1) // string does not end with a number
      {
        name = id;
      }
      else
      {
        name = id.substr(0, i + 1);
        std::string num = id.substr(i + 1);
        new_index = atoi(num.c_str());
      }
      std::size_t old_index = m_index.find(name) == m_index.end() ? 0 : m_index[name];
      m_index[name] = (std::max)(old_index, new_index); // Windows requires brackets around std::max. 
    }
 
    template <typename Iter>
    void add_identifiers(Iter first, Iter last)
    {
      for (Iter i = first; i != last; ++i)
      {
        add_identifier(*i);
      }
    }
 
    template <typename Iter>
    number_postfix_generator(Iter first, Iter last, std::string hint = "FRESH_VAR")
      : m_hint(hint)
    {
      add_identifiers(first, last);
    }
 
    std::string operator()(std::string hint, bool add_to_context = true) const
    {
      // remove digits at the end of hint
      if (std::isdigit(hint[hint.size() - 1]))
      {
        std::string::size_type i = hint.find_last_not_of("0123456789");
        hint = hint.substr(0, i + 1);
      }
 
      auto j = m_index.find(hint);
      if (j == m_index.end())
      {
        if (add_to_context)
        {
          m_index[hint] = 0;
        }
        return hint;
      }
      return hint + utilities::number2string(add_to_context ? ++(j->second) : j->second + 1);
    }
 
    std::string operator()() const
    {
      return (*this)(m_hint, true);
    }
 
    const std::string& hint() const
    {
      return m_hint;
    }
 
    std::string& hint()
    {
      return m_hint;
    }
 
    void clear()
    {
      m_index.clear();
    }
};
 
} // namespace utilities
 
} // namespace mcrl2
 
#endif // MCRL2_UTILITIES_NUMBER_POSTFIX_GENERATOR_H