Merge branch 'main' into dev-v0.9.1

Project.toml

@@ -32,9 +32,18 @@ UniqueVectors = "2fbcfb34-fd0c-5fbb-b5d7-e826d8f5b0a9"
 
 [compat]
 BenchmarkTools = "1"
-SoleLogics = "0.3.0"
-SoleData = "0.9.0"
+DataStructures = "0.18"
+FillArrays = "1"
+FunctionWrappers = "1"
 julia = "1"
+ProgressMeter = "1"
+Reexport = "1"
+Revise = "3"
+SoleBase = "0.9.2"
+SoleData = "0.9.0"
+SoleLogics = "0.3.0"
+StatsBase = "0.34"
+Suppressor = "0.2"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

src/conditional-data/active-featured-dataset.jl

@@ -0,0 +1,137 @@
+# Active datasets comprehend structures for representing relation sets, features, enumerating worlds,
+#  etc. While learning a model can be done only with active modal datasets, testing a model
+#  can be done with both active and passive modal datasets.
+#
+abstract type AbstractActiveFeaturedDataset{
+    V<:Number,
+    W<:AbstractWorld,
+    FR<:AbstractFrame{W,Bool},
+    FT<:AbstractFeature{V}
+} <: AbstractActiveConditionalDataset{W,AbstractCondition,Bool,FR} end
+
+featvaltype(::Type{<:AbstractActiveFeaturedDataset{V}}) where {V} = V
+featvaltype(d::AbstractActiveFeaturedDataset) = featvaltype(typeof(d))
+
+featuretype(::Type{<:AbstractActiveFeaturedDataset{V,W,FR,FT}}) where {V,W,FR,FT} = FT
+featuretype(d::AbstractActiveFeaturedDataset) = featuretype(typeof(d))
+
+function grouped_featsaggrsnops(X::AbstractActiveFeaturedDataset)
+    return error("Please, provide method grouped_featsaggrsnops(::$(typeof(X))).")
+end
+
+function features(X::AbstractActiveFeaturedDataset)
+    return error("Please, provide method features(::$(typeof(X))).")
+end
+
+function grouped_metaconditions(X::AbstractActiveFeaturedDataset)
+    grouped_featsnops = grouped_featsaggrsnops2grouped_featsnops(grouped_featsaggrsnops(X))
+    [begin
+        (feat,[FeatMetaCondition(feat,op) for op in ops])
+    end for (feat,ops) in zip(features(X),grouped_featsnops)]
+end
+
+function alphabet(X::AbstractActiveFeaturedDataset)
+    conds = vcat([begin
+        thresholds = unique([
+                X[i_instance, w, feature]
+                for i_instance in 1:ninstances(X)
+                    for w in allworlds(X, i_instance)
+            ])
+        [(mc, thresholds) for mc in metaconditions]
+    end for (feature, metaconditions) in grouped_metaconditions(X)]...)
+    C = FeatCondition{featvaltype(X),FeatMetaCondition{featuretype(X)}}
+    BoundedExplicitConditionalAlphabet{C}(collect(conds))
+end
+
+
+# Base.length(X::AbstractActiveFeaturedDataset) = ninstances(X)
+# Base.iterate(X::AbstractActiveFeaturedDataset, state=1) = state > ninstances(X) ? nothing : (get_instance(X, state), state+1)
+
+function find_feature_id(X::AbstractActiveFeaturedDataset, feature::AbstractFeature)
+    id = findfirst(x->(Base.isequal(x, feature)), features(X))
+    if isnothing(id)
+        error("Could not find feature $(feature) in AbstractActiveFeaturedDataset of type $(typeof(X)).")
+    end
+    id
+end
+function find_relation_id(X::AbstractActiveFeaturedDataset, relation::AbstractRelation)
+    id = findfirst(x->x==relation, relations(X))
+    if isnothing(id)
+        error("Could not find relation $(relation) in AbstractActiveFeaturedDataset of type $(typeof(X)).")
+    end
+    id
+end
+
+
+# By default an active modal dataset cannot be minified
+isminifiable(::AbstractActiveFeaturedDataset) = false
+
+# Convenience functions
+function grouped_featsnops2grouped_featsaggrsnops(
+    grouped_featsnops::AbstractVector{<:AbstractVector{<:TestOperator}}
+)::AbstractVector{<:AbstractDict{<:Aggregator,<:AbstractVector{<:TestOperator}}}
+    grouped_featsaggrsnops = Dict{<:Aggregator,<:AbstractVector{<:TestOperator}}[]
+    for (i_feature, test_operators) in enumerate(grouped_featsnops)
+        aggrsnops = Dict{Aggregator,AbstractVector{<:TestOperator}}()
+        for test_operator in test_operators
+            aggregator = existential_aggregator(test_operator)
+            if (!haskey(aggrsnops, aggregator))
+                aggrsnops[aggregator] = TestOperator[]
+            end
+            push!(aggrsnops[aggregator], test_operator)
+        end
+        push!(grouped_featsaggrsnops, aggrsnops)
+    end
+    grouped_featsaggrsnops
+end
+
+function grouped_featsaggrsnops2grouped_featsnops(
+    grouped_featsaggrsnops::AbstractVector{<:AbstractDict{<:Aggregator,<:AbstractVector{<:TestOperator}}}
+)::AbstractVector{<:AbstractVector{<:TestOperator}}
+    grouped_featsnops = [begin
+        vcat(values(grouped_featsaggrsnops)...)
+    end for grouped_featsaggrsnops in grouped_featsaggrsnops]
+    grouped_featsnops
+end
+
+function features_grouped_featsaggrsnops2featsnaggrs_grouped_featsnaggrs(features, grouped_featsaggrsnops)
+    featsnaggrs = Tuple{<:AbstractFeature,<:Aggregator}[]
+    grouped_featsnaggrs = AbstractVector{Tuple{<:Integer,<:Aggregator}}[]
+    i_featsnaggr = 1
+    for (feat,aggrsnops) in zip(features, grouped_featsaggrsnops)
+        aggrs = []
+        for aggr in keys(aggrsnops)
+            push!(featsnaggrs, (feat,aggr))
+            push!(aggrs, (i_featsnaggr,aggr))
+            i_featsnaggr += 1
+        end
+        push!(grouped_featsnaggrs, aggrs)
+    end
+    featsnaggrs, grouped_featsnaggrs
+end
+
+function features_grouped_featsaggrsnops2featsnaggrs(features, grouped_featsaggrsnops)
+    featsnaggrs = Tuple{<:AbstractFeature,<:Aggregator}[]
+    i_featsnaggr = 1
+    for (feat,aggrsnops) in zip(features, grouped_featsaggrsnops)
+        for aggr in keys(aggrsnops)
+            push!(featsnaggrs, (feat,aggr))
+            i_featsnaggr += 1
+        end
+    end
+    featsnaggrs
+end
+
+function features_grouped_featsaggrsnops2grouped_featsnaggrs(features, grouped_featsaggrsnops)
+    grouped_featsnaggrs = AbstractVector{Tuple{<:Integer,<:Aggregator}}[]
+    i_featsnaggr = 1
+    for (feat,aggrsnops) in zip(features, grouped_featsaggrsnops)
+        aggrs = []
+        for aggr in keys(aggrsnops)
+            push!(aggrs, (i_featsnaggr,aggr))
+            i_featsnaggr += 1
+        end
+        push!(grouped_featsnaggrs, aggrs)
+    end
+    grouped_featsnaggrs
+end

