structured sort. More...

#include <structured_sort.h>

Inheritance diagram for mcrl2::data::structured_sort:

Public Member Functions
	structured_sort ()
	\brief Default constructor X3.

	structured_sort (const atermpp::aterm &term)

	structured_sort (const structured_sort_constructor_list &constructors)
	\brief Constructor Z14.

template<typename Container > requires (atermpp::is_container<Container, structured_sort_constructor>::value)
	structured_sort (const Container &constructors)
	\brief Constructor Z2.

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

	structured_sort (structured_sort &&) noexcept=default

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

structured_sort &	operator= (structured_sort &&) noexcept=default

const structured_sort_constructor_list &	constructors () const

function_symbol_vector	constructor_functions () const
	Returns the constructor functions of this sort, such that the result can be used by the rewriter.

function_symbol_vector	comparison_functions () const
	Returns the additional functions of this sort, used to implement its comparison operators.

function_symbol_vector	projection_functions () const
	Returns the projection functions of this sort, such that the result can be used by the rewriter.

function_symbol_vector	recogniser_functions () const
	Returns the recogniser functions of this sort, such that the result can be used by the rewriter.

data_equation_vector	constructor_equations () const
	Returns the equations for ==, < and <= for this sort, such that the result can be used by the rewriter internally.

data_equation_vector	comparison_equations () const
	Returns the equations for the functions used to implement comparison operators on this sort. Needed to do proper rewriting.

data_equation_vector	projection_equations () const
	Generate equations for the projection functions of this sort.

data_equation_vector	recogniser_equations () const
	Generate equations for the recognisers of this sort, assuming that this sort is referred to with s.

Public Member Functions inherited from mcrl2::data::sort_expression
	sort_expression ()
	\brief Default constructor X3.

	sort_expression (const atermpp::aterm &term)

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

	sort_expression (sort_expression &&) noexcept=default

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

sort_expression &	operator= (sort_expression &&) noexcept=default

const sort_expression &	target_sort () const
	Returns the target sort of this 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
function_symbol	to_pos_function (const sort_expression &s) const

function_symbol	equal_arguments_function (const sort_expression &s) const

function_symbol	smaller_arguments_function (const sort_expression &s) const

function_symbol	smaller_equal_arguments_function (const sort_expression &s) const

function_symbol_vector	constructor_functions (const sort_expression &s) const

function_symbol_vector	comparison_functions (const sort_expression &s) const

function_symbol_vector	projection_functions (const sort_expression &s) const

function_symbol_vector	recogniser_functions (const sort_expression &s) const

data_equation_vector	comparison_equations (const sort_expression &s) const

data_equation_vector	constructor_equations (const sort_expression &s) const

data_equation_vector	projection_equations (const sort_expression &s) const

data_equation_vector	recogniser_equations (const sort_expression &s) const

Static Private Member Functions
static bool	has_recogniser (structured_sort_constructor const &s)

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

structured sort.

A structured sort is a sort with the following structure: struct c1(pr1,1:S1,1, ..., pr1,k1:S1,k1)?is_c1 | ... | cn(prn,1:Sn,1, ..., prn,kn:Sn,kn)?is_cn in this:

c1, ..., cn are called constructors.
pri,j are the projection functions (or constructor arguments).
is_ci are the recognisers. \brief A structured sort

Definition at line 53 of file structured_sort.h.

Constructor & Destructor Documentation

◆ structured_sort() [1/6]

mcrl2::data::structured_sort::structured_sort ( )

inline

\brief Default constructor X3.

Definition at line 57 of file structured_sort.h.

◆ structured_sort() [2/6]

mcrl2::data::structured_sort::structured_sort ( const atermpp::aterm & term )

inlineexplicit

\brief Constructor Z9. \param term A term

Definition at line 63 of file structured_sort.h.

◆ structured_sort() [3/6]

mcrl2::data::structured_sort::structured_sort ( const structured_sort_constructor_list & constructors )

inlineexplicit

\brief Constructor Z14.

Definition at line 70 of file structured_sort.h.

◆ structured_sort() [4/6]

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

mcrl2::data::structured_sort::structured_sort ( const Container & constructors )

inline

\brief Constructor Z2.

Definition at line 76 of file structured_sort.h.

◆ structured_sort() [5/6]

mcrl2::data::structured_sort::structured_sort ( const structured_sort & )

defaultnoexcept

Move semantics.

