Merge branch 'dev' into gio/refractoring

Project.toml

@@ -43,6 +43,7 @@ DataFrames = "1"
 DataStructures = "0.18"
 Graphs = "1.8"
 HTTP = "1.9"
+IntervalSets = "0.7.10"
 Lazy = "0.15"
 MLJModelInterface = "1.9"
 MultiData = "0 - 0.1"
@@ -53,7 +54,7 @@ Reexport = "1"
 Revise = "3"
 ScientificTypes = "3"
 SoleBase = "0.12"
-SoleLogics = "0.11"
+SoleLogics = "0.9 - 0.11"
 StatsBase = "0.30 - 0.34"
 Tables = "1"
 ThreadSafeDicts = "0.1"
@@ -66,8 +67,8 @@ Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6"
 InteractiveUtils = "b77e0a4c-d291-57a0-90e8-8db25a27a240"
 MLJBase = "a7f614a8-145f-11e9-1d2a-a57a1082229d"
 Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a"
-PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
 Plots = "91a5bcdd-55d7-5caf-9e0b-520d859cae80"
+PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
 
 [targets]

src/deprecate.jl

@@ -1,4 +1,4 @@
-const BoundedScalarConditions = MultivariateScalarAlphabet{ScalarCondition}
+const BoundedScalarConditions = MultivariateScalarAlphabet{ScalarCondition} 
 
 function BoundedScalarConditions(
     metaconditions::Vector{<:ScalarMetaCondition},

src/minimize.jl

@@ -1,7 +1,17 @@
 
-function espresso_minimize(syntaxtree::SoleLogics.Formula, silent::Bool = true, Dflag = "exact", Sflag = nothing, eflag = nothing, args...; otherflags = [], kwargs...)
+function espresso_minimize(
+    syntaxtree::SoleLogics.Formula,
+    silent::Bool = true,
+    Dflag = "exact",
+    Sflag = nothing,
+    eflag = nothing,
+    args...;
+    otherflags = [],
+    use_scalar_range_conditions = false,
+    kwargs...
+)
     dc_set = false
-    pla_string, others... = PLA._formula_to_pla(syntaxtree, dc_set, silent, args...; kwargs...)
+    pla_string, pla_args, pla_kwargs = PLA._formula_to_pla(syntaxtree, dc_set, silent, args...; use_scalar_range_conditions, kwargs...)
 
     silent || println()
     silent || println(pla_string)
@@ -41,5 +51,6 @@ function espresso_minimize(syntaxtree::SoleLogics.Formula, silent::Bool = true,
 
     minimized_pla = String(read(out))
     silent || println(minimized_pla)
-    return PLA._pla_to_formula(minimized_pla, others...)
+    conditionstype = use_scalar_range_conditions ? SoleData.RangeScalarCondition : SoleData.ScalarCondition
+    return PLA._pla_to_formula(minimized_pla, silent, pla_args...; conditionstype, pla_kwargs...)
 end

src/scalar/conditions.jl

@@ -5,6 +5,68 @@ const DEFAULT_SCALARCOND_FEATTYPE = SoleData.VarFeature
 
 abstract type AbstractScalarCondition{FT} <: AbstractCondition{FT} end
 
+
+_patchnothing(v, d) = isnothing(v) ? d : v
+function _scalarcondition_sortby(cond)
+    (syntaxstring(SoleData.feature(cond)),
+    _patchnothing(SoleData.minval(cond), -Inf),
+    !SoleData.minincluded(cond),
+    _patchnothing(SoleData.maxval(cond), Inf),
+    SoleData.maxincluded(cond)
+    )
+end
+
+function scalartiling(conditions::Vector, features = unique(SoleData.feature.(conditions)))
+    newconds = SoleData.AbstractScalarCondition[]
+    for feat in features
+        conds = filter(c->feature(c) == feat, conditions)
+        # @show syntaxstring.(conds)
+        minextremes = [(true, (SoleData.minval(cond), !SoleData.minincluded(cond))) for cond in conds]
+        maxextremes = [(false, (SoleData.maxval(cond), SoleData.maxincluded(cond))) for cond in conds]
+        extremes = [minextremes..., maxextremes...]
+        sort!(extremes, by=((ismin, (mv, mi)),)->(_patchnothing(mv, ismin ? -Inf : Inf), mi))
+        extremes = map(last, extremes)
+        extremes = unique(extremes)
+        @show extremes
+        for (minextreme,maxextreme) in zip(extremes[1:end-1], extremes[2:end])
+            # @show maxextreme
+            cond = SoleData.RangeScalarCondition(feat, minextreme[1], maxextreme[1], !minextreme[2], maxextreme[2])
+            push!(newconds, cond)
+        end
+    end
+    # @show syntaxstring.(newconds)
+    newconds
+end
+
+function tointervalset(a::AbstractScalarCondition)
+    f1 = minincluded(a) ? :closed : :open
+    f2 = maxincluded(a) ? :closed : :open
+    IntervalSetsWrap.Interval{f1,f2}(isnothing(minval(a)) ? -Inf : minval(a), isnothing(maxval(a)) ? Inf : maxval(a))
+end
+
+function includes(a::AbstractScalarCondition, b::AbstractScalarCondition)
+    (feature(a) == feature(b)) || return false
+    return issubset(tointervalset(b),tointervalset(a))
+end
+
+function excludes(a::AbstractScalarCondition, b::AbstractScalarCondition)
+    (feature(a) == feature(b)) || return false
+    # @show tointervalset(a)
+    # @show tointervalset(b)
+    return isdisjoint(tointervalset(a),tointervalset(b))
+end
+
+function removeduals(values::Vector)
+    newvalues = similar(values, (0,))
+    for cond in values
+        if !SoleData.hasdual(cond) || !(SoleData.dual(cond) in newvalues)
+            push!(newvalues, cond)
+        end
+    end
+    newvalues
+end
+
+
 # TODO ScalarMetaCondition is more like... an Alphabet, than a Condition.
 """
     struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractScalarCondition{FT}
@@ -184,6 +246,51 @@ test_operator(c::ScalarCondition) = test_operator(metacond(c))
 hasdual(::ScalarCondition) = true
 dual(c::ScalarCondition) = ScalarCondition(dual(metacond(c)), threshold(c))
 
+function minval(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        threshold(c)
+    elseif isnothing(pol)
+        error("Unknown minval for test_operator $(testop).")
+    else
+        pol ? threshold(c) : -Inf
+    end
+end
+function minincluded(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        true
+    elseif isnothing(pol)
+        error("Unknown minincluded for test_operator $(testop).")
+    else
+        pol ? !isstrict(testop) : true
+    end
+end
+function maxval(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        threshold(c)
+    elseif isnothing(pol)
+        error("Unknown maxval for test_operator $(testop).")
+    else
+        pol ? Inf : threshold(c)
+    end
+end
+function maxincluded(c::ScalarCondition)
+    testop = test_operator(c)
+    pol = polarity(testop)
+    if pol == (==)
+        true
+    elseif isnothing(pol)
+        error("Unknown maxincluded for test_operator $(testop).")
+    else
+        pol ? true : !isstrict(test_operator(c))
+    end
+end
+
 function checkcondition(c::ScalarCondition, args...; kwargs...)
     apply_test_operator(test_operator(c), featvalue(feature(c), args...; kwargs...), threshold(c))
 end
@@ -253,9 +360,9 @@ function _parsecondition(
     expr::AbstractString;
     kwargs...
 ) where {U,FT<:AbstractFeature,C<:ScalarCondition{U,FT}}
-    r = Regex("^\\s*(\\S+)\\s*([^\\s\\d]+)\\s*(\\S+)\\s*\$")
+    r = Regex("^\\s*([^\\s><!=≥≤]+)\\s*([^\\s\\d]+)\\s*(\\S+)\\s*\$")
     slices = match(r, expr)
-    
+
     if isnothing(slices) || length(slices) != 3
         throw(ArgumentError("Could not parse ScalarCondition from " *
             "expression $(repr(expr)). Regex slices = $(slices)"))
@@ -264,6 +371,7 @@ function _parsecondition(
     slices = string.(slices)
 
     feature = parsefeature(FT, slices[1]; featvaltype = U, kwargs...)
+    # @show slices
     test_operator = eval(Meta.parse(slices[2]))
     threshold = eval(Meta.parse(slices[3]))
 
@@ -547,6 +655,13 @@ function hasdual(c::RangeScalarCondition)
     )
 end
 
+function _rangescalarcond_to_scalarconds_in_conjunction(cond)
+    conds = []
+    !isnothing(SoleData.minval(cond)) && push!(conds, ScalarCondition(feature(cond), _isgreater_test_operator(cond), SoleData.minval(cond)))
+    !isnothing(SoleData.maxval(cond)) && push!(conds, ScalarCondition(feature(cond), _isless_test_operator(cond), SoleData.maxval(cond)))
+    conds
+end
+
 module IntervalSetsWrap
 using IntervalSets: Interval
 end
@@ -567,29 +682,6 @@ end
 #     return aismin && !bismin
 # end
 
-function tointervalset(a::RangeScalarCondition)
-    f1 = minincluded(a) ? :closed : :open
-    f2 = maxincluded(a) ? :closed : :open
-    IntervalSetsWrap.Interval{f1,f2}(isnothing(minval(a)) ? -Inf : minval(a), isnothing(maxval(a)) ? Inf : maxval(a))
-end
-
-function includes(a::RangeScalarCondition, b::RangeScalarCondition)
-    (feature(a) == feature(b)) || return false
-    return issubset(tointervalset(b),tointervalset(a))
-    # return 
-    #         (minincluded(a) ? (!myisless(b.minval, true, a.minval, true)) : (myisless(a.minval, true, b.minval, true) || (!(minincluded(b)) && a.minval == b.minval))) &&
-    #         (maxincluded(a) ? (!myisless(a.maxval, false, b.maxval, false)) : (myisless(a.maxval, false, b.maxval, false) || (!(maxincluded(b)) && a.maxval == b.maxval)))
-end
-
-function excludes(a::RangeScalarCondition, b::RangeScalarCondition)
-    (feature(a) == feature(b)) || return false
-    return isdisjoint(tointervalset(a),tointervalset(b))
-    # intersect = 
-    #         (minincluded(a) ? (!myisless(b.maxval, false, a.minval, true) || ((maxincluded(b)) && a.minval == b.maxval)) : (myisless(a.minval, true, b.maxval, false))) ||
-    #         (maxincluded(a) ? (!myisless(a.maxval, false, b.minval, true) || ((minincluded(b)) && a.maxval == b.minval)) : (myisless(a.maxval, false, b.minval, true)))
-    # return !intersect
-end
-
 @inline function honors_minval(c::RangeScalarCondition, featval)
     isnothing(c.minval) || apply_test_operator(_isgreater_test_operator(c), featval, c.minval)
 end
@@ -650,7 +742,7 @@ function _parsecondition(
     # r = Regex("^\\s*(\\S+)\\s*([^\\s\\d]+)\\s*(\\[|\\()\\s*(\\S+)\\s*,\\s*(\\S+)\\s*(\\]|\\))\\s*\$")
     slices = match(r, expr)
     if isnothing(slices) || length(slices) != 5
-        throw(ArgumentError("Could not parse ScalarCondition from " *
+        throw(ArgumentError("Could not parse RangeScalarCondition from " *
             "expression $(repr(expr)). Regex slices = $(slices)"))
     end
 

src/scalar/propositional-formula-simplification.jl

@@ -16,22 +16,38 @@ function scalar_simplification(φ::SoleLogics.SyntaxLeaf; silent = false, kwargs
 end
 
 function scalar_simplification(φ::DNF, args...; kwargs...)
-    return map(d->scalar_simplification(d; args...), SoleLogics.disjuncts(φ)) |> LeftmostDisjunctiveForm
+    return map(d->scalar_simplification(d, args...; kwargs...), SoleLogics.disjuncts(φ)) |> LeftmostDisjunctiveForm
 end
 function scalar_simplification(φ::CNF, args...; kwargs...)
-    return map(d->scalar_simplification(d; args...), SoleLogics.conjuncts(φ)) |> LeftmostConjunctiveForm
+    return map(d->scalar_simplification(d, args...; kwargs...), SoleLogics.conjuncts(φ)) |> LeftmostConjunctiveForm
 end
 function scalar_simplification(
     φ::Union{LeftmostConjunctiveForm,LeftmostDisjunctiveForm};
     silent = false,
     force_scalar_range_conditions = false,
-    force_no_scalar_range_conditions = false,
+    # force_no_scalar_range_conditions = false,
     allow_scalar_range_conditions = true,
-    kwargs...,
 )
     # @show φ
     # @show typeof.(SoleLogics.grandchildren(φ))
     # @show all(c->c isa Atom{<:ScalarCondition}, SoleLogics.grandchildren(φ))
+
+    φ = LeftmostLinearForm(SoleLogics.connective(φ), map(ch->begin
+        if ch isa Atom
+            ch
+        elseif ch isa Literal
+            if SoleLogics.ispos(ch)
+                atom(ch)
+            elseif SoleLogics.hasdual(atom(ch))
+                SoleLogics.dual(atom(ch))
+            else
+                ch
+            end
+        else
+            ch
+        end
+    end, SoleLogics.grandchildren(φ)))
+
     if !all(c->c isa Atom{<:Union{ScalarCondition,RangeScalarCondition}}, SoleLogics.grandchildren(φ))
     # if (!all(c->c isa Atom{<:ScalarCondition}, SoleLogics.grandchildren(φ)))
         !silent && println("Cannot perform scalar simplification on linear form:\n$(syntaxstring(φ))\n on" *
@@ -69,14 +85,27 @@ function scalar_simplification(
     ch = collect(Iterators.flatten([begin
             conds = scalar_conditions[bitmask]
 
+            conds = [if cond isa ScalarCondition && (test_operator(cond) == (==))
+                        RangeScalarCondition(
+                            SoleData.feature(cond),
+                            SoleData.minval(cond),
+                            SoleData.maxval(cond),
+                            SoleData.minincluded(cond),
+                            SoleData.maxincluded(cond),
+                        )
+                    else
+                        cond
+                    end for cond in conds]
+
             conds = Iterators.flatten([
                 if cond isa ScalarCondition
                     [cond]
                 elseif cond isa RangeScalarCondition
-                    conds = []
-                    !isnothing(SoleData.minval(cond)) && push!(conds, ScalarCondition(feat, _isgreater_test_operator(cond), SoleData.minval(cond)))
-                    !isnothing(SoleData.maxval(cond)) && push!(conds, ScalarCondition(feat, _isless_test_operator(cond), SoleData.maxval(cond)))
-                    conds
+                    if conn_polarity
+                        conds = _rangescalarcond_to_scalarconds_in_conjunction(cond)
+                    else
+                        error("Cannot convert RangeScalarCondition to ScalarCondition: $(cond).")
+                    end
                 else
                     error("Unexpected condition: $(cond)")
                 end for cond in conds])

src/scalar/scalarlogiset.jl

@@ -438,7 +438,7 @@ function naturalconditions(
     metaconditions = ScalarMetaCondition[]
 
     mixed_conditions = vcat(unpackcondition.(mixed_conditions)...)
-    @show mixed_conditions
+    # @show mixed_conditions
     readymade_conditions          = filter(x->
         isa(x, ScalarMetaCondition),
         mixed_conditions,