mcrl2::utilities::number_postfix_generator

Include file:

#include "mcrl2/utilities/number_postfix_generator.h
class mcrl2::utilities::number_postfix_generator

Identifier generator that generates names consisting of a prefix followed by a number. For each prefix an index is maintained, that is incremented after each call to operator()(prefix).

Protected attributes

std::string m_hint

The default hint.

std::map<std::string, std::size_t> m_index

A map that maintains the highest index for each prefix.

Public member functions

void add_identifier(const std::string &id)

Adds the strings in the range [first, last) to the context.

Parameters:

  • id A string
void add_identifiers(Iter first, Iter last)

Adds the strings in the range [first, last) to the context.

Parameters:

  • first
  • last [first, last) is a sequence of strings that is used as context.
void clear()

Clear the context of the generator.

const std::string &hint() const

Returns the default hint.

std::string &hint()

Returns the default hint.

number_postfix_generator(std::string hint = "FRESH_VAR")

Constructor.

number_postfix_generator(Iter first, Iter last, std::string hint = "FRESH_VAR")

Constructor.

Parameters:

  • first
  • last
  • hint String hint to use as prefix for generated strings. [first, last) is a sequence of strings that is used as context.
std::string operator()(std::string hint, bool add_to_context = true) const

Generates a fresh identifier that doesn’t appear in the context.

Returns: A fresh identifier.

std::string operator()() const

Generates a fresh identifier that doesn’t appear in the context.

Returns: A fresh identifier.