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/set_identifier_generator.h
      10             : /// \brief The classes set_identifier_generator and multiset_identifier_generator.
      11             : 
      12             : #ifndef MCRL2_DATA_SET_IDENTIFIER_GENERATOR_H
      13             : #define MCRL2_DATA_SET_IDENTIFIER_GENERATOR_H
      14             : 
      15             : #include "mcrl2/data/identifier_generator.h"
      16             : #include "mcrl2/utilities/detail/container_utility.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             : /// \brief Identifier generator that stores the identifiers of the
      25             : /// context in a set.
      26             : /// Using the operator()() and operator()(std::string) fresh
      27             : /// identifiers can be generated that do not appear in the
      28             : /// context.
      29             : class set_identifier_generator: public identifier_generator<>
      30             : {
      31             :   protected:
      32             :     /// \brief The context of the identifier generator.
      33             :     std::set<core::identifier_string> m_identifiers;
      34             : 
      35             :   public:
      36             :     /// \brief Constructor.
      37       29648 :     set_identifier_generator() = default;
      38             : 
      39             :     /// \brief Clears the context.
      40         151 :     void clear_context() override
      41             :     {
      42         151 :       m_identifiers.clear();
      43         151 :       m_generator.clear();
      44         151 :     }
      45             : 
      46             :     /// \brief Adds the identifier s to the context.
      47             :     /// \param s A
      48      346943 :     void add_identifier(const core::identifier_string& s) override
      49             :     {
      50      346943 :       m_identifiers.insert(s);
      51      346943 :     }
      52             : 
      53             :     /// \brief Removes one occurrence of the identifier s from the context.
      54             :     /// \param s A
      55         244 :     void remove_identifier(const core::identifier_string& s) override
      56             :     {
      57         244 :       m_identifiers.erase(s);
      58         244 :     }
      59             : 
      60             :     /// \brief Returns true if the identifier s appears in the context.
      61             :     /// \param s A
      62             :     /// \return True if the identifier s appears in the context.
      63       41550 :     bool has_identifier(const core::identifier_string& s) const override
      64             :     {
      65             :       using utilities::detail::contains;
      66       41550 :       return contains(m_identifiers, s);
      67             :     }
      68             : 
      69             :     /// \brief Returns the context.
      70             :     /// \return The context.
      71           5 :     const std::set<core::identifier_string>& context() const
      72             :     {
      73           5 :       return m_identifiers;
      74             :     }
      75             : };
      76             : 
      77             : /// \brief Identifier generator that stores the identifiers of the
      78             : /// context in a multiset.
      79             : /// If an identifier occurs multiple times,
      80             : /// multiple calls to remove_from_context are required to
      81             : /// remove it.
      82             : /// Using the operator()() and operator()(std::string) fresh
      83             : /// identifiers can be generated that do not appear in the
      84             : /// context.
      85             : class multiset_identifier_generator: public identifier_generator<>
      86             : {
      87             :   protected:
      88             :     /// \brief The context of the identifier generator.
      89             :     std::multiset<core::identifier_string> m_identifiers;
      90             : 
      91             :   public:
      92             :     /// \brief Constructor.
      93         300 :     multiset_identifier_generator() = default;
      94             : 
      95             :     /// \brief Clears the context.
      96           0 :     void clear_context() override
      97             :     {
      98           0 :       m_identifiers.clear();
      99           0 :       m_generator.clear();
     100           0 :     }
     101             : 
     102             :     /// \brief Adds the identifier s to the context.
     103             :     /// \param s A
     104        1098 :     void add_identifier(const core::identifier_string& s) override
     105             :     {
     106        1098 :       m_identifiers.insert(s);
     107        1098 :     }
     108             : 
     109             :     /// \brief Removes one occurrence of the identifier s from the context.
     110             :     /// \param s A
     111           2 :     void remove_identifier(const core::identifier_string& s) override
     112             :     {
     113           2 :       auto i = m_identifiers.find(s);
     114           2 :       if (i != m_identifiers.end())
     115             :       {
     116           2 :         m_identifiers.erase(i);
     117             :       }
     118           2 :     }
     119             : 
     120             :     /// \brief Returns true if the identifier s appears in the context.
     121             :     /// \param s A
     122             :     /// \return True if the identifier s appears in the context.
     123           9 :     bool has_identifier(const core::identifier_string& s) const override
     124             :     {
     125             :         using utilities::detail::contains;
     126           9 :       return contains(m_identifiers, s);
     127             :     }
     128             : 
     129             :     /// \brief Returns the context.
     130             :     /// \return The context.
     131             :     const std::multiset<core::identifier_string>& context() const
     132             :     {
     133             :       return m_identifiers;
     134             :     }
     135             : };
     136             : 
     137             : } // namespace data
     138             : 
     139             : } // namespace mcrl2
     140             : 
     141             : #endif // MCRL2_DATA_SET_IDENTIFIER_GENERATOR_H