◆ structured_sort() [6/6]

mcrl2::data::structured_sort::structured_sort ( structured_sort && )

defaultnoexcept

Member Function Documentation

◆ comparison_equations() [1/2]

data_equation_vector mcrl2::data::structured_sort::comparison_equations ( ) const

inline

Returns the equations for the functions used to implement comparison operators on this sort. Needed to do proper rewriting.

Definition at line 420 of file structured_sort.h.

◆ comparison_equations() [2/2]

data_equation_vector mcrl2::data::structured_sort::comparison_equations ( const sort_expression & s ) const

inlineprivate

Definition at line 182 of file structured_sort.h.

◆ comparison_functions() [1/2]

function_symbol_vector mcrl2::data::structured_sort::comparison_functions ( ) const

inline

Returns the additional functions of this sort, used to implement its comparison operators.

Definition at line 390 of file structured_sort.h.

◆ comparison_functions() [2/2]

function_symbol_vector mcrl2::data::structured_sort::comparison_functions ( const sort_expression & s ) const

inlineprivate

Definition at line 143 of file structured_sort.h.

◆ constructor_equations() [1/2]

data_equation_vector mcrl2::data::structured_sort::constructor_equations ( ) const

inline

Returns the equations for ==, < and <= for this sort, such that the result can be used by the rewriter internally.

Definition at line 412 of file structured_sort.h.

◆ constructor_equations() [2/2]

data_equation_vector mcrl2::data::structured_sort::constructor_equations ( const sort_expression & s ) const

inlineprivate

Definition at line 265 of file structured_sort.h.

◆ constructor_functions() [1/2]

function_symbol_vector mcrl2::data::structured_sort::constructor_functions ( ) const

inline

Returns the constructor functions of this sort, such that the result can be used by the rewriter.

Definition at line 383 of file structured_sort.h.

◆ constructor_functions() [2/2]

function_symbol_vector mcrl2::data::structured_sort::constructor_functions ( const sort_expression & s ) const

inlineprivate

Definition at line 133 of file structured_sort.h.

◆ constructors()

const structured_sort_constructor_list & mcrl2::data::structured_sort::constructors ( ) const

inline

Definition at line 86 of file structured_sort.h.

◆ equal_arguments_function()

function_symbol mcrl2::data::structured_sort::equal_arguments_function ( const sort_expression & s ) const

inlineprivate

Definition at line 115 of file structured_sort.h.

◆ has_recogniser()

static bool mcrl2::data::structured_sort::has_recogniser ( structured_sort_constructor const & s )

inlinestaticprivate

Definition at line 104 of file structured_sort.h.

◆ operator=() [1/2]

structured_sort & mcrl2::data::structured_sort::operator= ( const structured_sort & )

defaultnoexcept

◆ operator=() [2/2]

structured_sort & mcrl2::data::structured_sort::operator= ( structured_sort && )

defaultnoexcept

◆ projection_equations() [1/2]

data_equation_vector mcrl2::data::structured_sort::projection_equations ( ) const

inline

Generate equations for the projection functions of this sort.

Returns: A vector of equations for the projection functions of this sort.

Definition at line 427 of file structured_sort.h.

◆ projection_equations() [2/2]

data_equation_vector mcrl2::data::structured_sort::projection_equations ( const sort_expression & s ) const

inlineprivate

Definition at line 298 of file structured_sort.h.

◆ projection_functions() [1/2]

function_symbol_vector mcrl2::data::structured_sort::projection_functions ( ) const

inline

Returns the projection functions of this sort, such that the result can be used by the rewriter.

Definition at line 397 of file structured_sort.h.

◆ projection_functions() [2/2]

function_symbol_vector mcrl2::data::structured_sort::projection_functions ( const sort_expression & s ) const

inlineprivate

Definition at line 153 of file structured_sort.h.

◆ recogniser_equations() [1/2]

data_equation_vector mcrl2::data::structured_sort::recogniser_equations ( ) const

inline

Generate equations for the recognisers of this sort, assuming that this sort is referred to with s.

Returns: A vector of equations for the recognisers of this sort.

Definition at line 435 of file structured_sort.h.

◆ recogniser_equations() [2/2]

data_equation_vector mcrl2::data::structured_sort::recogniser_equations ( const sort_expression & s ) const

inlineprivate

Definition at line 336 of file structured_sort.h.

◆ recogniser_functions() [1/2]

