diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala index 4d4da90005991913da0ff058bc9b071c21799788..43a890488577af624189560563435246e1c7f377 100644 --- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala +++ b/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) } ) diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala index f1757835bbd8da9faa33278e0fa41d8aa59d8edd..e09e288d4d66618b684e9d023943d0b607d3f337 100644 --- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala +++ b/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")