mCRL2
Loading...
Searching...
No Matches
mcrl2::data::sort_bag Namespace Reference

Namespace for system defined sort bag. More...

Typedefs

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

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 &)
 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 &)
 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 148 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
sA sort expression.
Returns
Function symbol add_function.

Definition at line 951 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of @add_ to a number of arguments.

Definition at line 976 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 941 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
eA data expression.
Precondition
arg is defined for e.
Returns
The argument of e that corresponds to arg.

Definition at line 1643 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
eA data expression.
Precondition
arg1 is defined for e.
Returns
The argument of e that corresponds to arg1.

Definition at line 1655 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
eA data expression.
Precondition
arg2 is defined for e.
Returns
The argument of e that corresponds to arg2.

Definition at line 1667 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
eA data expression.
Precondition
arg3 is defined for e.
Returns
The argument of e that corresponds to arg3.

Definition at line 1679 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
eA data expression.
Precondition
arg4 is defined for e.
Returns
The argument of e that corresponds to arg4.

Definition at line 1691 of file bag1.h.

◆ bag()

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

Constructor for sort expression Bag(S)

Parameters
sA sort expression
Returns
Sort expression bag(s)

Definition at line 41 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
sA sort expression.
Returns
Function symbol bag2set.

Definition at line 703 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of Bag2Set to a number of arguments.

Definition at line 727 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 693 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
sA sort expression.
Returns
Function symbol bag_comprehension.

Definition at line 234 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @bagcomp to a number of arguments.

Definition at line 258 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 224 of file bag1.h.

◆ bag_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_bag::bag_cpp_implementable_constructors ( const sort_expression &  )
inline

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

Parameters
sA sort expression.
Returns
All system defined constructors that are to be implemented in C++ for bag.

Definition at line 153 of file bag1.h.

◆ bag_cpp_implementable_mappings()

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

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

Parameters
sA sort expression
Returns
A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for bag

Definition at line 1608 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
sA sort expression
Returns
Function symbol bag_enumeration

Definition at line 290 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
sA sort expression
rangeA range of data expressions
Returns
Application of bag_enum to the data expressions in range.

Definition at line 348 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
sA sort expression
rangeA range of data expressions
Returns
Application of bag_enum to the data expressions in range.

Definition at line 318 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 280 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
sA sort expression.
Returns
Function symbol bag_fbag.

Definition at line 172 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @bagfbag to a number of arguments.

Definition at line 196 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 162 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
sA sort expression
Returns
All system defined mappings for bag

Definition at line 1558 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
sA sort expression.
Returns
All system defined constructors for bag.

Definition at line 129 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
sA sort expression
Returns
All system defined equations for sort bag

Definition at line 1701 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
sA sort expression
Returns
All system defined mappings for bag

Definition at line 1525 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
sA sort expression.
Returns
All system defined constructors that can be used in an mCRL2 specification for bag.

Definition at line 140 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
sA sort expression
Returns
All system defined mappings for that can be used in mCRL2 specificationis bag

Definition at line 1572 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
sA sort expression.
Returns
Function symbol bool2nat_function.

Definition at line 1205 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @Bool2Nat_ to a number of arguments.

Definition at line 1229 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 1195 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
sA sort expression.
Returns
Function symbol constructor.

Definition at line 75 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of @bag to a number of arguments.

Definition at line 100 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 65 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 294 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of count to a number of arguments.

Definition at line 321 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 286 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of - to a number of arguments.

Definition at line 664 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 608 of file bag1.h.

◆ difference_name()

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

Generate identifier -.

Returns
Identifier -.

Definition at line 600 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
sA sort expression.
Returns
Function symbol fbag2fset.

Definition at line 1471 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of @fbag2fset to a number of arguments.

Definition at line 1496 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 1461 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
sA sort expression.
Returns
Function symbol fbag_difference.

Definition at line 1403 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.
Returns
Application of @fbag_diff to a number of arguments.

Definition at line 1430 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 1393 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
sA sort expression.
Returns
Function symbol fbag_intersect.

Definition at line 1335 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.
Returns
Application of @fbag_inter to a number of arguments.

Definition at line 1362 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 1325 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
sA sort expression.
Returns
Function symbol fbag_join.

Definition at line 1267 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.
Returns
Application of @fbag_join to a number of arguments.

Definition at line 1294 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 1257 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
sA sort expression.
Returns
Function symbol fset2fbag.

Definition at line 1535 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @fset2fbag to a number of arguments.

