Merge pull request #1799 from JuliaReach/schillic/1125

#1125 - isuniversal methods for bounded sets

docs/src/lib/interfaces.md

@@ -112,6 +112,7 @@ This interface defines the following functions:
 ```@docs
 dim(::AbstractCentrallySymmetric)
 isbounded(::AbstractCentrallySymmetric)
+isuniversal(::AbstractCentrallySymmetric{N}, ::Bool=false) where {N<:Real}
 an_element(::AbstractCentrallySymmetric{N}) where {N<:Real}
 isempty(::AbstractCentrallySymmetric)
 ```
@@ -129,6 +130,7 @@ This interface defines the following functions:
 
 ```@docs
 ∈(::AbstractVector{N}, ::AbstractPolyhedron{N}) where {N<:Real}
+isuniversal(::AbstractPolyhedron{N}, ::Bool=false) where {N<:Real}
 constrained_dimensions(::AbstractPolyhedron)
 linear_map(::AbstractMatrix{N}, ::AbstractPolyhedron{N}) where {N<:Real}
 chebyshev_center(::AbstractPolyhedron{N}) where {N<:AbstractFloat}
@@ -155,6 +157,7 @@ This interface defines the following functions:
 
 ```@docs
 isbounded(::AbstractPolytope)
+isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real}
 singleton_list(::AbstractPolytope{N}) where {N<:Real}
 isempty(::AbstractPolytope)
 ```

docs/src/lib/representations.md

@@ -35,6 +35,7 @@ Inherited from [`AbstractCentrallySymmetric`](@ref):
 * [`dim`](@ref dim(::AbstractCentrallySymmetric))
 * [`isbounded`](@ref isbounded(::AbstractCentrallySymmetric))
 * [`isempty`](@ref isempty(::AbstractCentrallySymmetric))
+* [`isuniversal`](@ref isuniversal(::AbstractCentrallySymmetric{N}, ::Bool=false) where {N<:Real})
 * [`an_element`](@ref an_element(::AbstractCentrallySymmetric{N}) where {N<:Real})
 
 ### Infinity norm ball
@@ -56,6 +57,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -98,6 +100,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -124,6 +127,7 @@ Inherited from [`AbstractCentrallySymmetric`](@ref):
 * [`dim`](@ref dim(::AbstractCentrallySymmetric))
 * [`isbounded`](@ref isbounded(::AbstractCentrallySymmetric))
 * [`isempty`](@ref isempty(::AbstractCentrallySymmetric))
+* [`isuniversal`](@ref isuniversal(::AbstractCentrallySymmetric{N}, ::Bool=false) where {N<:Real})
 * [`an_element`](@ref an_element(::AbstractCentrallySymmetric{N}) where {N<:Real})
 
 ## Ellipsoid
@@ -146,6 +150,7 @@ Inherited from [`AbstractCentrallySymmetric`](@ref):
 * [`dim`](@ref dim(::AbstractCentrallySymmetric))
 * [`isbounded`](@ref isbounded(::AbstractCentrallySymmetric))
 * [`isempty`](@ref isempty(::AbstractCentrallySymmetric))
+* [`isuniversal`](@ref isuniversal(::AbstractCentrallySymmetric{N}, ::Bool=false) where {N<:Real})
 * [`an_element`](@ref an_element(::AbstractCentrallySymmetric{N}) where {N<:Real})
 
 ## Empty set
@@ -161,6 +166,7 @@ an_element(::EmptySet)
 rand(::Type{EmptySet})
 isbounded(::EmptySet)
 isempty(::EmptySet)
+isuniversal(::EmptySet{N}, ::Bool=false) where {N<:Real}
 norm(::EmptySet, ::Real=Inf)
 radius(::EmptySet, ::Real=Inf)
 diameter(::EmptySet, ::Real=Inf)
@@ -240,6 +246,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -297,6 +304,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -362,6 +370,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
 * [`isempty`](@ref isempty(::AbstractCentrallySymmetricPolytope))
@@ -387,6 +396,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isempty`](@ref isempty(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 * [`linear_map`](@ref linear_map(::AbstractMatrix{N}, ::AbstractPolyhedron{N}) where {N<:Real})
 
@@ -419,6 +429,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isempty`](@ref isempty(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractPolygon`](@ref):
@@ -460,6 +471,7 @@ Inherited from [`LazySet`](@ref):
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
 * [`isempty`](@ref isempty(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 * [`linear_map`](@ref linear_map(::AbstractMatrix{N}, ::AbstractPolyhedron{N}) where {N<:Real})
 
@@ -528,6 +540,7 @@ isbounded(::HPolytope, ::Bool=true)
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 
 #### Polyhedra
 
@@ -536,11 +549,13 @@ The following methods are specific for `HPolyhedron`.
 ```@docs
 rand(::Type{HPolyhedron})
 isbounded(::HPolyhedron)
-isuniversal(::HPolyhedron{N}, ::Bool=false) where {N<:Real}
 vertices_list(::HPolyhedron{N}) where {N<:Real}
 singleton_list(::HPolyhedron{N}) where {N<:Real}
 ```
 
+Inherited from [`AbstractPolyhedron`](@ref):
+* [`isuniversal`](@ref isuniversal(::AbstractPolyhedron{N}, ::Bool=false) where {N<:Real})
+
 ### Vertex representation
 
 ```@docs
@@ -566,6 +581,7 @@ Inherited from [`LazySet`](@ref):
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
 * [`isempty`](@ref isempty(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 * [`linear_map`](@ref linear_map(::AbstractMatrix{N}, ::AbstractPolyhedron{N}) where {N<:Real})
 
@@ -596,6 +612,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -665,6 +682,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):
@@ -711,6 +729,7 @@ Inherited from [`LazySet`](@ref):
 
 Inherited from [`AbstractPolytope`](@ref):
 * [`isbounded`](@ref isbounded(::AbstractPolytope))
+* [`isuniversal`](@ref isuniversal(::AbstractPolytope{N}, ::Bool=false) where {N<:Real})
 * [`singleton_list`](@ref singleton_list(::AbstractPolytope{N}) where {N<:Real})
 
 Inherited from [`AbstractCentrallySymmetricPolytope`](@ref):

src/Interfaces/AbstractCentrallySymmetric.jl

@@ -94,3 +94,35 @@ Return if a centrally symmetric set is empty or not.
 function isempty(::AbstractCentrallySymmetric)::Bool
     return false
 end
+
+"""
+    isuniversal(S::AbstractCentrallySymmetric{N}, [witness]::Bool=false
+               )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether a centrally symmetric set is universal.
+
+### Input
+
+- `S`       -- centrally symmetric set
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+* If `witness` option is deactivated: `false`
+* If `witness` option is activated: `(false, v)` where ``v ∉ S``
+
+### Algorithm
+
+A witness is obtained by computing the support vector in direction
+`d = [1, 0, …, 0]` and adding `d` on top.
+"""
+function isuniversal(S::AbstractCentrallySymmetric{N}, witness::Bool=false
+                    )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    if witness
+        d = SingleEntryVector{N}(1, dim(S))
+        w = σ(d, S) + d
+        return (false, w)
+    else
+        return false
+    end
+end

src/Interfaces/AbstractPolyhedron_functions.jl

@@ -53,6 +53,41 @@ function ∈(x::AbstractVector{N}, P::AbstractPolyhedron{N})::Bool where {N<:Rea
     return true
 end
 
+"""
+    isuniversal(P::AbstractPolyhedron{N}, [witness]::Bool=false
+               )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether a polyhedron is universal.
+
+### Input
+
+- `P`       -- polyhedron
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+* If `witness` option is deactivated: `true` iff ``P`` is universal
+* If `witness` option is activated:
+  * `(true, [])` iff ``P`` is universal
+  * `(false, v)` iff ``P`` is not universal and ``v ∉ P``
+
+### Algorithm
+
+`P` is universal iff it has no constraints.
+
+A witness is produced using `isuniversal(H)` where `H` is the first linear
+constraint of `P`.
+"""
+function isuniversal(P::AbstractPolyhedron{N}, witness::Bool=false
+                    )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    constraints = constraints_list(P)
+    if isempty(constraints)
+        return witness ? (true, N[]) : true
+    else
+        return witness ? isuniversal(constraints[1], true) : false
+    end
+end
+
 """
     constrained_dimensions(P::AbstractPolyhedron)::Vector{Int} where {N<:Real}
 

src/Interfaces/AbstractPolytope.jl

@@ -96,6 +96,40 @@ function isempty(P::AbstractPolytope)::Bool
     return isempty(vertices_list(P))
 end
 
+"""
+    isuniversal(P::AbstractPolytope{N}, [witness]::Bool=false
+               )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether a polyhedron is universal.
+
+### Input
+
+- `P`       -- polyhedron
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+* If `witness` option is deactivated: `false`
+* If `witness` option is activated: `(false, v)` where ``v ∉ P``
+
+### Algorithm
+
+A witness is produced using `isuniversal(H)` where `H` is the first linear
+constraint of `P`.
+"""
+function isuniversal(P::AbstractPolytope{N}, witness::Bool=false
+                    )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    if witness
+        constraints = constraints_list(P)
+        if isempty(constraints)
+            return (true, N[])  # special case for polytopes without constraints
+        end
+        return isuniversal(constraints[1], true)
+    else
+        return false
+    end
+end
+
 # given a polytope P, apply the linear map P to each vertex of P
 # it is assumed that the interface function `vertices_list(P)` is available 
 @inline function _linear_map_vrep(M::AbstractMatrix{N}, P::AbstractPolytope{N}) where {N<:Real}

src/Sets/EmptySet.jl

@@ -99,6 +99,33 @@ function isbounded(::EmptySet)::Bool
     return true
 end
 
+"""
+    isuniversal(∅::EmptySet{N}, [witness]::Bool=false
+               )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+
+Check whether an empty is universal.
+
+### Input
+
+- `∅`       -- empty set
+- `witness` -- (optional, default: `false`) compute a witness if activated
+
+### Output
+
+* If `witness` option is deactivated: `false`
+* If `witness` option is activated: `(false, v)` where ``v ∉ S``, although
+  we currently throw an error
+"""
+function isuniversal(∅::EmptySet{N}, witness::Bool=false
+                    )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
+    if witness
+        error("witness production is currently not supported")
+        # return (false, zeros(N, dim(∅)))  # deactivated, see #1201
+    else
+        return false
+    end
+end
+
 """
     ∈(x::AbstractVector{N}, ∅::EmptySet{N})::Bool where {N<:Real}
 

src/Sets/HPolyhedron.jl

@@ -215,40 +215,6 @@ function isbounded(P::HPolyhedron)::Bool
     return isbounded_unit_dimensions(P)
 end
 
-"""
-    isuniversal(P::HPolyhedron{N}, [witness]::Bool=false
-               )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
-
-Check whether a polyhedron is universal.
-
-### Input
-
-- `P`       -- polyhedron
-- `witness` -- (optional, default: `false`) compute a witness if activated
-
-### Output
-
-* If `witness` option is deactivated: `true` iff ``P`` is universal
-* If `witness` option is activated:
-  * `(true, [])` iff ``P`` is universal
-  * `(false, v)` iff ``P`` is not universal and ``v ∉ P``
-
-### Algorithm
-
-`P` is universal iff it has no constraints.
-
-A witness is produced using `isuniversal(H)` where `H` is the first linear
-constraint of `P`.
-"""
-function isuniversal(P::HPolyhedron{N}, witness::Bool=false
-                    )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}
-    if isempty(P.constraints)
-        return witness ? (true, N[]) : true
-    else
-        return witness ? isuniversal(P.constraints[1], true) : false
-    end
-end
-
 """
     rand(::Type{HPolyhedron}; [N]::Type{<:Real}=Float64, [dim]::Int=2,
          [rng]::AbstractRNG=GLOBAL_RNG, [seed]::Union{Int, Nothing}=nothing

test/unit_Ball1.jl

@@ -65,6 +65,10 @@ for N in [Float64, Rational{Int}, Float32]
     # isempty
     @test !isempty(b)
 
+    # isuniversal
+    answer, w = isuniversal(b, true)
+    @test !isuniversal(b) && !answer && w ∉ b
+
     # an_element & membership function
     @test an_element(b) ∈ b
 

test/unit_Ball2.jl

@@ -62,6 +62,10 @@ for N in [Float64, Float32]
     # isempty
     @test !isempty(b)
 
+    # isuniversal
+    answer, w = isuniversal(b, true)
+    @test !isuniversal(b) && !answer && w ∉ b
+
     # an_element function
     b = Ball2(N[1, 2], N(2))
     @test an_element(b) ∈ b