SoleModels

Documentation for SoleModels.

Logical foundations

SoleLogics lays the logical foundations for this package. While the full reference for SoleLogics can be found here, these are the basic logical concepts needed for symbolic modelling.

SoleLogics.Atom — Type
struct Atom{V} <: SyntaxLeaf
    value::V
end

An atom, sometimes called an atomic proposition, propositional letter (or simply letter), of type Atom{V} wraps a value::V representing a fact which truth can be assessed on a logical interpretation.

Atoms are nullary tokens (i.e, they are at the leaves of a syntax tree); note that their atoms cannot be Atoms.

See also AbstractInterpretation, atoms, check, SyntaxToken.

SoleLogics.Formula — Type
abstract type Formula <: Syntactical end

Abstract type for logical formulas. Examples of Formulas are SyntaxLeafs (for example, Atoms and Truth values), AbstractSyntaxStructures (for example, SyntaxTrees and LeftmostLinearForms) and TruthTables ( enriched representation, which associates a syntactic structure with additional memoization structures, which can save computational time upon model checking).

Any formula can be converted into its SyntaxTree representation via tree; its height can be computed, and it can be queried for its syntax tokens, atoms, etc... It can be parsed from its syntaxstring representation via parseformula.

See also tree, AbstractSyntaxStructure, SyntaxLeaf.

SoleLogics.syntaxstring — Function
syntaxstring(s::Syntactical; kwargs...)::String

Return the string representation of any syntactic object (e.g., Formula, SyntaxTree, SyntaxToken, Atom, Truth, etc). Note that this representation may introduce redundant parentheses. kwargs can be used to specify how to display syntax tokens/trees under some specific conditions.

The following kwargs are currently supported:

  • function_notation = false::Bool: when set to true, it forces the use of function notation for binary operators (see here).
  • remove_redundant_parentheses = true::Bool: when set to false, it prints a syntaxstring where each syntactical element is wrapped in parentheses.
  • parenthesize_atoms = !remove_redundant_parentheses::Bool: when set to true, it forces the atoms (which are the leaves of a formula's tree structure) to be wrapped in parentheses.

Examples

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"))
"p ∧ q ∧ r ∧ s ∧ t"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), function_notation=true)
"∧(∧(∧(∧(p, q), r), s), t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=false)
"((((p) ∧ (q)) ∧ (r)) ∧ (s)) ∧ (t)"

julia> syntaxstring(parseformula("p∧q∧r∧s∧t"), remove_redundant_parentheses=true, parenthesize_atoms=true)
"(p) ∧ (q) ∧ (r) ∧ (s) ∧ (t)"

julia> syntaxstring(parseformula("◊((p∧s)→q)"))
"◊((p ∧ s) → q)"

julia> syntaxstring(parseformula("◊((p∧s)→q)"); function_notation = true)
"◊(→(∧(p, s), q))"

See also parseformula, SyntaxBranch, SyntaxToken.

Implementation

In the case of a syntax tree, syntaxstring is a recursive function that calls itself on the syntax children of each node. For a correct functioning, the syntaxstring must be defined (including kwargs...) for every newly defined SyntaxToken (e.g., SyntaxLeafs, that is, Atoms and Truth values, and Operators), in a way that it produces a unique string representation, since Base.hash and Base.isequal, at least for SyntaxBranchs, rely on it.

In particular, for the case of Atoms, the function calls itself on the wrapped value:

syntaxstring(a::Atom; kwargs...) = syntaxstring(value(a); kwargs...)

The syntaxstring for any value defaults to its string representation, but it can be defined by defining the appropriate syntaxstring method.

Warning

The syntaxstring for syntax tokens (e.g., atoms, operators) should not be prefixed/suffixed by whitespaces, as this may cause ambiguities upon parsing. For similar reasons, syntaxstrings should not contain parentheses ('(', ')'), and, when parsing in function notation, commas (',').

See also SyntaxLeaf, Operator, parseformula.

SoleLogics.AbstractAlphabet — Type
abstract type AbstractAlphabet{V} end

Abstract type for representing an alphabet of atoms with values of type V. An alphabet (or propositional alphabet) is a set of atoms (assumed to be countable).

Examples

julia> Atom(1) in ExplicitAlphabet(Atom.(1:10))
true

julia> Atom(1) in ExplicitAlphabet(1:10)
true

julia> Atom(1) in AlphabetOfAny{String}()
false

julia> Atom("mystring") in AlphabetOfAny{String}()
true

julia> "mystring" in AlphabetOfAny{String}()
┌ Warning: Please, use Base.in(Atom(mystring), alphabet::AlphabetOfAny{String}) instead of Base.in(mystring, alphabet::AlphabetOfAny{String})
└ @ SoleLogics ...
true

Implementation

When implementing a new alphabet type MyAlphabet, you should provide a method for establishing whether an atom belongs to it or not; while, in general, this method should be:

function Base.in(p::Atom, a::MyAlphabet)::Bool

in the case of finite alphabets, it suffices to define a method:

function atoms(a::AbstractAlphabet)::AbstractVector{atomstype(a)}

By default, an alphabet is considered finite:

Base.isfinite(::Type{<:AbstractAlphabet}) = true
Base.isfinite(a::AbstractAlphabet) = Base.isfinite(typeof(a))
Base.in(p::Atom, a::AbstractAlphabet) = Base.isfinite(a) ? Base.in(p, atoms(a)) : error(...)

See also AbstractGrammar, AlphabetOfAny, Atom, ExplicitAlphabet.

SoleLogics.AbstractInterpretationSet — Type
abstract type AbstractInterpretationSet{M<:AbstractInterpretation} <: AbstractDataset end