src/conditional-data/main.jl

@@ -0,0 +1,70 @@
+using SoleLogics: OneWorld, Interval, Interval2D
+using SoleLogics: Full0DFrame, Full1DFrame, Full2DFrame
+using SoleLogics: X, Y, Z
+using SoleLogics: AbstractWorld, IdentityRel
+import SoleLogics: syntaxstring
+import SoleLogics: frame
+
+import SoleData: nvariables
+import SoleData: ninstances
+import SoleData: nmodalities, hasnans, instances
+# import SoleData: frame # TODO
+
+# Minification interface for lossless data compression
+include("minify.jl")
+
+# Scalar features to be computed on worlds of dataset instances
+include("features.jl")
+
+export inverse_test_operator, dual_test_operator,
+        apply_test_operator,
+        TestOperator
+
+# Test operators to be used for comparing features and threshold values
+include("test-operators.jl")
+
+# Scalar conditions on the features, to be wrapped in Proposition's
+include("conditions.jl")
+
+# Alphabets of conditions on the features, to be used in logical datasets
+include("conditional-alphabets.jl")
+
+export MixedFeature, CanonicalFeature, canonical_geq, canonical_leq
+
+export canonical_geq_95, canonical_geq_90, canonical_geq_85, canonical_geq_80, canonical_geq_75, canonical_geq_70, canonical_geq_60,
+       canonical_leq_95, canonical_leq_90, canonical_leq_85, canonical_leq_80, canonical_leq_75, canonical_leq_70, canonical_leq_60
+
+# Types for representing common associations between features and operators
+include("canonical-conditions.jl") # TODO fix
+
+const MixedFeature = Union{AbstractFeature,CanonicalFeature,Function,Tuple{TestOperator,Function},Tuple{TestOperator,AbstractFeature}}
+
+# Representative accessibles, for optimized model checking
+include("representatives.jl")
+
+# Datasets where the instances are Kripke models with conditional alphabets
+include("conditional-datasets.jl")
+
+include("active-featured-dataset.jl")
+
+export nmodalities, modalities, frame,
+        display_structure,
+        MultiFrameConditionalDataset,
+        worldtypes
+
+# #
+# # TODO figure out which convert function works best:
+# convert(::Type{<:MultiFrameConditionalDataset{T}}, X::MD) where {T,MD<:AbstractConditionalDataset{T}} = MultiFrameConditionalDataset{MD}([X])
+# convert(::Type{<:MultiFrameConditionalDataset}, X::AbstractConditionalDataset) = MultiFrameConditionalDataset([X])
+
+# Multi-frame version of conditional datasets, for representing multimodal datasets
+include("multi-frame-conditional-datasets.jl") # TODO define interface
+
+const ActiveMultiFrameConditionalDataset{T} = MultiFrameConditionalDataset{<:AbstractActiveFeaturedDataset{<:T}}
+
+# TODO decide how to name this.
+getframe = frame
+
+# include("featured-datasets.jl") TODO?
+
+include("random.jl")

