The main namespace for the aterm++ library. More...

Namespaces
namespace	anonymous_namespace{aterm_balanced_tree.h}

namespace	detail

namespace	utilities

Classes
class	aterm
	The aterm base class that provides protection of the underlying shared terms. More...

class	aterm_int
	An integer term stores a single std::size_t value. It carries no arguments. More...

class	aterm_istream
	The interface for a class that reads aterm from a stream. The default constructed term aterm() indicates the end of the stream. More...

class	aterm_ostream
	The interface for a class that writes aterm to a stream. Every written term is retrieved by the corresponding aterm_istream::get() call. More...

class	aterm_stream
	The general aterm stream interface, which enables the use of a transformer to change the written/read terms. More...

class	aterm_stream_state
	A helper class to restore the state of the aterm_{i,o}stream objects upon destruction. Currently, onlt preserves the transformer object. More...

class	aterm_string
	Term containing a string. More...

class	binary_aterm_istream
	Reads terms from a stream in the steamable binary aterm format. More...

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

struct	builder

class	deque
	A deque class in which aterms can be stored. More...

struct	disable_if_container

struct	enable_if_container

class	function_symbol

class	function_symbol_generator
	Generates unique function symbols with a given prefix. More...

class	global_function_symbol

class	indexed_set
	A set that assigns each element an unique index, and protects its internal terms en masse. More...

struct	is_container

struct	is_container< T, void >

struct	is_convertible

struct	is_set

class	reverse_term_list_iterator
	Reverse iterator for term_list. More...

class	stack
	A deque class in which aterms can be stored. More...

class	term_appl

class	term_appl_iterator
	Iterator for term_appl. More...

class	term_balanced_tree
	Read-only balanced binary tree of terms. More...

class	term_list
	A list of aterm objects. More...

class	term_list_iterator
	Iterator for term_list. More...

class	text_aterm_istream
	Reads terms in textual format from an input stream. More...

class	text_aterm_ostream
	Writes terms in textual format to an output stream. More...

struct	unary_template_swap

class	unordered_map
	A unordered_map class in which aterms can be stored. More...

class	unprotected_aterm
	An unprotected term does not change the reference count of the shared term when it is copied or moved. More...

class	vector
	A vector class in which aterms can be stored. More...

struct	write_todo
	Keep track of whether the term can be written to the stream. More...

Typedefs
typedef void(*	term_callback) (const aterm &)

typedef term_appl< aterm >	aterm_appl

typedef term_balanced_tree< aterm >	aterm_balanced_tree
	A term_balanced_tree with elements of type aterm.

using	aterm_transformer = aterm_appl(const aterm_appl &)
	A function that is applied to all terms. The resulting term should only use a subset of the original arguments (i.e. not introduce new terms).

typedef term_list< aterm >	aterm_list
	A term_list with elements of type aterm.

typedef std::stack< std::reference_wrapper< detail::_aterm > >	term_mark_stack

Enumerations
enum class	packet_type { function_symbol = 0 , aterm , aterm_output , aterm_int_output }
	Each packet has a header consisting of a type. More...

Functions
template<typename UnaryFunction , typename Term >
UnaryFunction	for_each (Term t, UnaryFunction op)
	Calls op(elem) for subterms of the term t.

template<typename Term , typename MatchPredicate >
aterm_appl	find_if (const Term &t, MatchPredicate match)
	Finds a subterm of t that matches a given predicate.

template<typename Term , typename MatchPredicate , typename StopPredicate >
aterm_appl	partial_find_if (Term t, MatchPredicate match, StopPredicate stop)
	Finds a subterm of t that matches a given predicate. The term is only partially traversed. If the stop predicate returns true in a subterm, the recursion is not continued.

template<typename Term , typename MatchPredicate , typename OutputIterator >
void	find_all_if (const Term &t, MatchPredicate match, OutputIterator destBegin)
	Finds all subterms of t that match a given predicate, and writes the found terms to the destination range starting with destBegin.

template<typename Term , typename MatchPredicate , typename StopPredicate , typename OutputIterator >
void	partial_find_all_if (Term t, MatchPredicate match, StopPredicate stop, OutputIterator destBegin)
	Finds all subterms of t that match a given predicate, and writes the found terms to the destination range starting with destBegin. The term is only partially traversed. If the stop predicate returns true in a subterm, the recursion is not continued.

template<typename Term , typename ReplaceFunction >
Term	replace (const Term &t, ReplaceFunction r)
	Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in top down order.

template<typename Term >
Term	replace (const Term &t, const aterm &old_value, const aterm &new_value)
	Replaces each subterm in t that is equal to old_value with new_value. The replacements are performed in top down order. For example, replace(f(f(x)), f(x), x) returns f(x) and not x.

template<typename Term , typename ReplaceFunction >
Term	bottom_up_replace (Term t, ReplaceFunction r)
	Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in bottom up order. For example, replace(f(f(x)), f(x), x) returns x.

template<typename Term >
Term	bottom_up_replace (Term t, const aterm_appl &old_value, const aterm_appl &new_value)
	Replaces each subterm in t that is equal to old_value with new_value. The replacements are performed in top down order. For example, replace(f(f(x)), f(x), x) returns f(x) and not x.

template<typename Term , typename ReplaceFunction >
Term	partial_replace (Term t, ReplaceFunction r)
	Replaces subterms x of t by r(x). The replace function r returns an additional boolean value. This value is used to prevent further recursion. The ReplaceFunction r has the following signature: aterm_appl x; std::pair<aterm_appl, bool> result = r(x); result.first is the result r(x) of the replacement result.second denotes if the recursion should be continued The replacements are performed in top down order.

template<typename Term , typename ReplaceFunction >
Term	bottom_up_replace (Term t, ReplaceFunction r, std::unordered_map< aterm_appl, aterm > &cache)
	Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in bottom up order. For example, replace(f(f(x)), f(x), x) returns x.

void	add_deletion_hook (const function_symbol &, term_callback)
	Check for reasonably sized aterm (32 bits, 4 bytes) This check might break on perfectly valid architectures that have char == 2 bytes, and sizeof(header_type) == 2.

