From 7566fdaa29f6d5dfb2b26252141db27f3f7f0ab2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 13 Apr 2020 21:59:25 +0200
Subject: [PATCH] Support n-ary biconditionals
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
---
 src/ast.rs             | 24 +++---------------------
 src/format/formulas.rs | 16 +++++++++++++---
 2 files changed, 16 insertions(+), 24 deletions(-)

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<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>,
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),