# mcrl2/pbes/join.h¶

Include file:

#include "mcrl2/pbes/join.h"


## Functions¶

pbes_expression mcrl2::pbes_system::join_and(FwdIt first, FwdIt last)

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

Parameters:

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

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

pbes_expression mcrl2::pbes_system::join_or(FwdIt first, FwdIt last)

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

Parameters:

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

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

pbes_expression mcrl2::pbes_system::optimized_join_and(FwdIt first, FwdIt last)

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

Parameters:

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

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

pbes_expression mcrl2::pbes_system::optimized_join_or(FwdIt first, FwdIt last)

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

Parameters:

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

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

std::set<pbes_expression> mcrl2::pbes_system::split_and(const pbes_expression &expr, bool split_data_expressions = false)

Splits a conjunction into a sequence of operands Given a pbes 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 PBES expression
• split_data_expressions if true, both data and pbes conjunctions are split, otherwise only pbes conjunctions are split.

Returns: A sequence of operands

std::set<pbes_expression> mcrl2::pbes_system::split_or(const pbes_expression &expr, bool split_data_expressions = false)

Splits a disjunction into a sequence of operands Given a pbes 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 PBES expression
• split_data_expressions if true, both data and pbes disjunctions are split, otherwise only pbes disjunctions are split.

Returns: A sequence of operands