From 7b5c18f7e3c9f9601d70c2e3d575885ccb63ca29 Mon Sep 17 00:00:00 2001
From: Michele21 <ghiottimichele12@gmail.com>
Date: Thu, 17 Aug 2023 20:52:32 +0200
Subject: [PATCH] fixing evaluation functions, adding dispatch to already
 existing function as npropositions, check and creating new function
 conjunctiveformulas

---
 src/logisets/multilogiset.jl | 55 ++++++++++++++++++++++++++++++++++++
 src/models/base.jl           |  2 +-
 src/models/evaluation.jl     |  8 ++++--
 3 files changed, 61 insertions(+), 4 deletions(-)

diff --git a/src/logisets/multilogiset.jl b/src/logisets/multilogiset.jl
index 4ff824f..6c4c378 100644
--- a/src/logisets/multilogiset.jl
+++ b/src/logisets/multilogiset.jl
@@ -280,6 +280,28 @@ function SoleLogics.normalize(φ::MultiFormula{F}; kwargs...) where {F<:Abstract
     MultiFormula(Dict{Int,F}([i_modality => SoleLogics.normalize(f; kwargs...) for (i_modality,f) in pairs(modforms(φ))]))
 end
 
+function conjunctiveformulas(children::NTuple{N,MultiFormula}) where {N}
+    @assert N > 0 "Nothing in tuple passed, there must be at least one element"
+
+    if N == 1
+        return first(children)
+    end
+
+    return joinformulas(∧,(children[1],conjunctiveformulas(children[2:end])))
+end
+
+npropositions(φ::LeftmostConjunctiveForm{<:MultiFormula}) = npropositions(children(φ))
+npropositions(φ::MultiFormula{<:SyntaxTree}) = npropositions((φ,))
+function npropositions(children::NTuple{N,MultiFormula}) where {N}
+    i_modalities = unique(vcat(collect.(keys.([modforms(ch) for ch in children]))...))
+
+    return sum([begin
+        chs = filter(ch->haskey(modforms(ch), i_modality), children)
+        fs = map(ch->modforms(ch)[i_modality], chs)
+        npropositions.(fs)
+    end for i_modality in i_modalities])
+end
+
 function check(
     φ::MultiFormula,
     X::MultiLogiset,
@@ -292,6 +314,39 @@ function check(
         for (i_modality, f) in modforms(φ)])
 end
 
+function check(
+    φ::MultiFormula,
+    d::AbstractInterpretationSet{M},
+    args...;
+    kwargs...,
+)::Vector{truthtype(M)} where {M<:AbstractInterpretation}
+    X = MultiLogiset(d)
+    map(i_instance->check(
+        φ,
+        X,
+        i_instance,
+        args...;
+        kwargs...
+    ), 1:ninstances(d))
+end
+
 # # TODO join MultiFormula leads to a SyntaxTree with MultiFormula children
 # function joinformulas(op::AbstractOperator, children::NTuple{N,MultiFormula{F}}) where {N,F}
 # end
+
+function check(
+    φ::LeftmostConjunctiveForm{<:MultiFormula},
+    X::AbstractInterpretationSet{<:AbstractKripkeStructure},
+    i_instance::Integer,
+    args...;
+    kwargs...
+)
+    λ = conjunctiveformulas((children(φ)...,))
+    check(λ, MultiLogiset(X), i_instance, args...; kwargs...)
+end
+
+function npropositions(
+    φ::LeftmostConjunctiveForm{<:MultiFormula},
+)
+
+end
diff --git a/src/models/base.jl b/src/models/base.jl
index 44e7bb5..e73ef52 100644
--- a/src/models/base.jl
+++ b/src/models/base.jl
@@ -2,7 +2,7 @@ import Base: convert, length, getindex, isopen
 
 using SoleData: slicedataset
 
-import SoleLogics: check, syntaxstring
+import SoleLogics: check, syntaxstring, conjuncts, nconjuncts, disjuncts, ndisjuncts
 using SoleLogics: LeftmostLinearForm, LeftmostConjunctiveForm, LeftmostDisjunctiveForm
 using SoleModels: TopFormula
 
diff --git a/src/models/evaluation.jl b/src/models/evaluation.jl
index abf0a2e..efd845d 100644
--- a/src/models/evaluation.jl
+++ b/src/models/evaluation.jl
@@ -70,7 +70,8 @@ See also
 function evaluaterule(
     rule::Rule{O,A,FM},
     X::AbstractInterpretationSet,
-    Y::AbstractVector{<:Label}
+    Y::AbstractVector{<:Label};
+    kwargs...,
 ) where {O,A,FM<:AbstractModel}
     ys = apply(rule,X)
 
@@ -143,9 +144,10 @@ See also
 function rulemetrics(
     rule::Rule{O,A,FM},
     X::AbstractInterpretationSet,
-    Y::AbstractVector{<:Label}
+    Y::AbstractVector{<:Label};
+    kwargs...,
 ) where {O,A,FM<:AbstractModel}
-    eval_result = evaluaterule(rule, X, Y)
+    eval_result = evaluaterule(rule, X, Y; kwargs...)
     ys = eval_result[:ys]
     antsat = eval_result[:antsat]
     n_instances = ninstances(X)