Support printing 'and' and 'or' ConnectorFormulas with more than two arguments

lisa-utils/src/main/scala/lisa/utils/Parser.scala

@@ -328,8 +328,15 @@ object Parser {
       or is LeftAssociative
     )(
       (l, conn, r) => ConnectorFormula(conn, Seq(l, r)),
-      { case ConnectorFormula(conn, Seq(l, r)) =>
-        (l, conn, r)
+      {
+        case ConnectorFormula(conn, Seq(l, r)) =>
+          (l, conn, r)
+        case ConnectorFormula(conn, l +: rest) if rest.nonEmpty =>
+          val last = rest.last
+          val leftSide = rest.dropRight(1)
+          // parser only knows about connector formulas of two arguments, so we unfold the formula of many arguments to
+          // multiple nested formulas of two arguments
+          (leftSide.foldLeft(l)((f1, f2) => ConnectorFormula(conn, Seq(f1, f2))), conn, last)
       }
     )
 

lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala

@@ -98,6 +98,16 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c")
   }
 
+  test("connectors of >2 arguments") {
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b, c))) == "a ∧ b ∧ c")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b, c))) == "a ∨ b ∨ c")
+
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b, c, a))) == "a ∧ b ∧ c ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b, c, b))) == "a ∨ b ∨ c ∨ b")
+
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, b, c)), ConnectorFormula(And, Seq(c, b, a))))) == "a ∧ b ∧ c ∨ c ∧ b ∧ a")
+  }
+
   test("connector priority") {
     // a ∨ (b ∧ c)
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∨ b ∧ c")