mcrl2::data::sort_fset Namespace Reference

Namespace for system defined sort fset. More...

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

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 &s)
	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 #.
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 &s)
	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 182 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 768 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 732 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 744 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 756 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 271 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.
arg2	A data expression.

Returns

Application of @fset_cinsert to a number of arguments.

Definition at line 297 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 261 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 207 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of @fset_cons to a number of arguments.

Definition at line 232 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 197 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 593 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

s	A sort expression.
arg0	A data expression.

Returns

Application of # to a number of arguments.

Definition at line 617 of file fset1.h.

count_name()

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

inline

Generate identifier #.

Returns

Identifier #.

Definition at line 583 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 401 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of - to a number of arguments.

Definition at line 426 of file fset1.h.

difference_name()

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

inline

Generate identifier -.

Returns

Identifier -.

Definition at line 391 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 75 of file fset1.h.

empty_name()

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

inline

Generate identifier {}.

Returns

Identifier {}.

Definition at line 65 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 41 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 268 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 247 of file standard_container_utility.h.

fset_cpp_implementable_constructors()

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

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 187 of file fset1.h.

fset_cpp_implementable_mappings()

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

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 696 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 662 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 161 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 778 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 645 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 173 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 676 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 337 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of in to a number of arguments.

Definition at line 362 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 327 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 107 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of @fset_insert to a number of arguments.

Definition at line 132 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 97 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 529 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of * to a number of arguments.

Definition at line 554 of file fset1.h.

intersection_name()

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

inline

Generate identifier *.

Returns

Identifier *.

Definition at line 519 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 319 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 281 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 253 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 217 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 637 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 603 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 447 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 411 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 85 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 52 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 383 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 347 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 153 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 117 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 575 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 539 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 511 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 475 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 708 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

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

Definition at line 309 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

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

Definition at line 243 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

result	The data expression where the # expression is put.
s	A sort expression.
arg0	A data expression.

Definition at line 627 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

result	The data expression where the - expression is put.
s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Definition at line 437 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

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

Definition at line 373 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

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

Definition at line 143 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

result	The data expression where the * expression is put.
s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Definition at line 565 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

result	The data expression where the + expression is put.
s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Definition at line 501 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 720 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 465 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

s	A sort expression.
arg0	A data expression.
arg1	A data expression.

Returns

Application of + to a number of arguments.

Definition at line 490 of file fset1.h.

union_name()

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

inline

Generate identifier +.

Returns

Identifier +.

Definition at line 455 of file fset1.h.