mcrl2::data::sort_fset Namespace Reference

Namespace for system defined sort fset. More...

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

Functions
container_sort	fset (const sort_expression &s)
	Constructor for sort expression FSet(S)
bool	is_fset (const sort_expression &e)
	Recogniser for sort expression FSet(s)
const core::identifier_string &	empty_name ()
	Generate identifier {}.
function_symbol	empty (const sort_expression &s)
	Constructor for function symbol {}.
bool	is_empty_function_symbol (const atermpp::aterm &e)
	Recogniser for function {}.
const core::identifier_string &	insert_name ()
	Generate identifier @fset_insert.
function_symbol	insert (const sort_expression &s)
	Constructor for function symbol @fset_insert.
bool	is_insert_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_insert.
application	insert (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @fset_insert.
void	make_insert (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @fset_insert.
bool	is_insert_application (const atermpp::aterm &e)
	Recogniser for application of @fset_insert.
function_symbol_vector	fset_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for fset.
function_symbol_vector	fset_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for fset.
implementation_map	fset_cpp_implementable_constructors (const sort_expression &)
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for fset.
const core::identifier_string &	cons_name ()
	Generate identifier @fset_cons.
function_symbol	cons_ (const sort_expression &s)
	Constructor for function symbol @fset_cons.
bool	is_cons_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_cons.
application	cons_ (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @fset_cons.
void	make_cons (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @fset_cons.
bool	is_cons_application (const atermpp::aterm &e)
	Recogniser for application of @fset_cons.
const core::identifier_string &	cinsert_name ()
	Generate identifier @fset_cinsert.
function_symbol	cinsert (const sort_expression &s)
	Constructor for function symbol @fset_cinsert.
bool	is_cinsert_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_cinsert.
application	cinsert (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @fset_cinsert.
void	make_cinsert (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @fset_cinsert.
bool	is_cinsert_application (const atermpp::aterm &e)
	Recogniser for application of @fset_cinsert.
const core::identifier_string &	in_name ()
	Generate identifier in.
function_symbol	in (const sort_expression &s)
	Constructor for function symbol in.
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 &	difference_name ()
	Generate identifier -.
function_symbol	difference (const sort_expression &s)
	Constructor for function symbol -.
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 &	union_name ()
	Generate identifier +.
function_symbol	union_ (const sort_expression &s)
	Constructor for function symbol +.
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)
	Constructor for function symbol *.
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 &	count_name ()
	Generate identifier #.
function_symbol	count (const sort_expression &s)
	Constructor for function symbol #.
bool	is_count_function_symbol (const atermpp::aterm &e)
	Recogniser for function #.
application	count (const sort_expression &s, const data_expression &arg0)
	Application of function symbol #.
void	make_count (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol #.
bool	is_count_application (const atermpp::aterm &e)
	Recogniser for application of #.
const core::identifier_string &	pick_name ()
	Generate identifier pick.
function_symbol	pick (const sort_expression &s)
	Constructor for function symbol pick.
bool	is_pick_function_symbol (const atermpp::aterm &e)
	Recogniser for function pick.
application	pick (const sort_expression &s, const data_expression &arg0)
	Application of function symbol pick.
void	make_pick (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol pick.
bool	is_pick_application (const atermpp::aterm &e)
	Recogniser for application of pick.
function_symbol_vector	fset_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for fset.
function_symbol_vector	fset_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for fset.
function_symbol_vector	fset_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for fset.
implementation_map	fset_cpp_implementable_mappings (const sort_expression &)
	Give all system defined mappings that are to be implemented in C++ code for fset.
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 &	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 &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.
data_equation_vector	fset_generate_equations_code (const sort_expression &s)
	Give all system defined equations for fset.
template<typename Sequence >
application	fset (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=nullptr)
	Constructs a finite set expression from a range of expressions.
application	fset (const sort_expression &s, const data_expression_list &range)
	Constructs a finite set expression from a list of expressions.

Detailed Description

Namespace for system defined sort fset.

Typedef Documentation

implementation_map

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

Definition at line 179 of file fset1.h.

Function Documentation

arg()

const data_expression & mcrl2::data::sort_fset::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 827 of file fset1.h.

arg1()

const data_expression & mcrl2::data::sort_fset::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 791 of file fset1.h.

arg2()

const data_expression & mcrl2::data::sort_fset::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 803 of file fset1.h.

arg3()

const data_expression & mcrl2::data::sort_fset::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 815 of file fset1.h.

cinsert() [1/2]

function_symbol mcrl2::data::sort_fset::cinsert ( const sort_expression &  s )

inline

Constructor for function symbol @fset_cinsert.

Parameters

s	A sort expression.

Returns

Function symbol cinsert.

Definition at line 267 of file fset1.h.

cinsert() [2/2]

application mcrl2::data::sort_fset::cinsert ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @fset_cinsert.

Parameters

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

Returns

Application of @fset_cinsert to a number of arguments.

Definition at line 293 of file fset1.h.

cinsert_name()

const core::identifier_string & mcrl2::data::sort_fset::cinsert_name ( )

inline

Generate identifier @fset_cinsert.

Returns

Identifier @fset_cinsert.

Definition at line 257 of file fset1.h.

cons_() [1/2]

function_symbol mcrl2::data::sort_fset::cons_ ( const sort_expression &  s )

inline

Constructor for function symbol @fset_cons.

Parameters

s	A sort expression.

Returns

Function symbol cons_.

Definition at line 203 of file fset1.h.

cons_() [2/2]

application mcrl2::data::sort_fset::cons_ ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @fset_cons.

Parameters

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

Returns

Application of @fset_cons to a number of arguments.

Definition at line 228 of file fset1.h.

cons_name()

const core::identifier_string & mcrl2::data::sort_fset::cons_name ( )

inline

Generate identifier @fset_cons.

Returns

Identifier @fset_cons.

Definition at line 193 of file fset1.h.

count() [1/2]

function_symbol mcrl2::data::sort_fset::count ( const sort_expression &  s )

inline

Constructor for function symbol #.

Parameters

s	A sort expression.

Returns

Function symbol count.

Definition at line 589 of file fset1.h.

count() [2/2]

application mcrl2::data::sort_fset::count ( 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 613 of file fset1.h.

count_name()

const core::identifier_string & mcrl2::data::sort_fset::count_name ( )

inline

Generate identifier #.

Returns

Identifier #.

Definition at line 579 of file fset1.h.

difference() [1/2]

function_symbol mcrl2::data::sort_fset::difference ( const sort_expression &  s )

inline

Constructor for function symbol -.

Parameters

s	A sort expression.

Returns

Function symbol difference.

Definition at line 397 of file fset1.h.

difference() [2/2]

application mcrl2::data::sort_fset::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 422 of file fset1.h.

difference_name()

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

inline

Generate identifier -.

Returns

Identifier -.

Definition at line 387 of file fset1.h.

empty()

function_symbol mcrl2::data::sort_fset::empty ( const sort_expression &  s )

inline

Constructor for function symbol {}.

Parameters

s	A sort expression.

Returns

Function symbol empty.

Definition at line 72 of file fset1.h.

empty_name()

const core::identifier_string & mcrl2::data::sort_fset::empty_name ( )

inline

Generate identifier {}.

Returns

Identifier {}.

Definition at line 62 of file fset1.h.

fset() [1/3]

container_sort mcrl2::data::sort_fset::fset ( const sort_expression &  s )

inline

Constructor for sort expression FSet(S)

Parameters

s	A sort expression

Returns

Sort expression fset(s)

Definition at line 38 of file fset1.h.

fset() [2/3]

application mcrl2::data::sort_fset::fset ( const sort_expression &  s, const data_expression_list &  range  )

inline

Constructs a finite set expression from a list of expressions.

Parameters

[in]	s	the sort of list elements
[in]	range	a sequence of elements

Definition at line 267 of file standard_container_utility.h.

fset() [3/3]

template<typename Sequence >

application mcrl2::data::sort_fset::fset ( const sort_expression &  s, Sequence const &  range, typename atermpp::enable_if_container< Sequence, data_expression >::type *  = nullptr  )

inline

Constructs a finite set expression from a range of expressions.

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

Parameters

[in]	s	the sort of list elements
[in]	range	a sequence of elements

Definition at line 246 of file standard_container_utility.h.

fset_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_fset::fset_cpp_implementable_constructors ( const sort_expression &  )

inline

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

Parameters

s	A sort expression.

Returns

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

Definition at line 184 of file fset1.h.

fset_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_fset::fset_cpp_implementable_mappings ( const sort_expression &  )

inline

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

Parameters

s	A sort expression

Returns

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

Definition at line 756 of file fset1.h.

fset_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_fset::fset_generate_constructors_and_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings and constructors for fset.

Parameters

s	A sort expression

Returns

All system defined mappings for fset

Definition at line 721 of file fset1.h.

fset_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_fset::fset_generate_constructors_code ( const sort_expression &  s )

inline

Give all system defined constructors for fset.

Parameters

s	A sort expression.

Returns

All system defined constructors for fset.

Definition at line 158 of file fset1.h.

fset_generate_equations_code()

data_equation_vector mcrl2::data::sort_fset::fset_generate_equations_code ( const sort_expression &  s )

inline

Give all system defined equations for fset.

Parameters

s	A sort expression

Returns

All system defined equations for sort fset

Definition at line 837 of file fset1.h.

fset_generate_functions_code()

function_symbol_vector mcrl2::data::sort_fset::fset_generate_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings for fset.

Parameters

s	A sort expression

Returns

All system defined mappings for fset

Definition at line 703 of file fset1.h.

fset_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_fset::fset_mCRL2_usable_constructors ( const sort_expression &  s )

inline

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

Parameters

s	A sort expression.

Returns

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

Definition at line 170 of file fset1.h.

fset_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_fset::fset_mCRL2_usable_mappings ( const sort_expression &  s )

inline

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

Parameters

s	A sort expression

Returns

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

Definition at line 735 of file fset1.h.

in() [1/2]

function_symbol mcrl2::data::sort_fset::in ( const sort_expression &  s )

inline

Constructor for function symbol in.

Parameters

s	A sort expression.

Returns

Function symbol in.

Definition at line 333 of file fset1.h.

in() [2/2]

application mcrl2::data::sort_fset::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 358 of file fset1.h.

in_name()

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

inline

Generate identifier in.

Returns

Identifier in.

Definition at line 323 of file fset1.h.

insert() [1/2]

function_symbol mcrl2::data::sort_fset::insert ( const sort_expression &  s )

inline

Constructor for function symbol @fset_insert.

Parameters

s	A sort expression.

Returns

Function symbol insert.

Definition at line 104 of file fset1.h.

insert() [2/2]

application mcrl2::data::sort_fset::insert ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol @fset_insert.

Parameters

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

Returns

Application of @fset_insert to a number of arguments.

Definition at line 129 of file fset1.h.

insert_name()

const core::identifier_string & mcrl2::data::sort_fset::insert_name ( )

inline

Generate identifier @fset_insert.

Returns

Identifier @fset_insert.

Definition at line 94 of file fset1.h.

intersection() [1/2]

function_symbol mcrl2::data::sort_fset::intersection ( const sort_expression &  s )

inline

Constructor for function symbol *.

Parameters

s	A sort expression.

Returns

Function symbol intersection.

Definition at line 525 of file fset1.h.

intersection() [2/2]

application mcrl2::data::sort_fset::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 550 of file fset1.h.

intersection_name()

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

inline

Generate identifier *.

Returns

Identifier *.

Definition at line 515 of file fset1.h.

is_cinsert_application()

bool mcrl2::data::sort_fset::is_cinsert_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset_cinsert.

Parameters

e	A data expression.

Returns

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

Definition at line 315 of file fset1.h.

is_cinsert_function_symbol()

bool mcrl2::data::sort_fset::is_cinsert_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset_cinsert.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_cinsert.

Definition at line 277 of file fset1.h.

is_cons_application()

bool mcrl2::data::sort_fset::is_cons_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset_cons.

Parameters

e	A data expression.

Returns

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

Definition at line 249 of file fset1.h.

is_cons_function_symbol()

bool mcrl2::data::sort_fset::is_cons_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset_cons.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_cons.

Definition at line 213 of file fset1.h.

is_count_application()

bool mcrl2::data::sort_fset::is_count_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 count to a number of arguments.

Definition at line 633 of file fset1.h.

is_count_function_symbol()

bool mcrl2::data::sort_fset::is_count_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 599 of file fset1.h.

is_difference_application()

bool mcrl2::data::sort_fset::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 443 of file fset1.h.

is_difference_function_symbol()

bool mcrl2::data::sort_fset::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 407 of file fset1.h.

is_empty_function_symbol()

bool mcrl2::data::sort_fset::is_empty_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 82 of file fset1.h.

is_fset()

bool mcrl2::data::sort_fset::is_fset ( const sort_expression &  e )

inline

Recogniser for sort expression FSet(s)

Parameters

e	A sort expression

Returns

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

Definition at line 49 of file fset1.h.

is_in_application()

bool mcrl2::data::sort_fset::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 379 of file fset1.h.

is_in_function_symbol()

bool mcrl2::data::sort_fset::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 343 of file fset1.h.

is_insert_application()

bool mcrl2::data::sort_fset::is_insert_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset_insert.

Parameters

e	A data expression.

Returns

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

Definition at line 150 of file fset1.h.

is_insert_function_symbol()

bool mcrl2::data::sort_fset::is_insert_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset_insert.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_insert.

Definition at line 114 of file fset1.h.

is_intersection_application()

bool mcrl2::data::sort_fset::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 571 of file fset1.h.

is_intersection_function_symbol()

bool mcrl2::data::sort_fset::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 535 of file fset1.h.

is_pick_application()

bool mcrl2::data::sort_fset::is_pick_application ( const atermpp::aterm &  e )

inline

Recogniser for application of pick.

Parameters

e	A data expression.

Returns

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

Definition at line 695 of file fset1.h.

is_pick_function_symbol()

bool mcrl2::data::sort_fset::is_pick_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function pick.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching pick.

Definition at line 661 of file fset1.h.

is_union_application()

bool mcrl2::data::sort_fset::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 507 of file fset1.h.

is_union_function_symbol()

bool mcrl2::data::sort_fset::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 471 of file fset1.h.

left()

const data_expression & mcrl2::data::sort_fset::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 767 of file fset1.h.

make_cinsert()

void mcrl2::data::sort_fset::make_cinsert ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @fset_cinsert.

Parameters

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

Definition at line 305 of file fset1.h.

make_cons()

void mcrl2::data::sort_fset::make_cons ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @fset_cons.

Parameters

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

Definition at line 239 of file fset1.h.

make_count()

void mcrl2::data::sort_fset::make_count ( 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 623 of file fset1.h.

make_difference()

void mcrl2::data::sort_fset::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 433 of file fset1.h.

make_in()

void mcrl2::data::sort_fset::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 369 of file fset1.h.

make_insert()

void mcrl2::data::sort_fset::make_insert ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol @fset_insert.

Parameters

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

Definition at line 140 of file fset1.h.

make_intersection()

void mcrl2::data::sort_fset::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 561 of file fset1.h.

make_pick()

void mcrl2::data::sort_fset::make_pick ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol pick.

Parameters

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

Definition at line 685 of file fset1.h.

make_union()

void mcrl2::data::sort_fset::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 497 of file fset1.h.

pick() [1/2]

function_symbol mcrl2::data::sort_fset::pick ( const sort_expression &  s )

inline

Constructor for function symbol pick.

Parameters

s	A sort expression.

Returns

Function symbol pick.

Definition at line 651 of file fset1.h.

pick() [2/2]

application mcrl2::data::sort_fset::pick ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol pick.

Parameters

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

Returns

Application of pick to a number of arguments.

Definition at line 675 of file fset1.h.

pick_name()

const core::identifier_string & mcrl2::data::sort_fset::pick_name ( )

inline

Generate identifier pick.

Returns

Identifier pick.

Definition at line 641 of file fset1.h.

right()

const data_expression & mcrl2::data::sort_fset::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 779 of file fset1.h.

union_() [1/2]

function_symbol mcrl2::data::sort_fset::union_ ( const sort_expression &  s )

inline

Constructor for function symbol +.

Parameters

s	A sort expression.

Returns

Function symbol union_.

Definition at line 461 of file fset1.h.

union_() [2/2]

application mcrl2::data::sort_fset::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 486 of file fset1.h.

union_name()

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

inline

Generate identifier +.

Returns

Identifier +.

Definition at line 451 of file fset1.h.