Abstract type for ordered sets of interpretations. A set of interpretations, also referred to as a dataset in this context, is a collection of instances, each of which is an interpretation, and is identified by an index iinstance::Integer. These structures are especially useful when performing [model checking](https://en.wikipedia.org/wiki/Modelchecking).

See alsotruthtype, InterpretationVector.

SoleLogics.check — Function
check(
    φ::Formula,
    i::AbstractInterpretation,
    args...;
    kwargs...
)::Bool

Check a formula on a logical interpretation (or model), returning true if the truth value for the formula istop. This process is referred to as (finite) model checking, and there are many algorithms for it, typically depending on the complexity of the logic.

Examples

julia> @atoms String p q
2-element Vector{Atom{String}}:
 Atom{String}("p")
 Atom{String}("q")

julia> td = TruthDict([p => TOP, q => BOT])
TruthDict with values:
┌────────┬────────┐
│      q │      p │
│ String │ String │
├────────┼────────┤
│      ⊥ │      ⊤ │
└────────┴────────┘

julia> check(CONJUNCTION(p,q), td)
false

See also interpret, Formula, AbstractInterpretation, TruthDict.

function check(
    φ::SyntaxTree,
    i::AbstractKripkeStructure,
    w::Union{Nothing,<:AbstractWorld} = nothing;
    use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing,
    perform_normalization::Bool = true,
    memo_max_height::Union{Nothing,Int} = nothing,
)::Bool

Check a formula on a specific word in a KripkeStructure.

Examples

julia> using Graphs, Random

julia> @atoms String p q
2-element Vector{Atom{String}}:
 Atom{String}("p")
 Atom{String}("q")

julia> fmodal = randformula(Random.MersenneTwister(14), 3, [p,q], SoleLogics.BASE_MODAL_OPERATORS)
¬□(p ∨ q)

# A special graph, called Kripke Frame, is created.
# Nodes are called worlds, and the edges are relations between worlds.
julia> worlds = SoleLogics.World.(1:5) # 5 worlds are created, numerated from 1 to 5

julia> edges = Edge.([ (1, 2), (1, 3), (2, 4), (3, 4), (3, 5)])

julia> kframe = SoleLogics.ExplicitCrispUniModalFrame(worlds, Graphs.SimpleDiGraph(edges))

# A valuation function establishes which fact are true on each world
julia> valuation = Dict([
    worlds[1] => TruthDict([p => true, q => false]),
    worlds[2] => TruthDict([p => true, q => true]),
    worlds[3] => TruthDict([p => true, q => false]),
    worlds[4] => TruthDict([p => false, q => false]),
    worlds[5] => TruthDict([p => false, q => true]),
 ])

# Kripke Frame and valuation function are merged in a Kripke Structure
julia> kstruct = KripkeStructure(kframe, valuation)

julia> [w => check(fmodal, kstruct, w) for w in worlds]
5-element Vector{Pair{SoleLogics.World{Int64}, Bool}}:
 SoleLogics.World{Int64}(1) => 0
 SoleLogics.World{Int64}(2) => 1
 SoleLogics.World{Int64}(3) => 1
 SoleLogics.World{Int64}(4) => 0
 SoleLogics.World{Int64}(5) => 0

See also SyntaxTree, AbstractWorld, KripkeStructure.

check(
    φ::Formula,
    s::AbstractInterpretationSet,
    i_instance::Integer,
    args...;
    kwargs...
)::Bool

Check a formula on the $i$-th instance of an AbstractInterpretationSet.

See also AbstractInterpretationSet, Formula.

check(
    φ::Formula,
    s::AbstractInterpretationSet,
    args...;
    kwargs...
)::Vector{Bool}

Check a formula on all instances of an AbstractInterpretationSet.

See also AbstractInterpretationSet, Formula.

SoleLogics.AbstractWorld — Type
abstract type AbstractWorld end

Abstract type for the nodes of an annotated accessibility graph (Kripke structure). This is used, for example, in modal logic, where the truth of formulas is relativized to worlds, that is, nodes of a graph.

Implementing

When implementing a new world type, the logical semantics should be defined via accessibles methods; refer to the help for accessibles.

See also AbstractKripkeStructure, AbstractFrame.

SoleLogics.Interval — Type
struct Interval{T} <: GeometricalWorld
    x :: T
    y :: T
end

An interval in a 1-dimensional space, with coordinates of type T.

Examples

julia> SoleLogics.goeswithdim(SoleLogics.Interval(1,2),1)
true

julia> SoleLogics.goeswithdim(SoleLogics.Interval(1,2),2)
false

julia> collect(accessibles(SoleLogics.FullDimensionalFrame(5), Interval(1,2), SoleLogics.IA_L))
6-element Vector{Interval{Int64}}:
 (3−4)
 (3−5)
 (4−5)
 (3−6)
 (4−6)
 (5−6)

See also goeswithdim, accessibles, FullDimensionalFrame, Point, Interval2D, GeometricalWorld, AbstractWorld.

SoleLogics.Interval2D — Type
struct Interval2D{T} <: GeometricalWorld
    x :: Interval{T}
    y :: Interval{T}
end

A orthogonal rectangle in a 2-dimensional space, with coordinates of type T. This is the 2-dimensional Interval counterpart, that is, the combination of two orthogonal Intervals.

Examples

julia> SoleLogics.goeswithdim(SoleLogics.Interval2D((1,2),(3,4)),1)
false

julia> SoleLogics.goeswithdim(SoleLogics.Interval2D((1,2),(3,4)),2)
true

julia> collect(accessibles(SoleLogics.FullDimensionalFrame(5,5), Interval2D((2,3),(2,4)), SoleLogics.IA_LL))
3-element Vector{Interval2D{Int64}}:
 ((4−5)×(5−6))
 ((4−6)×(5−6))
 ((5−6)×(5−6))

See also goeswithdim, accessibles, FullDimensionalFrame, Point, Interval, GeometricalWorld, AbstractWorld.

SoleLogics.AbstractRelation — Type
abstract type AbstractRelation end

Abstract type for the relations of a multi-modal annotated accessibility graph (Kripke structure). Two noteworthy relations are identityrel and globalrel, which access the current world and all worlds, respectively.

Examples

julia> fr = SoleLogics.FullDimensionalFrame((10,),);

julia> Interval(8,11) in (accessibles(fr, Interval(2,5), IA_L))
true

Implementation

When implementing a new relation type R, please provide the methods:

arity(::R)::Int = ...
syntaxstring(::R; kwargs...)::String = ...

If the relation is symmetric, please specify its converse relation cr with:

hasconverse(::R) = true
converse(::R) = cr

If the relation is many-to-one or one-to-one, please flag it with:

istoone(::R) = true

If the relation is reflexive or transitive, flag it with:

isreflexive(::R) = true
istransitive(::R) = true

Most importantly, the logical semantics for R should be defined via accessibles methods; refer to the help for accessibles.

See also issymmetric, isreflexive, istransitive, isgrounding, arity, syntaxstring, converse, hasconverse, istoone, identityrel, globalrel, accessibles, AbstractKripkeStructure, AbstractFrame, AbstractWorld.

SoleLogics.globalrel — Constant
struct GlobalRel <: AbstractRelation end;
const globalrel  = GlobalRel();

Singleton type for the global relation. This is a binary relation via which a world accesses every other world within the frame. The relation is also symmetric, reflexive and transitive.

Examples

julia> syntaxstring(SoleLogics.globalrel)
"G"

julia> SoleLogics.converse(globalrel)
GlobalRel()

See also identityrel, AbstractRelation, AbstractWorld, AbstractFrame. AbstractKripkeStructure,

SoleLogics.accessibles — Function
accessibles(fr::AbstractUniModalFrame{W}, w::W)::Worlds{W} where {W<:AbstractWorld}

Return the worlds in frame fr that are accessible from world w.

See also AbstractWorld, AbstractUniModalFrame.

accessibles(
    fr::AbstractMultiModalFrame{W},
    w::W,
    r::AbstractRelation
) where {W<:AbstractWorld}

Return the worlds in frame fr that are accessible from world w via relation r.

Examples

julia> fr = SoleLogics.FullDimensionalFrame((10,),);

julia> typeof(accessibles(fr, Interval(2,5), IA_L))
Base.Generator{...}

julia> typeof(accessibles(fr, globalrel))
Base.Generator{...}

julia> @assert SoleLogics.nworlds(fr) == length(collect(accessibles(fr, globalrel)))

julia> typeof(accessibles(fr, Interval(2,5), identityrel))
Vector{Interval{Int64}}

julia> Interval(8,11) in collect(accessibles(fr, Interval(2,5), IA_L))
true

Implementation

Since accessibles always returns an iterator of worlds of the same type W, the current implementation of accessibles for multi-modal frames delegates the enumeration to a lower level _accessibles function, which returns an iterator of parameter tuples that are, then, fed to the world constructor the using IterTools generators, as in:

function accessibles(
    fr::AbstractMultiModalFrame{W},
    w::W,
    r::AbstractRelation,
) where {W<:AbstractWorld}
    IterTools.imap(W, _accessibles(fr, w, r))
end

As such, when defining new frames, worlds, and/or relations, one should provide new methods for _accessibles. For example:

_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1)