Definition at line 1559 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 1525 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 358 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of in to a number of arguments.

Definition at line 385 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 350 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of * to a number of arguments.

Definition at line 571 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 507 of file bag1.h.

◆ intersection_name()

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

Generate identifier *.

Returns
Identifier *.

Definition at line 499 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
eA data expression.
Returns
true iff e is an application of function symbol add_function to a number of arguments.

Definition at line 997 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
eA data expression.
Returns
true iff e is the function symbol matching @add_.

Definition at line 961 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
eA sort expression
Returns
true iff e is a container sort of which the name matches bag

Definition at line 52 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
eA data expression.
Returns
true iff e is an application of function symbol bag2set to a number of arguments.

Definition at line 747 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
eA data expression.
Returns
true iff e is the function symbol matching Bag2Set.

Definition at line 713 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
eA data expression.
Returns
true iff e is an application of function symbol bag_comprehension to a number of arguments.

Definition at line 278 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
eA data expression.
Returns
true iff e is the function symbol matching @bagcomp.

Definition at line 244 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
eA data expression
Returns
true iff e is an application of function symbol bag_enumeration to a number of arguments

Definition at line 376 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
eA data expression
Returns
true iff e is the function symbol matching bag_enumeration

Definition at line 300 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
eA data expression.
Returns
true iff e is an application of function symbol bag_fbag to a number of arguments.

Definition at line 216 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
eA data expression.
Returns
true iff e is the function symbol matching @bagfbag.

Definition at line 182 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
eA data expression.
Returns
true iff e is an application of function symbol bool2nat_function to a number of arguments.

Definition at line 1249 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
eA data expression.
Returns
true iff e is the function symbol matching @Bool2Nat_.

Definition at line 1215 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
eA data expression.
Returns
true iff e is an application of function symbol constructor to a number of arguments.

Definition at line 121 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
eA data expression.
Returns
true iff e is the function symbol matching @bag.

Definition at line 85 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
eA data expression.
Returns
true iff e is an application of function symbol count to a number of arguments.

Definition at line 342 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
eA data expression.
Returns
true iff e is the function symbol matching count.

Definition at line 305 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
eA data expression.
Returns
true iff e is an application of function symbol difference to a number of arguments.

Definition at line 685 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
eA data expression.
Returns
true iff e is the function symbol matching -.

Definition at line 648 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
eA data expression.
Returns
true iff e is an application of function symbol fbag2fset to a number of arguments.

Definition at line 1517 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
eA data expression.
Returns
true iff e is the function symbol matching @fbag2fset.

Definition at line 1481 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
eA data expression.
Returns
true iff e is an application of function symbol fbag_difference to a number of arguments.

Definition at line 1453 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
eA data expression.
Returns
true iff e is the function symbol matching @fbag_diff.

Definition at line 1413 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
eA data expression.
Returns
true iff e is an application of function symbol fbag_intersect to a number of arguments.

Definition at line 1385 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
eA data expression.
Returns
true iff e is the function symbol matching @fbag_inter.

Definition at line 1345 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
eA data expression.
Returns
true iff e is an application of function symbol fbag_join to a number of arguments.

Definition at line 1317 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
eA data expression.
Returns
true iff e is the function symbol matching @fbag_join.

Definition at line 1277 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
eA data expression.
Returns
true iff e is an application of function symbol fset2fbag to a number of arguments.

Definition at line 1579 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
eA data expression.
Returns
true iff e is the function symbol matching @fset2fbag.

Definition at line 1545 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
eA data expression.
Returns
true iff e is an application of function symbol in to a number of arguments.

Definition at line 406 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
eA data expression.
Returns
true iff e is the function symbol matching in.

Definition at line 369 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
eA data expression.
Returns
true iff e is an application of function symbol intersection to a number of arguments.

Definition at line 592 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
eA data expression.
Returns
true iff e is the function symbol matching *.

Definition at line 555 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
eA data expression.
Returns
true iff e is an application of function symbol join to a number of arguments.

Definition at line 1317 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
eA data expression.
Returns
true iff e is the function symbol matching @fbag_join.

Definition at line 1277 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
eA data expression.
Returns
true iff e is an application of function symbol min_function to a number of arguments.

Definition at line 1061 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
eA data expression.
Returns
true iff e is the function symbol matching @min_.

Definition at line 1025 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
eA data expression.
Returns
true iff e is an application of function symbol monus_function to a number of arguments.

Definition at line 1125 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
eA data expression.
Returns
true iff e is the function symbol matching @monus_.