template<class Derived , class Base >
const Derived &	down_cast (const Base &t, typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *=nullptr)
	A cheap cast from one aterm based type to another When casting one aterm based type into another, generally a new aterm is constructed, and the old one is destroyed. This can cause undesired overhead, for instance due to increasing and decreasing of reference counts. This cast changes the type, without changing the aterm itself. It can only be used if Base and Derived inherit from aterm, and contain no additional information than a single aterm.

template<class Derived , class Base >
Derived &	reference_cast (Base &t, typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *=nullptr)
	A cast from one aterm based type to another, as a reference, allowing to assign to it.

template<typename DerivedCont , typename Base , template< typename Elem > class Cont>
const DerivedCont &	container_cast (const Cont< Base > &t, typename std::enable_if_t< is_container< DerivedCont, aterm >::value &&std::is_same_v< Cont< typename DerivedCont::value_type >, DerivedCont > &&!std::is_base_of_v< DerivedCont, Cont< Base > > &&is_convertible< Base, typename DerivedCont::value_type >::value > *=nullptr)

template<class Derived , class Base >
const Derived &	vertical_cast (const Base &t, typename std::enable_if< is_convertible< Base, Derived >::value >::type *=nullptr)
	A cast form an aterm derived class to a class that inherits in possibly multiple steps from this class.

template<typename DerivedCont , typename Base , template< typename Elem > class Cont>
const DerivedCont &	vertical_cast (const Cont< Base > &t, typename std::enable_if_t< is_container< DerivedCont, aterm >::value &&std::is_same_v< Cont< typename DerivedCont::value_type >, DerivedCont > &&is_convertible< Base, typename DerivedCont::value_type >::value > *=nullptr)

std::ostream &	operator<< (std::ostream &out, const atermpp::aterm &t)
	Send the term in textual form to the ostream.

std::string	pp (const atermpp::aterm &t)
	Transform an aterm to an ascii string.

template<class Term , class ForwardIterator , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr>
void	make_term_appl (Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
	Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.

template<class Term , class InputIterator , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr>
void	make_term_appl (Term &target, const function_symbol &sym, InputIterator begin, InputIterator end)
	Constructor an aterm_appl in a variable based on a function symbol and an input iterator providing the arguments.

template<class Term , class InputIterator , class TermConverter , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>
void	make_term_appl (Term &target, const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
	Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.

template<class Term >
void	make_term_appl (Term &target, const function_symbol &sym)
	Make an term_appl consisting of a single function symbol.

template<class Term , typename ... Terms>
void	make_term_appl (Term &target, const function_symbol &symbol, const Terms &...arguments)
	Make an aterm application for n-arity function application.

template<class Term , class INDEX_TYPE , typename ... Terms>
void	make_term_appl_with_index (aterm &target, const function_symbol &symbol, const Terms &...arguments)
	Constructor for n-arity function application with an index.

template<class Term , class ForwardTraversalIterator , class Transformer >
void	make_term_balanced_tree (term_balanced_tree< Term > &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)

bool	is_aterm_balanced_tree (const aterm_appl &t)

template<class Term >
std::string	pp (const term_balanced_tree< Term > t)

void	make_aterm_int (aterm_int &target, std::size_t value)
	Constructs an integer term from a value.

aterm_appl	identity (const aterm_appl &x)
	The default transformer that maps each term to itself.

aterm_istream &	operator>> (aterm_istream &stream, aterm_transformer transformer)
	Sets the given transformer to be applied to following reads.

aterm_ostream &	operator<< (aterm_ostream &stream, aterm_transformer transformer)

aterm_ostream &	operator<< (aterm_ostream &stream, const aterm &term)
	Write the given term to the stream.

aterm_istream &	operator>> (aterm_istream &stream, aterm &term)
	Read the given term from the stream, but for aterm_list we want to use a specific one that performs validation (defined below).

template<typename T , typename std::enable_if_t< mcrl2::utilities::is_iterable_v< T >, int > = 0, typename std::enable_if_t<!std::is_base_of< aterm, T >::value, int > = 0>
aterm_ostream &	operator<< (aterm_ostream &stream, const T &container)
	Write any container (that is not an aterm itself) to the stream.

template<typename T , typename std::enable_if_t< mcrl2::utilities::is_iterable_v< T >, int > = 0, typename std::enable_if_t<!std::is_base_of< aterm, T >::value, int > = 0>
aterm_istream &	operator>> (aterm_istream &stream, T &container)
	Read any container (that is not an aterm itself) from the stream.

template<typename T >
aterm_ostream &	operator<< (aterm_ostream &&stream, const T &t)

template<typename T >
aterm_istream &	operator>> (aterm_istream &&stream, T &t)

std::ostream &	operator<< (std::ostream &out, const function_symbol &f)
	Sends the name of a function symbol to an ostream.

const std::string &	pp (const function_symbol &f)
	Prints the name of a function symbol as a string.

void	write_term_to_binary_stream (const aterm &t, std::ostream &os)
	Writes term t to a stream in binary aterm format.

void	read_term_from_binary_stream (std::istream &is, aterm &t)
	Reads a term from a stream in binary aterm format.

void	write_term_to_text_stream (const aterm &t, std::ostream &os)
	Writes term t to a stream in textual format.

void	read_term_from_text_stream (std::istream &is, aterm &t)
	Reads a term from a stream which contains the term in textual format.

aterm	read_term_from_string (const std::string &s)
	Reads an aterm from a string. The string can be in either binary or text format.

aterm_list	read_list_from_string (const std::string &s)
	Reads an aterm_list from a string. The string can be in either binary or text format.

aterm_int	read_int_from_string (const std::string &s)
	Reads an aterm_int from a string. The string can be in either binary or text format.

aterm_appl	read_appl_from_string (const std::string &s)
	Reads an aterm_appl from a string. The string can be in either binary or text format.

template<class Term >
void	make_term_list (term_list< Term > &target)
	Make an empty list and put it in target;.

template<class Term , class Iter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
	Creates a term_list with the elements from first to last.

template<class Term , class Iter , class ATermConverter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0)
	Creates a term_list with the elements from first to last converting the elements before inserting.

template<class Term , class Iter , class ATermConverter , class ATermFilter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0)
	Creates a term_list with the elements from first to last, converting and filtering the list.

