LCOV - code coverage report
Current view: top level - atermpp/include/mcrl2/atermpp - aterm_io_binary.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 1 100.0 %
Date: 2020-02-13 00:44:47 Functions: 1 2 50.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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_ATERMPP_ATERM_IO_BINARY_H
      11             : #define MCRL2_ATERMPP_ATERM_IO_BINARY_H
      12             : 
      13             : #include "mcrl2/atermpp/aterm_io.h"
      14             : 
      15             : #include "mcrl2/utilities/bitstream.h"
      16             : #include "mcrl2/utilities/indexed_set.h"
      17             : 
      18             : namespace atermpp
      19             : {
      20             : 
      21             : /// \brief Writes terms in a streamable binary aterm format to an output stream.
      22             : /// \details The streamable aterm format:
      23             : ///
      24             : ///          Aterms (and function symbols) are written as packets (with an identifier in the header) and their
      25             : ///          indices are derived from the number of aterms, resp. symbols, that occur before them in this stream. For each term
      26             : ///          we first ensure that its arguments and symbol are written to the stream (avoiding duplicates). Then its
      27             : ///          symbol index followed by a number of indices (depending on the arity) for its argments are written as integers.
      28             : ///          Packet headers also contain a special value to indicate that the read term should be visible as output as opposed to
      29             : ///          being only a subterm.
      30             : ///          The start of the stream is a zero followed by a header and a version and a term with function symbol index zero
      31             : ///          indicates the end of the stream.
      32             : ///
      33             : class binary_aterm_ostream final : public aterm_ostream
      34             : {
      35             : public:
      36             :   /// \brief Provide the output stream to which the terms are written.
      37             :   binary_aterm_ostream(std::ostream& os);
      38             :   ~binary_aterm_ostream() override;
      39             : 
      40             :   /// \brief Writes an aterm in a compact binary format where subterms are shared. The term that is
      41             :   ///        written itself is not shared whenever it occurs as the argument of another term.
      42             :   void put(const aterm &term) override;
      43             : 
      44             : private:
      45             :   /// \brief Write a function symbol to the output stream.
      46             :   std::size_t write_function_symbol(const function_symbol& symbol);
      47             : 
      48             :   /// \returns The number of bits needed to index terms.
      49             :   unsigned int term_index_width();
      50             : 
      51             :   /// \returns The number of bits needed to index function symbols.
      52             :   unsigned int function_symbol_index_width();
      53             : 
      54             :   mcrl2::utilities::obitstream m_stream;
      55             : 
      56             :   unsigned int m_term_index_width; ///< caches the result of term_index_width().
      57             :   unsigned int m_function_symbol_index_width; ///< caches the result of function_symbol_index_width().
      58             : 
      59             :   mcrl2::utilities::indexed_set<aterm> m_terms; ///< An index of already written terms.
      60             :   mcrl2::utilities::indexed_set<function_symbol> m_function_symbols; ///< An index of already written function symbols.
      61             : };
      62             : 
      63             : /// \brief Reads terms from a stream in the steamable binary aterm format.
      64         131 : class binary_aterm_istream final : public aterm_istream
      65             : {
      66             : public:
      67             :   /// \brief Provide the input stream from which terms are read.
      68             :   binary_aterm_istream(std::istream& is);
      69             : 
      70             :   aterm get() override;
      71             : 
      72             : private:
      73             :   /// \returns The number of bits needed to index terms.
      74             :   unsigned int term_index_width();
      75             : 
      76             :   /// \returns The number of bits needed to index function symbols.
      77             :   unsigned int function_symbol_index_width();
      78             : 
      79             :   mcrl2::utilities::ibitstream m_stream;
      80             : 
      81             :   unsigned int m_term_index_width; ///< caches the result of term_index_width().
      82             :   unsigned int m_function_symbol_index_width; ///< caches the result of function_symbol_index_width().
      83             : 
      84             :   std::deque<aterm> m_terms; ///< An index of read terms.
      85             :   std::deque<function_symbol> m_function_symbols; ///< An index of read function symbols.
      86             : };
      87             : 
      88             : } // namespace atermpp
      89             : 
      90             : #endif // MCRL2_ATERMPP_ATERM_IO_BINARY_H

Generated by: LCOV version 1.13