mcrl2::data::sort_set Namespace Reference

Namespace for system defined sort set_. More...

Typedefs
using	implementation_map = std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > >

Functions
container_sort	set_ (const sort_expression &s)
	Constructor for sort expression Set(S)
bool	is_set (const sort_expression &e)
	Recogniser for sort expression Set(s)
const core::identifier_string &	constructor_name ()
	Generate identifier @set.
function_symbol	constructor (const sort_expression &s)
	Constructor for function symbol @set.
bool	is_constructor_function_symbol (const atermpp::aterm &e)
	Recogniser for function @set.
application	constructor (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @set.
void	make_constructor (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @set.
bool	is_constructor_application (const atermpp::aterm &e)
	Recogniser for application of @set.
function_symbol_vector	set_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for set_.
function_symbol_vector	set_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for set_.
implementation_map	set_cpp_implementable_constructors (const sort_expression &)
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for set_.
const core::identifier_string &	set_fset_name ()
	Generate identifier @setfset.
function_symbol	set_fset (const sort_expression &s)
	Constructor for function symbol @setfset.
bool	is_set_fset_function_symbol (const atermpp::aterm &e)
	Recogniser for function @setfset.
application	set_fset (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @setfset.
void	make_set_fset (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @setfset.
bool	is_set_fset_application (const atermpp::aterm &e)
	Recogniser for application of @setfset.
const core::identifier_string &	set_comprehension_name ()
	Generate identifier @setcomp.
function_symbol	set_comprehension (const sort_expression &s)
	Constructor for function symbol @setcomp.
bool	is_set_comprehension_function_symbol (const atermpp::aterm &e)
	Recogniser for function @setcomp.
application	set_comprehension (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @setcomp.
void	make_set_comprehension (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @setcomp.
bool	is_set_comprehension_application (const atermpp::aterm &e)
	Recogniser for application of @setcomp.
const core::identifier_string &	in_name ()
	Generate identifier in.
function_symbol	in (const sort_expression &, const sort_expression &s0, const sort_expression &s1)
bool	is_in_function_symbol (const atermpp::aterm &e)
	Recogniser for function in.
application	in (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol in.
void	make_in (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol in.
bool	is_in_application (const atermpp::aterm &e)
	Recogniser for application of in.
const core::identifier_string &	complement_name ()
	Generate identifier !.
function_symbol	complement (const sort_expression &s)
	Constructor for function symbol !.
bool	is_complement_function_symbol (const atermpp::aterm &e)
	Recogniser for function !.
application	complement (const sort_expression &s, const data_expression &arg0)
	Application of function symbol !.
void	make_complement (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol !.
bool	is_complement_application (const atermpp::aterm &e)
	Recogniser for application of !.
const core::identifier_string &	union_name ()
	Generate identifier +.
function_symbol	union_ (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_union_function_symbol (const atermpp::aterm &e)
	Recogniser for function +.
application	union_ (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol +.
void	make_union (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol +.
bool	is_union_application (const atermpp::aterm &e)
	Recogniser for application of +.
const core::identifier_string &	intersection_name ()
	Generate identifier *.
function_symbol	intersection (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_intersection_function_symbol (const atermpp::aterm &e)
	Recogniser for function *.
application	intersection (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol *.
void	make_intersection (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol *.
bool	is_intersection_application (const atermpp::aterm &e)
	Recogniser for application of *.
const core::identifier_string &	difference_name ()
	Generate identifier -.
function_symbol	difference (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_difference_function_symbol (const atermpp::aterm &e)
	Recogniser for function -.
application	difference (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol -.
void	make_difference (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol -.
bool	is_difference_application (const atermpp::aterm &e)
	Recogniser for application of -.
const core::identifier_string &	false_function_name ()
	Generate identifier @false_.
function_symbol	false_function (const sort_expression &s)
	Constructor for function symbol @false_.
bool	is_false_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @false_.
application	false_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @false_.
void	make_false_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @false_.
bool	is_false_function_application (const atermpp::aterm &e)
	Recogniser for application of @false_.
const core::identifier_string &	true_function_name ()
	Generate identifier @true_.
function_symbol	true_function (const sort_expression &s)
	Constructor for function symbol @true_.
bool	is_true_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @true_.
application	true_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @true_.
void	make_true_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @true_.
bool	is_true_function_application (const atermpp::aterm &e)
	Recogniser for application of @true_.
const core::identifier_string &	not_function_name ()
	Generate identifier @not_.
function_symbol	not_function (const sort_expression &s)
	Constructor for function symbol @not_.
bool	is_not_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @not_.
application	not_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @not_.
void	make_not_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @not_.
bool	is_not_function_application (const atermpp::aterm &e)
	Recogniser for application of @not_.
const core::identifier_string &	and_function_name ()
	Generate identifier @and_.
function_symbol	and_function (const sort_expression &s)
	Constructor for function symbol @and_.
bool	is_and_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @and_.
application	and_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @and_.
void	make_and_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @and_.
bool	is_and_function_application (const atermpp::aterm &e)
	Recogniser for application of @and_.
const core::identifier_string &	or_function_name ()
	Generate identifier @or_.
function_symbol	or_function (const sort_expression &s)
	Constructor for function symbol @or_.
bool	is_or_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @or_.
application	or_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @or_.
void	make_or_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @or_.
bool	is_or_function_application (const atermpp::aterm &e)
	Recogniser for application of @or_.
const core::identifier_string &	fset_union_name ()
	Generate identifier @fset_union.
function_symbol	fset_union (const sort_expression &s)
	Constructor for function symbol @fset_union.
bool	is_fset_union_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_union.
application	fset_union (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fset_union.
void	make_fset_union (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Make an application of function symbol @fset_union.
bool	is_fset_union_application (const atermpp::aterm &e)
	Recogniser for application of @fset_union.
const core::identifier_string &	fset_intersection_name ()
	Generate identifier @fset_inter.
function_symbol	fset_intersection (const sort_expression &s)
	Constructor for function symbol @fset_inter.
bool	is_fset_intersection_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_inter.
application	fset_intersection (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fset_inter.
void	make_fset_intersection (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Make an application of function symbol @fset_inter.
bool	is_fset_intersection_application (const atermpp::aterm &e)
	Recogniser for application of @fset_inter.
function_symbol_vector	set_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for set_.
function_symbol_vector	set_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for set_.
function_symbol_vector	set_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for set_.
implementation_map	set_cpp_implementable_mappings (const sort_expression &)
	Give all system defined mappings that are to be implemented in C++ code for set_.
const data_expression &	left (const data_expression &e)
	Function for projecting out argument. left from an application.
const data_expression &	right (const data_expression &e)
	Function for projecting out argument. right from an application.
const data_expression &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.
const data_expression &	arg1 (const data_expression &e)
	Function for projecting out argument. arg1 from an application.
const data_expression &	arg2 (const data_expression &e)
	Function for projecting out argument. arg2 from an application.
const data_expression &	arg3 (const data_expression &e)
	Function for projecting out argument. arg3 from an application.
const data_expression &	arg4 (const data_expression &e)
	Function for projecting out argument. arg4 from an application.
data_equation_vector	set_generate_equations_code (const sort_expression &s)
	Give all system defined equations for set_.
core::identifier_string const &	set_enumeration_name ()
	Generate identifier set_enumeration.
function_symbol	set_enumeration (const sort_expression &s)
	Constructor for function symbol set_enumeration.
bool	is_set_enumeration_function_symbol (const atermpp::aterm &e)
	Recogniser for function set_enumeration.
template<typename Sequence >
data_expression	set_enumeration (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
	Application of function symbol set_enumeration.
data_expression	set_enumeration (const sort_expression &s, data_expression_list const &range)
	Application of function symbol set_enumeration.
bool	is_set_enumeration_application (const atermpp::aterm &e)
	Recogniser for application of set_enumeration.

Detailed Description

Namespace for system defined sort set_.

Typedef Documentation

implementation_map

typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > mcrl2::data::sort_set::implementation_map

Definition at line 146 of file set1.h.

Function Documentation

and_function() [1/2]

function_symbol mcrl2::data::sort_set::and_function ( const sort_expression &  s )

inline

Constructor for function symbol @and_.

Parameters

s	A sort expression.

Returns

Function symbol and_function.

Definition at line 849 of file set1.h.

and_function() [2/2]

application mcrl2::data::sort_set::and_function ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @and_.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of @and_ to a number of arguments.

Definition at line 874 of file set1.h.

and_function_name()

const core::identifier_string & mcrl2::data::sort_set::and_function_name ( )

inline

Generate identifier @and_.

Returns

Identifier @and_.

Definition at line 839 of file set1.h.

arg()

const data_expression & mcrl2::data::sort_set::arg ( const data_expression &  e )

inline

Function for projecting out argument. arg from an application.

Parameters

e	A data expression.

Precondition

arg is defined for e.

Returns

The argument of e that corresponds to arg.

Definition at line 1209 of file set1.h.

arg1()

const data_expression & mcrl2::data::sort_set::arg1 ( const data_expression &  e )

inline

Function for projecting out argument. arg1 from an application.

Parameters

e	A data expression.

Precondition

arg1 is defined for e.

Returns

The argument of e that corresponds to arg1.

Definition at line 1221 of file set1.h.

arg2()

const data_expression & mcrl2::data::sort_set::arg2 ( const data_expression &  e )

inline

Function for projecting out argument. arg2 from an application.

Parameters

e	A data expression.

Precondition

arg2 is defined for e.

Returns

The argument of e that corresponds to arg2.

Definition at line 1233 of file set1.h.

arg3()

const data_expression & mcrl2::data::sort_set::arg3 ( const data_expression &  e )

inline

Function for projecting out argument. arg3 from an application.

Parameters

e	A data expression.

Precondition

arg3 is defined for e.

Returns

The argument of e that corresponds to arg3.

Definition at line 1245 of file set1.h.

arg4()

const data_expression & mcrl2::data::sort_set::arg4 ( const data_expression &  e )

inline

Function for projecting out argument. arg4 from an application.

Parameters

e	A data expression.

Precondition

arg4 is defined for e.

Returns

The argument of e that corresponds to arg4.

Definition at line 1257 of file set1.h.

complement() [1/2]

function_symbol mcrl2::data::sort_set::complement ( const sort_expression &  s )

inline

Constructor for function symbol !.

Parameters

s	A sort expression.

Returns

Function symbol complement.

Definition at line 358 of file set1.h.

complement() [2/2]

application mcrl2::data::sort_set::complement ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol !.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of ! to a number of arguments.

Definition at line 382 of file set1.h.

complement_name()

const core::identifier_string & mcrl2::data::sort_set::complement_name ( )

inline

Generate identifier !.

Returns

Identifier !.

Definition at line 348 of file set1.h.

constructor() [1/2]

function_symbol mcrl2::data::sort_set::constructor ( const sort_expression &  s )

inline

Constructor for function symbol @set.

Parameters

s	A sort expression.

Returns

Function symbol constructor.

Definition at line 73 of file set1.h.

constructor() [2/2]

application mcrl2::data::sort_set::constructor ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @set.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of @set to a number of arguments.

Definition at line 98 of file set1.h.

constructor_name()

const core::identifier_string & mcrl2::data::sort_set::constructor_name ( )

inline

Generate identifier @set.

Returns

Identifier @set.

Definition at line 63 of file set1.h.

difference() [1/2]

application mcrl2::data::sort_set::difference ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol -.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of - to a number of arguments.

Definition at line 624 of file set1.h.

difference() [2/2]

function_symbol mcrl2::data::sort_set::difference ( const sort_expression &  s, const sort_expression &  s0, const sort_expression &  s1  )

inline

Definition at line 580 of file set1.h.

difference_name()

const core::identifier_string & mcrl2::data::sort_set::difference_name ( )

inline

Generate identifier -.

Returns

Identifier -.

Definition at line 572 of file set1.h.

false_function() [1/2]

function_symbol mcrl2::data::sort_set::false_function ( const sort_expression &  s )

inline

Constructor for function symbol @false_.

Parameters

s	A sort expression.

Returns

Function symbol false_function.

Definition at line 663 of file set1.h.

false_function() [2/2]

application mcrl2::data::sort_set::false_function ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @false_.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @false_ to a number of arguments.

Definition at line 687 of file set1.h.

false_function_name()

const core::identifier_string & mcrl2::data::sort_set::false_function_name ( )

inline

Generate identifier @false_.

Returns

Identifier @false_.

Definition at line 653 of file set1.h.

fset_intersection() [1/2]

function_symbol mcrl2::data::sort_set::fset_intersection ( const sort_expression &  s )

inline

Constructor for function symbol @fset_inter.

Parameters

s	A sort expression.

Returns

Function symbol fset_intersection.

Definition at line 1045 of file set1.h.

fset_intersection() [2/2]

application mcrl2::data::sort_set::fset_intersection ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Application of function symbol @fset_inter.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.
[in]	arg3	A data expression.

Returns

Application of @fset_inter to a number of arguments.

Definition at line 1072 of file set1.h.

fset_intersection_name()

const core::identifier_string & mcrl2::data::sort_set::fset_intersection_name ( )

inline

Generate identifier @fset_inter.

Returns

Identifier @fset_inter.

Definition at line 1035 of file set1.h.

fset_union() [1/2]

function_symbol mcrl2::data::sort_set::fset_union ( const sort_expression &  s )

inline

Constructor for function symbol @fset_union.

Parameters

s	A sort expression.

Returns

Function symbol fset_union.

Definition at line 977 of file set1.h.

fset_union() [2/2]

application mcrl2::data::sort_set::fset_union ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Application of function symbol @fset_union.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.
[in]	arg3	A data expression.

Returns

Application of @fset_union to a number of arguments.

Definition at line 1004 of file set1.h.

fset_union_name()

const core::identifier_string & mcrl2::data::sort_set::fset_union_name ( )

inline

Generate identifier @fset_union.

Returns

Identifier @fset_union.

Definition at line 967 of file set1.h.

in() [1/2]

function_symbol mcrl2::data::sort_set::in ( const sort_expression &  , const sort_expression &  s0, const sort_expression &  s1  )

inline

Definition at line 292 of file set1.h.

in() [2/2]

application mcrl2::data::sort_set::in ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol in.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of in to a number of arguments.

Definition at line 319 of file set1.h.

in_name()

const core::identifier_string & mcrl2::data::sort_set::in_name ( )

inline

Generate identifier in.

Returns

Identifier in.

Definition at line 284 of file set1.h.

intersection() [1/2]

application mcrl2::data::sort_set::intersection ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol *.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of * to a number of arguments.

Definition at line 543 of file set1.h.

intersection() [2/2]

function_symbol mcrl2::data::sort_set::intersection ( const sort_expression &  s, const sort_expression &  s0, const sort_expression &  s1  )

inline

Definition at line 495 of file set1.h.

intersection_name()

const core::identifier_string & mcrl2::data::sort_set::intersection_name ( )

inline

Generate identifier *.

Returns

Identifier *.

Definition at line 487 of file set1.h.

is_and_function_application()

bool mcrl2::data::sort_set::is_and_function_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @and_.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol and_function to a number of arguments.

Definition at line 895 of file set1.h.

is_and_function_function_symbol()

bool mcrl2::data::sort_set::is_and_function_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @and_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @and_.

Definition at line 859 of file set1.h.

is_complement_application()

bool mcrl2::data::sort_set::is_complement_application ( const atermpp::aterm &  e )

inline

Recogniser for application of !.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol complement to a number of arguments.

Definition at line 402 of file set1.h.

is_complement_function_symbol()

bool mcrl2::data::sort_set::is_complement_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function !.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching !.

Definition at line 368 of file set1.h.

is_constructor_application()

bool mcrl2::data::sort_set::is_constructor_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @set.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol constructor to a number of arguments.

Definition at line 119 of file set1.h.

is_constructor_function_symbol()

bool mcrl2::data::sort_set::is_constructor_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @set.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @set.

Definition at line 83 of file set1.h.

is_difference_application()

bool mcrl2::data::sort_set::is_difference_application ( const atermpp::aterm &  e )

inline

Recogniser for application of -.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol difference to a number of arguments.

Definition at line 645 of file set1.h.

is_difference_function_symbol()

bool mcrl2::data::sort_set::is_difference_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function -.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching -.

Definition at line 608 of file set1.h.

is_false_function_application()

bool mcrl2::data::sort_set::is_false_function_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @false_.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol false_function to a number of arguments.

Definition at line 707 of file set1.h.

is_false_function_function_symbol()

bool mcrl2::data::sort_set::is_false_function_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @false_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @false_.

Definition at line 673 of file set1.h.

is_fset_intersection_application()

bool mcrl2::data::sort_set::is_fset_intersection_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset_inter.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol fset_intersection to a number of arguments.

Definition at line 1095 of file set1.h.

is_fset_intersection_function_symbol()

bool mcrl2::data::sort_set::is_fset_intersection_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset_inter.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_inter.

Definition at line 1055 of file set1.h.

is_fset_union_application()

bool mcrl2::data::sort_set::is_fset_union_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset_union.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol fset_union to a number of arguments.

Definition at line 1027 of file set1.h.

is_fset_union_function_symbol()

bool mcrl2::data::sort_set::is_fset_union_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset_union.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_union.

Definition at line 987 of file set1.h.

is_in_application()

bool mcrl2::data::sort_set::is_in_application ( const atermpp::aterm &  e )

inline

Recogniser for application of in.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol in to a number of arguments.

Definition at line 340 of file set1.h.

is_in_function_symbol()

bool mcrl2::data::sort_set::is_in_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function in.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching in.

Definition at line 303 of file set1.h.

is_intersection_application()

bool mcrl2::data::sort_set::is_intersection_application ( const atermpp::aterm &  e )

inline

Recogniser for application of *.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol intersection to a number of arguments.

Definition at line 564 of file set1.h.

is_intersection_function_symbol()

bool mcrl2::data::sort_set::is_intersection_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function *.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching *.

Definition at line 527 of file set1.h.

is_not_function_application()

bool mcrl2::data::sort_set::is_not_function_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @not_.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol not_function to a number of arguments.

Definition at line 831 of file set1.h.

is_not_function_function_symbol()

bool mcrl2::data::sort_set::is_not_function_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @not_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @not_.

Definition at line 797 of file set1.h.

is_or_function_application()

bool mcrl2::data::sort_set::is_or_function_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @or_.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol or_function to a number of arguments.

Definition at line 959 of file set1.h.

is_or_function_function_symbol()

bool mcrl2::data::sort_set::is_or_function_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @or_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @or_.

Definition at line 923 of file set1.h.

is_set()

bool mcrl2::data::sort_set::is_set ( const sort_expression &  e )

inline

Recogniser for sort expression Set(s)

Parameters

e	A sort expression

Returns

true iff e is a container sort of which the name matches set_

Definition at line 50 of file set1.h.

is_set_comprehension_application()

bool mcrl2::data::sort_set::is_set_comprehension_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @setcomp.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol set_comprehension to a number of arguments.

Definition at line 276 of file set1.h.

is_set_comprehension_function_symbol()

bool mcrl2::data::sort_set::is_set_comprehension_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @setcomp.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @setcomp.

Definition at line 242 of file set1.h.

is_set_enumeration_application()

bool mcrl2::data::sort_set::is_set_enumeration_application ( const atermpp::aterm &  e )

inline

Recogniser for application of set_enumeration.

Parameters

e	A data expression

Returns

true iff e is an application of function symbol set_enumeration to a number of arguments

Definition at line 225 of file standard_container_utility.h.

is_set_enumeration_function_symbol()

bool mcrl2::data::sort_set::is_set_enumeration_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function set_enumeration.

Parameters

e	A data expression

Returns

true iff e is the function symbol matching set_enumeration

Definition at line 166 of file standard_container_utility.h.

is_set_fset_application()

bool mcrl2::data::sort_set::is_set_fset_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @setfset.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol set_fset to a number of arguments.

Definition at line 214 of file set1.h.

is_set_fset_function_symbol()

bool mcrl2::data::sort_set::is_set_fset_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @setfset.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @setfset.

Definition at line 180 of file set1.h.

is_true_function_application()

bool mcrl2::data::sort_set::is_true_function_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @true_.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol true_function to a number of arguments.

Definition at line 769 of file set1.h.

is_true_function_function_symbol()

bool mcrl2::data::sort_set::is_true_function_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @true_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @true_.

Definition at line 735 of file set1.h.

is_union_application()

bool mcrl2::data::sort_set::is_union_application ( const atermpp::aterm &  e )

inline

Recogniser for application of +.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol union_ to a number of arguments.

Definition at line 479 of file set1.h.

is_union_function_symbol()

bool mcrl2::data::sort_set::is_union_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function +.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching +.

Definition at line 442 of file set1.h.

left()

const data_expression & mcrl2::data::sort_set::left ( const data_expression &  e )

inline

Function for projecting out argument. left from an application.

Parameters

e	A data expression.

Precondition

left is defined for e.

Returns

The argument of e that corresponds to left.

Definition at line 1185 of file set1.h.

make_and_function()

void mcrl2::data::sort_set::make_and_function ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @and_.

Parameters

[out]	result	The data expression where the @and_ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 885 of file set1.h.

make_complement()

void mcrl2::data::sort_set::make_complement ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol !.

Parameters

[out]	result	The data expression where the ! expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 392 of file set1.h.

make_constructor()

void mcrl2::data::sort_set::make_constructor ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @set.

Parameters

[out]	result	The data expression where the @set expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 109 of file set1.h.

make_difference()

void mcrl2::data::sort_set::make_difference ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol -.

Parameters

[out]	result	The data expression where the - expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 635 of file set1.h.

make_false_function()

void mcrl2::data::sort_set::make_false_function ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @false_.

Parameters

[out]	result	The data expression where the @false_ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 697 of file set1.h.

make_fset_intersection()

void mcrl2::data::sort_set::make_fset_intersection ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Make an application of function symbol @fset_inter.

Parameters

[out]	result	The data expression where the @fset_inter expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.
[in]	arg3	A data expression.

Definition at line 1085 of file set1.h.

make_fset_union()

void mcrl2::data::sort_set::make_fset_union ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2, const data_expression &  arg3  )

inline

Make an application of function symbol @fset_union.

Parameters

[out]	result	The data expression where the @fset_union expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.
[in]	arg3	A data expression.

Definition at line 1017 of file set1.h.

make_in()

void mcrl2::data::sort_set::make_in ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol in.

Parameters

[out]	result	The data expression where the in expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 330 of file set1.h.

make_intersection()

void mcrl2::data::sort_set::make_intersection ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol *.

Parameters

[out]	result	The data expression where the * expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 554 of file set1.h.

make_not_function()

void mcrl2::data::sort_set::make_not_function ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @not_.

Parameters

[out]	result	The data expression where the @not_ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 821 of file set1.h.

make_or_function()

void mcrl2::data::sort_set::make_or_function ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @or_.

Parameters

[out]	result	The data expression where the @or_ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 949 of file set1.h.

make_set_comprehension()

void mcrl2::data::sort_set::make_set_comprehension ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @setcomp.

Parameters

[out]	result	The data expression where the @setcomp expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 266 of file set1.h.

make_set_fset()

void mcrl2::data::sort_set::make_set_fset ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @setfset.

Parameters

[out]	result	The data expression where the @setfset expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 204 of file set1.h.

make_true_function()

void mcrl2::data::sort_set::make_true_function ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @true_.

Parameters

[out]	result	The data expression where the @true_ expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 759 of file set1.h.

make_union()

void mcrl2::data::sort_set::make_union ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol +.

Parameters

[out]	result	The data expression where the + expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 469 of file set1.h.

not_function() [1/2]

function_symbol mcrl2::data::sort_set::not_function ( const sort_expression &  s )

inline

Constructor for function symbol @not_.

Parameters

s	A sort expression.

Returns

Function symbol not_function.

Definition at line 787 of file set1.h.

not_function() [2/2]

application mcrl2::data::sort_set::not_function ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @not_.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @not_ to a number of arguments.

Definition at line 811 of file set1.h.

not_function_name()

const core::identifier_string & mcrl2::data::sort_set::not_function_name ( )

inline

Generate identifier @not_.

Returns

Identifier @not_.

Definition at line 777 of file set1.h.

or_function() [1/2]

function_symbol mcrl2::data::sort_set::or_function ( const sort_expression &  s )

inline

Constructor for function symbol @or_.

Parameters

s	A sort expression.

Returns

Function symbol or_function.

Definition at line 913 of file set1.h.

or_function() [2/2]

application mcrl2::data::sort_set::or_function ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @or_.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of @or_ to a number of arguments.

Definition at line 938 of file set1.h.

or_function_name()

const core::identifier_string & mcrl2::data::sort_set::or_function_name ( )

inline

Generate identifier @or_.

Returns

Identifier @or_.

Definition at line 903 of file set1.h.

right()

const data_expression & mcrl2::data::sort_set::right ( const data_expression &  e )

inline

Function for projecting out argument. right from an application.

Parameters

e	A data expression.

Precondition

right is defined for e.

Returns

The argument of e that corresponds to right.

Definition at line 1197 of file set1.h.

set_()

container_sort mcrl2::data::sort_set::set_ ( const sort_expression &  s )

inline

Constructor for sort expression Set(S)

Parameters

s	A sort expression

Returns

Sort expression set_(s)

Definition at line 39 of file set1.h.

set_comprehension() [1/2]

function_symbol mcrl2::data::sort_set::set_comprehension ( const sort_expression &  s )

inline

Constructor for function symbol @setcomp.

Parameters

s	A sort expression.

Returns

Function symbol set_comprehension.

Definition at line 232 of file set1.h.

set_comprehension() [2/2]

application mcrl2::data::sort_set::set_comprehension ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @setcomp.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @setcomp to a number of arguments.

Definition at line 256 of file set1.h.

set_comprehension_name()

const core::identifier_string & mcrl2::data::sort_set::set_comprehension_name ( )

inline

Generate identifier @setcomp.

Returns

Identifier @setcomp.

Definition at line 222 of file set1.h.

set_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_set::set_cpp_implementable_constructors ( const sort_expression &  )

inline

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for set_.

Parameters

s	A sort expression.

Returns

All system defined constructors that are to be implemented in C++ for set_.

Definition at line 151 of file set1.h.

set_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_set::set_cpp_implementable_mappings ( const sort_expression &  )

inline

Give all system defined mappings that are to be implemented in C++ code for set_.

Parameters

s	A sort expression

Returns

A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for set_

Definition at line 1174 of file set1.h.

set_enumeration() [1/3]

function_symbol mcrl2::data::sort_set::set_enumeration ( const sort_expression &  s )

inline

Constructor for function symbol set_enumeration.

Parameters

s	A sort expression

Returns

Function symbol set_enumeration

Definition at line 156 of file standard_container_utility.h.

set_enumeration() [2/3]

data_expression mcrl2::data::sort_set::set_enumeration ( const sort_expression &  s, data_expression_list const &  range  )

inline

Application of function symbol set_enumeration.

Parameters

s	A sort expression
range	A range of data expressions

Returns

Application of set_enum to the data expressions in range.

Definition at line 205 of file standard_container_utility.h.

set_enumeration() [3/3]

template<typename Sequence >

data_expression mcrl2::data::sort_set::set_enumeration ( const sort_expression &  s, Sequence const &  range, typename atermpp::enable_if_container< Sequence, data_expression >::type *  = 0  )

inline

Application of function symbol set_enumeration.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters

s	A sort expression
range	A range of data expressions

Returns

Application of set_enum to the data expressions in range.

Definition at line 184 of file standard_container_utility.h.

set_enumeration_name()

core::identifier_string const & mcrl2::data::sort_set::set_enumeration_name ( )

inline

Generate identifier set_enumeration.

Returns

Identifier set_enumeration

Definition at line 146 of file standard_container_utility.h.

set_fset() [1/2]

function_symbol mcrl2::data::sort_set::set_fset ( const sort_expression &  s )

inline

Constructor for function symbol @setfset.

Parameters

s	A sort expression.

Returns

Function symbol set_fset.

Definition at line 170 of file set1.h.

set_fset() [2/2]

application mcrl2::data::sort_set::set_fset ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @setfset.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @setfset to a number of arguments.

Definition at line 194 of file set1.h.

set_fset_name()

const core::identifier_string & mcrl2::data::sort_set::set_fset_name ( )

inline

Generate identifier @setfset.

Returns

Identifier @setfset.

Definition at line 160 of file set1.h.

set_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_set::set_generate_constructors_and_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings and constructors for set_.

Parameters

s	A sort expression

Returns

All system defined mappings for set_

Definition at line 1130 of file set1.h.

set_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_set::set_generate_constructors_code ( const sort_expression &  s )

inline

Give all system defined constructors for set_.

Parameters

s	A sort expression.

Returns

All system defined constructors for set_.

Definition at line 127 of file set1.h.

set_generate_equations_code()

data_equation_vector mcrl2::data::sort_set::set_generate_equations_code ( const sort_expression &  s )

inline

Give all system defined equations for set_.

Parameters

s	A sort expression

Returns

All system defined equations for sort set_

Definition at line 1267 of file set1.h.

set_generate_functions_code()

function_symbol_vector mcrl2::data::sort_set::set_generate_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings for set_.

Parameters

s	A sort expression

Returns

All system defined mappings for set_

Definition at line 1103 of file set1.h.

set_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_set::set_mCRL2_usable_constructors ( const sort_expression &  s )

inline

Give all defined constructors which can be used in mCRL2 specs for set_.

Parameters

s	A sort expression.

Returns

All system defined constructors that can be used in an mCRL2 specification for set_.

Definition at line 138 of file set1.h.

set_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_set::set_mCRL2_usable_mappings ( const sort_expression &  s )

inline

Give all system defined mappings that can be used in mCRL2 specs for set_.

Parameters

s	A sort expression

Returns

All system defined mappings for that can be used in mCRL2 specificationis set_

Definition at line 1144 of file set1.h.

true_function() [1/2]

function_symbol mcrl2::data::sort_set::true_function ( const sort_expression &  s )

inline

Constructor for function symbol @true_.

Parameters

s	A sort expression.

Returns

Function symbol true_function.

Definition at line 725 of file set1.h.

true_function() [2/2]

application mcrl2::data::sort_set::true_function ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @true_.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @true_ to a number of arguments.

Definition at line 749 of file set1.h.

true_function_name()

const core::identifier_string & mcrl2::data::sort_set::true_function_name ( )

inline

Generate identifier @true_.

Returns

Identifier @true_.

Definition at line 715 of file set1.h.

union_() [1/2]

application mcrl2::data::sort_set::union_ ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol +.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of + to a number of arguments.

Definition at line 458 of file set1.h.

union_() [2/2]

function_symbol mcrl2::data::sort_set::union_ ( const sort_expression &  s, const sort_expression &  s0, const sort_expression &  s1  )

inline

Definition at line 418 of file set1.h.

union_name()

const core::identifier_string & mcrl2::data::sort_set::union_name ( )

inline

Generate identifier +.

Returns

Identifier +.

Definition at line 410 of file set1.h.