HalfSpace: revise docs entries, shorten docs, shorten signatures, move and fix isdisjoint method

docs/src/lib/sets/HalfSpace.md

@@ -9,41 +9,216 @@ HalfSpace
 LinearConstraint
 ```
 
+## Conversion
+
+```julia
+convert(::Type{HalfSpace{N,Vector{N}}}, hs::HalfSpace{N,<:AbstractVector{N}}) where {N}
+```
+
+The following method requires the [`SymEngine`](https://github.com/symengine/SymEngine.jl) package.
+
+```@docs
+LazySets.convert(::Type{HalfSpace{N}}, ::Expr; vars::Vector{Basic}=Basic[]) where {N}
+```
+
 ## Operations
 
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+an_element(::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
 ```@docs
 an_element(::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+complement(::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 complement(::HalfSpace)
 constrained_dimensions(::HalfSpace)
-constraints_list(::HalfSpace)
-dim(::HalfSpace)
-isbounded(::HalfSpace)
-isempty(::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+isuniversal(::LazySet, ::Bool=false)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 isuniversal(::HalfSpace, ::Bool=false)
 normalize(::HalfSpace{N}, p::Real=N(2)) where {N}
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+rand(::Type{LazySet})
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 rand(::Type{HalfSpace})
-distance(::AbstractVector, ::HalfSpace{N}) where {N}
+distance(::AbstractVector, ::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+∈(::AbstractVector, ::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 ∈(::AbstractVector, ::HalfSpace)
-halfspace_left(::AbstractVector, ::AbstractVector)
-halfspace_right(::AbstractVector, ::AbstractVector)
-iscomplement(::HalfSpace{N}, ::HalfSpace) where {N}
-project(::HalfSpace{N}, ::AbstractVector{Int}) where {N}
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+project(::LazySet, ::AbstractVector{Int})
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
+project(::HalfSpace, ::AbstractVector{Int})
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+ρ(::AbstractVector, ::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 ρ(::AbstractVector, ::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+σ(::AbstractVector, ::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 σ(::AbstractVector, ::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+translate(::LazySet, ::AbstractVector)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
 translate(::HalfSpace, ::AbstractVector)
+iscomplement(::HalfSpace, ::HalfSpace)
+```
+```@meta
+CurrentModule = LazySets.API
+```
+```@docs; canonical=false
+isdisjoint(::LazySet, ::LazySet)
+```
+```@meta
+CurrentModule = LazySets.HalfSpaceModule
+```
+```@docs
+isdisjoint(::HalfSpace, ::HalfSpace)
+```
+
+```@docs
+halfspace_left(::AbstractVector, ::AbstractVector)
+halfspace_right(::AbstractVector, ::AbstractVector)
+HalfSpaceModule._ishalfspace
 ```
 
+```@meta
+CurrentModule = LazySets.API
+```
+
+Undocumented implementations:
+
+* [`constraints_list`](@ref constraints_list(::LazySet))
+* [`dim`](@ref dim(::LazySet))
+* [`isbounded`](@ref isbounded(::LazySet))
+* [`isempty`](@ref isempty(::LazySet))
+* [`isoperationtype`](@ref isoperationtype(::Type{LazySet}))
+* [`permute`](@ref permute(::LazySet, ::AbstractVector{Int}))
+
 ```@meta
 CurrentModule = LazySets
 ```
 
 Inherited from [`LazySet`](@ref):
-* [`diameter`](@ref diameter(::LazySet, ::Real))
-* [`high`](@ref high(::LazySet))
-* [`low`](@ref low(::LazySet))
-* [`norm`](@ref norm(::LazySet, ::Real))
-* [`radius`](@ref radius(::LazySet, ::Real))
+* [`area`](@ref area(::LazySet))
+* [`concretize`](@ref concretize(::LazySet))
+* [`constraints`](@ref constraints(::LazySet))
+* [`convex_hull`](@ref convex_hull(::LazySet))
+* `copy(::Type{LazySet})`
+* [`diameter`](@ref diameter(::LazySet, ::Real=Inf))
+* [`eltype`](@ref eltype(::Type{<:LazySet}))
+* [`eltype`](@ref eltype(::LazySet))
+* [`isboundedtype`](@ref isboundedtype(::Type{LazySet}))
+* [`isoperation`](@ref isoperation(::LazySet))
+* [`norm`](@ref norm(::LazySet, ::Real=Inf))
+* [`radius`](@ref radius(::LazySet, ::Real=Inf))
+* [`rectify`](@ref rectify(::LazySet))
 * [`reflect`](@ref reflect(::LazySet))
+* [`singleton_list`](@ref singleton_list(::LazySet))
+* [`surface`](@ref surface(::LazySet))
+* [`vertices`](@ref vertices(::LazySet))
+* [`affine_map`](@ref affine_map(::AbstractMatrix, ::LazySet, ::AbstractVector))
+* [`exponential_map`](@ref exponential_map(::AbstractMatrix, ::LazySet))
+* [`is_interior_point`](@ref is_interior_point(::AbstractVector, ::LazySet))
+* [`linear_map`](@ref linear_map(::AbstractMatrix, ::LazySet))
+* [`sample`](@ref sample(::LazySet, ::Int=1))
+* [`scale`](@ref scale(::Real, ::LazySet))
+* [`cartesian_product`](@ref cartesian_product(::LazySet, ::LazySet))
+* [`convex_hull`](@ref convex_hull(::LazySet, ::LazySet))
+* [`difference`](@ref difference(::LazySet, ::LazySet))
+* [`distance`](@ref distance(::LazySet, ::LazySet; ::Real=2.0))
+* [`exact_sum`](@ref exact_sum(::LazySet, ::LazySet))
+* [`≈`](@ref ≈(::LazySet, ::LazySet))
+* [`==`](@ref ==(::LazySet, ::LazySet))
+* [`isequivalent`](@ref isequivalent(::LazySet, ::LazySet))
+* [`⊂`](@ref ⊂(::LazySet, ::LazySet))
+* [`minkowski_difference`](@ref minkowski_difference(::LazySet, ::LazySet))
+
+Inherited from [`ConvexSet`](@ref):
+* [`linear_combination`](@ref linear_combination(::ConvexSet, ::ConvexSet))
 
 Inherited from [`AbstractPolyhedron`](@ref):
-* [`linear_map`](@ref linear_map(::AbstractMatrix, ::AbstractPolyhedron))
+* [`extrema`](@ref extrema(::AbstractPolyhedron))
+* [`extrema`](@ref extrema(::AbstractPolyhedron, ::Int))
+* [`high`](@ref high(::AbstractPolyhedron))
+* [`high`](@ref high(::AbstractPolyhedron, ::Int))
+* [`isconvextype`](@ref isconvextype(::Type{AbstractPolyhedron}))
+* [`ispolyhedral`](@ref ispolyhedral(::AbstractPolyhedron))
+* [`low`](@ref low(::AbstractPolyhedron))
+* [`low`](@ref low(::AbstractPolyhedron, ::Int))
+* [`vertices_list`](@ref vertices_list(::AbstractPolyhedron))
+* [`intersection`](@ref intersection(::AbstractPolyhedron, ::AbstractPolyhedron))
+* [`⊆`](@ref ⊆(::LazySet, ::AbstractPolyhedron))
+* [`minkowski_sum`](@ref minkowski_sum(::AbstractPolyhedron, ::AbstractPolyhedron))

docs/src/lib/sets/Hyperplane.md

@@ -120,6 +120,10 @@ CurrentModule = LazySets.HyperplaneModule
 translate(::Hyperplane, ::AbstractVector)
 ```
 
+```@docs
+HyperplaneModule._ishyperplanar
+```
+
 ```@meta
 CurrentModule = LazySets.API
 ```

docs/src/lib/utils.md

@@ -61,9 +61,6 @@ LazySets._vec
 ```@docs
 LazySets.free_symbols
 LazySets._is_linear_combination
-LazySets._ishalfspace
-LazySets._ishyperplanar
-LazySets.convert(::Type{HalfSpace{N}}, ::Expr; vars::Vector{Basic}=Basic[]) where {N}
 ```
 
 ## Functions for numbers

src/ConcreteOperations/isdisjoint.jl

@@ -539,78 +539,6 @@ The support vector is thus also a witness if the sets are not disjoint.
     return _isdisjoint_halfspace(hs, X, witness)
 end
 
-"""
-    isdisjoint(H1::HalfSpace, H2::HalfSpace, [witness]::Bool=false)
-
-Check whether two half-spaces do not intersect, and otherwise optionally compute
-a witness.
-
-### Input
-
-- `H1`     -- half-space
-- `H2`     -- half-space
-- `witness` -- (optional, default: `false`) compute a witness if activated
-
-### Output
-
-* If `witness` option is deactivated: `true` iff ``H1 ∩ H2 = ∅``
-* If `witness` option is activated:
-  * `(true, [])` iff ``H1 ∩ H2 = ∅``
-  * `(false, v)` iff ``H1 ∩ H2 ≠ ∅`` and ``v ∈ H1 ∩ H2``
-
-### Algorithm
-
-Two half-spaces do not intersect if and only if their normal vectors point in
-the opposite direction and there is a gap between the two defining hyperplanes.
-
-The latter can be checked as follows:
-Let ``H1 : a_1⋅x = b_1`` and ``H2 : a_2⋅x = b_2``.
-Then we already know that ``a_2 = -k⋅a_1`` for some positive scaling factor
-``k``.
-Let ``x_1`` be a point on the defining hyperplane of ``H1``.
-We construct a line segment from ``x_1`` to the point ``x_2`` on the defining
-hyperplane of ``hs_2`` by shooting a ray from ``x_1`` with direction ``a_1``.
-Thus we look for a factor ``s`` such that ``(x_1 + s⋅a_1)⋅a_2 = b_2``.
-This gives us ``s = (b_2 - x_1⋅a_2) / (-k a_1⋅a_1)``.
-The gap exists if and only if ``s`` is positive.
-
-If the normal vectors do not point in opposite directions, then the defining
-hyperplanes intersect and we can produce a witness as follows.
-All points ``x`` in this intersection satisfy ``a_1⋅x = b_1`` and
-``a_2⋅x = b_2``. Thus we have ``(a_1 + a_2)⋅x = b_1+b_2``.
-We now find a dimension where ``a_1 + a_2`` is non-zero, say, ``i``.
-Then the result is a vector with one non-zero entry in dimension ``i``, defined
-as ``[0, …, 0, (b_1 + b_2)/(a_1[i] + a_2[i]), 0, …, 0]``.
-Such a dimension ``i`` always exists.
-"""
-function isdisjoint(H1::HalfSpace, H2::HalfSpace, witness::Bool=false)
-    a1 = H1.a
-    a2 = H2.a
-    N = promote_type(eltype(H1), eltype(H2))
-    issamedir, k = samedir(a1, -a2)
-    if issamedir
-        x1 = an_element(Hyperplane(a1, H1.b))
-        b2 = H2.b
-        s = (b2 - dot(x1, a2)) / (-k * dot(a1, a1))
-        empty_intersection = s > 0
-        # if `!empty_intersection`, x1 is a witness because both defining
-        # hyperplanes are contained in each half-space
-        return _witness_result_empty(witness, empty_intersection, H1, H2, x1)
-    elseif !witness
-        return false
-    end
-    # compute witness
-    v = zeros(N, length(a1))
-    for i in eachindex(a1)
-        a_sum_i = a1[i] + a2[i]
-        if a_sum[i] != 0
-            v[i] = (H1.b + H2.b) / a_sum_i
-            break
-        end
-    end
-    return (false, v)
-end
-
 # disambiguations
 for ST in [:AbstractPolyhedron, :AbstractZonotope, :Hyperplane, :Line2D,
            :CartesianProductArray]

src/Sets/HalfSpace/HalfSpaceModule.jl

@@ -14,9 +14,10 @@ using ReachabilityBase.Require: require
 
 @reexport import ..API: an_element, complement, constraints_list, dim,
                         isbounded, isempty, isoperationtype, isuniversal, rand,
-                        distance, ∈, permute, project, ρ, σ, translate
+                        distance, ∈, permute, project, ρ, σ, translate,
+                        isdisjoint
 @reexport import ..LazySets: constrained_dimensions, normalize
-import ..LazySets: _ishalfspace, _linear_map_hrep_helper
+import ..LazySets: _ishalfspace, _linear_map_hrep_helper, _witness_result_empty
 import ..Base: convert
 @reexport using ..API
 
@@ -43,13 +44,14 @@ include("project.jl")
 include("support_function.jl")
 include("support_vector.jl")
 include("translate.jl")
+include("isdisjoint.jl")
 
-include("constrained_dimensions.jl")
 include("halfspace_left.jl")
 include("halfspace_right.jl")
-include("iscomplement.jl")
+include("constrained_dimensions.jl")
 include("ishalfspace.jl")
 include("normalize.jl")
+include("iscomplement.jl")
 
 include("convert.jl")
 

src/Sets/HalfSpace/an_element.jl

@@ -1,15 +1,11 @@
 """
-    an_element(hs::HalfSpace)
-
-Return some element of a half-space.
+# Extended help
 
-### Input
-
-- `hs` -- half-space
+    an_element(hs::HalfSpace)
 
 ### Output
 
-An element on the defining hyperplane.
+This method returns an element on the defining hyperplane.
 """
 function an_element(hs::HalfSpace)
     return _an_element_helper_hyperplane(hs.a, hs.b)