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

#include <structured_sort_constructor.h>

Inheritance diagram for mcrl2::data::structured_sort_constructor:

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 > requires (atermpp::is_container<Container, structured_sort_constructor_argument>::value)
	structured_sort_constructor (const std::string &name, const Container &arguments, const std::string &recogniser)
	\brief Constructor Z1.

	structured_sort_constructor (const structured_sort_constructor &) noexcept=default
	Move semantics.

	structured_sort_constructor (structured_sort_constructor &&) noexcept=default

structured_sort_constructor &	operator= (const structured_sort_constructor &) noexcept=default

structured_sort_constructor &	operator= (structured_sort_constructor &&) noexcept=default

const core::identifier_string &	name () const

const structured_sort_constructor_argument_list &	arguments () const

const core::identifier_string &	recogniser () 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.

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.

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
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 Attributes inherited from atermpp::unprotected_aterm_core
const detail::_aterm *	m_term

Detailed Description

\brief A constructor for a structured sort

Definition at line 25 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 29 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 35 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 42 of file structured_sort_constructor.h.

◆ structured_sort_constructor() [4/13]

template<typename Container >
requires (atermpp::is_container<Container, structured_sort_constructor_argument>::value)

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

inline

\brief Constructor Z1.

Definition at line 48 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 99 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 104 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 110 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 116 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 121 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 126 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 134 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 89 of file structured_sort_constructor.h.

◆ arguments()

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

inline

Definition at line 63 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

s	Sort 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 151 of file structured_sort_constructor.h.

◆ name()

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

inline

Definition at line 58 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

s	The sort as which the structured sort this constructor corresponds to is treated internally.

Definition at line 163 of file structured_sort_constructor.h.

◆ recogniser()

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

inline

Definition at line 68 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

s	The sort as which the structured sort this constructor corresponds to is treated internally.

Definition at line 180 of file structured_sort_constructor.h.

Friends And Related Symbol Documentation

◆ structured_sort

friend class structured_sort

friend

Definition at line 73 of file structured_sort_constructor.h.

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

data/include/mcrl2/data/structured_sort_constructor.h

Classes

Public Member Functions

Protected Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ structured_sort_constructor() [1/13]

◆ structured_sort_constructor() [2/13]

◆ structured_sort_constructor() [3/13]

◆ structured_sort_constructor() [4/13]

◆ structured_sort_constructor() [5/13]

◆ structured_sort_constructor() [6/13]

◆ structured_sort_constructor() [7/13]

◆ structured_sort_constructor() [8/13]

◆ structured_sort_constructor() [9/13]

◆ structured_sort_constructor() [10/13]

◆ structured_sort_constructor() [11/13]

◆ structured_sort_constructor() [12/13]

◆ structured_sort_constructor() [13/13]

Member Function Documentation

◆ argument_sorts()

◆ arguments()

◆ constructor_function()

◆ name()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ projection_functions()

◆ recogniser()

◆ recogniser_function()

Friends And Related Symbol Documentation

◆ structured_sort