Support n-ary biconditionals

For convenience, support biconditionals with more than one argument.
An n-ary “if and only if” statement

    F_1 <-> F_2 <-> ... <-> F_n

is to be interpreted as

    F_1 <-> F_2 and F2 <-> F3 and ... and F_(n - 1) <-> F_n
This commit is contained in:
Patrick Lühne 2020-04-13 21:59:25 +02:00
parent 855fd9abcf
commit 7566fdaa29
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 16 additions and 24 deletions

View File

@ -282,24 +282,6 @@ impl ForAll
}
}
pub struct IfAndOnlyIf
{
pub left: Box<Formula>,
pub right: Box<Formula>,
}
impl IfAndOnlyIf
{
pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
{
Self
{
left,
right,
}
}
}
pub struct Implies
{
pub direction: ImplicationDirection,
@ -469,7 +451,7 @@ pub enum Formula
Compare(Compare),
Exists(Exists),
ForAll(ForAll),
IfAndOnlyIf(IfAndOnlyIf),
IfAndOnlyIf(Formulas),
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
@ -531,9 +513,9 @@ impl Formula
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
}
pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
pub fn if_and_only_if(arguments: Formulas) -> Self
{
Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
Self::IfAndOnlyIf(arguments)
}
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,

View File

@ -160,9 +160,19 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
direction: crate::ImplicationDirection::RightToLeft, antecedent, implication})
=> write!(format, "{:?} <- {:?}", display_formula(implication, precedence),
display_formula(antecedent, precedence))?,
crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
display_formula(right, precedence))?,
crate::Formula::IfAndOnlyIf(arguments) =>
{
let mut separator = "";
assert!(!arguments.is_empty());
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
separator = " <-> "
}
},
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
=> write!(format, "{:?} < {:?}", display_term(left, None),