This pattern is generally convenient; it can, however, be bypassed, although this requires defining two additional methods in order to resolve dispatch ambiguities. When defining a new frame type FR{W}, one can resolve the ambiguities and define a custom accessibles method by providing these three methods:

# access worlds through relation `r`
function accessibles(
    fr::FR{W},
    w::W,
    r::AbstractRelation,
) where {W<:AbstractWorld}
    ...
end

# access current world
function accessibles(
    fr::FR{W},
    w::W,
    r::IdentityRel,
) where {W<:AbstractWorld}
    [w]
end

# access all worlds
function accessibles(
    fr::FR{W},
    w::W,
    r::GlobalRel,
) where {W<:AbstractWorld}
    allworlds(fr)
end

In general, it should be true that collect(accessibles(fr, w, r)) isa AbstractWorlds{W}.

See also AbstractWorld, AbstractRelation, AbstractMultiModalFrame.

SoleModels.CLabel — Type
const CLabel  = Union{String,Integer,CategoricalValue}
const RLabel  = AbstractFloat
const Label   = Union{CLabel,RLabel}

Types for supervised machine learning labels (classification and regression).

SoleModels.Label — Type
const CLabel  = Union{String,Integer,CategoricalValue}
const RLabel  = AbstractFloat
const Label   = Union{CLabel,RLabel}

Types for supervised machine learning labels (classification and regression).

