Include file:
#include "mcrl2/data/optimized_boolean_operators.h"
add your file description here.
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.
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.
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.
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.
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.
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.
mcrl2::data::
optimized_not
(const Term &arg)¶Make a negation.
Parameters:
arg A term
Returns: The application of not to the argument.
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.
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
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
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
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
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
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
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
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
mcrl2::data::detail::
optimized_not
(const typename TermTraits::term_type &arg, TermTraits)¶Returns: The value !arg
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
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
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