mcrl2/data/optimized_boolean_operators.h

Include file:

#include "mcrl2/data/optimized_boolean_operators.h"

add your file description here.

Functions

Term mcrl2::data::optimized_and(const Term &p, const Term &q)

Make a conjunction.

Parameters:

  • p A term

  • q A term

Returns: The application of and to the arguments.

Term mcrl2::data::optimized_exists(const VariableSequence &l, const Term &p, bool remove_variables = false)

Make an existential quantification.

Parameters:

  • l A sequence of variables

  • p A term

  • remove_variables If true, unused quantifier variables are removed

Returns: The application of existential quantification to the arguments.

Term mcrl2::data::optimized_exists_no_empty_domain(const VariableSequence &l, const Term &p, bool remove_variables = false)

Make an existential quantification.

Parameters:

  • l A sequence of variables

  • p A term

  • remove_variables If true, unused quantifier variables are removed

Returns: The application of existential quantification to the arguments. The optimization exists x:empty_set. phi = false is not applied.

Term mcrl2::data::optimized_forall(const VariableSequence &l, const Term &p, bool remove_variables = false)

Make a universal quantification.

Parameters:

  • l A sequence of variables

  • p A term

  • remove_variables If true, unused quantifier variables are removed

Returns: The application of universal quantification to the arguments.

Term mcrl2::data::optimized_forall_no_empty_domain(const VariableSequence &l, const Term &p, bool remove_variables = false)

Make a universal quantification.

Parameters:

  • l A sequence of variables

  • p A term

  • remove_variables If true, unused quantifier variables are removed

Returns: The application of universal quantification to the arguments. The optimization forall x:empty_set. phi = true is not applied.

Term mcrl2::data::optimized_imp(const Term &p, const Term &q)

Make an implication.

Parameters:

  • p A term

  • q A term

Returns: The application of implication to the arguments.

Term mcrl2::data::optimized_not(const Term &arg)

Make a negation.

Parameters:

  • arg A term

Returns: The application of not to the argument.

Term mcrl2::data::optimized_or(const Term &p, const Term &q)

Make a disjunction.

Parameters:

  • p A term

  • q A term

Returns: The application of or to the arguments.

Functions

TermTraits::term_type mcrl2::data::detail::optimized_and(const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)

Make a conjunction.

Parameters:

  • left A term

  • right A term

Returns: The value left && right

T1 mcrl2::data::detail::optimized_and(T1 left, T1 right, BinaryFunction and_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make a conjunction.

Parameters:

  • left A term

  • right A term

  • and_ The operation and

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The value left && right

TermTraits::term_type mcrl2::data::detail::optimized_exists(const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)

Make an existential quantification.

Parameters:

  • v A sequence of variables

  • arg A term

  • remove_variables If true, remove bound variables that do not occur in arg.

  • empty_domain_allowed If true, and there are no variables in v, treat as empty domain, hence yielding false, otherwise arg arg is returned in this case.

Returns: The existential quantification exists v.arg

T1 mcrl2::data::detail::optimized_exists(VariableSequence v, T1 arg, Exists exists, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make an existential quantification.

Parameters:

  • v A sequence of variables

  • arg A term

  • exists The existential quantification operator

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The existential quantification exists v.arg

TermTraits::term_type mcrl2::data::detail::optimized_forall(const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)

Make a universal quantification.

Parameters:

  • v A sequence of variables

  • arg A term

  • remove_variables If true, remove bound variables that do not occur in arg.

  • empty_domain_allowed If true, and there are no variables in v, treat as empty domain, hence yielding true, otherwise arg arg is returned in this case.

Returns: The universal quantification forall v.arg

T1 mcrl2::data::detail::optimized_forall(VariableSequence v, T1 arg, Forall forall, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make a universal quantification.

Parameters:

  • v A sequence of variables

  • arg A term

  • forall The universal quantification operator

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The universal quantification forall v.arg

TermTraits::term_type mcrl2::data::detail::optimized_imp(const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)

Make an implication.

Parameters:

  • left A term

  • right A term

Returns: The value left => right

T1 mcrl2::data::detail::optimized_imp(T1 left, T1 right, BinaryFunction imp, UnaryFunction not_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make an implication.

Parameters:

  • left A term

  • right A term

  • imp The implication operator

  • not_ The operation not

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The value left => right

TermTraits::term_type mcrl2::data::detail::optimized_not(const typename TermTraits::term_type &arg, TermTraits)

Returns: The value !arg

T1 mcrl2::data::detail::optimized_not(T1 arg, UnaryFunction not_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make a negation.

Parameters:

  • arg A term

  • not_ The operation not

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The value !arg

TermTraits::term_type mcrl2::data::detail::optimized_or(const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)

Make a disjunction.

Parameters:

  • left A term

  • right A term

Returns: The value left || right

T1 mcrl2::data::detail::optimized_or(T1 left, T1 right, BinaryFunction or_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)

Make a disjunction.

Parameters:

  • left A term

  • right A term

  • or_ The operation or

  • true_ The value true

  • is_true Function that tests for the value true

  • false_ The value false

  • is_false Function that tests for the value false

Returns: The value left || right