template<class Term , class Iter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
	Creates a term_list from the elements from first to last.

template<class Term , class Iter , class ATermConverter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
	Creates a term_list from the elements from first to last converting the elements before inserting.

template<class Term , class Iter , class ATermConverter , class ATermFilter >
void	make_term_list (term_list< Term > &target, Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter, typename std::enable_if< !std::is_base_of< std::random_access_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
	Creates a term_list from the elements from first to last converting and filtering the elements before inserting.

template<class Term >
void	make_term_list (term_list< Term > &target, std::initializer_list< Term > init)
	A constructor based on an initializer list.

template<typename Term >
term_list< Term >	reverse (const term_list< Term > &l)
	Returns the list with the elements in reversed order.

template<typename Term >
term_list< Term >	sort_list (const term_list< Term > &l, const std::function< bool(const Term &, const Term &)> &ordering=[](const Term &t1, const Term &t2){ return t1< t2;})
	Returns the list with the elements sorted according to the <-operator on the addresses of terms.

template<typename Term1 , typename Term2 >
std::conditional< std::is_convertible< Term2, Term1 >::value, term_list< Term1 >, term_list< Term2 > >::type	operator+ (const term_list< Term1 > &l, const term_list< Term2 > &m)
	Returns the concatenation of two lists with convertible element types.

template<typename Term >
term_list< Term >	push_back (const term_list< Term > &l, const Term &el)
	Appends a new element at the end of the list. Note that the complexity of this function is O(n), with n the number of elements in the list!!!

template<typename T >
std::vector< T >	as_vector (const atermpp::term_list< T > &x)
	Converts the given term list to a vector.

template<typename T >
std::set< T >	as_set (const atermpp::term_list< T > &x)
	Converts the given term list to a set.

const aterm_string &	empty_string ()
	Returns the empty aterm string.

void	mark_term (const aterm &t, term_mark_stack &todo)

template<typename Term >
void	make_reverse (term_list< Term > &result, const term_list< Term > &l)

template<typename Term >
term_list< Term >	remove_one_element (const term_list< Term > &list, const Term &t)

static std::mutex &	function_symbol_generator_mutex ()

static std::size_t &	generator_sequence_number ()

template<typename Term >
term_list< Term >	term_list_union (const term_list< Term > &v, const term_list< Term > &w)
	Returns the union of v and w.

template<typename Term >
term_list< Term >	term_list_difference (const term_list< Term > &v, const term_list< Term > &w)
	Returns v minus w.

static void	write_string_with_escape_symbols (const std::string &s, std::ostream &os)

Variables
constexpr std::size_t	LengthOfShortList = 10000

static constexpr std::uint16_t	BAF_MAGIC = 0x8baf
	The magic value for a binary aterm format stream.

static constexpr std::uint16_t	BAF_VERSION = 0x8307
	The BAF_VERSION constant is the version number of the ATerms written in BAF format. As of 29 August 2013 this version number is used by the mCRL2 toolset. Whenever the file format of mCRL2 files is changed, the BAF_VERSION has to be increased.

static constexpr unsigned int	packet_bits = 2
	The number of bits needed to store an element of packet_type.

Detailed Description

The main namespace for the aterm++ library.

Typedef Documentation

◆ aterm_appl

typedef term_appl<aterm> atermpp::aterm_appl

Definition at line 353 of file aterm_appl.h.

◆ aterm_balanced_tree

typedef term_balanced_tree<aterm> atermpp::aterm_balanced_tree

A term_balanced_tree with elements of type aterm.

Definition at line 431 of file aterm_balanced_tree.h.

◆ aterm_list

typedef term_list< aterm > atermpp::aterm_list

A term_list with elements of type aterm.

Definition at line 496 of file aterm_list.h.

◆ aterm_transformer

using atermpp::aterm_transformer = typedef aterm_appl(const aterm_appl&)

A function that is applied to all terms. The resulting term should only use a subset of the original arguments (i.e. not introduce new terms).

Typical usage is removing the index traits from function symbols that represent operators.

Definition at line 23 of file aterm_io.h.

◆ term_callback

typedef void(* atermpp::term_callback) (const aterm &)

Definition at line 23 of file aterm.h.

◆ term_mark_stack

typedef std::stack<std::reference_wrapper<detail::_aterm> > atermpp::term_mark_stack

Definition at line 23 of file aterm_container.h.

Enumeration Type Documentation

◆ packet_type

enum class atermpp::packet_type

strong

Each packet has a header consisting of a type.

Either indicates a function symbol, a term (either shared or output) or an arbitrary integer.

Enumerator
function_symbol
aterm
aterm_output
aterm_int_output

Definition at line 43 of file aterm_io_binary.cpp.

Function Documentation

◆ add_deletion_hook()

void atermpp::add_deletion_hook	(	const function_symbol &	function,
		term_callback	callback
	)

Check for reasonably sized aterm (32 bits, 4 bytes) This check might break on perfectly valid architectures that have char == 2 bytes, and sizeof(header_type) == 2.

Definition at line 23 of file aterm_implementation.cpp.

◆ as_set()

template<typename T >

std::set< T > atermpp::as_set ( const atermpp::term_list< T > & x )

Converts the given term list to a set.

Definition at line 554 of file aterm_list.h.

◆ as_vector()

template<typename T >

std::vector< T > atermpp::as_vector ( const atermpp::term_list< T > & x )

Converts the given term list to a vector.

Definition at line 547 of file aterm_list.h.

◆ bottom_up_replace() [1/3]

template<typename Term >

Term atermpp::bottom_up_replace	(	Term	t,
		const aterm_appl &	old_value,
		const aterm_appl &	new_value
	)

Replaces each subterm in t that is equal to old_value with new_value. The replacements are performed in top down order. For example, replace(f(f(x)), f(x), x) returns f(x) and not x.

Parameters

t	A term
old_value	The value of the subterm that is replaced.
new_value	The value that is substituted.

Returns: The result of the replacement.

Definition at line 291 of file algorithm.h.

◆ bottom_up_replace() [2/3]

template<typename Term , typename ReplaceFunction >

Term atermpp::bottom_up_replace	(	Term	t,
		ReplaceFunction	r
	)

Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in bottom up order. For example, replace(f(f(x)), f(x), x) returns x.

Parameters

t	A term
r	The replace function that is applied to subterms.

Returns: The result of the replacement.

Definition at line 276 of file algorithm.h.

◆ bottom_up_replace() [3/3]

template<typename Term , typename ReplaceFunction >

Term atermpp::bottom_up_replace	(	Term	t,
		ReplaceFunction	r,
		std::unordered_map< aterm_appl, aterm > &	cache
	)

Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in bottom up order. For example, replace(f(f(x)), f(x), x) returns x.

Parameters

t	A term
r	The replace function that is applied to subterms.
cache	A cache for the result of aterm_appl terms.

Returns: The result of the replacement.

Definition at line 326 of file algorithm.h.

◆ container_cast()

template<typename DerivedCont , typename Base , template< typename Elem > class Cont>

const DerivedCont & atermpp::container_cast	(	const Cont< Base > &	t,
		typename std::enable_if_t< is_container< DerivedCont, aterm >::value &&std::is_same_v< Cont< typename DerivedCont::value_type >, DerivedCont > &&!std::is_base_of_v< DerivedCont, Cont< Base > > &&is_convertible< Base, typename DerivedCont::value_type >::value > *	= `nullptr`
	)

Definition at line 287 of file aterm.h.

◆ down_cast()

template<class Derived , class Base >

const Derived & atermpp::down_cast	(	const Base &	t,
		typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *	= `nullptr`
	)

A cheap cast from one aterm based type to another When casting one aterm based type into another, generally a new aterm is constructed, and the old one is destroyed. This can cause undesired overhead, for instance due to increasing and decreasing of reference counts. This cast changes the type, without changing the aterm itself. It can only be used if Base and Derived inherit from aterm, and contain no additional information than a single aterm.

Parameters

t	A term of a type inheriting from an aterm.

Returns: A term of type const Derived&.

Definition at line 259 of file aterm.h.

◆ empty_string()

const aterm_string & atermpp::empty_string ( )

inline

Returns the empty aterm string.

Definition at line 77 of file aterm_string.h.

◆ find_all_if()

template<typename Term , typename MatchPredicate , typename OutputIterator >

void atermpp::find_all_if	(	const Term &	t,
		MatchPredicate	match,
		OutputIterator	destBegin
	)

Finds all subterms of t that match a given predicate, and writes the found terms to the destination range starting with destBegin.

Parameters

t	A term
match	The predicate that determines if a subterm is a match
destBegin	The iterator range to which output is written.

Definition at line 215 of file algorithm.h.

◆ find_if()

template<typename Term , typename MatchPredicate >

aterm_appl atermpp::find_if	(	const Term &	t,
		MatchPredicate	match
	)

Finds a subterm of t that matches a given predicate.

Parameters

t	A term
match	The predicate that determines if a subterm is a match

Returns: A subterm that matches the given predicate, or aterm_appl() if none was found.

Definition at line 189 of file algorithm.h.

◆ for_each()

template<typename UnaryFunction , typename Term >

UnaryFunction atermpp::for_each	(	Term	t,
		UnaryFunction	op
	)

Calls op(elem) for subterms of the term t.

Parameters

t	A term
op	The operation that is applied to subterms

Returns: a copy of the (internally modified) op. The function op must have the signature bool op(aterm_appl t). When op(t) is false, the children of t are skipped.

Definition at line 179 of file algorithm.h.

◆ function_symbol_generator_mutex()

static std::mutex & atermpp::function_symbol_generator_mutex ( )

inlinestatic

Definition at line 21 of file function_symbol_generator.h.

◆ generator_sequence_number()

static std::size_t & atermpp::generator_sequence_number ( )

inlinestatic

Definition at line 27 of file function_symbol_generator.h.

◆ identity()

aterm_appl atermpp::identity ( const aterm_appl & x )

inline

The default transformer that maps each term to itself.

Definition at line 26 of file aterm_io.h.

◆ is_aterm_balanced_tree()

bool atermpp::is_aterm_balanced_tree ( const aterm_appl & t )

inline

Definition at line 434 of file aterm_balanced_tree.h.

◆ make_aterm_int()

void atermpp::make_aterm_int	(	aterm_int &	target,
		std::size_t	value
	)

inline

Constructs an integer term from a value.

Parameters

target The term into which the term is constructed.

Definition at line 68 of file aterm_int.h.

◆ make_reverse()

template<typename Term >

void atermpp::make_reverse	(	term_list< Term > &	result,
		const term_list< Term > &	l
	)

inline

Definition at line 96 of file aterm_list_implementation.h.

◆ make_term_appl() [1/5]

template<class Term >

void atermpp::make_term_appl	(	Term &	target,
		const function_symbol &	sym
	)

Make an term_appl consisting of a single function symbol.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
sym	A function symbol.

Definition at line 312 of file aterm_appl.h.

◆ make_term_appl() [2/5]

template<class Term , class ForwardIterator , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr>

void atermpp::make_term_appl	(	Term &	target,
		const function_symbol &	sym,
		ForwardIterator	begin,
		ForwardIterator	end
	)

Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.

The iterator range is traversed more than once. If only one traversal is required use term_appl with a TermConverter argument. But this function is substantially less efficient. The length of the iterator range must match the arity of the function symbol.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
sym	A function symbol.
begin	The start of a range of elements.
end	The end of a range of elements.

Definition at line 239 of file aterm_appl.h.

◆ make_term_appl() [3/5]

template<class Term , class InputIterator , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr>

void atermpp::make_term_appl	(	Term &	target,
		const function_symbol &	sym,
		InputIterator	begin,
		InputIterator	end
	)

Constructor an aterm_appl in a variable based on a function symbol and an input iterator providing the arguments.

The given iterator is traversed only once. So it can be used with an input iterator. This means that the TermConverter is applied exactly once to each element. The length of the iterator range must be equal to the arity of the function symbol.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
sym	A function symbol.
begin	The start of a range of elements.
end	The end of a range of elements.

Definition at line 267 of file aterm_appl.h.

◆ make_term_appl() [4/5]

template<class Term , class InputIterator , class TermConverter , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>

void atermpp::make_term_appl	(	Term &	target,
		const function_symbol &	sym,
		InputIterator	begin,
		InputIterator	end,
		TermConverter	converter
	)

Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.

The given iterator is traversed only once. So it can be used with an input iterator. This means that the TermConverter is applied exactly once to each element. The length of the iterator range must be equal to the arity of the function symbol.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
sym	A function symbol.
begin	The start of a range of elements.
end	The end of a range of elements.
converter	An class or lambda term containing an operator Term operator()(const Term& t) which is applied to each each element in the iterator range before it becomes an argument of this term.

Definition at line 294 of file aterm_appl.h.

◆ make_term_appl() [5/5]

template<class Term , typename ... Terms>

void atermpp::make_term_appl	(	Term &	target,
		const function_symbol &	symbol,
		const Terms &...	arguments
	)

Make an aterm application for n-arity function application.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
symbol	A function symbol.
arguments	The arguments of the function application.

Definition at line 327 of file aterm_appl.h.

◆ make_term_appl_with_index()

template<class Term , class INDEX_TYPE , typename ... Terms>

void atermpp::make_term_appl_with_index	(	aterm &	target,
		const function_symbol &	symbol,
		const Terms &...	arguments
	)

Constructor for n-arity function application with an index.

Parameters

target	The variable in which the result will be put. This variable may be used for scratch purposes.
symbol	A function symbol.
arguments	The arguments of the function application.

Definition at line 344 of file aterm_appl.h.

◆ make_term_balanced_tree()

template<class Term , class ForwardTraversalIterator , class Transformer >

void atermpp::make_term_balanced_tree	(	term_balanced_tree< Term > &	result,
		ForwardTraversalIterator	p,
		const std::size_t	size,
		Transformer	transformer
	)

Definition at line 422 of file aterm_balanced_tree.h.

◆ make_term_list() [1/8]

template<class Term >

void atermpp::make_term_list ( term_list< Term > & target )

Make an empty list and put it in target;.

Parameters

target The variable to which the empty list is assigned.

Definition at line 313 of file aterm_list.h.

◆ make_term_list() [2/8]

template<class Term , class Iter , class ATermConverter , class ATermFilter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		const ATermConverter &	convert_to_aterm,
		const ATermFilter &	aterm_filter,
		typename std::enable_if< !std::is_base_of< std::random_access_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `nullptr`
	)

