bag.h¶

Include file:

#include "mcrl2/data/bag.h"

The standard sort bag.

This file was generated from the data sort specification mcrl2/data/build/bag.spec.

Typedefs¶

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

Functions¶

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

Constructor for function symbol @add_.

Parameters:

s A sort expression.

Returns: Function symbol add_function.

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

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.

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

Generate identifier @add_.

Returns: Identifier @add_.

const data_expression &mcrl2::data::sort_bag::arg(const data_expression &e)¶

Function for projecting out argument. arg from an application.

Parameters:

e A data expression.

Pre: arg is defined for e.

Returns: The argument of e that corresponds to arg.

const data_expression &mcrl2::data::sort_bag::arg1(const data_expression &e)¶

Function for projecting out argument. arg1 from an application.

Parameters:

e A data expression.

Pre: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

const data_expression &mcrl2::data::sort_bag::arg2(const data_expression &e)¶

Function for projecting out argument. arg2 from an application.

Parameters:

e A data expression.

Pre: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

const data_expression &mcrl2::data::sort_bag::arg3(const data_expression &e)¶

Function for projecting out argument. arg3 from an application.

Parameters:

e A data expression.

Pre: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

const data_expression &mcrl2::data::sort_bag::arg4(const data_expression &e)¶

Function for projecting out argument. arg4 from an application.

Parameters:

e A data expression.

Pre: arg4 is defined for e.

Returns: The argument of e that corresponds to arg4.

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

Constructor for sort expression Bag(S)

Parameters:

s A sort expression

Returns: Sort expression bag(s)

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

Constructor for function symbol Bag2Set.

Parameters:

s A sort expression.

Returns: Function symbol bag2set.

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

Application of function symbol Bag2Set.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of Bag2Set to a number of arguments.

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

Generate identifier Bag2Set.

Returns: Identifier Bag2Set.

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

Constructor for function symbol @bagcomp.

Parameters:

s A sort expression.

Returns: Function symbol bag_comprehension.

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

Application of function symbol @bagcomp.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @bagcomp.

Returns: Identifier @bagcomp.

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

Parameters:

s A sort expression.

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

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

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

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

Constructor for function symbol @bagfbag.

Parameters:

s A sort expression.

Returns: Function symbol bag_fbag.

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

Application of function symbol @bagfbag.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @bagfbag.

Returns: Identifier @bagfbag.

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

Give all system defined mappings and constructors for bag.

Parameters:

s A sort expression

Returns: All system defined mappings for bag

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

Give all system defined constructors for bag.

Parameters:

s A sort expression.

Returns: All system defined constructors for bag.

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

Give all system defined equations for bag.

Parameters:

s A sort expression

Returns: All system defined equations for sort bag

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

Give all system defined mappings for bag.

Parameters:

s A sort expression

Returns: All system defined mappings for bag

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

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.

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

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

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

Constructor for function symbol @Bool2Nat_.

Parameters:

s A sort expression.

Returns: Function symbol bool2nat_function.

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

Application of function symbol @Bool2Nat_.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @Bool2Nat_.

Returns: Identifier @Bool2Nat_.

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

Constructor for function symbol @bag.

Parameters:

s A sort expression.

Returns: Function symbol constructor.

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

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.

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

Generate identifier @bag.

Returns: Identifier @bag.

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

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

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.

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

Generate identifier count.

Returns: Identifier count.

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

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.

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

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

Generate identifier -.

Returns: Identifier -.

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

Constructor for function symbol @fbag2fset.

Parameters:

s A sort expression.

Returns: Function symbol fbag2fset.

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

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.

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

Generate identifier @fbag2fset.

Returns: Identifier @fbag2fset.

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

Constructor for function symbol @fbag_diff.

Parameters:

s A sort expression.

Returns: Function symbol fbag_difference.

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)¶

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.

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

Generate identifier @fbag_diff.

Returns: Identifier @fbag_diff.

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

Constructor for function symbol @fbag_inter.

Parameters:

s A sort expression.

Returns: Function symbol fbag_intersect.

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)¶

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.

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

Generate identifier @fbag_inter.

Returns: Identifier @fbag_inter.

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

Constructor for function symbol @fbag_join.

Parameters:

s A sort expression.

Returns: Function symbol fbag_join.

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)¶

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.

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

Generate identifier @fbag_join.