function_symbol_vector mcrl2::data::structured_sort::recogniser_functions ( ) const

inline

Returns the recogniser functions of this sort, such that the result can be used by the rewriter.

Definition at line 405 of file structured_sort.h.

◆ recogniser_functions() [2/2]

function_symbol_vector mcrl2::data::structured_sort::recogniser_functions ( const sort_expression & s ) const

inlineprivate

Definition at line 168 of file structured_sort.h.

◆ smaller_arguments_function()

function_symbol mcrl2::data::structured_sort::smaller_arguments_function ( const sort_expression & s ) const

inlineprivate

Definition at line 121 of file structured_sort.h.

◆ smaller_equal_arguments_function()

function_symbol mcrl2::data::structured_sort::smaller_equal_arguments_function ( const sort_expression & s ) const

inlineprivate

Definition at line 127 of file structured_sort.h.

◆ to_pos_function()

function_symbol mcrl2::data::structured_sort::to_pos_function ( const sort_expression & s ) const

inlineprivate

Definition at line 109 of file structured_sort.h.

Friends And Related Symbol Documentation

◆ data_specification

friend class data_specification

friend

Definition at line 92 of file structured_sort.h.

◆ sort_fbag::fbag_generate_constructors_code

function_symbol_vector sort_fbag::fbag_generate_constructors_code ( const sort_expression & )

friend

◆ sort_fbag::fbag_generate_equations_code

data_equation_vector sort_fbag::fbag_generate_equations_code ( const sort_expression & )

friend

◆ sort_fbag::fbag_generate_functions_code

function_symbol_vector sort_fbag::fbag_generate_functions_code ( const sort_expression & )

friend

◆ sort_fset::fset_generate_constructors_code

function_symbol_vector sort_fset::fset_generate_constructors_code ( const sort_expression & )

friend

◆ sort_fset::fset_generate_equations_code

data_equation_vector sort_fset::fset_generate_equations_code ( const sort_expression & )

friend

◆ sort_fset::fset_generate_functions_code

function_symbol_vector sort_fset::fset_generate_functions_code ( const sort_expression & )

friend

◆ sort_specification

friend class sort_specification

friend

Definition at line 93 of file structured_sort.h.

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

data/include/mcrl2/data/structured_sort.h

Friends
class	data_specification

class	sort_specification

function_symbol_vector	sort_fset::fset_generate_constructors_code (const sort_expression &)

function_symbol_vector	sort_fset::fset_generate_functions_code (const sort_expression &)

data_equation_vector	sort_fset::fset_generate_equations_code (const sort_expression &)

function_symbol_vector	sort_fbag::fbag_generate_constructors_code (const sort_expression &)

function_symbol_vector	sort_fbag::fbag_generate_functions_code (const sort_expression &)

data_equation_vector	sort_fbag::fbag_generate_equations_code (const sort_expression &)

Public Member Functions

Private Member Functions

Static Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ structured_sort() [1/6]

◆ structured_sort() [2/6]

◆ structured_sort() [3/6]

◆ structured_sort() [4/6]

◆ structured_sort() [5/6]

◆ structured_sort() [6/6]

Member Function Documentation

◆ comparison_equations() [1/2]

◆ comparison_equations() [2/2]

◆ comparison_functions() [1/2]

◆ comparison_functions() [2/2]

◆ constructor_equations() [1/2]

◆ constructor_equations() [2/2]

◆ constructor_functions() [1/2]

◆ constructor_functions() [2/2]

◆ constructors()

◆ equal_arguments_function()

◆ has_recogniser()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ projection_equations() [1/2]

◆ projection_equations() [2/2]

◆ projection_functions() [1/2]

◆ projection_functions() [2/2]

◆ recogniser_equations() [1/2]

◆ recogniser_equations() [2/2]

◆ recogniser_functions() [1/2]

◆ recogniser_functions() [2/2]

◆ smaller_arguments_function()

◆ smaller_equal_arguments_function()

◆ to_pos_function()

Friends And Related Symbol Documentation

◆ data_specification

◆ sort_fbag::fbag_generate_constructors_code

◆ sort_fbag::fbag_generate_equations_code

◆ sort_fbag::fbag_generate_functions_code

◆ sort_fset::fset_generate_constructors_code

◆ sort_fset::fset_generate_equations_code

◆ sort_fset::fset_generate_functions_code

◆ sort_specification