Creates a term_list from the elements from first to last converting and filtering the elements before inserting.

The range is traversed from first to last. This requires to copy the elements internally, which is less efficient than this function with random access iterators as arguments. The operator () in the class ATermConverter is applied to each element before inserting it in the list. Elements are only inserted if the operator () of the class ATermFilter yields true when applied to such an element.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.
convert_to_aterm	A class with a () operation, whic is applied to each element before it is put into the list.
aterm_filter	A class with an operator () that is used to determine whether elements can be inserted in the list.

Definition at line 429 of file aterm_list.h.

◆ make_term_list() [3/8]

template<class Term , class Iter , class ATermConverter , class ATermFilter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		const ATermConverter &	convert_to_aterm,
		const ATermFilter &	aterm_filter,
		typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `0`
	)

Creates a term_list with the elements from first to last, converting and filtering the list.

It is assumed that the range can be traversed from last to first. The operator () in the class ATermConverter is applied to each element before inserting it in the list. Elements are only inserted if the operator () of the class ATermFilter yields true when applied to such an element.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.
convert_to_aterm	A class with a () operation, which is applied to each element before it is put into the list.
aterm_filter	A class with an operator () that is used to determine whether elements can be inserted in the list.

Definition at line 363 of file aterm_list.h.

◆ make_term_list() [4/8]