Returns: Identifier @fbag_join.

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

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

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.

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

Generate identifier in.

Returns: Identifier in.

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

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.

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

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

Generate identifier *.

Returns: Identifier *.

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

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.

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

Recogniser for function @add_.

Parameters:

e A data expression.

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

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

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

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

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.

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

Recogniser for function Bag2Set.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @bagcomp.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @bagfbag.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @Bool2Nat_.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @bag.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function count.

Parameters:

e A data expression.

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

bool mcrl2::data::sort_bag::is_difference_application(const atermpp::aterm_appl &e)¶

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.

bool mcrl2::data::sort_bag::is_difference_function_symbol(const atermpp::aterm_appl &e)¶

Recogniser for function -.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @fbag2fset.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @fbag_diff.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @fbag_inter.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @fbag_join.

Parameters:

e A data expression.

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

bool mcrl2::data::sort_bag::is_in_application(const atermpp::aterm_appl &e)¶

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.

bool mcrl2::data::sort_bag::is_in_function_symbol(const atermpp::aterm_appl &e)¶

Recogniser for function in.

Parameters:

e A data expression.

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

bool mcrl2::data::sort_bag::is_intersection_application(const atermpp::aterm_appl &e)¶

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.

bool mcrl2::data::sort_bag::is_intersection_function_symbol(const atermpp::aterm_appl &e)¶

Recogniser for function *.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @min_.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @monus_.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @Nat2Bool_.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @one_.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function Set2Bag.

Parameters:

e A data expression.

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

bool mcrl2::data::sort_bag::is_union_application(const atermpp::aterm_appl &e)¶

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.

bool mcrl2::data::sort_bag::is_union_function_symbol(const atermpp::aterm_appl &e)¶

Recogniser for function +.

Parameters:

e A data expression.

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

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

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.

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

Recogniser for function @zero_.

Parameters:

e A data expression.

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

const data_expression &mcrl2::data::sort_bag::left(const data_expression &e)¶

Function for projecting out argument. left from an application.

Parameters:

e A data expression.

Pre: left is defined for e.

Returns: The argument of e that corresponds to left.

void mcrl2::data::sort_bag::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_.

Parameters:

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

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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)¶

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.

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)¶

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.

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)¶

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.

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

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.

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

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.

void mcrl2::data::sort_bag::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_.

Parameters:

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

void mcrl2::data::sort_bag::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_.

Parameters:

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

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

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.

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

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.

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

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.

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

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.

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

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.

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

Constructor for function symbol @min_.

Parameters:

s A sort expression.

Returns: Function symbol min_function.

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

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.

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

Generate identifier @min_.

Returns: Identifier @min_.

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

Constructor for function symbol @monus_.

Parameters:

s A sort expression.

Returns: Function symbol monus_function.

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

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.

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

Generate identifier @monus_.

Returns: Identifier @monus_.

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

Constructor for function symbol @Nat2Bool_.

Parameters:

s A sort expression.

Returns: Function symbol nat2bool_function.

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

Application of function symbol @Nat2Bool_.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @Nat2Bool_.

Returns: Identifier @Nat2Bool_.

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

Constructor for function symbol @one_.

Parameters:

s A sort expression.

Returns: Function symbol one_function.

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

Application of function symbol @one_.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @one_.

Returns: Identifier @one_.

const data_expression &mcrl2::data::sort_bag::right(const data_expression &e)¶

Function for projecting out argument. right from an application.

Parameters:

e A data expression.

Pre: right is defined for e.

Returns: The argument of e that corresponds to right.

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

Constructor for function symbol Set2Bag.

Parameters:

s A sort expression.

Returns: Function symbol set2bag.

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

Application of function symbol Set2Bag.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of Set2Bag to a number of arguments.

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

Generate identifier Set2Bag.

Returns: Identifier Set2Bag.

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

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.

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

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

Generate identifier +.

Returns: Identifier +.

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

Constructor for function symbol @zero_.

Parameters:

s A sort expression.

Returns: Function symbol zero_function.

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

Application of function symbol @zero_.

Parameters:

s A sort expression.
arg0 A data expression.

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

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

Generate identifier @zero_.

Returns: Identifier @zero_.

mcrl2/data/bag.h¶

Typedefs¶

Functions¶

Table of Contents

Previous topic

Next topic

This page