diff --git a/docs/src/lib/interfaces.md b/docs/src/lib/interfaces.md index 9f555f66da..94a7e8d33e 100644 --- a/docs/src/lib/interfaces.md +++ b/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) ``` diff --git a/docs/src/lib/representations.md b/docs/src/lib/representations.md index e06c928020..ca671e2c0b 100644 --- a/docs/src/lib/representations.md +++ b/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): diff --git a/src/Interfaces/AbstractCentrallySymmetric.jl b/src/Interfaces/AbstractCentrallySymmetric.jl index d725c11500..163267bc6a 100644 --- a/src/Interfaces/AbstractCentrallySymmetric.jl +++ b/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 diff --git a/src/Interfaces/AbstractPolyhedron_functions.jl b/src/Interfaces/AbstractPolyhedron_functions.jl index 162fa1b3ba..55a42bc23a 100644 --- a/src/Interfaces/AbstractPolyhedron_functions.jl +++ b/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} diff --git a/src/Interfaces/AbstractPolytope.jl b/src/Interfaces/AbstractPolytope.jl index ec1224946f..933b703eaa 100644 --- a/src/Interfaces/AbstractPolytope.jl +++ b/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} diff --git a/src/Sets/EmptySet.jl b/src/Sets/EmptySet.jl index ab90cb4805..022401bdcb 100644 --- a/src/Sets/EmptySet.jl +++ b/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} diff --git a/src/Sets/HPolyhedron.jl b/src/Sets/HPolyhedron.jl index 831a2784c3..01b16877ec 100644 --- a/src/Sets/HPolyhedron.jl +++ b/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 diff --git a/test/unit_Ball1.jl b/test/unit_Ball1.jl index a1dec22fde..716a10db9b 100644 --- a/test/unit_Ball1.jl +++ b/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 diff --git a/test/unit_Ball2.jl b/test/unit_Ball2.jl index 8cc83345d4..5559f191a4 100644 --- a/test/unit_Ball2.jl +++ 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 diff --git a/test/unit_BallInf.jl b/test/unit_BallInf.jl index c1d694c6b6..8cb287febb 100644 --- a/test/unit_BallInf.jl +++ b/test/unit_BallInf.jl @@ -69,6 +69,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(b) + # isuniversal + answer, w = isuniversal(b, true) + @test !isuniversal(b) && !answer && w ∉ b + # membership b = BallInf(N[1, 1], N(1)) @test N[0.5, -0.5] ∉ b diff --git a/test/unit_Ballp.jl b/test/unit_Ballp.jl index a59e0ca779..66c2c46e0d 100644 --- a/test/unit_Ballp.jl +++ b/test/unit_Ballp.jl @@ -43,6 +43,10 @@ for N in [Float64, Float32] # isempty @test !isempty(b) + # isuniversal + answer, w = isuniversal(b, true) + @test !isuniversal(b) && !answer && w ∉ b + # membership & an_element @test an_element(b) ∈ b diff --git a/test/unit_Ellipsoid.jl b/test/unit_Ellipsoid.jl index 09eb6e8438..4dc674b7df 100644 --- a/test/unit_Ellipsoid.jl +++ b/test/unit_Ellipsoid.jl @@ -67,6 +67,10 @@ for N in [Float64, Float32] # isempty @test !isempty(E) + # isuniversal + answer, w = isuniversal(E, true) + @test !isuniversal(E) && !answer && w ∉ E + # an_element and set membership functions M = Matrix{N}(2I, 2, 2) E = Ellipsoid(N[1, 2], M) diff --git a/test/unit_EmptySet.jl b/test/unit_EmptySet.jl index 118fdf00eb..9940fb22f2 100644 --- a/test/unit_EmptySet.jl +++ b/test/unit_EmptySet.jl @@ -45,6 +45,10 @@ for N in [Float64, Rational{Int}, Float32] # boundedness @test isbounded(E) + # isuniversal + @test !isuniversal(E) + @test_throws ErrorException isuniversal(E, true) # see #1201 + # membership @test N[0] ∉ E @test N[0, 0] ∉ E diff --git a/test/unit_Hyperrectangle.jl b/test/unit_Hyperrectangle.jl index a08eaa375a..553cab50b1 100644 --- a/test/unit_Hyperrectangle.jl +++ b/test/unit_Hyperrectangle.jl @@ -117,6 +117,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(H) + # isuniversal + answer, w = isuniversal(H, true) + @test !isuniversal(H) && !answer && w ∉ H + # membership H = Hyperrectangle(N[1, 1], N[2, 3]) @test N[-1.1, 4.1] ∉ H diff --git a/test/unit_Interval.jl b/test/unit_Interval.jl index 2ff53aa590..b987305f1a 100644 --- a/test/unit_Interval.jl +++ b/test/unit_Interval.jl @@ -61,6 +61,10 @@ for N in [Float64, Float32, Rational{Int}] # isempty @test !isempty(x) + # isuniversal + answer, w = isuniversal(x, true) + @test !isuniversal(x) && !answer && w ∉ x + # translation @test translate(x, N[2]) == Interval(N(2), N(3)) diff --git a/test/unit_LineSegment.jl b/test/unit_LineSegment.jl index f9d1507ca7..c8c2dbe8ac 100644 --- a/test/unit_LineSegment.jl +++ b/test/unit_LineSegment.jl @@ -43,6 +43,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(l) + # isuniversal + answer, w = isuniversal(l, true) + @test !isuniversal(l) && !answer && w ∉ l + # an_element function @test an_element(l) ∈ l diff --git a/test/unit_Polygon.jl b/test/unit_Polygon.jl index 7debf4bdd3..acb9a7881d 100644 --- a/test/unit_Polygon.jl +++ b/test/unit_Polygon.jl @@ -153,6 +153,10 @@ for N in [Float64, Float32, Rational{Int}] addconstraint!(hp_shallow, c1) @test_throws AssertionError an_element(hp_shallow) + # isuniversal + answer, w = isuniversal(hp, true) + @test !isuniversal(hp) && !answer && w ∉ hp + # hrep conversion @test tohrep(hp) == hp diff --git a/test/unit_Polytope.jl b/test/unit_Polytope.jl index 44183f25bf..608e7a2ae1 100644 --- a/test/unit_Polytope.jl +++ b/test/unit_Polytope.jl @@ -42,6 +42,15 @@ for N in [Float64, Rational{Int}, Float32] # support vector of polytope with no constraints @test_throws ErrorException σ(N[0], HPolytope{N}()) + # boundedness + @test isbounded(p) && isbounded(p, false) + p2 = HPolytope{N}() + @test isbounded(p2) && !isbounded(p2, false) + + # isuniversal + answer, w = isuniversal(p, true) + @test !isuniversal(p) && !answer && w ∉ p + # membership @test N[5 / 4, 7 / 4] ∈ p @test N[4, 1] ∉ p @@ -342,6 +351,10 @@ for N in [Float64] vlist = vertices_list(cap) @test vlist == [N[1, 1]] + # isuniversal + answer, w = isuniversal(p1, true) + @test !isuniversal(p1) && !answer && w ∉ p1 + # convex hull v1 = N[1, 0] v2 = N[0, 1] diff --git a/test/unit_Singleton.jl b/test/unit_Singleton.jl index 5affd0c675..e0811ce955 100644 --- a/test/unit_Singleton.jl +++ b/test/unit_Singleton.jl @@ -53,6 +53,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(s) + # isuniversal + answer, w = isuniversal(s, true) + @test !isuniversal(s) && !answer && w ∉ s + # membership S = Singleton(N[1, 1]) @test N[0.9, 1.1] ∉ S diff --git a/test/unit_SymmetricIntervalHull.jl b/test/unit_SymmetricIntervalHull.jl index 432f0c989d..57e91444ca 100644 --- a/test/unit_SymmetricIntervalHull.jl +++ b/test/unit_SymmetricIntervalHull.jl @@ -24,6 +24,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(h) + # isuniversal + answer, w = isuniversal(h, true) + @test !isuniversal(h) && !answer && w ∉ h + # an_element function @test an_element(h) == N[0, 0] diff --git a/test/unit_Universe.jl b/test/unit_Universe.jl index a1a63e242f..6033686745 100644 --- a/test/unit_Universe.jl +++ b/test/unit_Universe.jl @@ -78,11 +78,8 @@ for N in [Float64, Rational{Int}, Float32] # subset res, w = ⊆(B, U, true) @test B ⊆ U && res && w == N[] - # TODO witness production currently not supported - @test_throws ErrorException (⊆(U, B, true)) - # res, w = ⊆(U, B, true) - # @test U ⊈ B && !res && w ∉ B - @test U ⊈ B + res, w = ⊆(U, B, true) + @test U ⊈ B && !res && w ∉ B res, w = ⊆(U, U, true) @test U ⊆ U && res && w == N[] end diff --git a/test/unit_ZeroSet.jl b/test/unit_ZeroSet.jl index 434cd82e75..564dd382ed 100644 --- a/test/unit_ZeroSet.jl +++ b/test/unit_ZeroSet.jl @@ -33,6 +33,10 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(Z) + # isuniversal + answer, w = isuniversal(Z, true) + @test !isuniversal(Z) && !answer && w ∉ Z + # subset z = ZeroSet{N}(1) s1 = Singleton(N[0]) diff --git a/test/unit_Zonotope.jl b/test/unit_Zonotope.jl index 66a7f80767..75618a1561 100644 --- a/test/unit_Zonotope.jl +++ b/test/unit_Zonotope.jl @@ -59,6 +59,13 @@ for N in [Float64, Rational{Int}, Float32] # isempty @test !isempty(z) + # isuniversal + answer, w = isuniversal(z, true) + @test !isuniversal(z) && !answer && w ∉ z + + # an_element function + @test an_element(z) ∈ z + # concrete operations gens = N[1 1; -1 1] Z1 = Zonotope(N[1, 1], gens)