atermpp::binary_aterm_ostream

Include file:

#include "mcrl2/atermpp/aterm_io_binary.h
class atermpp::binary_aterm_ostream

Writes terms in a streamable binary aterm format to an output stream.

The streamable aterm format: Aterms (and function symbols) are written as packets (with an identifier in the header) and their

indices are derived from the number of aterms, resp. symbols, that occur before them in this stream. For each term we first ensure that its arguments and symbol are written to the stream (avoiding duplicates). Then its symbol index followed by a number of indices (depending on the arity) for its argments are written as integers. Packet headers also contain a special value to indicate that the read term should be visible as output as opposed to being only a subterm. The start of the stream is a zero followed by a header and a version and a term with function symbol index zero indicates the end of the stream.

Private attributes

unsigned int atermpp::binary_aterm_ostream::m_function_symbol_index_width

caches the result of function_symbol_index_width().

mcrl2::utilities::indexed_set<function_symbol> atermpp::binary_aterm_ostream::m_function_symbols

An index of already written function symbols.

mcrl2::utilities::obitstream atermpp::binary_aterm_ostream::m_stream
unsigned int atermpp::binary_aterm_ostream::m_term_index_width

caches the result of term_index_width().

mcrl2::utilities::indexed_set<aterm> atermpp::binary_aterm_ostream::m_terms

An index of already written terms.

Public member functions

binary_aterm_ostream(std::ostream &os)

Provide the output stream to which the terms are written.

void put(const aterm &term) override

Writes an aterm in a compact binary format where subterms are shared. The term that is written itself is not shared whenever it occurs as the argument of another term.

~binary_aterm_ostream() override

Private member functions

unsigned int function_symbol_index_width()

Returns: The number of bits needed to index function symbols.

unsigned int term_index_width()

Returns: The number of bits needed to index terms.

std::size_t write_function_symbol(const function_symbol &symbol)

Write a function symbol to the output stream.