template<class Term , class Iter , class ATermConverter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		const ATermConverter &	convert_to_aterm,
		typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `nullptr`
	)

Creates a term_list from the elements from first to last converting the elements before inserting.

The range is traversed from first to last. This requires to copy the elements internally, which is less efficient than this function with random access iterators as arguments. The operator () in the class ATermConverter is applied to each element before inserting it in the list.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.
convert_to_aterm	A class with a () operation, which is applied to each element before it is put into the list.

Definition at line 404 of file aterm_list.h.

◆ make_term_list() [5/8]

template<class Term , class Iter , class ATermConverter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		const ATermConverter &	convert_to_aterm,
		typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `0`
	)

Creates a term_list with the elements from first to last converting the elements before inserting.

It is assumed that the range can be traversed from last to first. The operator () in the class ATermConverter is applied to each element before inserting it in the list.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.
convert_to_aterm	A class with a () operation, which is applied to each element before it is put into the list.

Definition at line 342 of file aterm_list.h.

◆ make_term_list() [6/8]

template<class Term , class Iter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `nullptr`
	)

Creates a term_list from the elements from first to last.

The range is traversed from first to last. This requires to copy the elements internally, which is less efficient than this function with random access iterators as arguments.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.

Definition at line 381 of file aterm_list.h.

◆ make_term_list() [7/8]

template<class Term , class Iter >

void atermpp::make_term_list	(	term_list< Term > &	target,
		Iter	first,
		Iter	last,
		typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *	= `nullptr`
	)

Creates a term_list with the elements from first to last.

It is assumed that the range can be traversed from last to first.

Parameters

target	The variable to which the list is assigned.
first	The start of a range of elements.
last	The end of a range of elements.

