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             : 
      10             : #ifndef MCRL2_SYMBOLIC_DATA_INDEX_H
      11             : #define MCRL2_SYMBOLIC_DATA_INDEX_H
      12             : 
      13             : #include "mcrl2/utilities/indexed_set.h"
      14             : #include "mcrl2/core/detail/print_utility.h"
      15             : #include "mcrl2/data/data_expression.h"
      16             : 
      17             : namespace mcrl2::symbolic
      18             : {
      19             : 
      20             : /// \brief A bidirectional mapping between data expressions of a given sort and numbers
      21             : class data_expression_index : public mcrl2::utilities::indexed_set<data::data_expression>
      22             : {
      23             :     friend std::ostream& operator<<(std::ostream&, const data_expression_index&);
      24             : 
      25             :   protected:
      26             :     data::sort_expression m_sort;
      27             : 
      28             :   public:
      29           0 :     data_expression_index(const data::sort_expression& sort)
      30           0 :       : m_sort(sort)
      31           0 :     {}
      32             : 
      33           0 :     std::pair<size_type, bool> insert(const key_type& key)
      34             :     {
      35           0 :       assert(key.sort() == m_sort);
      36           0 :       return mcrl2::utilities::indexed_set<data::data_expression>::insert(key);
      37             :     }
      38             :     
      39             :     const data::sort_expression& sort() const
      40             :     {
      41             :       return m_sort;
      42             :     }
      43             : };
      44             : 
      45             : inline
      46             : std::ostream& operator<<(std::ostream& out, const data_expression_index& x)
      47             : {
      48             :   out << "data index with sort = " << x.sort() << " values = " << core::detail::print_list(x);
      49             :   return out;
      50             : }
      51             : 
      52             : } // namespace mcrl2::symbolic
      53             : 
      54             : #endif // MCRL2_SYMBOLIC_DATA_INDEX_H