Namespace for system defined sort bag. More...

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

Functions
container_sort	bag (const sort_expression &s)
	Constructor for sort expression Bag(S)

bool	is_bag (const sort_expression &e)
	Recogniser for sort expression Bag(s)

const core::identifier_string &	constructor_name ()
	Generate identifier @bag.

function_symbol	constructor (const sort_expression &s)
	Constructor for function symbol @bag.

bool	is_constructor_function_symbol (const atermpp::aterm &e)
	Recogniser for function @bag.

application	constructor (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @bag.

void	make_constructor (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @bag.

bool	is_constructor_application (const atermpp::aterm &e)
	Recogniser for application of @bag.

function_symbol_vector	bag_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for bag.

function_symbol_vector	bag_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for bag.

implementation_map	bag_cpp_implementable_constructors (const sort_expression &s)
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for bag.

const core::identifier_string &	bag_fbag_name ()
	Generate identifier @bagfbag.

function_symbol	bag_fbag (const sort_expression &s)
	Constructor for function symbol @bagfbag.

bool	is_bag_fbag_function_symbol (const atermpp::aterm &e)
	Recogniser for function @bagfbag.

application	bag_fbag (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @bagfbag.

void	make_bag_fbag (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @bagfbag.

bool	is_bag_fbag_application (const atermpp::aterm &e)
	Recogniser for application of @bagfbag.

const core::identifier_string &	bag_comprehension_name ()
	Generate identifier @bagcomp.

function_symbol	bag_comprehension (const sort_expression &s)
	Constructor for function symbol @bagcomp.

bool	is_bag_comprehension_function_symbol (const atermpp::aterm &e)
	Recogniser for function @bagcomp.

application	bag_comprehension (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @bagcomp.

void	make_bag_comprehension (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @bagcomp.

bool	is_bag_comprehension_application (const atermpp::aterm &e)
	Recogniser for application of @bagcomp.

const core::identifier_string &	count_name ()
	Generate identifier count.

function_symbol	count (const sort_expression &, const sort_expression &s0, const sort_expression &s1)

bool	is_count_function_symbol (const atermpp::aterm &e)
	Recogniser for function count.

application	count (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol count.

void	make_count (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol count.

bool	is_count_application (const atermpp::aterm &e)
	Recogniser for application of count.

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 &	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 &	bag2set_name ()
	Generate identifier Bag2Set.

function_symbol	bag2set (const sort_expression &s)
	Constructor for function symbol Bag2Set.

bool	is_bag2set_function_symbol (const atermpp::aterm &e)
	Recogniser for function Bag2Set.

application	bag2set (const sort_expression &s, const data_expression &arg0)
	Application of function symbol Bag2Set.

void	make_bag2set (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol Bag2Set.

bool	is_bag2set_application (const atermpp::aterm &e)
	Recogniser for application of Bag2Set.

const core::identifier_string &	set2bag_name ()
	Generate identifier Set2Bag.

function_symbol	set2bag (const sort_expression &s)
	Constructor for function symbol Set2Bag.

bool	is_set2bag_function_symbol (const atermpp::aterm &e)
	Recogniser for function Set2Bag.

application	set2bag (const sort_expression &s, const data_expression &arg0)
	Application of function symbol Set2Bag.

void	make_set2bag (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol Set2Bag.

bool	is_set2bag_application (const atermpp::aterm &e)
	Recogniser for application of Set2Bag.

const core::identifier_string &	zero_function_name ()
	Generate identifier @zero_.

function_symbol	zero_function (const sort_expression &s)
	Constructor for function symbol @zero_.

bool	is_zero_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @zero_.

application	zero_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @zero_.

void	make_zero_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @zero_.

bool	is_zero_function_application (const atermpp::aterm &e)
	Recogniser for application of @zero_.

const core::identifier_string &	one_function_name ()
	Generate identifier @one_.

function_symbol	one_function (const sort_expression &s)
	Constructor for function symbol @one_.

bool	is_one_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @one_.

application	one_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @one_.

void	make_one_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @one_.

bool	is_one_function_application (const atermpp::aterm &e)
	Recogniser for application of @one_.

const core::identifier_string &	add_function_name ()
	Generate identifier @add_.

function_symbol	add_function (const sort_expression &s)
	Constructor for function symbol @add_.

bool	is_add_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @add_.

application	add_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @add_.

void	make_add_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @add_.

bool	is_add_function_application (const atermpp::aterm &e)
	Recogniser for application of @add_.

const core::identifier_string &	min_function_name ()
	Generate identifier @min_.

function_symbol	min_function (const sort_expression &s)
	Constructor for function symbol @min_.

bool	is_min_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @min_.

application	min_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @min_.

void	make_min_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @min_.

bool	is_min_function_application (const atermpp::aterm &e)
	Recogniser for application of @min_.

const core::identifier_string &	monus_function_name ()
	Generate identifier @monus_.

function_symbol	monus_function (const sort_expression &s)
	Constructor for function symbol @monus_.

bool	is_monus_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @monus_.

application	monus_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @monus_.

void	make_monus_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @monus_.

bool	is_monus_function_application (const atermpp::aterm &e)
	Recogniser for application of @monus_.

const core::identifier_string &	nat2bool_function_name ()
	Generate identifier @Nat2Bool_.

function_symbol	nat2bool_function (const sort_expression &s)
	Constructor for function symbol @Nat2Bool_.

bool	is_nat2bool_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @Nat2Bool_.

application	nat2bool_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @Nat2Bool_.

void	make_nat2bool_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @Nat2Bool_.

bool	is_nat2bool_function_application (const atermpp::aterm &e)
	Recogniser for application of @Nat2Bool_.

const core::identifier_string &	bool2nat_function_name ()
	Generate identifier @Bool2Nat_.

function_symbol	bool2nat_function (const sort_expression &s)
	Constructor for function symbol @Bool2Nat_.

bool	is_bool2nat_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @Bool2Nat_.

application	bool2nat_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @Bool2Nat_.

void	make_bool2nat_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @Bool2Nat_.

bool	is_bool2nat_function_application (const atermpp::aterm &e)
	Recogniser for application of @Bool2Nat_.

const core::identifier_string &	fbag_join_name ()
	Generate identifier @fbag_join.

function_symbol	fbag_join (const sort_expression &s)
	Constructor for function symbol @fbag_join.

bool	is_fbag_join_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_join.

application	fbag_join (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fbag_join.

void	make_fbag_join (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 @fbag_join.

bool	is_fbag_join_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_join.

const core::identifier_string &	fbag_intersect_name ()
	Generate identifier @fbag_inter.

function_symbol	fbag_intersect (const sort_expression &s)
	Constructor for function symbol @fbag_inter.

bool	is_fbag_intersect_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_inter.

application	fbag_intersect (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fbag_inter.

void	make_fbag_intersect (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 @fbag_inter.

bool	is_fbag_intersect_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_inter.

const core::identifier_string &	fbag_difference_name ()
	Generate identifier @fbag_diff.

function_symbol	fbag_difference (const sort_expression &s)
	Constructor for function symbol @fbag_diff.

bool	is_fbag_difference_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_diff.

application	fbag_difference (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fbag_diff.

void	make_fbag_difference (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 @fbag_diff.

bool	is_fbag_difference_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_diff.

const core::identifier_string &	fbag2fset_name ()
	Generate identifier @fbag2fset.

function_symbol	fbag2fset (const sort_expression &s)
	Constructor for function symbol @fbag2fset.

bool	is_fbag2fset_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag2fset.

application	fbag2fset (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @fbag2fset.

void	make_fbag2fset (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @fbag2fset.

bool	is_fbag2fset_application (const atermpp::aterm &e)
	Recogniser for application of @fbag2fset.

function_symbol_vector	bag_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for bag.

function_symbol_vector	bag_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for bag.

function_symbol_vector	bag_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for bag.

implementation_map	bag_cpp_implementable_mappings (const sort_expression &s)
	Give all system defined mappings that are to be implemented in C++ code for bag.

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	bag_generate_equations_code (const sort_expression &s)
	Give all system defined equations for bag.

const core::identifier_string &	join_name ()
	Generate identifier @fbag_join.

function_symbol	join (const sort_expression &s)
	Constructor for function symbol @fbag_join.

bool	is_join_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_join.

application	join (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
	Application of function symbol @fbag_join.

void	make_join (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 @fbag_join.

bool	is_join_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_join.

const core::identifier_string &	fset2fbag_name ()
	Generate identifier @fset2fbag.

function_symbol	fset2fbag (const sort_expression &s)
	Constructor for function symbol @fset2fbag.

bool	is_fset2fbag_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset2fbag.

application	fset2fbag (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @fset2fbag.

void	make_fset2fbag (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @fset2fbag.

bool	is_fset2fbag_application (const atermpp::aterm &e)
	Recogniser for application of @fset2fbag.

core::identifier_string const &	bag_enumeration_name ()
	Generate identifier bag_enumeration.

function_symbol	bag_enumeration (const sort_expression &s)
	Constructor for function symbol bag_enumeration.

bool	is_bag_enumeration_function_symbol (const atermpp::aterm &e)
	Recogniser for function bag_enumeration.

template<typename Sequence >
data_expression	bag_enumeration (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
	Application of function symbol bag_enumeration.

data_expression	bag_enumeration (const sort_expression &s, data_expression_list const &range)
	Application of function symbol bag_enumeration.

bool	is_bag_enumeration_application (const atermpp::aterm &e)
	Recogniser for application of bag_enumeration.

Detailed Description

Namespace for system defined sort bag.

Typedef Documentation

◆ implementation_map

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

Definition at line 151 of file bag1.h.

Function Documentation

◆ add_function() [1/2]

function_symbol mcrl2::data::sort_bag::add_function ( const sort_expression & s )

inline

Constructor for function symbol @add_.

Parameters

s	A sort expression.

Returns: Function symbol add_function.

Definition at line 955 of file bag1.h.

◆ add_function() [2/2]

application mcrl2::data::sort_bag::add_function	(	const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @add_.

Parameters

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

Returns: Application of @add_ to a number of arguments.

Definition at line 980 of file bag1.h.

◆ add_function_name()

const core::identifier_string & mcrl2::data::sort_bag::add_function_name ( )

inline

Generate identifier @add_.

Returns: Identifier @add_.

Definition at line 945 of file bag1.h.

◆ arg()

const data_expression & mcrl2::data::sort_bag::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 1648 of file bag1.h.

◆ arg1()

const data_expression & mcrl2::data::sort_bag::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 1660 of file bag1.h.

◆ arg2()

const data_expression & mcrl2::data::sort_bag::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 1672 of file bag1.h.

◆ arg3()

const data_expression & mcrl2::data::sort_bag::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 1684 of file bag1.h.

◆ arg4()

const data_expression & mcrl2::data::sort_bag::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 1696 of file bag1.h.

◆ bag()

container_sort mcrl2::data::sort_bag::bag ( const sort_expression & s )

inline

Constructor for sort expression Bag(S)

Parameters

s	A sort expression

Returns: Sort expression bag(s)

Definition at line 44 of file bag1.h.

◆ bag2set() [1/2]

function_symbol mcrl2::data::sort_bag::bag2set ( const sort_expression & s )

inline

Constructor for function symbol Bag2Set.

Parameters

s	A sort expression.

Returns: Function symbol bag2set.

Definition at line 707 of file bag1.h.

◆ bag2set() [2/2]

application mcrl2::data::sort_bag::bag2set	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol Bag2Set.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of Bag2Set to a number of arguments.

Definition at line 731 of file bag1.h.

◆ bag2set_name()

const core::identifier_string & mcrl2::data::sort_bag::bag2set_name ( )

inline

Generate identifier Bag2Set.

Returns: Identifier Bag2Set.

Definition at line 697 of file bag1.h.

◆ bag_comprehension() [1/2]

function_symbol mcrl2::data::sort_bag::bag_comprehension ( const sort_expression & s )

inline

Constructor for function symbol @bagcomp.

Parameters

s	A sort expression.

Returns: Function symbol bag_comprehension.

Definition at line 238 of file bag1.h.

◆ bag_comprehension() [2/2]

application mcrl2::data::sort_bag::bag_comprehension	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @bagcomp.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @bagcomp to a number of arguments.

Definition at line 262 of file bag1.h.

◆ bag_comprehension_name()

const core::identifier_string & mcrl2::data::sort_bag::bag_comprehension_name ( )

inline

Generate identifier @bagcomp.

Returns: Identifier @bagcomp.

Definition at line 228 of file bag1.h.

◆ bag_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_bag::bag_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 bag.

Parameters

s	A sort expression.

Returns: All system defined constructors that are to be implemented in C++ for bag.

Definition at line 156 of file bag1.h.

◆ bag_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_bag::bag_cpp_implementable_mappings ( const sort_expression & s )

inline

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

Parameters

s	A sort expression

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

Definition at line 1612 of file bag1.h.

◆ bag_enumeration() [1/3]

function_symbol mcrl2::data::sort_bag::bag_enumeration ( const sort_expression & s )

inline

Constructor for function symbol bag_enumeration.

Parameters

s	A sort expression

Returns: Function symbol bag_enumeration

Definition at line 291 of file standard_container_utility.h.

◆ bag_enumeration() [2/3]

data_expression mcrl2::data::sort_bag::bag_enumeration	(	const sort_expression &	s,
		data_expression_list const &	range
	)

inline

Application of function symbol bag_enumeration.

Parameters

s	A sort expression
range	A range of data expressions

Returns: Application of bag_enum to the data expressions in range.

Definition at line 349 of file standard_container_utility.h.

◆ bag_enumeration() [3/3]

template<typename Sequence >

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

inline

Application of function symbol bag_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 bag_enum to the data expressions in range.

Definition at line 319 of file standard_container_utility.h.

◆ bag_enumeration_name()

core::identifier_string const & mcrl2::data::sort_bag::bag_enumeration_name ( )

inline

Generate identifier bag_enumeration.

Returns: Identifier bag_enumeration

Definition at line 281 of file standard_container_utility.h.

◆ bag_fbag() [1/2]

function_symbol mcrl2::data::sort_bag::bag_fbag ( const sort_expression & s )

inline

Constructor for function symbol @bagfbag.

Parameters

s	A sort expression.

Returns: Function symbol bag_fbag.

Definition at line 176 of file bag1.h.

◆ bag_fbag() [2/2]

application mcrl2::data::sort_bag::bag_fbag	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @bagfbag.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @bagfbag to a number of arguments.

Definition at line 200 of file bag1.h.

◆ bag_fbag_name()

const core::identifier_string & mcrl2::data::sort_bag::bag_fbag_name ( )

inline

Generate identifier @bagfbag.

Returns: Identifier @bagfbag.

Definition at line 166 of file bag1.h.

◆ bag_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_and_functions_code ( const sort_expression & s )

inline

Give all system defined mappings and constructors for bag.

Parameters

s	A sort expression

Returns: All system defined mappings for bag

Definition at line 1562 of file bag1.h.

◆ bag_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_code ( const sort_expression & s )

inline

Give all system defined constructors for bag.

Parameters

s	A sort expression.

Returns: All system defined constructors for bag.

Definition at line 132 of file bag1.h.

◆ bag_generate_equations_code()

data_equation_vector mcrl2::data::sort_bag::bag_generate_equations_code ( const sort_expression & s )

inline

Give all system defined equations for bag.

Parameters

s	A sort expression

Returns: All system defined equations for sort bag

Definition at line 1706 of file bag1.h.

◆ bag_generate_functions_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_functions_code ( const sort_expression & s )

inline

Give all system defined mappings for bag.

Parameters

s	A sort expression

Returns: All system defined mappings for bag

Definition at line 1529 of file bag1.h.

◆ bag_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_constructors ( const sort_expression & s )

inline

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

Parameters

s	A sort expression.

Returns: All system defined constructors that can be used in an mCRL2 specification for bag.

Definition at line 143 of file bag1.h.

◆ bag_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_mappings ( const sort_expression & s )

inline

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

Parameters

s	A sort expression

Returns: All system defined mappings for that can be used in mCRL2 specificationis bag

Definition at line 1576 of file bag1.h.

◆ bool2nat_function() [1/2]

function_symbol mcrl2::data::sort_bag::bool2nat_function ( const sort_expression & s )

inline

Constructor for function symbol @Bool2Nat_.

Parameters

s	A sort expression.

Returns: Function symbol bool2nat_function.

Definition at line 1209 of file bag1.h.

◆ bool2nat_function() [2/2]

application mcrl2::data::sort_bag::bool2nat_function	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @Bool2Nat_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @Bool2Nat_ to a number of arguments.

Definition at line 1233 of file bag1.h.

◆ bool2nat_function_name()

const core::identifier_string & mcrl2::data::sort_bag::bool2nat_function_name ( )

inline

Generate identifier @Bool2Nat_.

Returns: Identifier @Bool2Nat_.

Definition at line 1199 of file bag1.h.

◆ constructor() [1/2]

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

inline

Constructor for function symbol @bag.

Parameters

s	A sort expression.

Returns: Function symbol constructor.

Definition at line 78 of file bag1.h.

◆ constructor() [2/2]

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

inline

Application of function symbol @bag.

Parameters

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

Returns: Application of @bag to a number of arguments.

Definition at line 103 of file bag1.h.

◆ constructor_name()

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

inline

Generate identifier @bag.

Returns: Identifier @bag.

Definition at line 68 of file bag1.h.

◆ count() [1/2]

function_symbol mcrl2::data::sort_bag::count	(	const sort_expression &	,
		const sort_expression &	s0,
		const sort_expression &	s1
	)

inline

Definition at line 298 of file bag1.h.

◆ count() [2/2]

application mcrl2::data::sort_bag::count	(	const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol count.

Parameters

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

Returns: Application of count to a number of arguments.

Definition at line 325 of file bag1.h.

◆ count_name()

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

inline

Generate identifier count.

Returns: Identifier count.

Definition at line 290 of file bag1.h.

◆ difference() [1/2]

application mcrl2::data::sort_bag::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 668 of file bag1.h.

◆ difference() [2/2]

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

inline

Definition at line 612 of file bag1.h.

◆ difference_name()

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

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 604 of file bag1.h.

◆ fbag2fset() [1/2]

function_symbol mcrl2::data::sort_bag::fbag2fset ( const sort_expression & s )

inline

Constructor for function symbol @fbag2fset.

Parameters

s	A sort expression.

Returns: Function symbol fbag2fset.

Definition at line 1475 of file bag1.h.

◆ fbag2fset() [2/2]

application mcrl2::data::sort_bag::fbag2fset	(	const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @fbag2fset.

Parameters

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

Returns: Application of @fbag2fset to a number of arguments.

Definition at line 1500 of file bag1.h.

◆ fbag2fset_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag2fset_name ( )

inline

Generate identifier @fbag2fset.

Returns: Identifier @fbag2fset.

Definition at line 1465 of file bag1.h.

◆ fbag_difference() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_difference ( const sort_expression & s )

inline

Constructor for function symbol @fbag_diff.

Parameters

s	A sort expression.

Returns: Function symbol fbag_difference.

Definition at line 1407 of file bag1.h.

◆ fbag_difference() [2/2]

application mcrl2::data::sort_bag::fbag_difference	(	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 @fbag_diff.

Parameters

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

Returns: Application of @fbag_diff to a number of arguments.

Definition at line 1434 of file bag1.h.

◆ fbag_difference_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_difference_name ( )

inline

Generate identifier @fbag_diff.

Returns: Identifier @fbag_diff.

Definition at line 1397 of file bag1.h.

◆ fbag_intersect() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_intersect ( const sort_expression & s )

inline

Constructor for function symbol @fbag_inter.

Parameters

s	A sort expression.

Returns: Function symbol fbag_intersect.

Definition at line 1339 of file bag1.h.

◆ fbag_intersect() [2/2]

application mcrl2::data::sort_bag::fbag_intersect	(	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 @fbag_inter.

Parameters

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

Returns: Application of @fbag_inter to a number of arguments.

Definition at line 1366 of file bag1.h.

◆ fbag_intersect_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_intersect_name ( )

inline

Generate identifier @fbag_inter.

Returns: Identifier @fbag_inter.

Definition at line 1329 of file bag1.h.

◆ fbag_join() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_join ( const sort_expression & s )

inline

Constructor for function symbol @fbag_join.

Parameters

s	A sort expression.

Returns: Function symbol fbag_join.

Definition at line 1271 of file bag1.h.

◆ fbag_join() [2/2]

application mcrl2::data::sort_bag::fbag_join	(	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 @fbag_join.

Parameters

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

Returns: Application of @fbag_join to a number of arguments.

Definition at line 1298 of file bag1.h.

◆ fbag_join_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_join_name ( )

inline

Generate identifier @fbag_join.

Returns: Identifier @fbag_join.

Definition at line 1261 of file bag1.h.

◆ fset2fbag() [1/2]

function_symbol mcrl2::data::sort_bag::fset2fbag ( const sort_expression & s )

inline

Constructor for function symbol @fset2fbag.

Parameters

s	A sort expression.

Returns: Function symbol fset2fbag.

Definition at line 1539 of file bag64.h.

◆ fset2fbag() [2/2]

application mcrl2::data::sort_bag::fset2fbag	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @fset2fbag.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @fset2fbag to a number of arguments.

Definition at line 1563 of file bag64.h.

◆ fset2fbag_name()

const core::identifier_string & mcrl2::data::sort_bag::fset2fbag_name ( )

inline

Generate identifier @fset2fbag.

Returns: Identifier @fset2fbag.

Definition at line 1529 of file bag64.h.

◆ in() [1/2]

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

inline

Definition at line 362 of file bag1.h.

◆ in() [2/2]

application mcrl2::data::sort_bag::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 389 of file bag1.h.

◆ in_name()

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

inline

Generate identifier in.

Returns: Identifier in.

Definition at line 354 of file bag1.h.

◆ intersection() [1/2]

application mcrl2::data::sort_bag::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 575 of file bag1.h.

◆ intersection() [2/2]

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

inline

Definition at line 511 of file bag1.h.

◆ intersection_name()

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

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 503 of file bag1.h.

◆ is_add_function_application()

bool mcrl2::data::sort_bag::is_add_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @add_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol add_function to a number of arguments.

Definition at line 1001 of file bag1.h.

◆ is_add_function_function_symbol()

bool mcrl2::data::sort_bag::is_add_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @add_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @add_.

Definition at line 965 of file bag1.h.

◆ is_bag()

bool mcrl2::data::sort_bag::is_bag ( const sort_expression & e )

inline

Recogniser for sort expression Bag(s)

Parameters

e	A sort expression

Returns: true iff e is a container sort of which the name matches bag

Definition at line 55 of file bag1.h.

◆ is_bag2set_application()

bool mcrl2::data::sort_bag::is_bag2set_application ( const atermpp::aterm & e )

inline

Recogniser for application of Bag2Set.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol bag2set to a number of arguments.

Definition at line 751 of file bag1.h.

◆ is_bag2set_function_symbol()

bool mcrl2::data::sort_bag::is_bag2set_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Bag2Set.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Bag2Set.

Definition at line 717 of file bag1.h.

◆ is_bag_comprehension_application()

bool mcrl2::data::sort_bag::is_bag_comprehension_application ( const atermpp::aterm & e )

inline

Recogniser for application of @bagcomp.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol bag_comprehension to a number of arguments.

Definition at line 282 of file bag1.h.

◆ is_bag_comprehension_function_symbol()

bool mcrl2::data::sort_bag::is_bag_comprehension_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @bagcomp.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @bagcomp.

Definition at line 248 of file bag1.h.

◆ is_bag_enumeration_application()

bool mcrl2::data::sort_bag::is_bag_enumeration_application ( const atermpp::aterm & e )

inline

Recogniser for application of bag_enumeration.

Parameters

e	A data expression

Returns: true iff e is an application of function symbol bag_enumeration to a number of arguments

Definition at line 377 of file standard_container_utility.h.

◆ is_bag_enumeration_function_symbol()

bool mcrl2::data::sort_bag::is_bag_enumeration_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function bag_enumeration.

Parameters

e	A data expression

Returns: true iff e is the function symbol matching bag_enumeration

Definition at line 301 of file standard_container_utility.h.

◆ is_bag_fbag_application()

bool mcrl2::data::sort_bag::is_bag_fbag_application ( const atermpp::aterm & e )

inline

Recogniser for application of @bagfbag.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol bag_fbag to a number of arguments.

Definition at line 220 of file bag1.h.

◆ is_bag_fbag_function_symbol()

bool mcrl2::data::sort_bag::is_bag_fbag_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @bagfbag.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @bagfbag.

Definition at line 186 of file bag1.h.

◆ is_bool2nat_function_application()

bool mcrl2::data::sort_bag::is_bool2nat_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @Bool2Nat_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol bool2nat_function to a number of arguments.

Definition at line 1253 of file bag1.h.

◆ is_bool2nat_function_function_symbol()

bool mcrl2::data::sort_bag::is_bool2nat_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @Bool2Nat_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @Bool2Nat_.

Definition at line 1219 of file bag1.h.

◆ is_constructor_application()

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

inline

Recogniser for application of @bag.

Parameters

e	A data expression.

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

Definition at line 124 of file bag1.h.

◆ is_constructor_function_symbol()

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

inline

Recogniser for function @bag.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @bag.

Definition at line 88 of file bag1.h.

◆ is_count_application()

bool mcrl2::data::sort_bag::is_count_application ( const atermpp::aterm & e )

inline

Recogniser for application of count.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol count to a number of arguments.

Definition at line 346 of file bag1.h.

◆ is_count_function_symbol()

bool mcrl2::data::sort_bag::is_count_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function count.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching count.

Definition at line 309 of file bag1.h.

◆ is_difference_application()

bool mcrl2::data::sort_bag::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 689 of file bag1.h.

◆ is_difference_function_symbol()

bool mcrl2::data::sort_bag::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 652 of file bag1.h.

◆ is_fbag2fset_application()

bool mcrl2::data::sort_bag::is_fbag2fset_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fbag2fset.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol fbag2fset to a number of arguments.

Definition at line 1521 of file bag1.h.

◆ is_fbag2fset_function_symbol()

bool mcrl2::data::sort_bag::is_fbag2fset_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fbag2fset.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fbag2fset.

Definition at line 1485 of file bag1.h.

◆ is_fbag_difference_application()

bool mcrl2::data::sort_bag::is_fbag_difference_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fbag_diff.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol fbag_difference to a number of arguments.

Definition at line 1457 of file bag1.h.

◆ is_fbag_difference_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_difference_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fbag_diff.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fbag_diff.

Definition at line 1417 of file bag1.h.

◆ is_fbag_intersect_application()

bool mcrl2::data::sort_bag::is_fbag_intersect_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fbag_inter.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol fbag_intersect to a number of arguments.

Definition at line 1389 of file bag1.h.

◆ is_fbag_intersect_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_intersect_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fbag_inter.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fbag_inter.

Definition at line 1349 of file bag1.h.

◆ is_fbag_join_application()

bool mcrl2::data::sort_bag::is_fbag_join_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fbag_join.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol fbag_join to a number of arguments.

Definition at line 1321 of file bag1.h.

◆ is_fbag_join_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_join_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fbag_join.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fbag_join.

Definition at line 1281 of file bag1.h.

◆ is_fset2fbag_application()

bool mcrl2::data::sort_bag::is_fset2fbag_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fset2fbag.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol fset2fbag to a number of arguments.

Definition at line 1583 of file bag64.h.

◆ is_fset2fbag_function_symbol()

bool mcrl2::data::sort_bag::is_fset2fbag_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fset2fbag.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fset2fbag.

Definition at line 1549 of file bag64.h.

◆ is_in_application()

bool mcrl2::data::sort_bag::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 410 of file bag1.h.

◆ is_in_function_symbol()

bool mcrl2::data::sort_bag::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 373 of file bag1.h.

◆ is_intersection_application()

bool mcrl2::data::sort_bag::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 596 of file bag1.h.

◆ is_intersection_function_symbol()

bool mcrl2::data::sort_bag::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 559 of file bag1.h.

◆ is_join_application()

bool mcrl2::data::sort_bag::is_join_application ( const atermpp::aterm & e )

inline

Recogniser for application of @fbag_join.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol join to a number of arguments.

Definition at line 1321 of file bag64.h.

◆ is_join_function_symbol()

bool mcrl2::data::sort_bag::is_join_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @fbag_join.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @fbag_join.

Definition at line 1281 of file bag64.h.

◆ is_min_function_application()

bool mcrl2::data::sort_bag::is_min_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @min_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol min_function to a number of arguments.

Definition at line 1065 of file bag1.h.

◆ is_min_function_function_symbol()

bool mcrl2::data::sort_bag::is_min_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @min_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @min_.

Definition at line 1029 of file bag1.h.

◆ is_monus_function_application()

bool mcrl2::data::sort_bag::is_monus_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @monus_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol monus_function to a number of arguments.

Definition at line 1129 of file bag1.h.

◆ is_monus_function_function_symbol()

bool mcrl2::data::sort_bag::is_monus_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @monus_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @monus_.

Definition at line 1093 of file bag1.h.

◆ is_nat2bool_function_application()

bool mcrl2::data::sort_bag::is_nat2bool_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @Nat2Bool_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol nat2bool_function to a number of arguments.

Definition at line 1191 of file bag1.h.

◆ is_nat2bool_function_function_symbol()

bool mcrl2::data::sort_bag::is_nat2bool_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @Nat2Bool_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @Nat2Bool_.

Definition at line 1157 of file bag1.h.

◆ is_one_function_application()

bool mcrl2::data::sort_bag::is_one_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @one_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol one_function to a number of arguments.

Definition at line 937 of file bag1.h.

◆ is_one_function_function_symbol()

bool mcrl2::data::sort_bag::is_one_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @one_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @one_.

Definition at line 903 of file bag1.h.

◆ is_set2bag_application()

bool mcrl2::data::sort_bag::is_set2bag_application ( const atermpp::aterm & e )

inline

Recogniser for application of Set2Bag.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol set2bag to a number of arguments.

Definition at line 813 of file bag1.h.

◆ is_set2bag_function_symbol()

bool mcrl2::data::sort_bag::is_set2bag_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function Set2Bag.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching Set2Bag.

Definition at line 779 of file bag1.h.

◆ is_union_application()

bool mcrl2::data::sort_bag::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 495 of file bag1.h.

◆ is_union_function_symbol()

bool mcrl2::data::sort_bag::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 458 of file bag1.h.

◆ is_zero_function_application()

bool mcrl2::data::sort_bag::is_zero_function_application ( const atermpp::aterm & e )

inline

Recogniser for application of @zero_.

Parameters

e	A data expression.

Returns: true iff e is an application of function symbol zero_function to a number of arguments.

Definition at line 875 of file bag1.h.

◆ is_zero_function_function_symbol()

bool mcrl2::data::sort_bag::is_zero_function_function_symbol ( const atermpp::aterm & e )

inline

Recogniser for function @zero_.

Parameters

e	A data expression.

Returns: true iff e is the function symbol matching @zero_.

Definition at line 841 of file bag1.h.

◆ join() [1/2]

function_symbol mcrl2::data::sort_bag::join ( const sort_expression & s )

inline

Constructor for function symbol @fbag_join.

Parameters

s	A sort expression.

Returns: Function symbol join.

Definition at line 1271 of file bag64.h.

◆ join() [2/2]

application mcrl2::data::sort_bag::join	(	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 @fbag_join.

Parameters

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

Returns: Application of @fbag_join to a number of arguments.

Definition at line 1298 of file bag64.h.

◆ join_name()

const core::identifier_string & mcrl2::data::sort_bag::join_name ( )

inline

Generate identifier @fbag_join.

Returns: Identifier @fbag_join.

Definition at line 1261 of file bag64.h.

◆ left()

const data_expression & mcrl2::data::sort_bag::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 1624 of file bag1.h.

◆ make_add_function()

void mcrl2::data::sort_bag::make_add_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @add_.

Parameters

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

Definition at line 991 of file bag1.h.

◆ make_bag2set()

void mcrl2::data::sort_bag::make_bag2set	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Bag2Set.

Parameters

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

Definition at line 741 of file bag1.h.

◆ make_bag_comprehension()

void mcrl2::data::sort_bag::make_bag_comprehension	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @bagcomp.

Parameters

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

Definition at line 272 of file bag1.h.

◆ make_bag_fbag()

void mcrl2::data::sort_bag::make_bag_fbag	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @bagfbag.

Parameters

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

Definition at line 210 of file bag1.h.

◆ make_bool2nat_function()

void mcrl2::data::sort_bag::make_bool2nat_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @Bool2Nat_.

Parameters

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

Definition at line 1243 of file bag1.h.

◆ make_constructor()

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

inline

Make an application of function symbol @bag.

Parameters

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

Definition at line 114 of file bag1.h.

◆ make_count()

void mcrl2::data::sort_bag::make_count	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol count.

Parameters

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

Definition at line 336 of file bag1.h.

◆ make_difference()

void mcrl2::data::sort_bag::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 679 of file bag1.h.

◆ make_fbag2fset()

void mcrl2::data::sort_bag::make_fbag2fset	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @fbag2fset.

Parameters

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

Definition at line 1511 of file bag1.h.

◆ make_fbag_difference()

void mcrl2::data::sort_bag::make_fbag_difference	(	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 @fbag_diff.

Parameters

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

Definition at line 1447 of file bag1.h.

◆ make_fbag_intersect()

void mcrl2::data::sort_bag::make_fbag_intersect	(	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 @fbag_inter.

Parameters

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

Definition at line 1379 of file bag1.h.

◆ make_fbag_join()

void mcrl2::data::sort_bag::make_fbag_join	(	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 @fbag_join.

Parameters

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

Definition at line 1311 of file bag1.h.

◆ make_fset2fbag()

void mcrl2::data::sort_bag::make_fset2fbag	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @fset2fbag.

Parameters

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

Definition at line 1573 of file bag64.h.

◆ make_in()

void mcrl2::data::sort_bag::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 400 of file bag1.h.

◆ make_intersection()

void mcrl2::data::sort_bag::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 586 of file bag1.h.

◆ make_join()

void mcrl2::data::sort_bag::make_join	(	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 @fbag_join.

Parameters

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

Definition at line 1311 of file bag64.h.

◆ make_min_function()

void mcrl2::data::sort_bag::make_min_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @min_.

Parameters

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

Definition at line 1055 of file bag1.h.

◆ make_monus_function()

void mcrl2::data::sort_bag::make_monus_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Make an application of function symbol @monus_.

Parameters

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

Definition at line 1119 of file bag1.h.

◆ make_nat2bool_function()

void mcrl2::data::sort_bag::make_nat2bool_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @Nat2Bool_.

Parameters

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

Definition at line 1181 of file bag1.h.

◆ make_one_function()

void mcrl2::data::sort_bag::make_one_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @one_.

Parameters

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

Definition at line 927 of file bag1.h.

◆ make_set2bag()

void mcrl2::data::sort_bag::make_set2bag	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol Set2Bag.

Parameters

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

Definition at line 803 of file bag1.h.

◆ make_union_()

void mcrl2::data::sort_bag::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 485 of file bag1.h.

◆ make_zero_function()

void mcrl2::data::sort_bag::make_zero_function	(	data_expression &	result,
		const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Make an application of function symbol @zero_.

Parameters

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

Definition at line 865 of file bag1.h.

◆ min_function() [1/2]

function_symbol mcrl2::data::sort_bag::min_function ( const sort_expression & s )

inline

Constructor for function symbol @min_.

Parameters

s	A sort expression.

Returns: Function symbol min_function.

Definition at line 1019 of file bag1.h.

◆ min_function() [2/2]

application mcrl2::data::sort_bag::min_function	(	const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @min_.

Parameters

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

Returns: Application of @min_ to a number of arguments.

Definition at line 1044 of file bag1.h.

◆ min_function_name()

const core::identifier_string & mcrl2::data::sort_bag::min_function_name ( )

inline

Generate identifier @min_.

Returns: Identifier @min_.

Definition at line 1009 of file bag1.h.

◆ monus_function() [1/2]

function_symbol mcrl2::data::sort_bag::monus_function ( const sort_expression & s )

inline

Constructor for function symbol @monus_.

Parameters

s	A sort expression.

Returns: Function symbol monus_function.

Definition at line 1083 of file bag1.h.

◆ monus_function() [2/2]

application mcrl2::data::sort_bag::monus_function	(	const sort_expression &	s,
		const data_expression &	arg0,
		const data_expression &	arg1
	)

inline

Application of function symbol @monus_.

Parameters

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

Returns: Application of @monus_ to a number of arguments.

Definition at line 1108 of file bag1.h.

◆ monus_function_name()

const core::identifier_string & mcrl2::data::sort_bag::monus_function_name ( )

inline

Generate identifier @monus_.

Returns: Identifier @monus_.

Definition at line 1073 of file bag1.h.

◆ nat2bool_function() [1/2]

function_symbol mcrl2::data::sort_bag::nat2bool_function ( const sort_expression & s )

inline

Constructor for function symbol @Nat2Bool_.

Parameters

s	A sort expression.

Returns: Function symbol nat2bool_function.

Definition at line 1147 of file bag1.h.

◆ nat2bool_function() [2/2]

application mcrl2::data::sort_bag::nat2bool_function	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @Nat2Bool_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @Nat2Bool_ to a number of arguments.

Definition at line 1171 of file bag1.h.

◆ nat2bool_function_name()

const core::identifier_string & mcrl2::data::sort_bag::nat2bool_function_name ( )

inline

Generate identifier @Nat2Bool_.

Returns: Identifier @Nat2Bool_.

Definition at line 1137 of file bag1.h.

◆ one_function() [1/2]

function_symbol mcrl2::data::sort_bag::one_function ( const sort_expression & s )

inline

Constructor for function symbol @one_.

Parameters

s	A sort expression.

Returns: Function symbol one_function.

Definition at line 893 of file bag1.h.

◆ one_function() [2/2]

application mcrl2::data::sort_bag::one_function	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @one_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @one_ to a number of arguments.

Definition at line 917 of file bag1.h.

◆ one_function_name()

const core::identifier_string & mcrl2::data::sort_bag::one_function_name ( )

inline

Generate identifier @one_.

Returns: Identifier @one_.

Definition at line 883 of file bag1.h.

◆ right()

const data_expression & mcrl2::data::sort_bag::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 1636 of file bag1.h.

◆ set2bag() [1/2]

function_symbol mcrl2::data::sort_bag::set2bag ( const sort_expression & s )

inline

Constructor for function symbol Set2Bag.

Parameters

s	A sort expression.

Returns: Function symbol set2bag.

Definition at line 769 of file bag1.h.

◆ set2bag() [2/2]

application mcrl2::data::sort_bag::set2bag	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol Set2Bag.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of Set2Bag to a number of arguments.

Definition at line 793 of file bag1.h.

◆ set2bag_name()

const core::identifier_string & mcrl2::data::sort_bag::set2bag_name ( )

inline

Generate identifier Set2Bag.

Returns: Identifier Set2Bag.

Definition at line 759 of file bag1.h.

◆ union_() [1/2]

application mcrl2::data::sort_bag::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 474 of file bag1.h.

◆ union_() [2/2]

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

inline

Definition at line 426 of file bag1.h.

◆ union_name()

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

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 418 of file bag1.h.

◆ zero_function() [1/2]

function_symbol mcrl2::data::sort_bag::zero_function ( const sort_expression & s )

inline

Constructor for function symbol @zero_.

Parameters

s	A sort expression.

Returns: Function symbol zero_function.

Definition at line 831 of file bag1.h.

◆ zero_function() [2/2]

application mcrl2::data::sort_bag::zero_function	(	const sort_expression &	s,
		const data_expression &	arg0
	)

inline

Application of function symbol @zero_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns: Application of @zero_ to a number of arguments.

Definition at line 855 of file bag1.h.

◆ zero_function_name()

const core::identifier_string & mcrl2::data::sort_bag::zero_function_name ( )

inline

Generate identifier @zero_.

Returns: Identifier @zero_.

Definition at line 821 of file bag1.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ add_function() [1/2]

◆ add_function() [2/2]

◆ add_function_name()

◆ arg()

◆ arg1()

◆ arg2()

◆ arg3()

◆ arg4()

◆ bag()

◆ bag2set() [1/2]

◆ bag2set() [2/2]

◆ bag2set_name()

◆ bag_comprehension() [1/2]

◆ bag_comprehension() [2/2]

◆ bag_comprehension_name()

◆ bag_cpp_implementable_constructors()

◆ bag_cpp_implementable_mappings()

◆ bag_enumeration() [1/3]

◆ bag_enumeration() [2/3]

◆ bag_enumeration() [3/3]

◆ bag_enumeration_name()

◆ bag_fbag() [1/2]

◆ bag_fbag() [2/2]

◆ bag_fbag_name()

◆ bag_generate_constructors_and_functions_code()

◆ bag_generate_constructors_code()

◆ bag_generate_equations_code()

◆ bag_generate_functions_code()

◆ bag_mCRL2_usable_constructors()

◆ bag_mCRL2_usable_mappings()

◆ bool2nat_function() [1/2]

◆ bool2nat_function() [2/2]

◆ bool2nat_function_name()

◆ constructor() [1/2]

◆ constructor() [2/2]

◆ constructor_name()

◆ count() [1/2]

◆ count() [2/2]

◆ count_name()

◆ difference() [1/2]

◆ difference() [2/2]

◆ difference_name()

◆ fbag2fset() [1/2]

◆ fbag2fset() [2/2]

◆ fbag2fset_name()

◆ fbag_difference() [1/2]

◆ fbag_difference() [2/2]

◆ fbag_difference_name()

◆ fbag_intersect() [1/2]

◆ fbag_intersect() [2/2]

◆ fbag_intersect_name()

◆ fbag_join() [1/2]

◆ fbag_join() [2/2]

◆ fbag_join_name()

◆ fset2fbag() [1/2]

◆ fset2fbag() [2/2]

◆ fset2fbag_name()

◆ in() [1/2]

◆ in() [2/2]

◆ in_name()

◆ intersection() [1/2]

◆ intersection() [2/2]

◆ intersection_name()

◆ is_add_function_application()

◆ is_add_function_function_symbol()

◆ is_bag()

◆ is_bag2set_application()

◆ is_bag2set_function_symbol()

◆ is_bag_comprehension_application()

◆ is_bag_comprehension_function_symbol()

◆ is_bag_enumeration_application()

◆ is_bag_enumeration_function_symbol()

◆ is_bag_fbag_application()

◆ is_bag_fbag_function_symbol()