Definition at line 324 of file aterm_list.h.

◆ make_term_list() [8/8]

template<class Term >

void atermpp::make_term_list	(	term_list< Term > &	target,
		std::initializer_list< Term >	init
	)

A constructor based on an initializer list.

This constructor is not made explicit to conform to initializer lists in standard containers.

Parameters

target	The variable to which the list is assigned.
init	The initialiser list.

Definition at line 445 of file aterm_list.h.

◆ mark_term()

void atermpp::mark_term	(	const aterm &	t,
		term_mark_stack &	todo
	)

inline

Definition at line 25 of file aterm_container.h.

◆ operator+()

template<typename Term1 , typename Term2 >

std::conditional< std::is_convertible< Term2, Term1 >::value, term_list< Term1 >, term_list< Term2 > >::type atermpp::operator+	(	const term_list< Term1 > &	l,
		const term_list< Term2 > &	m
	)

inline

Returns the concatenation of two lists with convertible element types.

The type of the result is either the type of l, if the elements of m can be converted implicitly to the type of the elements of l. Otherwise if the elements of l can be converted implicitly to the type of the elements of m, the result type is that or m.

Parameters

l	A list.
m	A list.

The complexity of this operator is linear in the length of l.

Returns: The concatenation of the lists l followed by m.

Definition at line 231 of file aterm_list_implementation.h.

◆ operator<<() [1/6]

template<typename T >

aterm_ostream & atermpp::operator<<	(	aterm_ostream &&	stream,
		const T &	t
	)

inline

Definition at line 141 of file aterm_io.h.

◆ operator<<() [2/6]

aterm_ostream & atermpp::operator<<	(	aterm_ostream &	stream,
		aterm_transformer	transformer
	)

inline

Definition at line 71 of file aterm_io.h.

◆ operator<<() [3/6]

aterm_ostream & atermpp::operator<<	(	aterm_ostream &	stream,
		const aterm &	term
	)

inline

Write the given term to the stream.

Definition at line 74 of file aterm_io.h.

◆ operator<<() [4/6]

template<typename T , typename std::enable_if_t< mcrl2::utilities::is_iterable_v< T >, int > = 0, typename std::enable_if_t<!std::is_base_of< aterm, T >::value, int > = 0>

aterm_ostream & atermpp::operator<<	(	aterm_ostream &	stream,
		const T &	container
	)

inline

Write any container (that is not an aterm itself) to the stream.

Definition at line 106 of file aterm_io.h.

◆ operator<<() [5/6]

std::ostream & atermpp::operator<<	(	std::ostream &	out,
		const atermpp::aterm &	t
	)

Send the term in textual form to the ostream.

Parameters

out	The stream to which the term is sent.
t	The term that is printed to the stream.

Returns: The stream to which the term is written.

Definition at line 394 of file aterm_io_text.cpp.

◆ operator<<() [6/6]

std::ostream & atermpp::operator<<	(	std::ostream &	out,
		const function_symbol &	f
	)

inline

Sends the name of a function symbol to an ostream.

Parameters

out	The out stream.
f	The function symbol to be output.

Returns: The stream.

Definition at line 151 of file aterm_io.h.

◆ operator>>() [1/4]

template<typename T >

aterm_istream & atermpp::operator>>	(	aterm_istream &&	stream,
		T &	t
	)

inline

Definition at line 144 of file aterm_io.h.

◆ operator>>() [2/4]

aterm_istream & atermpp::operator>>	(	aterm_istream &	stream,
		aterm &	term
	)

inline

Read the given term from the stream, but for aterm_list we want to use a specific one that performs validation (defined below).

Definition at line 77 of file aterm_io.h.

◆ operator>>() [3/4]

aterm_istream & atermpp::operator>>	(	aterm_istream &	stream,
		aterm_transformer	transformer
	)

inline

Sets the given transformer to be applied to following reads.

Definition at line 70 of file aterm_io.h.

◆ operator>>() [4/4]

template<typename T , typename std::enable_if_t< mcrl2::utilities::is_iterable_v< T >, int > = 0, typename std::enable_if_t<!std::is_base_of< aterm, T >::value, int > = 0>

aterm_istream & atermpp::operator>>	(	aterm_istream &	stream,
		T &	container
	)

inline

Read any container (that is not an aterm itself) from the stream.

Definition at line 123 of file aterm_io.h.

◆ partial_find_all_if()

template<typename Term , typename MatchPredicate , typename StopPredicate , typename OutputIterator >

void atermpp::partial_find_all_if	(	Term	t,
		MatchPredicate	match,
		StopPredicate	stop,
		OutputIterator	destBegin
	)

Finds all subterms of t that match a given predicate, and writes the found terms to the destination range starting with destBegin. The term is only partially traversed. If the stop predicate returns true in a subterm, the recursion is not continued.

Parameters

t	A term
match	The predicate that determines if a subterm is a match
stop	The predicate that determines if the recursion should not be continued in a subterm
destBegin	The iterator range to which output is written.

Definition at line 230 of file algorithm.h.

◆ partial_find_if()

template<typename Term , typename MatchPredicate , typename StopPredicate >

aterm_appl atermpp::partial_find_if	(	Term	t,
		MatchPredicate	match,
		StopPredicate	stop
	)

Finds a subterm of t that matches a given predicate. The term is only partially traversed. If the stop predicate returns true in a subterm, the recursion is not continued.

Parameters

t	A term
match	The predicate that determines if a subterm is a match
stop	The predicate that determines if the recursion should not be continued in a subterm

Returns: A subterm that matches the given predicate, or aterm_appl() if none was found.

Definition at line 204 of file algorithm.h.

◆ partial_replace()

template<typename Term , typename ReplaceFunction >

Term atermpp::partial_replace	(	Term	t,
		ReplaceFunction	r
	)

Replaces subterms x of t by r(x). The replace function r returns an additional boolean value. This value is used to prevent further recursion. The ReplaceFunction r has the following signature: aterm_appl x; std::pair<aterm_appl, bool> result = r(x); result.first is the result r(x) of the replacement result.second denotes if the recursion should be continued The replacements are performed in top down order.

