Line data    Source code

       1             : // Author(s): Maurice Laveaux
       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_LDD_IOSTREAM_H
      11             : #define MCRL2_SYMBOLIC_LDD_IOSTREAM_H
      12             : 
      13             : #ifdef MCRL2_ENABLE_SYLVAN
      14             : 
      15             : #include "mcrl2/utilities/indexed_set.h"
      16             : #include "mcrl2/utilities/bitstream.h"
      17             : 
      18             : #include <sylvan_ldd.hpp>
      19             : 
      20             : #include <deque>
      21             : #include <iostream>
      22             : 
      23             : namespace std
      24             : {
      25             : 
      26             : /// \brief specialization of the standard std::hash function.
      27             : template<>
      28             : struct hash<sylvan::ldds::ldd>
      29             : {
      30           8 :   std::size_t operator()(const sylvan::ldds::ldd& ldd) const
      31             :   {
      32             :     std::hash<std::uint64_t> hasher;
      33           8 :     return hasher(ldd.get());
      34             :   }
      35             : };
      36             : 
      37             : } // namespace std
      38             : 
      39             : namespace mcrl2::symbolic
      40             : {
      41             : 
      42             : /// \brief Writes ldds in a streamable binary format to an output stream.
      43             : /// \details The streamable ldd format:
      44             : ///
      45             : ///          Every LDD is traversed in order and assigned a unique number.
      46             : ///          Whenever traversal encounters an LDD of which all children have
      47             : ///          been visited it is written to the stream as 0:[value, down_index,
      48             : ///          right_index]. An output LDD (as returned by
      49             : ///          binary_ldd_istream::get()) is written as 1:index.
      50             : class binary_ldd_ostream
      51             : {
      52             : public:
      53             :   binary_ldd_ostream(std::ostream& os);
      54             :   binary_ldd_ostream(std::shared_ptr<mcrl2::utilities::obitstream> stream);
      55             : 
      56             :   ~binary_ldd_ostream();
      57             : 
      58             :   void put(const sylvan::ldds::ldd& U);
      59             : 
      60             : private:
      61             :   /// \returns The number of bits needed to index ldds.
      62             :   unsigned int ldd_index_width();
      63             :   
      64             :   std::shared_ptr<mcrl2::utilities::obitstream> m_stream;
      65             :   mcrl2::utilities::indexed_set<sylvan::ldds::ldd> m_nodes; ///< An index of already written ldds.
      66             : 
      67             : };
      68             : 
      69             : class binary_ldd_istream
      70             : {
      71             : public:
      72             :   binary_ldd_istream(std::istream& os);
      73             :   binary_ldd_istream(std::shared_ptr<mcrl2::utilities::ibitstream> stream);
      74             : 
      75             :   sylvan::ldds::ldd get();
      76             : 
      77             : private:
      78             :   /// \returns The number of bits needed to index ldds.
      79             :   unsigned int ldd_index_width(bool input = false);
      80             :   
      81             :   std::shared_ptr<mcrl2::utilities::ibitstream> m_stream;
      82             :   std::deque<sylvan::ldds::ldd> m_nodes; ///< An index of read ldds.
      83             : };
      84             : 
      85             : /// \brief Write the given term to the stream.
      86           2 : inline binary_ldd_ostream& operator<<(binary_ldd_ostream& stream, const sylvan::ldds::ldd& term) { stream.put(term); return stream; }
      87             : 
      88             : /// \brief Read the given term from the stream, but for aterm_list we want to use a specific one that performs validation (defined below).
      89           2 : inline binary_ldd_istream& operator>>(binary_ldd_istream& stream, sylvan::ldds::ldd& term) { term = stream.get(); return stream; }
      90             : 
      91             : } // namespace mcrl2::symbolic
      92             : 
      93             : #endif // MCRL2_ENABLE_SYLVAN
      94             : 
      95             : #endif // MCRL2_SYMBOLIC_LDD_IOSTREAM_H