diff --git a/src/ast.rs b/src/ast.rs index 3c60ed2..08c9cd2 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -282,24 +282,6 @@ impl ForAll } } -pub struct IfAndOnlyIf -{ - pub left: Box, - pub right: Box, -} - -impl IfAndOnlyIf -{ - pub fn new(left: Box, right: Box) -> 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), Or(Formulas), @@ -531,9 +513,9 @@ impl Formula Self::compare(ComparisonOperator::GreaterOrEqual, left, right) } - pub fn if_and_only_if(left: Box, right: Box) -> 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, diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 27b644a..d3c0f8f 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -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),