Merge pull request #931 from JuliaReach/schillic/930

#930 - Define issubset for EmptySet

docs/src/lib/binary_functions.md

@@ -29,6 +29,8 @@ end
 ⊆(::LineSegment{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
 ⊆(::LineSegment{N}, ::Hyperrectangle{N}, ::Bool=false) where {N<:Real}
 ⊆(::Interval, ::Interval)
+⊆(::EmptySet{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
+⊆(::LazySet{N}, ::EmptySet{N}, ::Bool=false) where {N<:Real}
 ```
 
 ## Check for emptiness of intersection

src/Approximations/box_approximations.jl

@@ -37,6 +37,9 @@ box_approximation(S::Hyperrectangle) = S
 box_approximation(S::AbstractHyperrectangle) =
     Hyperrectangle(center(S), radius_hyperrectangle(S))
 
+# special case: empty set
+box_approximation(∅::EmptySet) = ∅
+
 """
     interval_hull
 
@@ -74,6 +77,9 @@ function box_approximation_symmetric(S::LazySet{N};
     return Hyperrectangle(zeros(N, length(c)), abs.(c) .+ r)
 end
 
+# special case: empty set
+box_approximation_symmetric(∅::EmptySet) = ∅
+
 """
     symmetric_interval_hull
 
@@ -176,3 +182,6 @@ function ballinf_approximation(S::LazySet{N};
     end
     return BallInf(c, r)
 end
+
+# special case: empty set
+ballinf_approximation(∅::EmptySet) = ∅

src/is_subset.jl

@@ -482,6 +482,10 @@ function ⊆(L::LineSegment{N}, H::AbstractHyperrectangle{N}, witness::Bool=fals
     end
 end
 
+
+# --- Interval ---
+
+
 """
     ⊆(x::Interval, y::Interval)
 
@@ -499,3 +503,87 @@ Check whether an interval is contained in another interval.
 function ⊆(x::Interval, y::Interval)
     return x.dat ⊆ y.dat
 end
+
+
+# --- EmptySet ---
+
+
+"""
+    ⊆(∅::EmptySet{N}, X::LazySet{N}, [witness]::Bool=false
+     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether an empty set is contained in another set.
+
+### Input
+
+- `∅`       -- empty set
+- `X`       -- another set
+- `witness` -- (optional, default: `false`) compute a witness if activated
+               (ignored, just kept for interface reasons)
+
+### Output
+
+`true`.
+"""
+function ⊆(∅::EmptySet{N}, X::LazySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    return witness ? (true, N[]) : true
+end
+
+# disambiguation
+function ⊆(∅::EmptySet{N}, H::AbstractHyperrectangle{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    return witness ? (true, N[]) : true
+end
+
+"""
+    ⊆(X::LazySet{N}, ∅::EmptySet{N}, [witness]::Bool=false
+     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether a set is contained in an empty set.
+
+### Input
+
+- `X`       -- another set
+- `∅`       -- empty set
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+`true` iff `X` is empty.
+
+### Algorithm
+
+We rely on `isempty(X)` for the emptiness check and on `an_element(X)` for
+witness production.
+"""
+function ⊆(X::LazySet{N}, ∅::EmptySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    if isempty(X)
+        return witness ? (true, N[]) : true
+    else
+        return witness ? (false, an_element(X)) : false
+    end
+end
+
+# disambiguation
+function ⊆(X::AbstractPolytope{N}, ∅::EmptySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    if isempty(X)
+        return witness ? (true, N[]) : true
+    else
+        return witness ? (false, an_element(X)) : false
+    end
+end
+function ⊆(X::AbstractSingleton{N}, ∅::EmptySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    return witness ? (false, an_element(X)) : false
+end
+function ⊆(X::LineSegment{N}, ∅::EmptySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    return witness ? (false, an_element(X)) : false
+end
+function ⊆(X::EmptySet{N}, ∅::EmptySet{N}, witness::Bool=false
+          )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    return witness ? (true, N[]) : true
+end

test/unit_EmptySet.jl

@@ -46,6 +46,12 @@ for N in [Float64, Rational{Int}, Float32]
     @test !∈(N[0], E)
     @test !∈(N[0, 0], E)
 
+    # subset
+    @test ⊆(E, B) && ⊆(E, B, true)[1]
+    subset, point = ⊆(B, E, true)
+    @test !⊆(B, E) && !subset && point ∈ B
+    @test ⊆(E, E) && ⊆(E, E, true)[1]
+
     # emptiness check
     @test isempty(E)
 

test/unit_ballinf_approximation.jl

@@ -19,4 +19,8 @@ for N in [Float64, Float32, Rational{Int}]
     biexp = BallInf(N[0.5, 0], N(1.5))
     @test bi.center ≈ biexp.center
     @test bi.radius ≈ biexp.radius
+
+    # empty set
+    E = EmptySet{N}()
+    @test ballinf_approximation(E) == E
 end

test/unit_box_approximation.jl

@@ -33,6 +33,10 @@ for N in [Float64, Rational{Int}, Float32]
     @test h.center ≈ hexp.center
     @test h.radius ≈ hexp.radius
 
+    # empty set
+    E = EmptySet{N}()
+    @test box_approximation(E) == E
+
     # ===================================================================
     # Testing box_approximation_symmetric (= symmetric interval hull)
     # ===================================================================
@@ -67,4 +71,8 @@ for N in [Float64, Rational{Int}, Float32]
 
     # Testing alias symmetric_interval_hull
     h = symmetric_interval_hull(b)
+
+    # empty set
+    E = EmptySet{N}()
+    @test box_approximation_symmetric(E) == E
 end