src/conditional-data/multi-frame-conditional-datasets.jl

@@ -0,0 +1,94 @@
+"""
+    struct MultiFrameConditionalDataset{MD<:AbstractConditionalDataset}
+        modalities  :: Vector{<:MD}
+    end
+
+A multi-frame conditional dataset. This structure is useful for representing
+multimodal datasets in logical terms.
+
+See also
+[`AbstractConditionalDataset`](@ref),
+[`minify`](@ref).
+"""
+struct MultiFrameConditionalDataset{MD<:AbstractConditionalDataset}
+
+    modalities  :: Vector{<:MD}
+
+    function MultiFrameConditionalDataset{MD}(X::MultiFrameConditionalDataset{MD}) where {MD<:AbstractConditionalDataset}
+        MultiFrameConditionalDataset{MD}(X.modalities)
+    end
+    function MultiFrameConditionalDataset{MD}(Xs::AbstractVector) where {MD<:AbstractConditionalDataset}
+        Xs = collect(Xs)
+        @assert length(Xs) > 0 && length(unique(ninstances.(Xs))) == 1 "Can't create an empty MultiFrameConditionalDataset or with mismatching number of samples (nmodalities: $(length(Xs)), frame_sizes: $(ninstances.(Xs)))."
+        new{MD}(Xs)
+    end
+    function MultiFrameConditionalDataset{MD}() where {MD<:AbstractConditionalDataset}
+        new{MD}(MD[])
+    end
+    function MultiFrameConditionalDataset{MD}(X::MD) where {MD<:AbstractConditionalDataset}
+        MultiFrameConditionalDataset{MD}(MD[X])
+    end
+    function MultiFrameConditionalDataset(Xs::AbstractVector{<:MD}) where {MD<:AbstractConditionalDataset}
+        MultiFrameConditionalDataset{MD}(Xs)
+    end
+    function MultiFrameConditionalDataset(X::MD) where {MD<:AbstractConditionalDataset}
+        MultiFrameConditionalDataset{MD}(X)
+    end
+end
+
+modalities(X::MultiFrameConditionalDataset) = X.modalities
+
+Base.iterate(X::MultiFrameConditionalDataset, state=1)                     = state > length(X) ? nothing : (get_instance(X, state), state+1)
+Base.length(X::MultiFrameConditionalDataset)                               = ninstances(X)
+Base.push!(X::MultiFrameConditionalDataset, f::AbstractConditionalDataset) = push!(modalities(X), f)
+
+Base.size(X::MultiFrameConditionalDataset)                                 = map(size, modalities(X))
+
+frame(X::MultiFrameConditionalDataset, i_frame::Integer)                   = nmodalities(X) > 0 ? modalities(X)[i_frame] : error("MultiFrameConditionalDataset has no frame!")
+nmodalities(X::MultiFrameConditionalDataset)                                   = length(modalities(X))
+ninstances(X::MultiFrameConditionalDataset)                                  = ninstances(frame(X, 1))
+
+# max_channel_size(X::MultiFrameConditionalDataset) = map(max_channel_size, modalities(X)) # TODO: figure if this is useless or not. Note: channel_size doesn't make sense at this point.
+nfeatures(X::MultiFrameConditionalDataset) = map(nfeatures, modalities(X)) # Note: used for safety checks in fit_tree.jl
+# nrelations(X::MultiFrameConditionalDataset) = map(nrelations, modalities(X)) # TODO: figure if this is useless or not
+nfeatures(X::MultiFrameConditionalDataset,  i_frame::Integer) = nfeatures(frame(X, i_frame))
+nrelations(X::MultiFrameConditionalDataset, i_frame::Integer) = nrelations(frame(X, i_frame))
+worldtype(X::MultiFrameConditionalDataset,  i_frame::Integer) = worldtype(frame(X, i_frame))
+worldtypes(X::MultiFrameConditionalDataset) = Vector{Type{<:AbstractWorld}}(worldtype.(modalities(X)))
+
+get_instance(X::MultiFrameConditionalDataset,  i_frame::Integer, idx_i::Integer, args...)  = get_instance(frame(X, i_frame), idx_i, args...)
+# get_instance(X::MultiFrameConditionalDataset, idx_i::Integer, args...)  = get_instance(frame(X, i), idx_i, args...) # TODO should slice across the modalities!
+
+instances(X::MultiFrameConditionalDataset{MD}, inds::AbstractVector{<:Integer}, return_view::Union{Val{true},Val{false}} = Val(false)) where {MD<:AbstractConditionalDataset} =
+    MultiFrameConditionalDataset{MD}(Vector{MD}(map(frame->instances(frame, inds, return_view), modalities(X))))
+
+function display_structure(Xs::MultiFrameConditionalDataset; indent_str = "")
+    out = "$(typeof(Xs))" # * "\t\t\t$(Base.summarysize(Xs) / 1024 / 1024 |> x->round(x, digits=2)) MBs"
+    for (i_frame, X) in enumerate(modalities(Xs))
+        if i_frame == nmodalities(Xs)
+            out *= "\n$(indent_str)└ "
+        else
+            out *= "\n$(indent_str)├ "
+        end
+        out *= "[$(i_frame)] "
+        # \t\t\t$(Base.summarysize(X) / 1024 / 1024 |> x->round(x, digits=2)) MBs\t(worldtype: $(worldtype(X)))"
+        out *= display_structure(X; indent_str = indent_str * (i_frame == nmodalities(Xs) ? "   " : "│  ")) * "\n"
+    end
+    out
+end
+
+hasnans(Xs::MultiFrameConditionalDataset) = any(hasnans.(modalities(Xs)))
+
+isminifiable(::MultiFrameConditionalDataset) = true
+
+function minify(Xs::MultiFrameConditionalDataset)
+    if !any(map(isminifiable, modalities(Xs)))
+        if !all(map(isminifiable, modalities(Xs)))
+            @error "Cannot perform minification with modalities of types $(typeof.(modalities(Xs))). Please use a minifiable format (e.g., SupportedFeaturedDataset)."
+        else
+            @warn "Cannot perform minification on some of the modalities provided. Please use a minifiable format (e.g., SupportedFeaturedDataset) ($(typeof.(modalities(Xs))) were used instead)."
+        end
+    end
+    Xs, backmap = zip([!isminifiable(X) ? minify(X) : (X, identity) for X in modalities(Xs)]...)
+    Xs, backmap
+end