mCRL2
Loading...
Searching...
No Matches
mcrl2::data::data_expression Class Reference

data expression. More...

#include <data_expression.h>

Inheritance diagram for mcrl2::data::data_expression:
atermpp::aterm atermpp::aterm_core atermpp::unprotected_aterm_core mcrl2::data::abstraction mcrl2::data::application mcrl2::data::function_symbol mcrl2::data::machine_number mcrl2::data::untyped_identifier mcrl2::data::variable mcrl2::data::where_clause mcrl2::lps::probabilistic_data_expression

Public Member Functions

 data_expression ()
 \brief Default constructor X3.
 
 data_expression (const atermpp::aterm &term)
 
 data_expression (const data_expression &) noexcept=default
 Move semantics.
 
 data_expression (data_expression &&) noexcept=default
 
data_expression & operator= (const data_expression &) noexcept=default
 
data_expression & operator= (data_expression &&) noexcept=default
 
bool is_default_data_expression () const
 A function to efficiently determine whether a data expression is made by the default constructor.
 
application operator() (const data_expression &e) const
 Apply a data expression to a data expression.
 
application operator() (const data_expression &e1, const data_expression &e2) const
 Apply a data expression to two data expressions.
 
application operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3) const
 Apply a data expression to three data expressions.
 
application operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
 Apply a data expression to four data expressions.
 
application operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
 Apply a data expression to five data expressions.
 
application operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
 Apply a data expression to six data expressions.
 
sort_expression sort () const
 Returns the sort of the data expression.
 
- Public Member Functions inherited from atermpp::aterm
 aterm ()
 Default constructor.
 
 aterm (const aterm &other) noexcept=default
 This class has user-declared copy constructor so declare default copy and move operators.
 
aterm & operator= (const aterm &other) noexcept=default
 
 aterm (aterm &&other) noexcept=default
 
aterm & operator= (aterm &&other) noexcept=default
 