SoleModels.AbstractLogiset — Type
abstract type AbstractLogiset{
    W<:AbstractWorld,
    U,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractInterpretationSet{AbstractKripkeStructure} end

Abstract type for logisets, that is, logical datasets for symbolic learning where each instance is a Kripke structure associating feature values to each world. Conditions (see AbstractCondition), and logical formulas with conditional letters can be checked on worlds of instances of the dataset.

See also AbstractCondition, AbstractFeature, SoleLogics.AbstractKripkeStructure, SoleLogics.AbstractInterpretationSet.

SoleModels.Aggregator — Type
const Aggregator = Function

A test operator is a binary Julia Function used for comparing a feature value and a threshold. In a crisp (i.e., boolean, non-fuzzy) setting, the test operator returns a Boolean value, and <, >, ≥, ≤, !=, and == are typically used.

See also ScalarCondition, ScalarOneStepMemoset, TestOperator.

SoleModels.Branch — Type
struct Branch{
    O,
    A<:Formula,
    FM<:AbstractModel
} <: ConstrainedModel{O,FM}
    antecedent::A
    posconsequent::FM
    negconsequent::FM
    info::NamedTuple
end

A Branch is one of the fundamental building blocks of symbolic modeling, and has the semantics:

IF (antecedent) THEN (positive consequent) ELSE (negative consequent) END

where the antecedent is a formula to be checked and the consequents are the feasible local outcomes of the block. If checking the antecedent evaluates to the top of the algebra, then the positive consequent is applied; otherwise, the negative consequenti is applied.

Note that FM refers to the Feasible Models (FM) allowed in the model's sub-tree.

See also antecedent, posconsequent, negconsequent, SoleLogics.check, SoleLogics.Formula, Rule, ConstrainedModel, AbstractModel.

SoleModels.ConstantModel — Type
struct ConstantModel{O} <: LeafModel{O}
    outcome::O
    info::NamedTuple
end

The simplest type of model is the ConstantModel; it is a LeafModel that always outputs the same outcome.

Examples

julia> SoleModels.LeafModel(2) isa SoleModels.ConstantModel

julia> SoleModels.LeafModel(sum) isa SoleModels.FunctionModel
┌ Warning: Over efficiency concerns, please consider wrappingJulia Function's into FunctionWrapper{O,Tuple{SoleModels.AbstractInterpretation}} structures,where O is their return type.
└ @ SoleModels ~/.julia/dev/SoleModels/src/models/base.jl:337
true

See also apply, FunctionModel, LeafModel.

SoleModels.ConstrainedModel — Type

An AbstractModel can wrap another AbstractModel, and use it to compute the outcome. As such, an AbstractModel can actually be the result of a composition of many models, and enclose a tree of AbstractModels (with LeafModels at the leaves). In order to typebound the Feasible Models (FM) allowed in the sub-tree, the ConstrainedModel type is introduced:

abstract type ConstrainedModel{O,FM<:AbstractModel} <: AbstractModel{O} end

For example, ConstrainedModel{String,Union{Branch{String},ConstantModel{String}}} supertypes models that with String outcomes that make use of Branch{String} and ConstantModel{String} (essentially, a decision trees with Strings at the leaves).

See also LeafModel, AbstractModel.

SoleModels.DecisionList — Type
struct DecisionList{
    O,
    A<:Formula,
    FM<:AbstractModel
} <: ConstrainedModel{O,FM}
    rulebase::Vector{Rule{_O,_C,_FM} where {_O<:O,_C<:A,_FM<:FM}}
    defaultconsequent::FM
    info::NamedTuple
end

A DecisionList (or decision table, or rule-based model) is a symbolic model that has the semantics of an IF-ELSEIF-ELSE block:

IF (antecedent_1)     THEN (consequent_1)
ELSEIF (antecedent_2) THEN (consequent_2)
...
ELSEIF (antecedent_n) THEN (consequent_n)
ELSE (consequent_default) END

where the antecedents are formulas to be, and the consequents are the feasible local outcomes of the block. Using the classical semantics, the antecedents are evaluated in order, and a consequent is returned as soon as a valid antecedent is found, or when the computation reaches the ELSE clause.

Note that FM refers to the Feasible Models (FM) allowed in the model's sub-tree.

See also Rule, ConstrainedModel, DecisionTree, AbstractModel.

SoleModels.DecisionTree — Type

A DecisionTree is a symbolic model that operates as a nested structure of IF-THEN-ELSE blocks:

IF (antecedent_1) THEN
    IF (antecedent_2) THEN
        (consequent_1)
    ELSE
        (consequent_2)
    END
ELSE
    IF (antecedent_3) THEN
        (consequent_3)
    ELSE
        (consequent_4)
    END
END

where the antecedents are formulas to be, and the consequents are the feasible local outcomes of the block.

In practice, a DecisionTree simply wraps a constrained sub-tree of Branch and LeafModel:

struct DecisionTree{
O,
    A<:Formula,
    FFM<:LeafModel
} <: ConstrainedModel{O,Union{<:Branch{<:O,<:A},<:FFM}}
    root::M where {M<:Union{FFM,Branch}}
    info::NamedTuple
end

Note that FM refers to the Feasible Models (FM) allowed in the model's sub-tree. Also note that this structure also includes an info::NamedTuple for storing additional information.

See also ConstrainedModel, MixedSymbolicModel, DecisionList.

SoleModels.ExplicitBooleanLogiset — Type
struct ExplicitBooleanLogiset{
    W<:AbstractWorld,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractLogiset{W,Bool,FT,FR}

    d :: Vector{Tuple{Dict{W,Vector{FT}},FR}}

end

A logiset where the features are boolean, and where each instance associates to each world the set of features with true.

See also AbstractLogiset.

SoleModels.ExplicitLogiset — Type
struct ExplicitLogiset{
    W<:AbstractWorld,
    U,
    FT<:AbstractFeature,
    FR<:AbstractFrame{W},
} <: AbstractLogiset{W,U,FT,FR}

    d :: Vector{Tuple{Dict{W,Dict{FT,U}},FR}}

end

A logiset where the features are boolean, and where each instance associates to each world the set of features with true.

See also AbstractLogiset.

SoleModels.Feature — Type
struct Feature{A} <: AbstractFeature
    atom::A
end

A feature solely identified by an atom (e.g., a string with its name, a tuple of strings, etc.)

See also AbstractFeature.

SoleModels.FullMemoset — Type

A generic, full memoization structure that works for any crisp logic; For each instance of a dataset, this structure associates formulas to the set of worlds where the formula holds; it was introduced by Emerson-Clarke for the well-known model checking algorithm for CTL*.

See also SupportedLogiset, AbstractMemoset, AbstractLogiset.

SoleModels.FunctionModel — Type
struct FunctionModel{O} <: LeafModel{O}
    f::FunctionWrapper{O}
    info::NamedTuple
end

A FunctionModel is a LeafModel that applies a native Julia Function in order to compute the outcome. Over efficiency concerns, it is mandatory to make explicit the output type O by wrapping the Function into an object of type FunctionWrapper{O} (see FunctionWrappers.

See also ConstantModel, LeafModel.

SoleModels.FunctionalCondition — Type
struct FunctionalCondition{FT<:AbstractFeature} <: AbstractCondition{FT}
    feature::FT
    f::FT
end

A condition which yields a truth value equal to the value of a function.

See also AbstractFeature.

SoleModels.LeafModel — Type
abstract type LeafModel{O} <: AbstractModel{O} end

Abstract type for leaf models, that is, models which outcomes do not depend other models, and represents the bottom of the computation. In general, an AbstractModel can generally wrap other AbstractModels; in such case, the outcome can depend on the inner models being applied on the instance object. Otherwise, the model is considered as a leaf, or final, and is the leaf of a tree of AbstractModels.

See also ConstantModel, FunctionModel, AbstractModel.

SoleModels.MixedSymbolicModel — Type

A MixedSymbolicModel is a symbolic model that operaters as a free nested structure of IF-THEN-ELSE and IF-ELSEIF-ELSE blocks:

IF (antecedent_1) THEN
    IF (antecedent_1)     THEN (consequent_1)
    ELSEIF (antecedent_2) THEN (consequent_2)
    ELSE (consequent_1_default) END
ELSE
    IF (antecedent_3) THEN
        (consequent_3)
    ELSE
        (consequent_4)
    END
END

where the antecedents are formulas to be checked, and the consequents are the feasible local outcomes of the block.

In Sole.jl, this logic can implemented using ConstrainedModels such as Rules, Branchs, DecisionLists, DecisionTrees, and the be wrapped into a MixedSymbolicModel:

struct MixedSymbolicModel{O,FM<:AbstractModel} <: ConstrainedModel{O,FM}
    root::M where {M<:Union{LeafModel{<:O},ConstrainedModel{<:O,<:FM}}}
    info::NamedTuple
end

Note that FM refers to the Feasible Models (FM) allowed in the model's sub-tree.

See also ConstrainedModel, DecisionTree, DecisionList.

SoleModels.MultiFormula — Type
struct MultiFormula{F<:Formula} <: AbstractSyntaxStructure
    modforms::Dict{Int,F}
end

A symbolic antecedent that can be checked on a MultiLogiset, associating antecedents to modalities.

SoleModels.MultivariateFeature — Type
struct MultivariateFeature <: VarFeature
    f::Function
end

A dimensional feature represented by the application of a function to a dimensional channel. For example, it can wrap a scalar function computing how much a Interval2D world, when interpreted on an image, resembles a horse. Note that the image has a number of spatial variables (3, for the case of RGB), and "resembling a horse" may require a computation involving all variables.

See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VarFeature, AbstractFeature.

SoleModels.RLabel — Type
const CLabel  = Union{String,Integer,CategoricalValue}
const RLabel  = AbstractFloat
const Label   = Union{CLabel,RLabel}

Types for supervised machine learning labels (classification and regression).

SoleModels.Rule — Type
struct Rule{
    O,
    A<:Formula,
    FM<:AbstractModel
} <: ConstrainedModel{O,FM}
    antecedent::A
    consequent::FM
    info::NamedTuple
end

A Rule is one of the fundamental building blocks of symbolic modeling, and has the semantics:

IF (antecedent) THEN (consequent) END

where the antecedent is a formula to be checked, and the consequent is the local outcome of the block.

Note that FM refers to the Feasible Models (FM) allowed in the model's sub-tree.

See also antecedent, consequent, SoleLogics.Formula, ConstrainedModel, AbstractModel.

SoleModels.ScalarCondition — Type
struct ScalarCondition{U,FT,M<:ScalarMetaCondition{FT}} <: AbstractCondition{FT}
    metacond::M
    a::U
end

A scalar condition comparing a computed feature value (see ScalarMetaCondition) and a threshold value a. It can be evaluated on a world of an instance of a logical dataset.

For example: $min[V1] ≥ 10$, which translates to "Within this world, the minimum of variable 1 is greater or equal than 10." In this case, the feature a UnivariateMin object.

See also AbstractCondition, ScalarMetaCondition.

SoleModels.ScalarMetaCondition — Type
struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractCondition{FT}
    feature::FT
    test_operator::O
end

A metacondition representing a scalar comparison method. Here, the feature is a scalar function that can be computed on a world of an instance of a logical dataset. A test operator is a binary mathematical relation, comparing the computed feature value and an external threshold value (see ScalarCondition). A metacondition can also be used for representing the infinite set of conditions that arise with a free threshold (see UnboundedScalarConditions): ${min[V1] ≥ a, a ∈ ℝ}$.

See also AbstractCondition, ScalarCondition.

SoleModels.ScalarOneStepMemoset — Type

One-step memoization structures for optimized check of formulas of type ⟨R⟩p, where p wraps a scalar condition, such as MyFeature ≥ 10. With such formulas, scalar one-step optimization can be performed.

For example, checking ⟨R⟩(MyFeature ≥ 10) on a world w of a Kripke structure involves comparing the maximum MyFeature across w's accessible worlds with 10; but the same maximum value can be reused to check sibling formulas such as ⟨R⟩(MyFeature ≥ 100). This sparks the idea of storing and reusing scalar aggregations (e.g., minimum/maximum) over the feature values. Each value refers to a specific world, and an object of type ⟨R⟩(f ⋈ ?), called a "scalar metacondition".

Similar cases arise depending on the relation and the test operator (or, better, its aggregator), and further optimizations can be applied for specific feature types (see representatives).

An immediate special case, however, arises when R is the global relation G since, in such case, a single aggregate value is enough for all worlds within the Kripke structure. Therefore, we differentiate between generic, relational memosets (see AbstractScalarOneStepRelationalMemoset), and global memosets (see AbstractScalarOneStepGlobalMemoset), which are usually much smaller.

Given a logiset X, a ScalarOneStepMemoset covers a set of relations and metaconditions, and it holds both a relational and a global memoset. It can be instantiated via:

ScalarOneStepMemoset(
    X                       :: AbstractLogiset{W,U},
    metaconditions          :: AbstractVector{<:ScalarMetaCondition},
    relations               :: AbstractVector{<:AbstractRelation};
    precompute_globmemoset  :: Bool = true,
    precompute_relmemoset   :: Bool = false,
    print_progress          :: Bool = false,
)

If precompute_relmemoset is false, then the relational memoset is simply initialized as an empty structure, and memoization is performed on it upon checking formulas. precompute_globmemoset works similarly.

See SupportedLogiset, ScalarMetaCondition, AbstractOneStepMemoset.

SoleModels.TestOperator — Type
const TestOperator = Function

A test operator is a binary Julia Function used for comparing a feature value and a threshold. In a crisp (i.e., boolean, non-fuzzy) setting, the test operator returns a Boolean value, and <, >, ≥, ≤, !=, and == are typically used.

See also Aggregator, ScalarCondition.

SoleModels.UnboundedScalarConditions — Type
struct UnboundedScalarConditions{C<:ScalarCondition} <: AbstractConditionalAlphabet{C}
    metaconditions::Vector{<:ScalarMetaCondition}
end

An infinite alphabet of conditions induced from a finite set of metaconditions. For example, if metaconditions = [ScalarMetaCondition(UnivariateMin(1), ≥)], the alphabet represents the (infinite) set: ${min[V1] ≥ a, a ∈ ℝ}$.

See also BoundedScalarConditions, ScalarCondition, ScalarMetaCondition.

SoleModels.ValueCondition — Type
struct ValueCondition{FT<:AbstractFeature} <: AbstractCondition{FT}
    feature::FT
end

A condition which yields a truth value equal to the value of a feature.

See also AbstractFeature.

SoleModels.VarFeature — Type
abstract type VarFeature <: AbstractFeature end

Abstract type for feature functions that can be computed on (multi)variate data. Instances of multivariate datasets have values for a number of variables, which can be used to define logical features.

For example, with dimensional data (e.g., multivariate time series, digital images and videos), features can be computed as the minimum value for a given variable on a specific interval/rectangle/cuboid (in general, a `SoleLogics.GeometricalWorld).

As an example of a dimensional feature, consider min[V1], which computes the minimum for variable 1 for a given world. ScalarConditions such as min[V1] >= 10 can be, then, evaluated on worlds.

See also scalarlogiset, featvaltype, computefeature, SoleLogics.Interval.

Base.isopen — Method
isopen(::AbstractModel)::Bool

Return whether a model is open. An AbstractModel{O} is closed if it is always able to provide an outcome of type O. Otherwise, the model can output nothing values and is referred to as open.

Rule is an example of an open model, while Branch is an example of closed model.

See also AbstractModel.

Base.rand — Method
Base.rand(
    rng::AbstractRNG,
    a::BoundedScalarConditions;
    metaconditions::Union{Nothing,ScalarMetaCondition,AbstractVector{<:ScalarMetaCondition}} = nothing,
    feature::Union{Nothing,AbstractFeature,AbstractVector{<:AbstractFeature}} = nothing,
    test_operator::Union{Nothing,TestOperator,AbstractVector{<:TestOperator}} = nothing,
)::Atom

Randomly sample an Atom holding a ScalarCondition from conditional alphabet a, such that:

  • if metaconditions are specified, then the set of metaconditions (feature-operator pairs)

is limited to metaconditions;

  • if feature is specified, then the set of metaconditions (feature-operator pairs)

is limited to those with feature;

  • if test_operator is specified, then the set of metaconditions (feature-operator pairs)

is limited to those with test_operator.

See also BoundedScalarConditions, ScalarCondition, ScalarMetaCondition, SoleLogics.AbstractAlphabet.

SoleModels.apply — Method
apply(
    m::AbstractModel,
    i::AbstractInterpretation;
    check_args::Tuple = (),
    check_kwargs::NamedTuple = (;),
    functional_args::Tuple = (),
    functional_kwargs::NamedTuple = (;),
    kwargs...
)::outputtype(m)

apply(
    m::AbstractModel,
    d::AbstractInterpretationSet;
    check_args::Tuple = (),
    check_kwargs::NamedTuple = (;),
    functional_args::Tuple = (),
    functional_kwargs::NamedTuple = (;),
    kwargs...
)::AbstractVector{<:outputtype(m)}

Return the output prediction of the model on an instance, or on each instance of a dataset. The predictions can be nothing if the model is open.

check_args and check_kwargs can influence check's behavior at the time of its computation (see `SoleLogics.check)

functional_args and functional_kwargs can influence FunctionModel's behavior when the corresponding function is applied to AbstractInterpretation (see FunctionModel, `SoleLogics.AbstractInterpretation)

See also isopen, outcometype, outputtype, AbstractModel, SoleLogics.AbstractInterpretation, SoleLogics.AbstractInterpretationSet.

SoleModels.apply_test_operator — Method

Apply a test operator by simply passing the feature value and threshold to the (binary) test operator function.

SoleModels.balanced_weights — Method
default_weights(Y::AbstractVector{L}) where {L<:CLabel}::AbstractVector{<:Number}

Return a class-rebalancing weight vector, given a label vector Y.

SoleModels.bestguess — Function
bestguess(
    labels::AbstractVector{<:Label},
    weights::Union{Nothing,AbstractVector} = nothing;
    suppress_parity_warning = false,
)

Return the best guess for a set of labels; that is, the label that best approximates the labels provided. For classification labels, this function returns the majority class; for regression labels, the average value. If no labels are provided, nothing is returned. The computation can be weighted.

See also CLabel, RLabel, Label.

SoleModels.checkantecedent — Function
checkantecedent(
    m::Union{Rule,Branch},
    args...;
    kwargs...
)
    check(antecedent(m), args...; kwargs...)
end

Simply check the antecedent of a rule on an instance or dataset.

See also antecedent, Rule, Branch.

SoleModels.computefeature — Method
computefeature(f::VarFeature, featchannel; kwargs...)

Compute a feature on a featchannel (i.e., world reading) of an instance.

See also VarFeature.

SoleModels.default_weights — Method
default_weights(n::Integer)::AbstractVector{<:Number}

Return a default weight vector of n values.

SoleModels.displaymodel — Method
printmodel(io::IO, m::AbstractModel; kwargs...)
displaymodel(m::AbstractModel; kwargs...)

prints or returns a string representation of model m.

Arguments

  • header::Bool = true: when set to true, a header is printed, displaying

the info structure for m;

  • show_subtree_info::Bool = false: when set to true, the header is printed for

models in the sub-tree of m;

  • show_metrics::Bool = false: when set to true, performance metrics at each point of the

subtree are shown, whenever they are available in the info structure;

  • max_depth::Union{Nothing,Int} = nothing: when it is an Int, models in the sub-tree

with a depth higher than max_depth are ellipsed with "...";

  • syntaxstring_kwargs::NamedTuple = (;): kwargs to be passed to syntaxstring for

formatting logical formulas.

See also syntaxstring, AbstractModel.

SoleModels.evaluaterule — Method
evaluaterule(
    r::Rule{O},
    X::AbstractInterpretationSet,
    Y::AbstractVector{L}
) where {O,L<:Label}

Evaluate the rule on a labelled dataset, and return a NamedTuple consisting of:

  • antsat::Vector{Bool}: satsfaction of the antecedent for each instance in the dataset;
  • ys::Vector{Union{Nothing,O}}: rule prediction. For each instance in X:
    • consequent(rule) if the antecedent is satisfied,
    • nothing otherwise.

See also Rule, SoleLogics.AbstractInterpretationSet, Label, checkantecedent.

SoleModels.feasiblemodelstype — Method
feasiblemodelstype(m::AbstractModel)

Return a Union of the Feasible Models (FM) allowed in the sub-tree of any AbstractModel. Note that for a ConstrainedModel{O,FM<:AbstractModel}, it simply returns FM.

See also ConstrainedModel.

SoleModels.featvaltype — Method
featvaltype(dataset, f::VarFeature)

Return the type of the values returned by feature f on logiseed dataset.

See also VarFeature.

SoleModels.immediatesubmodels — Method
immediatesubmodels(m::AbstractModel)

Return the list of immediate child models. Note: if the model is a leaf model, then the returned list will be empty.

Examples

julia> using SoleLogics

julia> branch = Branch(SoleLogics.parseformula("p∧q∨r"), "YES", "NO");

julia> immediatesubmodels(branch)
2-element Vector{SoleModels.ConstantModel{String}}:
 SoleModels.ConstantModel{String}
YES

 SoleModels.ConstantModel{String}
NO

julia> branch2 = Branch(SoleLogics.parseformula("s→p"), branch, 42);


julia> printmodel.(immediatesubmodels(branch2));
Branch
┐ p ∧ (q ∨ r)
├ ✔ YES
└ ✘ NO

ConstantModel
42

See also submodels, LeafModel, AbstractModel.

SoleModels.info — Method
info(m::AbstractModel)::NamedTuple = m.info
info(m::AbstractModel, key) = m.info[key]
info(m::AbstractModel, key, defaultval)
info!(m::AbstractModel, key, val)

Return the info structure for model m; this structure is used for storing additional information that does not affect the model's behavior. This structure can hold, for example, information about the model's statistical performance during the learning phase.

SoleModels.issymbolic — Method
issymbolic(::AbstractModel)::Bool

Return whether a model is symbolic or not. A model is said to be symbolic when its application relies on checking formulas of a certain logical language (see SoleLogics.jl package) on the instance. Symbolic models provide a form of transparent and interpretable modeling, as a symbolic model can be synthethised into a set of mutually exclusive logical rules that can often be translated into natural language.

Examples of purely symbolic models are Rules, Branch, DecisionLists and DecisionTrees. Examples of non-symbolic models are those encoding algebraic mathematical functions (e.g., neural networks). Note that DecisionForests are not purely symbolic, as they rely on an algebraic aggregation step.

See also apply, listrules, AbstractModel.

SoleModels.joinrules — Function
joinrules(rules::AbstractVector{<:Rule})::Vector{<:Rule}

Return a set of rules, with exactly one rule per different outcome from the input set of rules. For each outcome, the output rule is computed as the logical disjunction of the antecedents of the input rules for that outcome.

Examples

julia> using SoleLogics

julia> branch = Branch(SoleLogics.parseformula("p"), Branch(SoleLogics.parseformula("q"), "YES", "NO"), "NO")
 p
├✔ q
│├✔ YES
│└✘ NO
└✘ NO


julia> printmodel.(listrules(branch); tree_mode = true);
▣ p ∧ q
└✔ YES

▣ p ∧ ¬q
└✔ NO

▣ ¬p
└✔ NO

julia> printmodel.(joinrules(listrules(branch)); tree_mode = true);
▣ (p ∧ q)
└✔ YES

▣ (p ∧ ¬q) ∨ ¬p
└✔ NO

See also listrules, issymbolic, SoleLogics.DISJUNCTION, LeafModel, AbstractModel.

SoleModels.listimmediaterules — Method
listimmediaterules(m::AbstractModel{O} where {O})::Rule{<:O}

List the immediate rules equivalent to a symbolic model.

Examples

julia> using SoleLogics

julia> branch = Branch(SoleLogics.parseformula("p"), Branch(SoleLogics.parseformula("q"), "YES", "NO"), "NO")
 p
├✔ q
│├✔ YES
│└✘ NO
└✘ NO


julia> printmodel.(listimmediaterules(branch); tree_mode = true);
▣ p
└✔ q
 ├✔ YES
 └✘ NO

▣ ¬(p)
└✔ NO

See also listrules, issymbolic, AbstractModel.

SoleModels.listrules — Method
listrules(
    m::AbstractModel;
    use_shortforms::Bool = true,
    use_leftmostlinearform::Bool = false,
    normalize::Bool = false,
    force_syntaxtree::Bool = false,
)::Vector{<:Rule}

Return a list of rules capturing the knowledge enclosed in symbolic model. The behavior of any symbolic model can be synthesised and represented as a set of mutually exclusive (and jointly exaustive, if the model is closed) rules, which can be useful for many purposes.

The keyword argument force_syntaxtree, when set to true, causes the logical antecedents in the returned rules to be represented as SyntaxTrees, as opposed to other syntax structure (e.g., LeftmostConjunctiveForm).

Examples

julia> using SoleLogics

julia> branch = Branch(SoleLogics.parseformula("p"), Branch(SoleLogics.parseformula("q"), "YES", "NO"), "NO")
 p
├✔ q
│├✔ YES
│└✘ NO
└✘ NO


julia> printmodel.(listrules(branch); tree_mode = true);
▣ p ∧ q
└✔ YES

▣ p ∧ ¬q
└✔ NO

▣ ¬p
└✔ NO

See also listimmediaterules, SoleLogics.CONJUNCTION, joinrules, issymbolic, LeafModel, AbstractModel.

SoleModels.minify — Method
minify(dataset::D1)::Tuple{D2,Function} where {D1,D2}

Return a minified version of a dataset, as well as a backmap for reverting to the original dataset. Dataset minification remaps each scalar values in the dataset to a new value such that the overall order of the values is preserved; the output dataset is smaller in size, since it relies on values of type UInt8, UInt16, UInt32, etc.

See also isminifiable.

SoleModels.naturalgrouping — Method
naturalgrouping(
    X::AbstractDataFrame;
    allow_variable_drop = false,
)::AbstractVector{<:AbstractVector{<:Symbol}}

Return variables grouped by their logical nature; the nature of a variable is automatically derived from its type (e.g., Real, Vector{<:Real} or Matrix{<:Real}) and frame. All instances must have the same frame (e.g., channel size/number of worlds).

SoleModels.negconsequent — Method
negconsequent(m::Branch)::AbstractModel

Return the negative consequent of a branch; that is, the model to be applied if the antecedent evaluates to false.

See also antecedent, Branch.

SoleModels.outcometype — Method
outcometype(::Type{<:AbstractModel{O}}) where {O} = O
outcometype(m::AbstractModel) = outcometype(typeof(m))

Return the outcome type of a model (type).

See also AbstractModel.

SoleModels.outputtype — Method
outputtype(m::AbstractModel)

Return a supertype for the outputs obtained when applying a model. The result depends on whether the model is open or closed:

outputtype(M::AbstractModel{O}) = isopen(M) ? Union{Nothing,O} : O

Note that if the model is closed, then outputtype(m) is equal to outcometype(m).

See also isopen, apply, outcometype, AbstractModel.

SoleModels.parsecondition — Method
parsecondition(C::Type{<:AbstractCondition}, expr::String; kwargs...)

Parse a condition of type C from its syntaxstring representation. Depending on C, specifying keyword arguments such as featuretype::Type{<:AbstractFeature}, and featvaltype::Type may be required or recommended.

See also parsefeature.

SoleModels.parsefeature — Method
parsefeature(FT::Type{<:AbstractFeature}, expr::String; kwargs...)

Parse a feature of type FT from its syntaxstring representation. Depending on FT, specifying keyword arguments such as featvaltype::Type may be required or recommended.

See also parsecondition.

SoleModels.posconsequent — Method
posconsequent(m::Branch)::AbstractModel

Return the positive consequent of a branch; that is, the model to be applied if the antecedent evaluates to true.

See also antecedent, Branch.

SoleModels.printmodel — Method
printmodel(io::IO, m::AbstractModel; kwargs...)
displaymodel(m::AbstractModel; kwargs...)

prints or returns a string representation of model m.

Arguments

  • header::Bool = true: when set to true, a header is printed, displaying

the info structure for m;

  • show_subtree_info::Bool = false: when set to true, the header is printed for

models in the sub-tree of m;

  • show_metrics::Bool = false: when set to true, performance metrics at each point of the

subtree are shown, whenever they are available in the info structure;

  • max_depth::Union{Nothing,Int} = nothing: when it is an Int, models in the sub-tree

with a depth higher than max_depth are ellipsed with "...";

  • syntaxstring_kwargs::NamedTuple = (;): kwargs to be passed to syntaxstring for

formatting logical formulas.

See also syntaxstring, AbstractModel.

SoleModels.propagate_feasiblemodels — Method
propagate_feasiblemodels(M::Type{<:AbstractModel}) = Union{typename(M){outcometype(M)}, feasiblemodelstype(M)}
propagate_feasiblemodels(m::AbstractModel) = propagate_feasiblemodels(typeof(m))

This function is used upon construction of a ConstrainedModel, to compute its Feasible Models (FM). In general, its FM are a Union of the FM of its immediate child models, but a trick is used in order to avoid unneccessary propagation of types throughout the model tree. Note that this trick assumes that the first type parameter of any ConstrainedModel is its outcometype O.

See also feasiblemodelstype, ConstrainedModel.

SoleModels.readmetrics — Method
readmetrics(m::AbstractModel; kwargs...)

Return a NamedTuple with some performance metrics for the given symbolic model. Performance metrics can be computed when the info structure of the model: - :supportinglabels - :supportingpredictions

SoleModels.representatives — Method
representatives(
    fr::AbstractFrame{W},
    S::W,
    ::AbstractRelation,
    ::AbstractCondition
) where {W<:AbstractWorld}

Return an iterator to the (few) representative accessible worlds that are necessary for computing and propagating truth values through existential modal operators. When this optimization is possible (e.g., when checking specific formulas on scalar conditions), it allows to further boost "one-step" optimizations (see AbstractOneStepMemoset).

For example, consider a Kripke structure with a 1-dimensional FullDimensionalFrame of length 100, and the problem of checking a formula "⟨L⟩(max[V1] ≥ 10)" on a SoleLogics.Interval Interval{Int64}(1, 2) (with L being Allen's "Later" relation, see SoleLogics.IA_L). Comparing 10 with the (maximum) "max[V1]" computed on all worlds is the naïve strategy to check the formula. However, in this case, comparing 10 to the "max[V1]" computed on the single Interval Interval{Int64}(2, 101) suffice to establish whether the structure satisfies the formula. Similar cases arise depending on the relation, feature and test operator (or, better, its aggregator).

Note that this method fallsback to accessibles.

See also SoleLogics.accessibles, ScalarCondition, SoleLogics.AbstractFrame.

SoleModels.rulemetrics — Method
rulemetrics(
    r::Rule,
    X::AbstractInterpretationSet,
    Y::AbstractVector{<:Label}
)

Calculate metrics for a rule with respect to a labelled dataset and returns a NamedTuple consisting of:

  • support: number of instances satisfying the antecedent of the rule divided by the total number of instances;
  • error:
    • For classification problems: number of instances that were not classified
    correctly divided by the total number of instances;
    • For regression problems: mean squared error;
  • length: number of atoms in the rule's antecedent.

See also Rule, SoleLogics.AbstractInterpretationSet, Label, evaluaterule, outcometype, consequent.

SoleModels.scalarlogiset — Function
scalarlogiset(dataset, features; kwargs...)

Converts a dataset structure (with variables) to a logiset with scalar-valued features. If dataset is not a multimodal dataset, the following methods should be defined: TODO explain

    islogiseed(::typeof(dataset)) = true
    initlogiset(dataset, features)
    ninstances(dataset)
    nvariables(dataset)
    frame(dataset, i_instance::Integer)
    featvalue(dataset, i_instance::Integer, w::AbstractWorld, feature::VarFeature)
    vareltype(dataset, i_variable::Integer)

If dataset represents a multimodal dataset, the following methods should be defined, while its modalities (iterated via eachmodality) should provide the methods above:

    ismultilogiseed(dataset)
    nmodalities(dataset)
    eachmodality(dataset)

See also AbstractLogiset, VarFeature, ScalarCondition.

SoleModels.submodels — Method
submodels(m::AbstractModel)

Enumerate all submodels in the sub-tree. This function is the transitive closure of immediatesubmodels; in fact, the returned list includes the immediate submodels (immediatesubmodels(m)), but also their immediate submodels, and so on.

Examples

julia> using SoleLogics

julia> branch = Branch(SoleLogics.parseformula("p∧q∨r"), "YES", "NO");

julia> submodels(branch)
2-element Vector{SoleModels.ConstantModel{String}}:
 ConstantModel
YES

 ConstantModel
NO


julia> branch2 = Branch(SoleLogics.parseformula("s→p"), branch, 42);

julia> printmodel.(submodels(branch2));
Branch
┐ p ∧ (q ∨ r)
├ ✔ YES
└ ✘ NO

ConstantModel
YES

ConstantModel
NO

ConstantModel
42

julia> submodels(branch) == immediatesubmodels(branch)
true

julia> submodels(branch2) == immediatesubmodels(branch2)
false

See also immediatesubmodels, LeafModel, AbstractModel.

SoleModels.variable_name — Method
variable_name(
    f::AbstractUnivariateFeature;
    variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing,
    variable_name_prefix::Union{Nothing,String} = "V",
)::String

Return the name of the variable targeted by a univariate feature. By default, an variable name is a number prefixed by "V"; however, variable_names_map or variable_name_prefix can be used to customize variable names. The prefix can be customized by specifying variable_name_prefix. Alternatively, a mapping from string to integer (either via a Dictionary or a Vector) can be passed as variable_names_map. Note that only one in variable_names_map and variable_name_prefix should be provided.

See also parsecondition, ScalarCondition, syntaxstring.

SoleModels.wrap — Method
wrap(o::Any)::AbstractModel

This function wraps anything into an AbstractModel. The default behavior is the following:

  • when called on an AbstractModel, the model is

simply returned (no wrapping is performed);

  • Functions and FunctionWrappers are wrapped into a FunctionModel;
  • every other object is wrapped into a ConstantModel.

See also ConstantModel, FunctionModel, ConstrainedModel, LeafModel.

SoleModels.DimensionalDatasets.UniformFullDimensionalOneStepRelationalMemoset — Type

A relational memoset optimized for uniform scalar logisets with full dimensional frames of dimensionality N, storing values for each world in a ninstances × nmetaconditions × nrelations array. Each world is a hyper-interval, and its N*2 components are used to index different array dimensions, ultimately resulting in a (N*2+3)-dimensional array.

See also UniformFullDimensionalLogiset, `FullDimensionalFrame, AbstractLogiset.