Merge branch 'dev' of https://github.com/aclai-lab/SoleLogics.jl into…

… dev

Project.toml

@@ -1,7 +1,7 @@
 name = "SoleLogics"
 uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5"
-authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Alberto PAPARELLA", "Eduard I. STAN"]
-version = "0.8.2"
+authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Edoardo PONSANESI", "Alberto PAPARELLA", "Eduard I. STAN"]
+version = "0.9.0"
 
 [deps]
 AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"

docs/src/modal-logic.md

@@ -144,7 +144,7 @@ accessibles(fr::AbstractMultiModalFrame{W}, w::W, r::AbstractRelation) where {W<
 ```@docs
 AbstractKripkeStructure
 
-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)
+check(φ::SyntaxTree, i::AbstractKripkeStructure, w; use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing, perform_normalization::Bool = true, memo_max_height::Union{Nothing,Int} = nothing)
 
 KripkeStructure{FR<:AbstractFrame, MAS<:AbstractDict}
 ```

docs/src/more-on-formulas.md

@@ -50,6 +50,7 @@ parsebaseformula(expr::String, additional_operators::Union{Nothing,Vector{<:Oper
 
 ```@docs
 Base.rand(alphabet::AbstractAlphabet, args...; kwargs...)
+SoleLogics.randatom
 StatsBase.sample(alphabet::AbstractAlphabet, weights::AbstractWeights, args...; kwargs...)
 
 randformula(height::Integer, alphabet, operators::AbstractVector; rng::Union{Integer,AbstractRNG} = Random.GLOBAL_RNG)

src/SoleLogics.jl

@@ -27,7 +27,9 @@ export syntaxstring
 export arity, valuetype, tokentype, tokenstype,
  atomstype, operatorstype, truthtype,
  associativity, precedence
-export value, token, children, formulas
+
+# export value # TODO remove. The name is too generic, and it clashes, e.g., with JuMP.value.
+export token, children, formulas
 export tree
 
 export tokens, ntokens, atoms, natoms, truths, ntruths, leaves, nleaves,

src/core.jl

@@ -717,8 +717,8 @@ end
 ############################################################################################
 
 """
- struct SyntaxBranch{T<:Connective} <: SyntaxTree
- token::T
+ struct SyntaxBranch <: SyntaxTree
+ token::Connective
  children::NTuple{N,SyntaxTree} where {N}
  end
 
@@ -737,7 +737,7 @@ julia> p,q = Atom.([p, q])
  Atom{String}: q
 
 julia> branch = SyntaxBranch(CONJUNCTION, p, q)
-SyntaxBranch{NamedConnective{:∧}}: p ∧ q
+SyntaxBranch: p ∧ q
 
 julia> token(branch)
 ∧
@@ -764,47 +764,30 @@ See also
 [`operators`](@ref), [`noperators`](@ref),
 [`tokens`](@ref), [`ntokens`](@ref),
 """
-struct SyntaxBranch{T<:Connective} <: SyntaxTree
+struct SyntaxBranch <: SyntaxTree
 
  # The syntax token at the current node
- token::T
+ token::Connective
 
  # The child nodes of the current node
  children::NTuple{N,SyntaxTree} where {N}
 
- function _aritycheck(N, T, token, children)
- @assert arity(token) == N "Cannot instantiate SyntaxBranch{$(T)} with token " *
+ function _aritycheck(N, token, children)
+ @assert arity(token) == N "Cannot instantiate SyntaxBranch with token " *
  "$(token) of arity $(arity(token)) and $(N) children."
  return nothing
  end
 
- function SyntaxBranch{T}(
- token::T,
- children::NTuple{N,SyntaxTree} = (),
- ) where {T<:Connective,N}
- _aritycheck(N, T, token, children)
- return new{T}(token, children)
- end
-
- function SyntaxBranch{T}(
- φ::SyntaxBranch{T},
- ) where {T<:Connective}
- return SyntaxBranch{T}(token(φ), children(φ))
- end
-
  function SyntaxBranch(
- token::T,
+ token::Connective,
  children::NTuple{N,SyntaxTree} = (),
- ) where {T<:Connective,N}
- _aritycheck(N, T, token, children)
- return new{T}(token, children)
+ ) where {N}
+ _aritycheck(N, token, children)
+ return new(token, children)
  end
 
  # Helpers
- function SyntaxBranch{T}(token::T, children...) where {T<:Connective}
- return SyntaxBranch{T}(token, children)
- end
- function SyntaxBranch(token::T, children...) where {T<:Connective}
+ function SyntaxBranch(token::Connective, children...)
  return SyntaxBranch(token, children)
  end
 

src/interpretation-sets.jl

@@ -109,21 +109,41 @@ function check(
  i::LogicalInstance,
  args...;
  kwargs...
+)
+ return error("Please, provide method " *
+ "check(φ::SyntaxTree, i::$(typeof(i)), " *
+ "args...::$(typeof(args)); " *
+ "kwargs...::$(typeof(kwargs))).")
+end
+
+function check(
+ φ::SyntaxTree,
+ i::LogicalInstance,
+ args...;
+ kwargs...
 )
  return istop(interpret(φ, i, args...; kwargs...))
  # return check(tree(φ), i, args...; kwargs...)
 end
 
+# # General grounding
 # function check(
 # φ::SyntaxTree,
-# i::LogicalInstance,
-# args...;
+# i::LogicalInstance{AbstractInterpretationSet{<:AbstractKripkeStructure}};
 # kwargs...
 # )
-# return error("Please, provide method " *
-# "check(φ::SyntaxTree, i::$(typeof(i)), " *
-# "args...::$(typeof(args)); " *
-# "kwargs...::$(typeof(kwargs))).")
+# if token(φ) isa Union{DiamondRelationalConnective,BoxRelationalConnective}
+# rel = SoleLogics.relation(SoleLogics.token(φ))
+# if rel == tocenterrel
+# check(first(children(φ)), i, centralworld(frame(i)); kwargs...)
+# elseif rel == globalrel
+# check(first(children(φ)), i, AnyWorld(); kwargs...)
+# else
+# check(first(children(φ)), i, accessibles(frame(i), rel); kwargs...)
+# end
+# else
+# error("Unexpected formula: $φ!")
+# end
 # end
 
 function interpret(
@@ -306,44 +326,3 @@ end
 accessibles(s::AbstractInterpretationSet, i_instance::Integer, args...) = accessibles(frame(s, i_instance), args...)
 allworlds(s::AbstractInterpretationSet, i_instance::Integer, args...) = allworlds(frame(s, i_instance), args...)
 nworlds(s::AbstractInterpretationSet, i_instance::Integer) = nworlds(frame(s, i_instance))
-
-function check(
- φ::SyntaxBranch{
- Union{
- DiamondRelationalConnective{typeof(tocenterrel)},
- BoxRelationalConnective{typeof(tocenterrel)},
- }
- },
- i::AbstractInterpretation;
- kwargs...
-)
- check(first(children(φ)), i, centralworld(frame(i)); kwargs...)
-end
-
-function check(
- φ::SyntaxBranch{
- Union{
- DiamondRelationalConnective{typeof(globalrel)},
- BoxRelationalConnective{typeof(globalrel)},
- }
- },
- i::AbstractInterpretation;
- kwargs...
-)
- check(first(children(φ)), i, nothing; kwargs...)
-end
-
-# # General grounding
-# function check(
-# φ::SyntaxBranch{
-# Union{
-# DiamondRelationalConnective{R},
-# BoxRelationalConnective{R},
-# }
-# },
-# i::AbstractInterpretation;
-# kwargs...
-# ) where {R<:AbstractRelation}
-# rel = SoleLogics.relation(SoleLogics.token(φ))
-# check(first(children(φ)), i, accessibles(frame(i), rel); kwargs...)
-# end

src/logics.jl

@@ -1,3 +1,5 @@
+import SoleBase: initrng
+
 import Base: convert, promote_rule, _promote
 import Base: eltype, in, getindex, isiterable, iterate, IteratorSize, length, isequal, hash
 
@@ -117,20 +119,49 @@ function Base.in(value::Union{AbstractString,Number,AbstractChar}, a::AbstractAl
 end
 
 """
- Base.length(a::AbstractAlphabet)::Bool
+ natoms(a::AbstractAlphabet)::Integer
 
-Return the alphabet length, if it is finite.
+Return the number of atoms of a *finite* alphabet.
 
-See also [`AbstractAlphabet`](@ref), [`SyntaxBranch`](@ref).
+See also [`randatom`](@ref), [`AbstractAlphabet`](@ref).
 """
-function Base.length(a::AbstractAlphabet)
+function natoms(a::AbstractAlphabet)::Integer
+ if Base.isfinite(a)
+ return error("Please, provide method natoms(::$(typeof(a))).")
+ else
+ return error("Cannot compute natoms of (infinite) alphabet of type $(typeof(a)).")
+ end
+end
+
+"""
+ randatom(a::AbstractAlphabet)
+ randatom(rng, a::AbstractAlphabet)
+
+Return a random atom from a *finite* alphabet.
+
+See also [`natoms`](@ref), [`AbstractAlphabet`](@ref).
+"""
+function randatom(a::AbstractAlphabet, args...; kwargs...)
+ randatom(Random.GLOBAL_RNG, a, args...; kwargs...)
+end
+
+function randatom(rng::Union{Random.AbstractRNG, Integer}, a::AbstractAlphabet, args...; kwargs...)
  if isfinite(a)
- return Base.length(atoms(a))
+ # TODO: note that `atoms(a)` can lead to brutal reduction in performance,
+ # if one forgets to implement specific methods for `randatom` for custom alphabets!
+ return Base.rand(rng, atoms(a), args...; kwargs...)
  else
- return error("Cannot compute length of (infinite) alphabet of type $(typeof(a)).")
+ error("Please provide method randatom(rng::$(typeof(rng)), " *
+ "alphabet::$(typeof(a)), args...; kwargs...)")
  end
 end
 
+# Helper
+function Base.length(a::AbstractAlphabet)
+ @warn "Please use `natoms` instead of `Base.length` with alphabets."
+ return natoms(a)
+end
+
 """
  Base.iterate(a::AbstractAlphabet)
  Base.iterate(a::AbstractAlphabet, state)
@@ -188,6 +219,7 @@ struct ExplicitAlphabet{V} <: AbstractAlphabet{V}
  end
 end
 atoms(a::ExplicitAlphabet) = a.atoms
+natoms(a::ExplicitAlphabet) = length(atoms(a))
 
 Base.convert(::Type{AbstractAlphabet}, alphabet::Vector{<:Atom}) =
  ExplicitAlphabet(alphabet)
@@ -213,7 +245,7 @@ Base.in(::Atom{PV}, ::AlphabetOfAny{VV}) where {PV,VV} = (PV <: VV)
 
 # Finite alphabet of conditions induced from a set of metaconditions
 """
-Alphabet given by the union of many alphabets.
+Alphabet given by the *union* of a number of (sub-)alphabets.
 
 See also
 [`UnboundedScalarAlphabet`](@ref),
@@ -222,24 +254,80 @@ See also
 """
 
 struct UnionAlphabet{C,A<:AbstractAlphabet{C}} <: AbstractAlphabet{C}
- alphabets::Vector{A}
+ subalphabets::Vector{A}
 end
 
-alphabets(a::UnionAlphabet) = a.alphabets
+subalphabets(a::UnionAlphabet) = a.subalphabets
+nsubalphabets(a::UnionAlphabet) = length(subalphabets(a))
 
 function Base.show(io::IO, a::UnionAlphabet)
  println(io, "$(typeof(a)):")
- for cha in alphabets(a)
- Base.show(io, cha)
+ for sa in subalphabets(a)
+ Base.show(io, sa)
  end
 end
 
+
+
 function atoms(a::UnionAlphabet)
- return Iterators.flatten(Iterators.map(atoms, alphabets(a)))
+ return Iterators.flatten(Iterators.map(atoms, subalphabets(a)))
 end
 
+natoms(a::UnionAlphabet) = sum(natoms, subalphabets(a))
+
 function Base.in(p::Atom, a::UnionAlphabet)
- return any(cha -> Base.in(p, cha), alphabets(a))
+ return any(sa -> Base.in(p, sa), subalphabets(a))
+end
+
+"""
+ randatom(
+ rng::Union{Integer,AbstractRNG},
+ a::UnionAlphabet;
+ atompicking_mode::Symbol=:uniform,
+ subalphabets_weights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing
+ )::Atom
+
+Sample an atom from a `UnionAlphabet`. By default, the sampling is uniform with respect to the atoms.
+However, by setting `atompicking_mode = :uniform_subalphabets` one can force
+a uniform sampling with respect to the sub-alphabets.
+Moreover, one can specify a `:weighted` `atompicking_mode`,
+together with a `subalphabets_weights` vector.
+
+See also [`UnionAlphabet`](@ref).
+"""
+function randatom(
+ rng::Union{Integer,AbstractRNG},
+ a::UnionAlphabet;
+ atompicking_mode::Symbol=:uniform,
+ subalphabets_weights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing
+)::Atom
+
+ # @show a
+ @assert atompicking_mode in [:uniform, :uniform_subalphabets, :weighted] "Value for `atompicking_mode` not..."
+ rng = initrng(rng)
+ alphs = subalphabets(a)
+
+ if atompicking_mode == :weighted
+ if isnothing(subalphabets_weights)
+ error("`:weighted` picking_mode requires weights in `subalphabets_weights` ")
+ end
+ @assert length(subalphabets_weights) == length(alphs) "Mismatching numbers of alphabets " *
+ "($(length(alphs))) and weights ($(length(subalphabets_weights)))."
+ subalphabets_weights = StatsBase.weights(subalphabets_weights)
+ pickedalphabet = StatsBase.sample(rng, alphs, subalphabets_weights)
+ else
+ subalphabets_weights = begin
+ # This atomatically excludes subalphabets with empty threshold vector
+ if atompicking_mode == :uniform_subalphabets
+ Weights(ones(Int, length(alphs)))
+ elseif atompicking_mode == :uniform
+ Weights(natoms.(alphs))
+ end
+ end
+ pickedalphabet = sample(rng, alphs, subalphabets_weights)
+ end
+
+ return randatom(rng, pickedalphabet)
 end
 
 ############################################################################################