mcrl2/data/join.h

Include file:

#include "mcrl2/data/join.h"

Join and split functions for data expressions.

Functions

data_expression mcrl2::data::join_and(FwdIt first, FwdIt last)

Returns and applied to the sequence of data expressions [first, last)

Parameters:

• first Start of a sequence of data expressions
• last End of a sequence of of data expressions

Returns: And applied to the sequence of data expressions [first, last)

data_expression mcrl2::data::join_or(FwdIt first, FwdIt last)

Returns or applied to the sequence of data expressions [first, last)

Parameters:

• first Start of a sequence of data expressions
• last End of a sequence of of data expressions

Returns: Or applied to the sequence of data expressions [first, last)

std::set<data_expression> mcrl2::data::split_and(const data_expression &expr)

Splits a conjunction into a sequence of operands Given a data expression of the form p1 && p2 && …. && pn, this will yield a set of the form { p1, p2, …, pn }, assuming that pi does not have a && as main function symbol.

Parameters:

• expr A data expression

Returns: A sequence of operands

std::set<data_expression> mcrl2::data::split_or(const data_expression &expr)

Splits a disjunction into a sequence of operands Given a data expression of the form p1 || p2 || …. || pn, this will yield a set of the form { p1, p2, …, pn }, assuming that pi does not have a || as main function symbol.

Parameters:

• expr A data expression

Returns: A sequence of operands