Definition at line 1089 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
eA data expression.
Returns
true iff e is an application of function symbol nat2bool_function to a number of arguments.

Definition at line 1187 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
eA data expression.
Returns
true iff e is the function symbol matching @Nat2Bool_.

Definition at line 1153 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
eA data expression.
Returns
true iff e is an application of function symbol one_function to a number of arguments.

Definition at line 933 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
eA data expression.
Returns
true iff e is the function symbol matching @one_.

Definition at line 899 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
eA data expression.
Returns
true iff e is an application of function symbol set2bag to a number of arguments.

Definition at line 809 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
eA data expression.
Returns
true iff e is the function symbol matching Set2Bag.

Definition at line 775 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
eA data expression.
Returns
true iff e is an application of function symbol union_ to a number of arguments.

Definition at line 491 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
eA data expression.
Returns
true iff e is the function symbol matching +.

Definition at line 454 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
eA data expression.
Returns
true iff e is an application of function symbol zero_function to a number of arguments.

Definition at line 871 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
eA data expression.
Returns
true iff e is the function symbol matching @zero_.

Definition at line 837 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
sA sort expression.
Returns
Function symbol join.

Definition at line 1267 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.
Returns
Application of @fbag_join to a number of arguments.

Definition at line 1294 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 1257 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
eA data expression.
Precondition
left is defined for e.
Returns
The argument of e that corresponds to left.

Definition at line 1619 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
[out]resultThe data expression where the @add_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 987 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
[out]resultThe data expression where the Bag2Set expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 737 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
[out]resultThe data expression where the @bagcomp expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 268 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
[out]resultThe data expression where the @bagfbag expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 206 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
[out]resultThe data expression where the @Bool2Nat_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 1239 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
[out]resultThe data expression where the @bag expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 111 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
[out]resultThe data expression where the count expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 332 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
[out]resultThe data expression where the - expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 675 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
[out]resultThe data expression where the @fbag2fset expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 1507 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
[out]resultThe data expression where the @fbag_diff expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.

Definition at line 1443 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
[out]resultThe data expression where the @fbag_inter expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.

Definition at line 1375 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
[out]resultThe data expression where the @fbag_join expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.

Definition at line 1307 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
[out]resultThe data expression where the @fset2fbag expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 1569 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
[out]resultThe data expression where the in expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 396 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
[out]resultThe data expression where the * expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 582 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
[out]resultThe data expression where the @fbag_join expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
[in]arg2A data expression.
[in]arg3A data expression.

Definition at line 1307 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
[out]resultThe data expression where the @min_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 1051 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
[out]resultThe data expression where the @monus_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 1115 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
[out]resultThe data expression where the @Nat2Bool_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 1177 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
[out]resultThe data expression where the @one_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 923 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
[out]resultThe data expression where the Set2Bag expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 799 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
[out]resultThe data expression where the + expression is put.
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.

Definition at line 481 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
[out]resultThe data expression where the @zero_ expression is put.
[in]sA sort expression.
[in]arg0A data expression.

Definition at line 861 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
sA sort expression.
Returns
Function symbol min_function.

Definition at line 1015 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of @min_ to a number of arguments.

Definition at line 1040 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 1005 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
sA sort expression.
Returns
Function symbol monus_function.

Definition at line 1079 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of @monus_ to a number of arguments.

Definition at line 1104 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 1069 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
sA sort expression.
Returns
Function symbol nat2bool_function.

Definition at line 1143 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @Nat2Bool_ to a number of arguments.

Definition at line 1167 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 1133 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
sA sort expression.
Returns
Function symbol one_function.

Definition at line 889 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @one_ to a number of arguments.

Definition at line 913 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 879 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
eA data expression.
Precondition
right is defined for e.
Returns
The argument of e that corresponds to right.

Definition at line 1631 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
sA sort expression.
Returns
Function symbol set2bag.

Definition at line 765 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of Set2Bag to a number of arguments.

Definition at line 789 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 755 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
[in]sA sort expression.
[in]arg0A data expression.
[in]arg1A data expression.
Returns
Application of + to a number of arguments.

Definition at line 470 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 422 of file bag1.h.

◆ union_name()

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

Generate identifier +.

Returns
Identifier +.

Definition at line 414 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
sA sort expression.
Returns
Function symbol zero_function.

Definition at line 827 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
[in]sA sort expression.
[in]arg0A data expression.
Returns
Application of @zero_ to a number of arguments.

Definition at line 851 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 817 of file bag1.h.