Parameters

t	A term
r	The replace function that is applied to subterms.

Returns: The result of the replacement.

Definition at line 308 of file algorithm.h.

◆ pp() [1/3]

std::string atermpp::pp ( const atermpp::aterm & t )

inline

Transform an aterm to an ascii string.

Parameters

t	The input aterm.

Returns: A string representation of the given term derived from an aterm.

Definition at line 348 of file aterm.h.

◆ pp() [2/3]

const std::string & atermpp::pp ( const function_symbol & f )

inline

Prints the name of a function symbol as a string.

Parameters

f	The function symbol.

Returns: The string representation of r.

Definition at line 159 of file aterm_io.h.

◆ pp() [3/3]

template<class Term >

std::string atermpp::pp ( const term_balanced_tree< Term > t )

Definition at line 442 of file aterm_balanced_tree.h.

◆ push_back()

template<typename Term >

term_list< Term > atermpp::push_back	(	const term_list< Term > &	l,
		const Term &	el
	)

inline

Appends a new element at the end of the list. Note that the complexity of this function is O(n), with n the number of elements in the list!!!

Parameters

l	The list to which the term is appended.
el	A term.

Returns: The list l with elem appended at the end.

Definition at line 44 of file aterm_list_implementation.h.

◆ read_appl_from_string()

aterm_appl atermpp::read_appl_from_string ( const std::string & s )

inline

Reads an aterm_appl from a string. The string can be in either binary or text format.

If the input is not an aterm_appl, an aterm is returned of the wrong type.

Returns: The term corresponding to the string.

Definition at line 202 of file aterm_io.h.

◆ read_int_from_string()

aterm_int atermpp::read_int_from_string ( const std::string & s )

inline

Reads an aterm_int from a string. The string can be in either binary or text format.

If the input is not an int, an aterm is returned of the wrong type.

Returns: The aterm_int corresponding to the string.

Definition at line 192 of file aterm_io.h.

◆ read_list_from_string()

aterm_list atermpp::read_list_from_string ( const std::string & s )

inline

Reads an aterm_list from a string. The string can be in either binary or text format.

If the input is not a string, an aterm is returned of the wrong type.

Returns: The term corresponding to the string.

Definition at line 182 of file aterm_io.h.

◆ read_term_from_binary_stream()

void atermpp::read_term_from_binary_stream	(	std::istream &	is,
		aterm &	t
	)

Reads a term from a stream in binary aterm format.

Definition at line 326 of file aterm_io_binary.cpp.

◆ read_term_from_string()

aterm atermpp::read_term_from_string ( const std::string & s )

Reads an aterm from a string. The string can be in either binary or text format.

Definition at line 380 of file aterm_io_text.cpp.

◆ read_term_from_text_stream()

void atermpp::read_term_from_text_stream	(	std::istream &	is,
		aterm &	t
	)

Reads a term from a stream which contains the term in textual format.

Definition at line 388 of file aterm_io_text.cpp.

◆ reference_cast()

template<class Derived , class Base >

Derived & atermpp::reference_cast	(	Base &	t,
		typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *	= `nullptr`
	)

A cast from one aterm based type to another, as a reference, allowing to assign to it.

Parameters

t	A term of a type inheriting from an aterm.

Returns: A term of type Derived&.

Definition at line 274 of file aterm.h.

◆ remove_one_element()

template<typename Term >

term_list< Term > atermpp::remove_one_element	(	const term_list< Term > &	list,
		const Term &	t
	)

inline

Definition at line 185 of file aterm_list_implementation.h.

◆ replace() [1/2]

template<typename Term >

Term atermpp::replace	(	const Term &	t,
		const aterm &	old_value,
		const aterm &	new_value
	)

Replaces each subterm in t that is equal to old_value with new_value. The replacements are performed in top down order. For example, replace(f(f(x)), f(x), x) returns f(x) and not x.

Parameters

t	A term
old_value	The subterm that will be replaced.
new_value	The value that will be substituted.

Returns: The result of the replacement.

Definition at line 261 of file algorithm.h.

◆ replace() [2/2]

template<typename Term , typename ReplaceFunction >

Term atermpp::replace	(	const Term &	t,
		ReplaceFunction	r
	)

Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm_appl x; aterm_appl result = r(x); The replacements are performed in top down order.

Parameters

t	A term
r	The replace function that is applied to subterms.

Returns: The result of the replacement.

Definition at line 246 of file algorithm.h.

◆ reverse()

template<typename Term >

term_list< Term > atermpp::reverse ( const term_list< Term > & l )

inline

Returns the list with the elements in reversed order.

Parameters

l A list.

This operator is linear in the size of the list.

Returns: The reversed list.

Definition at line 107 of file aterm_list_implementation.h.

◆ sort_list()

template<typename Term >

term_list< Term > atermpp::sort_list	(	const term_list< Term > &	l,
		const std::function< bool(const Term &, const Term &)> &	ordering = `[](const Term& t1, const Term& t2){ return t1<t2;}`
	)

inline

Returns the list with the elements sorted according to the <-operator on the addresses of terms.

Parameters

l	A list.
ordering	An total orderings relation on Term, by default the ordering relation on Terms.

This operator has complexity nlog n where n is the size of the list.

Returns: The sorted list.

Definition at line 123 of file aterm_list_implementation.h.

◆ term_list_difference()

template<typename Term >

term_list< Term > atermpp::term_list_difference	(	const term_list< Term > &	v,
		const term_list< Term > &	w
	)

Returns v minus w.

Parameters

v	A term list.
w	A term list.

Returns: The difference of the term lists, interpreted as sets.

Definition at line 46 of file set_operations.h.

◆ term_list_union()

template<typename Term >

term_list< Term > atermpp::term_list_union	(	const term_list< Term > &	v,
		const term_list< Term > &	w
	)

Returns the union of v and w.

Parameters

v	A term list.
w	A term list.

