mcrl2/data/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.

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

core::identifier_string const &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

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

core::identifier_string const &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

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

Generate identifier @bagcomp.

Returns: Identifier @bagcomp

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

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

Generate identifier @bagfbag.

Returns: Identifier @bagfbag

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

core::identifier_string const &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

core::identifier_string const &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

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

Generate identifier count.

Returns: Identifier count

function_symbol mcrl2::data::sort_bag::difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier -.

Returns: Identifier -

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

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

Generate identifier in.

Returns: Identifier in

function_symbol mcrl2::data::sort_bag::intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
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

core::identifier_string const &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_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

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

core::identifier_string const &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

core::identifier_string const &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

core::identifier_string const &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

core::identifier_string const &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

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

Generate identifier Set2Bag.

Returns: Identifier Set2Bag

function_symbol mcrl2::data::sort_bag::union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
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

core::identifier_string const &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

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

Generate identifier @zero_.

Returns: Identifier @zero_