diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala index 3bc617538a08b2e5555898ac48ba9e68113d5398..7b6eda220c7b1141ddb8435289cecf9f3e6c7161 100644 --- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala +++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala @@ -460,6 +460,7 @@ object Parser { }, { case ConnectorFormula(c @ (Iff | Implies), Seq(left, right)) => Seq(left ~ Some(c ~ right)) + case ConnectorFormula((And | Or), Seq(f)) => Seq(f ~ None) case f => Seq(f ~ None) } ) diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala index 221f69e70940a381b4346a3700f9cb32e8cfc442..e7c2da63f0d76e90144530547ad3ae85bdbfff0e 100644 --- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala +++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala @@ -98,6 +98,15 @@ class PrinterTest extends AnyFunSuite with TestUtils { assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c") } + test("and/or of 1 argument") { + assert(Parser.printFormula(ConnectorFormula(And, Seq(a))) == "a") + assert(Parser.printFormula(ConnectorFormula(Or, Seq(a))) == "a") + + assert(Parser.printFormula(ConnectorFormula(Implies, Seq(ConnectorFormula(Or, Seq(a)), ConnectorFormula(And, Seq(a))))) == "(a) ⇒ (a)") + assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, a))) == "a ⇒ a") + assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(Or, Seq(a)))) == "∀'x. a") + } + 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")