template<class ForwardIterator >
requires (mcrl2::utilities::is_iterator<ForwardIterator>::value && !std::is_same_v<typename ForwardIterator::iterator_category, std::input_iterator_tag> && !std::is_same_v<typename ForwardIterator::iterator_category, std::output_iterator_tag>)
 aterm (const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
 Constructor that provides an aterm based on a function symbol and forward iterator providing the arguments.
 
template<class InputIterator >
requires mcrl2::utilities::is_iterator<InputIterator>
 aterm (const function_symbol &sym, InputIterator begin, InputIterator end)
 Constructor that provides an aterm based on a function symbol and an input iterator providing the arguments.
 
template<class InputIterator , class TermConverter >
requires mcrl2::utilities::is_iterator<InputIterator>
 aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
 Constructor.
 
template<typename... Terms>
 aterm (const function_symbol &symbol, const Terms &... arguments)
 Constructor for n-arity function application.
 
const function_symbol & function () const
 Returns the function symbol belonging to an aterm.
 
size_type size () const
 Returns the number of arguments of this term.
 
bool empty () const
 Returns true if the term has no arguments.
 
const_iterator begin () const
 Returns an iterator pointing to the first argument.
 
const_iterator end () const
 Returns a const_iterator pointing past the last argument.
 
constexpr size_type max_size () const
 Returns the largest possible number of arguments.
 
const aterm & operator[] (const size_type i) const
 Returns the i-th argument.
 
- Public Member Functions inherited from atermpp::aterm_core
 aterm_core () noexcept
 Default constructor.
 
 ~aterm_core () noexcept
 Standard destructor.
 
 aterm_core (const detail::_aterm *t) noexcept
 Constructor based on an internal term data structure. This is not for public use.
 
 aterm_core (const aterm_core &other) noexcept
 Copy constructor.
 
 aterm_core (aterm_core &&other) noexcept
 Move constructor.
 
aterm_core & operator= (const aterm_core &other) noexcept
 Assignment operator.
 
aterm_core & assign (const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
 Assignment operator, to be used if busy and forbidden flags are explicitly available.
 
template<bool CHECK_BUSY_FLAG = true>
aterm_core & unprotected_assign (const aterm_core &other) noexcept
 Assignment operator, to be used when the busy flags do not need to be set.
 
aterm_core & operator= (aterm_core &&other) noexcept
 Move assignment operator.
 
- Public Member Functions inherited from atermpp::unprotected_aterm_core
 unprotected_aterm_core () noexcept
 Default constuctor.
 
 unprotected_aterm_core (const detail::_aterm *term) noexcept
 Constructor.
 
bool type_is_appl () const noexcept
 Dynamic check whether the term is an aterm.
 
bool type_is_int () const noexcept
 Dynamic check whether the term is an aterm_int.
 
bool type_is_list () const noexcept
 Dynamic check whether the term is an aterm_list.
 
bool operator== (const unprotected_aterm_core &t) const
 Comparison operator.
 
std::weak_ordering operator<=> (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool defined () const
 Returns true if this term is not equal to the term assigned by the default constructor of aterms, aterm_appls and aterm_int.
 
void swap (unprotected_aterm_core &t) noexcept
 Swaps this term with its argument.
 
const function_symbol & function () const
 Yields the function symbol in an aterm.
 

Private Member Functions

const_iterator begin () const
 
const_iterator end () const
 

Additional Inherited Members

- Public Types inherited from atermpp::aterm
using size_type = std::size_t
 An unsigned integral type.
 
using difference_type = ptrdiff_t
 A signed integral type.
 
using iterator = term_appl_iterator< aterm >
 Iterator used to iterate through an term_appl.
 
using const_iterator = term_appl_iterator< aterm >
 Const iterator used to iterate through an term_appl.
 
- Protected Member Functions inherited from atermpp::aterm
 aterm (detail::_term_appl *t)
 Constructor.
 
- Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_aterm * m_term
 

Detailed Description

data expression.

A data expression can be any of:

  • variable
  • function symbol
  • application
  • abstraction
  • where clause
  • set enumeration
  • bag enumeration \brief A data expression

Definition at line 129 of file data_expression.h.

Constructor & Destructor Documentation

◆ data_expression() [1/4]

mcrl2::data::data_expression::data_expression ( )
inline

\brief Default constructor X3.

Definition at line 133 of file data_expression.h.

◆ data_expression() [2/4]

mcrl2::data::data_expression::data_expression ( const atermpp::aterm &  term)
inlineexplicit

\brief Constructor Z9. \param term A term

Definition at line 139 of file data_expression.h.

◆ data_expression() [3/4]

mcrl2::data::data_expression::data_expression ( const data_expression &  )
defaultnoexcept

Move semantics.

◆ data_expression() [4/4]

mcrl2::data::data_expression::data_expression ( data_expression &&  )
defaultnoexcept

Member Function Documentation

◆ begin()

const_iterator mcrl2::data::data_expression::begin ( ) const
private

◆ end()

const_iterator mcrl2::data::data_expression::end ( ) const
private

◆ is_default_data_expression()

bool mcrl2::data::data_expression::is_default_data_expression ( ) const
inline

A function to efficiently determine whether a data expression is made by the default constructor.

Definition at line 153 of file data_expression.h.

◆ operator()() [1/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e) const
inline

Apply a data expression to a data expression.

Definition at line 315 of file data_expression.h.

◆ operator()() [2/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e1,
const data_expression &  e2 
) const
inline

Apply a data expression to two data expressions.

Definition at line 322 of file data_expression.h.

◆ operator()() [3/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e1,
const data_expression &  e2,
const data_expression &  e3 
) const
inline

Apply a data expression to three data expressions.

Definition at line 329 of file data_expression.h.

◆ operator()() [4/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e1,
const data_expression &  e2,
const data_expression &  e3,
const data_expression &  e4 
) const
inline

Apply a data expression to four data expressions.

Definition at line 336 of file data_expression.h.

◆ operator()() [5/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e1,
const data_expression &  e2,
const data_expression &  e3,
const data_expression &  e4,
const data_expression &  e5 
) const
inline

Apply a data expression to five data expressions.

Definition at line 343 of file data_expression.h.

◆ operator()() [6/6]

application mcrl2::data::data_expression::operator() ( const data_expression &  e1,
const data_expression &  e2,
const data_expression &  e3,
const data_expression &  e4,
const data_expression &  e5,
const data_expression &  e6 
) const
inline

Apply a data expression to six data expressions.

Definition at line 350 of file data_expression.h.

◆ operator=() [1/2]

data_expression & mcrl2::data::data_expression::operator= ( const data_expression &  )
defaultnoexcept

◆ operator=() [2/2]

data_expression & mcrl2::data::data_expression::operator= ( data_expression &&  )
defaultnoexcept

◆ sort()

sort_expression mcrl2::data::data_expression::sort ( ) const

Returns the sort of the data expression.

Definition at line 107 of file data.cpp.


The documentation for this class was generated from the following files: