mcrl2::data::application

Include file:

#include "mcrl2/data/application.h
class mcrl2::data::application

An application of a data expression to a number of arguments.

Private types

type iterator

typedef for data_expression::iterator

Public types

type const_iterator

typedef for atermpp::term_appl_iterator< data_expression >

An iterator to traverse the arguments of an application.

There is a subtle difference with the arguments of an iterator on the arguments of an aterm_appl from which an application is derived. As an application has a head as its first argument, the iterator of the aterm_appl starts at this head, where the iterator of the application starts at the first argument. This also means that t[n] for t an application is equal to t[n+1] if t is interpreted as an aterm_appl.

Public member functions

application()

Default constructor.

application(const data_expression &head, const data_expression &arg1)

Constructor.

application(const data_expression &head, const data_expression &arg1, const data_expression &arg2)

Constructor.

application(const data_expression &head, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)

Constructor.

application(const data_expression &head, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4)

Constructor.

application(const data_expression &head, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5)

Constructor.

application(const data_expression &head, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3, const data_expression &arg4, const data_expression &arg5, const data_expression &arg6)

Constructor.

application(const atermpp::aterm &term)

Constructor.

Parameters:

  • term A term
application(const data_expression &head, const Container &arguments, typename atermpp::enable_if_container<Container, data_expression>::type * = nullptr)

Constructor.

application(const data_expression &head, FwdIter first, FwdIter last, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=nullptr)

Constructor.

application(const std::size_t arity, const data_expression &head, FwdIter first, FwdIter last, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=0)

Constructor.

application(const data_expression &head, FwdIter first, FwdIter last, ArgumentConverter convert_arguments, typename std::enable_if< !std::is_base_of< data_expression, FwdIter >::value >::type *=nullptr, typename std::enable_if< !std::is_base_of< data_expression, ArgumentConverter >::value >::type *=nullptr)

Constructor.

application(const application&) noexcept = default

Move semantics.

application(application&&) noexcept = default
const_iterator begin() const

Returns an iterator pointing to the first argument of the application.

const_iterator end() const

Returns an iterator pointing past the last argument of the application.

const data_expression &head() const

Get the function at the head of this expression.

application &operator=(const application&) noexcept = default
application &operator=(application&&) noexcept = default
const data_expression &operator[](std::size_t index) const

Get the i-th argument of this expression.

std::size_t size() const

Returns: The number of arguments of this application.