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. A structured sort

Friends

friend class data_specification

friend function_symbol_vector sort_fbag::fbag_generate_constructors_code

friend data_equation_vector sort_fbag::fbag_generate_equations_code

friend function_symbol_vector sort_fbag::fbag_generate_functions_code

friend function_symbol_vector sort_fset::fset_generate_constructors_code

friend data_equation_vector sort_fset::fset_generate_equations_code

friend function_symbol_vector sort_fset::fset_generate_functions_code

friend class 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()

Default constructor.

structured_sort(const atermpp::aterm &term)

Constructor.

Parameters:

  • term A term
structured_sort(const structured_sort_constructor_list &constructors)

Constructor.

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

Constructor.

structured_sort(const structured_sort&) noexcept = default

Move semantics.

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