From 098ff900b9a267aea178ea7f907567260e6da496 Mon Sep 17 00:00:00 2001
From: giopaglia <24519853+giopaglia@users.noreply.github.com>
Date: Fri, 5 Jul 2024 13:02:53 +0200
Subject: [PATCH] Add normalize case and bump version

---
 Project.toml        |  2 +-
 src/syntax-utils.jl | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/Project.toml b/Project.toml
index 95784391..c9134dac 100644
--- a/Project.toml
+++ b/Project.toml
@@ -1,7 +1,7 @@
 name = "SoleLogics"
 uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5"
 authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Edoardo PONSANESI", "Alberto PAPARELLA", "Eduard I. STAN"]
-version = "0.9.2"
+version = "0.9.3"
 
 [deps]
 AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"
diff --git a/src/syntax-utils.jl b/src/syntax-utils.jl
index df521a30..cafaa974 100644
--- a/src/syntax-utils.jl
+++ b/src/syntax-utils.jl
@@ -789,6 +789,22 @@ See also
 [`SyntaxTree`](@ref)), [`Formula`](@ref).
 """
 normalize(f::Formula, args...; kwargs...) = normalize(tree(f), args...; kwargs...)
+function normalize(
+    t::LLF;
+    kwargs...
+) where {LLF<:Union{LeftmostConjunctiveForm,LeftmostDisjunctiveForm}}
+    ch = children(t)
+    unique!(ch)
+    ch = normalize.(ch; kwargs...)
+    unique!(ch)
+    if connective(t) == (∧)
+        filter!(c->c != ⊤, ch)
+    elseif connective(t) == (∨)
+        filter!(c->c != ⊥, ch)
+    end
+    return LLF(ch)
+end
+
 function normalize(
     t::SyntaxTree;
     profile = :readability,