mcrl2::data::structured_sort

Include file:

#include "mcrl2/data/structured_sort.h

class mcrl2::data::structured_sort

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

Friends

friend class mcrl2::data::structured_sort::data_specification

friend function_symbol_vector mcrl2::data::structured_sort::sort_fbag::fbag_generate_constructors_code

friend data_equation_vector mcrl2::data::structured_sort::sort_fbag::fbag_generate_equations_code

friend function_symbol_vector mcrl2::data::structured_sort::sort_fbag::fbag_generate_functions_code

friend function_symbol_vector mcrl2::data::structured_sort::sort_fset::fset_generate_constructors_code

friend data_equation_vector mcrl2::data::structured_sort::sort_fset::fset_generate_equations_code

friend function_symbol_vector mcrl2::data::structured_sort::sort_fset::fset_generate_functions_code

friend class mcrl2::data::structured_sort::sort_specification

Public member functions

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.

function_symbol_vector comparison_functions() const

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

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.

function_symbol_vector constructor_functions() const

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

const structured_sort_constructor_list &constructors() const

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

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

data_equation_vector projection_equations() const

Generate equations for the projection functions of this sort.

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

function_symbol_vector projection_functions() const

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

data_equation_vector recogniser_equations() const

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.

function_symbol_vector recogniser_functions() const

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

structured_sort()

brief Default constructor.

structured_sort(const atermpp::aterm &term)

brief Constructor. param term A term

structured_sort(const Container &constructors, typename atermpp::enable_if_container<Container, structured_sort_constructor>::type * = nullptr)

brief Constructor.

structured_sort(const structured_sort&) noexcept = default

Move semantics.

structured_sort(const structured_sort_constructor_list &constructors)

brief Constructor.

structured_sort(structured_sort&&) noexcept = default

Private static member functions

static bool has_recogniser(structured_sort_constructor const &s)

Private member functions

data_equation_vector comparison_equations(const sort_expression &s) const

function_symbol_vector comparison_functions(const sort_expression &s) const

data_equation_vector constructor_equations(const sort_expression &s) const

function_symbol_vector constructor_functions(const sort_expression &s) const

function_symbol equal_arguments_function(const sort_expression &s) const

data_equation_vector projection_equations(const sort_expression &s) const

function_symbol_vector projection_functions(const sort_expression &s) const

data_equation_vector recogniser_equations(const sort_expression &s) const

function_symbol_vector recogniser_functions(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 to_pos_function(const sort_expression &s) const