Returns: The union of the term lists, interpreted as sets.

Definition at line 25 of file set_operations.h.

◆ vertical_cast() [1/2]

template<class Derived , class Base >

const Derived & atermpp::vertical_cast	(	const Base &	t,
		typename std::enable_if< is_convertible< Base, Derived >::value >::type *	= `nullptr`
	)

A cast form an aterm derived class to a class that inherits in possibly multiple steps from this class.

The derived class is not allowed to contain extra fields. This conversion does not require runtime computation effort. Also see down_cast.

Parameters

t	The term that is converted.

Returns: A term of type Derived.

Definition at line 307 of file aterm.h.

◆ vertical_cast() [2/2]

template<typename DerivedCont , typename Base , template< typename Elem > class Cont>

const DerivedCont & atermpp::vertical_cast	(	const Cont< Base > &	t,
		typename std::enable_if_t< is_container< DerivedCont, aterm >::value &&std::is_same_v< Cont< typename DerivedCont::value_type >, DerivedCont > &&is_convertible< Base, typename DerivedCont::value_type >::value > *	= `nullptr`
	)

Definition at line 317 of file aterm.h.

◆ write_string_with_escape_symbols()

static void atermpp::write_string_with_escape_symbols	(	const std::string &	s,
		std::ostream &	os
	)

static

Definition at line 19 of file aterm_io_text.cpp.

◆ write_term_to_binary_stream()

void atermpp::write_term_to_binary_stream	(	const aterm &	t,
		std::ostream &	os
	)

Writes term t to a stream in binary aterm format.

Definition at line 321 of file aterm_io_binary.cpp.

◆ write_term_to_text_stream()

void atermpp::write_term_to_text_stream	(	const aterm &	t,
		std::ostream &	os
	)

Writes term t to a stream in textual format.

Definition at line 375 of file aterm_io_text.cpp.

Variable Documentation

◆ BAF_MAGIC

constexpr std::uint16_t atermpp::BAF_MAGIC = 0x8baf

staticconstexpr

The magic value for a binary aterm format stream.

As of version 0x8305 the magic and version are written as 2 bytes not encoded as variable-width integers. To ensure compatibility with older formats the previously variable-width encoding is mimicked by prefixing them with 1000 (0x8).

Definition at line 21 of file aterm_io_binary.cpp.

◆ BAF_VERSION

constexpr std::uint16_t atermpp::BAF_VERSION = 0x8307

staticconstexpr

The BAF_VERSION constant is the version number of the ATerms written in BAF format. As of 29 August 2013 this version number is used by the mCRL2 toolset. Whenever the file format of mCRL2 files is changed, the BAF_VERSION has to be increased.

History:

before 2013 : version 0x0300 29 August 2013 : version changed to 0x0301 23 November 2013 : version changed to 0x0302 (introduction of index for variable types) 24 September 2014 : version changed to 0x0303 (introduction of stochastic distribution) 2 April 2017 : version changed to 0x0304 (removed a few superfluous fields in the format) 19 July 2019 : version changed to 0x8305 (introduction of the streamable aterm format) 28 February 2020 : version changed to 0x8306 (added ability to stream aterm_int, implemented structured streaming for all objects) 24 January 2023 : version changed to 0x8307 (removed NoIndex from Variables, Boolean variables. Made the .lts format more compact by not storing states with a default probability 1)

Definition at line 39 of file aterm_io_binary.cpp.

◆ LengthOfShortList

constexpr std::size_t atermpp::LengthOfShortList = 10000

constexpr

Definition at line 24 of file aterm_list_implementation.h.

◆ packet_bits

constexpr unsigned int atermpp::packet_bits = 2

staticconstexpr

The number of bits needed to store an element of packet_type.

Definition at line 52 of file aterm_io_binary.cpp.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Detailed Description

Typedef Documentation

◆ aterm_appl

◆ aterm_balanced_tree

◆ aterm_list

◆ aterm_transformer

◆ term_callback

◆ term_mark_stack

Enumeration Type Documentation

◆ packet_type

Function Documentation

◆ add_deletion_hook()

◆ as_set()

◆ as_vector()

◆ bottom_up_replace() [1/3]

◆ bottom_up_replace() [2/3]

◆ bottom_up_replace() [3/3]

◆ container_cast()

◆ down_cast()

◆ empty_string()

◆ find_all_if()

◆ find_if()

◆ for_each()

◆ function_symbol_generator_mutex()

◆ generator_sequence_number()

◆ identity()

◆ is_aterm_balanced_tree()

◆ make_aterm_int()

◆ make_reverse()

◆ make_term_appl() [1/5]

◆ make_term_appl() [2/5]

◆ make_term_appl() [3/5]

◆ make_term_appl() [4/5]

◆ make_term_appl() [5/5]

◆ make_term_appl_with_index()

◆ make_term_balanced_tree()

◆ make_term_list() [1/8]

◆ make_term_list() [2/8]

◆ make_term_list() [3/8]

◆ make_term_list() [4/8]

◆ make_term_list() [5/8]

◆ make_term_list() [6/8]

◆ make_term_list() [7/8]

◆ make_term_list() [8/8]

◆ mark_term()

◆ operator+()

◆ operator<<() [1/6]

◆ operator<<() [2/6]

◆ operator<<() [3/6]

◆ operator<<() [4/6]

◆ operator<<() [5/6]

◆ operator<<() [6/6]

◆ operator>>() [1/4]

◆ operator>>() [2/4]

◆ operator>>() [3/4]

◆ operator>>() [4/4]

◆ partial_find_all_if()

◆ partial_find_if()

◆ partial_replace()

◆ pp() [1/3]

◆ pp() [2/3]

◆ pp() [3/3]

◆ push_back()

◆ read_appl_from_string()

◆ read_int_from_string()

◆ read_list_from_string()

◆ read_term_from_binary_stream()

◆ read_term_from_string()

◆ read_term_from_text_stream()

◆ reference_cast()

◆ remove_one_element()

◆ replace() [1/2]

◆ replace() [2/2]

◆ reverse()