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

\brief A constructor for a structured sort More...

#include <structured_sort_constructor.h>

Inheritance diagram for mcrl2::data::structured_sort_constructor:
atermpp::aterm atermpp::aterm_core atermpp::unprotected_aterm_core

Classes

struct  get_argument_sort
 

Public Member Functions

 structured_sort_constructor ()
 \brief Default constructor X3.
 
 structured_sort_constructor (const atermpp::aterm &term)
 
 structured_sort_constructor (const core::identifier_string &name, const structured_sort_constructor_argument_list &arguments, core::identifier_string &recogniser)
 \brief Constructor Z12.
 
template<typename Container >
 structured_sort_constructor (const std::string &name, const Container &arguments, const std::string &recogniser, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
 \brief Constructor Z1.
 
 structured_sort_constructor (const structured_sort_constructor &) noexcept=default
 Move semantics.
 
 structured_sort_constructor (structured_sort_constructor &&) noexcept=default
 
structured_sort_constructoroperator= (const structured_sort_constructor &) noexcept=default
 
structured_sort_constructoroperator= (structured_sort_constructor &&) noexcept=default
 
const core::identifier_stringname () const
 
const structured_sort_constructor_argument_listarguments () const
 
const core::identifier_stringrecogniser () const
 
 structured_sort_constructor (const core::identifier_string &name, const core::identifier_string &recogniser)
 Constructor.
 
 structured_sort_constructor (const std::string &name, const std::string &recogniser)
 Constructor.
 
template<typename Container >
 structured_sort_constructor (const std::string &name, const structured_sort_constructor_argument_list &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=0)
 Constructor.
 
template<typename Container >
 structured_sort_constructor (const std::string &name, const Container &arguments, typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
 Constructor.
 
 structured_sort_constructor (const core::identifier_string &name)
 Constructor.
 
 structured_sort_constructor (const std::string &name)
 Constructor.
 
template<typename Container , std::size_t S, std::size_t S0>
 structured_sort_constructor (const char(&name)[S], const Container &arguments, const char(&recogniser)[S0], typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *=nullptr)
 
function_symbol constructor_function (const sort_expression &s) const
 Returns the constructor function for this constructor, assuming it is internally represented with sort s.
 
function_symbol_vector projection_functions (const sort_expression &s) const
 Returns the projection functions for this constructor.
 
function_symbol recogniser_function (const sort_expression &s) const
 Returns the function corresponding to the recogniser of this constructor, such that it is usable in the rewriter.
 
- 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.
 
atermoperator= (const aterm &other) noexcept=default
 
 aterm (aterm &&other) noexcept=default
 
atermoperator= (aterm &&other) noexcept=default
 
template<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>
 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 , 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>
 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 , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>
 aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
 
 aterm (const function_symbol &sym)
 Constructor.
 
template<typename ... Terms>
 aterm (const function_symbol &symbol, const Terms &...arguments)
 Constructor for n-arity function application.
 
const function_symbolfunction () 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 atermoperator[] (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_coreoperator= (const aterm_core &other) noexcept
 Assignment operator.
 
aterm_coreassign (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_coreunprotected_assign (const aterm_core &other) noexcept
 Assignment operator, to be used when the busy flags do not need to be set.
 
aterm_coreoperator= (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.
 
bool operator!= (const unprotected_aterm_core &t) const
 Inequality operator on two unprotected aterms.
 
bool operator< (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool operator> (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool operator<= (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool 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_symbolfunction () const
 Yields the function symbol in an aterm.
 

Protected Member Functions

template<typename OutIter >
void argument_sorts (OutIter out) const
 Returns the sorts of the arguments in an output iterator.
 
- Protected Member Functions inherited from atermpp::aterm
 aterm (detail::_term_appl *t)
 Constructor.
 

Friends

class structured_sort
 

Additional Inherited Members

- Public Types inherited from atermpp::aterm
typedef std::size_t size_type
 An unsigned integral type.
 
typedef ptrdiff_t difference_type
 A signed integral type.
 
typedef term_appl_iterator< atermiterator
 Iterator used to iterate through an term_appl.
 
typedef term_appl_iterator< atermconst_iterator
 Const iterator used to iterate through an term_appl.
 
- Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_atermm_term
 

Detailed Description

\brief A constructor for a structured sort

Definition at line 28 of file structured_sort_constructor.h.

Constructor & Destructor Documentation

◆ structured_sort_constructor() [1/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( )
inline

\brief Default constructor X3.

Definition at line 32 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [2/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const atermpp::aterm term)
inlineexplicit

\brief Constructor Z9. \param term A term

Definition at line 38 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [3/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const core::identifier_string name,
const structured_sort_constructor_argument_list arguments,
core::identifier_string recogniser 
)
inline

\brief Constructor Z12.

Definition at line 45 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [4/13]

template<typename Container >
mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const std::string &  name,
const Container &  arguments,
const std::string &  recogniser,
typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *  = nullptr 
)
inline

\brief Constructor Z1.

Definition at line 51 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [5/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const structured_sort_constructor )
defaultnoexcept

Move semantics.

◆ structured_sort_constructor() [6/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( structured_sort_constructor &&  )
defaultnoexcept

◆ structured_sort_constructor() [7/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const core::identifier_string name,
const core::identifier_string recogniser 
)
inline

Constructor.

Definition at line 102 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [8/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const std::string &  name,
const std::string &  recogniser 
)
inline

Constructor.

Definition at line 107 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [9/13]

template<typename Container >
mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const std::string &  name,
const structured_sort_constructor_argument_list arguments,
typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *  = 0 
)
inline

Constructor.

Definition at line 113 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [10/13]

template<typename Container >
mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const std::string &  name,
const Container &  arguments,
typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *  = nullptr 
)
inline

Constructor.

Definition at line 119 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [11/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const core::identifier_string name)
inline

Constructor.

Definition at line 124 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [12/13]

mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const std::string &  name)
inline

Constructor.

Definition at line 129 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [13/13]

template<typename Container , std::size_t S, std::size_t S0>
mcrl2::data::structured_sort_constructor::structured_sort_constructor ( const char(&)  name[S],
const Container &  arguments,
const char(&)  recogniser[S0],
typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type *  = nullptr 
)
inline

Definition at line 137 of file structured_sort_constructor.h.

Member Function Documentation

◆ argument_sorts()

template<typename OutIter >
void mcrl2::data::structured_sort_constructor::argument_sorts ( OutIter  out) const
inlineprotected

Returns the sorts of the arguments in an output iterator.

Definition at line 92 of file structured_sort_constructor.h.

◆ arguments()

const structured_sort_constructor_argument_list & mcrl2::data::structured_sort_constructor::arguments ( ) const
inline

Definition at line 66 of file structured_sort_constructor.h.

◆ constructor_function()

function_symbol mcrl2::data::structured_sort_constructor::constructor_function ( const sort_expression s) const
inline

Returns the constructor function for this constructor, assuming it is internally represented with sort s.

Parameters
sSort expression this sort is internally represented as.

In general, constructor_function is used with s the structured sort of which this constructor is a part. Consider for example struct c|d, be a structured sort, where this constructor is c, then this.constructor_function(struct c|d) returns the fuction symbol c : struct c|d, i.e. the function c of sort struct c|d.

Definition at line 154 of file structured_sort_constructor.h.

◆ name()

const core::identifier_string & mcrl2::data::structured_sort_constructor::name ( ) const
inline

Definition at line 61 of file structured_sort_constructor.h.

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

◆ projection_functions()

function_symbol_vector mcrl2::data::structured_sort_constructor::projection_functions ( const sort_expression s) const
inline

Returns the projection functions for this constructor.

Parameters
sThe sort as which the structured sort this constructor corresponds to is treated internally.

Definition at line 166 of file structured_sort_constructor.h.

◆ recogniser()

const core::identifier_string & mcrl2::data::structured_sort_constructor::recogniser ( ) const
inline

Definition at line 71 of file structured_sort_constructor.h.

◆ recogniser_function()

function_symbol mcrl2::data::structured_sort_constructor::recogniser_function ( const sort_expression s) const
inline

Returns the function corresponding to the recogniser of this constructor, such that it is usable in the rewriter.

Parameters
sThe sort as which the structured sort this constructor corresponds to is treated internally.

Definition at line 183 of file structured_sort_constructor.h.

Friends And Related Symbol Documentation

◆ structured_sort

friend class structured_sort
friend

Definition at line 76 of file structured_sort_constructor.h.


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