Merge pull request #3604 from JuliaReach/schillic/binary

Outsource binary operations to set modules
JuliaReach · Jul 21, 2024 · f95d739 · f95d739
2 parents 3a7a270 + 92412d3
commit f95d739
Show file tree

Hide file tree

Showing 60 changed files with 591 additions and 581 deletions.
diff --git a/docs/make.jl b/docs/make.jl
@@ -116,9 +116,7 @@ makedocs(; sitename="LazySets.jl",
                                                                   "lib/concrete_binary_operations/convex_hull.md",
                                                                   "lib/concrete_binary_operations/difference.md",
                                                                   "lib/concrete_binary_operations/distance.md",
-                                                                  "lib/concrete_binary_operations/exact_sum.md",
                                                                   "lib/concrete_binary_operations/intersection.md",
-                                                                  "lib/concrete_binary_operations/linear_combination.md",
                                                                   "lib/concrete_binary_operations/minkowski_sum.md",
                                                                   "lib/concrete_binary_operations/minkowski_difference.md",
                                                                   "lib/concrete_binary_operations/isdisjoint.md",

diff --git a/docs/src/lib/concrete_binary_operations/cartesian_product.md b/docs/src/lib/concrete_binary_operations/cartesian_product.md
@@ -10,9 +10,6 @@ CurrentModule = LazySets
 # Cartesian Product
 
 ```@docs
-cartesian_product(::VPolytope, ::VPolytope)
 cartesian_product(::LazySet, ::LazySet)
-cartesian_product(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
-cartesian_product(::SparsePolynomialZonotope, ::SparsePolynomialZonotope)
 cartesian_product(::SparsePolynomialZonotope, ::AbstractZonotope)
 ```
diff --git a/docs/src/lib/concrete_binary_operations/convex_hull.md b/docs/src/lib/concrete_binary_operations/convex_hull.md
@@ -12,9 +12,6 @@ CurrentModule = LazySets
 ```@docs
 convex_hull(::LazySet, ::LazySet)
 convex_hull(::HPoly, ::HPoly)
-convex_hull(::VPolytope, ::VPolytope)
-convex_hull(::VPolygon, ::VPolygon)
 convex_hull(::Vector{VN}) where {N, VN<:AbstractVector{N}}
-convex_hull(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
 monotone_chain!
 ```
diff --git a/docs/src/lib/concrete_binary_operations/exact_sum.md b/docs/src/lib/concrete_binary_operations/exact_sum.md
diff --git a/docs/src/lib/concrete_binary_operations/intersection.md b/docs/src/lib/concrete_binary_operations/intersection.md
@@ -11,15 +11,13 @@ CurrentModule = LazySets
 
 ```@docs
 intersection(::AbstractSingleton, ::LazySet)
-intersection(::Line2D, ::Line2D)
 intersection(::AbstractHyperrectangle, ::AbstractHyperrectangle)
 intersection(::Interval, ::HalfSpace)
 intersection(::Interval, ::Hyperplane)
 intersection(::Interval, ::LazySet)
 intersection(::AbstractHPolygon, ::AbstractHPolygon)
 intersection(::AbstractPolyhedron{N}, ::AbstractPolyhedron{N}) where {N}
 intersection(::Union{VPolytope, VPolygon}, ::Union{VPolytope, VPolygon})
-intersection(::VPolygon, ::VPolygon; ::Bool=true)
 intersection(::UnionSet, ::LazySet)
 intersection(::UnionSetArray, ::LazySet)
 intersection(::Universe, ::LazySet)

diff --git a/docs/src/lib/concrete_binary_operations/linear_combination.md b/docs/src/lib/concrete_binary_operations/linear_combination.md
diff --git a/docs/src/lib/concrete_binary_operations/minkowski_sum.md b/docs/src/lib/concrete_binary_operations/minkowski_sum.md
@@ -12,12 +12,8 @@ CurrentModule = LazySets
 ```@docs
 minkowski_sum(::LazySet, ::LazySet)
 minkowski_sum(::AbstractPolyhedron, ::AbstractPolyhedron)
-minkowski_sum(::VPolytope, ::VPolytope)
 minkowski_sum(::AbstractHyperrectangle, ::AbstractHyperrectangle)
 minkowski_sum(::AbstractZonotope, ::AbstractZonotope)
-minkowski_sum(::VPolygon, ::VPolygon)
 minkowski_sum(::DensePolynomialZonotope, ::AbstractZonotope)
 minkowski_sum(::AbstractSingleton, ::AbstractSingleton)
-minkowski_sum(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
-minkowski_sum(::SparsePolynomialZonotope, ::SparsePolynomialZonotope)
 ```
diff --git a/docs/src/lib/sets/Line2D.md b/docs/src/lib/sets/Line2D.md
@@ -23,6 +23,7 @@ rand(::Type{Line2D})
 project(::AbstractVector, ::Line2D)
 σ(::AbstractVector, ::Line2D)
 translate(::Line2D, ::AbstractVector)
+intersection(::Line2D, ::Line2D)
 ```
 
 ```@meta

diff --git a/docs/src/lib/sets/SimpleSparsePolynomialZonotope.md b/docs/src/lib/sets/SimpleSparsePolynomialZonotope.md
@@ -21,6 +21,10 @@ remove_redundant_generators(::SimpleSparsePolynomialZonotope)
 linear_map(::AbstractMatrix, ::SimpleSparsePolynomialZonotope)
 quadratic_map(::Vector{MT}, ::SimpleSparsePolynomialZonotope) where {N, MT<:AbstractMatrix{N}}
 quadratic_map(::Vector{MT}, ::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope) where {N, MT<:AbstractMatrix{N}}
+cartesian_product(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
+convex_hull(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
+linear_combination(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
+minkowski_sum(::SimpleSparsePolynomialZonotope, ::SimpleSparsePolynomialZonotope)
 ```
 
 ```@meta

diff --git a/docs/src/lib/sets/SparsePolynomialZonotope.md b/docs/src/lib/sets/SparsePolynomialZonotope.md
@@ -24,6 +24,9 @@ linear_map(::AbstractMatrix, ::SparsePolynomialZonotope)
 reduce_order(::SparsePolynomialZonotope, ::Real, ::AbstractReductionMethod=GIR05())
 ρ(::AbstractVector, ::SparsePolynomialZonotope)
 translate(::SparsePolynomialZonotope, ::AbstractVector)
+cartesian_product(::SparsePolynomialZonotope, ::SparsePolynomialZonotope)
+exact_sum(::SparsePolynomialZonotope, ::SparsePolynomialZonotope)
+minkowski_sum(::SparsePolynomialZonotope, ::SparsePolynomialZonotope)
 ```
 
 ```@meta

diff --git a/docs/src/lib/sets/VPolygon.md b/docs/src/lib/sets/VPolygon.md
@@ -32,6 +32,9 @@ permute(::VPolygon, ::AbstractVector{Int})
 σ(::AbstractVector, ::VPolygon)
 translate(::VPolygon, ::AbstractVector)
 translate!(::VPolygon, ::AbstractVector)
+convex_hull(::VPolygon, ::VPolygon)
+intersection(::VPolygon, ::VPolygon; ::Bool=true)
+minkowski_sum(::VPolygon, ::VPolygon)
 ```
 
 ```@meta

diff --git a/docs/src/lib/sets/VPolytope.md b/docs/src/lib/sets/VPolytope.md
@@ -32,6 +32,9 @@ linear_map(::AbstractMatrix, ::VPolytope)
 σ(::AbstractVector, ::VPolytope)
 translate(::VPolytope, ::AbstractVector)
 translate!(::VPolytope, ::AbstractVector)
+cartesian_product(::VPolytope, ::VPolytope)
+convex_hull(::VPolytope, ::VPolytope)
+minkowski_sum(::VPolytope, ::VPolytope)
 ```
 
 ```@meta

diff --git a/src/ConcreteOperations/cartesian_product.jl b/src/ConcreteOperations/cartesian_product.jl
@@ -66,50 +66,6 @@ function cartesian_product(X::LazySet, Y::LazySet; backend=nothing,
     return Pout
 end
 
-"""
-    cartesian_product(P1::VPolytope, P2::VPolytope; [backend]=nothing)
-
-Compute the Cartesian product of two polytopes in vertex representation.
-
-### Input
-
-- `P1`      -- polytope in vertex representation
-- `P2`      -- polytope in vertex representation
-- `backend` -- (optional, default: `nothing`) backend for polyhedral computation
-
-### Output
-
-The `VPolytope` obtained by the concrete Cartesian product of `P1` and `P2`.
-
-### Notes
-
-For further information on the supported backends see
-[Polyhedra's documentation](https://juliapolyhedra.github.io/).
-"""
-function cartesian_product(P1::VPolytope, P2::VPolytope; backend=nothing)
-    require(@__MODULE__, :Polyhedra; fun_name="cartesian_product")
-
-    return _cartesian_product_vrep(P1, P2; backend1=backend, backend2=backend)
-end
-
-function _cartesian_product_vrep(P1, P2; backend1=nothing, backend2=nothing)
-    if isnothing(backend1)
-        backend1 = default_polyhedra_backend(P1)
-    end
-    if isnothing(backend2)
-        backend2 = default_polyhedra_backend(P2)
-    end
-
-    P1′ = polyhedron(P1; backend=backend1)
-    P2′ = polyhedron(P2; backend=backend2)
-    Pout = Polyhedra.vcartesianproduct(P1′, P2′)
-    return VPolytope(Pout)
-end
-
-function cartesian_product(U1::Universe, U2::Universe)
-    return Universe(dim(U1) + dim(U2))
-end
-
 function _cartesian_product_hrep(X::S1, Y::S2) where {S1<:LazySet,S2<:LazySet}
     N = promote_type(eltype(X), eltype(Y))
     U1 = Universe{N}(dim(X))
@@ -200,67 +156,6 @@ function cartesian_product(U::Universe, H::HalfSpace)
     return HalfSpace(prepend_zeros(H.a, dim(U)), H.b)
 end
 
-"""
-    cartesian_product(P1::SimpleSparsePolynomialZonotope,
-                      P2::SimpleSparsePolynomialZonotope)
-
-Compute the Cartesian product of two simple sparse polynomial zonotopes.
-
-### Input
-
-- `P1` -- simple sparse polynomial zonotope
-- `P2` -- simple sparse polynomial zonotope
-
-### Output
-
-The Cartesian product of `P1` and `P2`.
-
-### Algorithm
-
-This method implements Proposition 3.1.22 in [1].
-
-[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application
-    to verification of cyber-physical systems.* PhD diss., Technische Universität
-    München, 2022.
-"""
-function cartesian_product(P1::SimpleSparsePolynomialZonotope,
-                           P2::SimpleSparsePolynomialZonotope)
-    c = vcat(center(P1), center(P2))
-    G = cat(genmat(P1), genmat(P2); dims=(1, 2))
-    E = cat(expmat(P1), expmat(P2); dims=(1, 2))
-    return SimpleSparsePolynomialZonotope(c, G, E)
-end
-
-"""
-    cartesian_product(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)
-
-Compute the Cartesian product of two sparse polynomial zonotopes.
-
-### Input
-
-- `P1` -- sparse polynomial zonotope
-- `P2` -- sparse polynomial zonotope
-
-### Output
-
-The Cartesian product of `P1` and `P2`.
-
-### Algorithm
-
-This method implements Proposition 3.1.22 in [1].
-
-[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application
-    to verification of cyber-physical systems.* PhD diss., Technische Universität
-    München, 2022.
-"""
-function cartesian_product(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)
-    c = vcat(center(P1), center(P2))
-    G = cat(genmat_dep(P1), genmat_dep(P2); dims=(1, 2))
-    GI = cat(genmat_indep(P1), genmat_indep(P2); dims=(1, 2))
-    E = cat(expmat(P1), expmat(P2); dims=(1, 2))
-    return SparsePolynomialZonotope(c, G, GI, E)
-end
-
 """
     cartesian_product(SPZ::SparsePolynomialZonotope, Z::AbstractZonotope)
 

diff --git a/src/ConcreteOperations/convex_hull.jl b/src/ConcreteOperations/convex_hull.jl
@@ -465,119 +465,6 @@ function monotone_chain!(points::Vector{VN}; sort::Bool=true) where {N,VN<:Abstr
     return resize!(points, m)
 end
 
-"""
-    convex_hull(P::VPolygon, Q::VPolygon; [algorithm]::String="monotone_chain")
-
-Return the convex hull of two polygons in vertex representation.
-
-### Input
-
-- `P`         -- polygon in vertex representation
-- `Q`         -- polygon in vertex representation
-- `algorithm` -- (optional, default: "monotone_chain") the algorithm used to
-                 compute the convex hull
-
-### Output
-
-A new polygon such that its vertices are the convex hull of the two polygons.
-
-### Notes
-
-The vertices of the output polygon are sorted in counter-clockwise fashion.
-"""
-function convex_hull(P::VPolygon, Q::VPolygon;
-                     algorithm::String="monotone_chain")
-    vunion = [P.vertices; Q.vertices]
-    convex_hull!(vunion; algorithm=algorithm)
-    return VPolygon(vunion; apply_convex_hull=false)
-end
-
-"""
-    convex_hull(P1::VPolytope, P2::VPolytope; [backend]=nothing)
-
-Compute the convex hull of two polytopes in vertex representation.
-
-### Input
-
-- `P1`      -- polytope in vertex representation
-- `P2`      -- polytope in vertex representation
-- `backend` -- (optional, default: `nothing`) the polyhedral computation backend
-
-### Output
-
-The `VPolytope` obtained by the concrete convex hull of `P1` and `P2`.
-
-### Notes
-
-This function takes the union of the vertices of each polytope and then relies
-on a concrete convex-hull algorithm.
-For low dimensions, a specialized implementation for polygons is used.
-For higher dimensions, `convex_hull` relies on the polyhedral backend that can
-be specified using the `backend` keyword argument.
-
-For performance reasons, it is suggested to use the `CDDLib.Library()` backend.
-"""
-function convex_hull(P1::VPolytope, P2::VPolytope; backend=nothing)
-    vunion = [P1.vertices; P2.vertices]
-    convex_hull!(vunion; backend=backend)
-    return VPolytope(vunion)
-end
-
-"""
-    convex_hull(P1::HPoly, P2::HPoly;
-               [backend]=default_polyhedra_backend(P1))
-
-Compute the convex hull of the set union of two polyhedra in constraint
-representation.
-
-### Input
-
-- `P1`      -- polyhedron
-- `P2`      -- polyhedron
-- `backend` -- (optional, default: `default_polyhedra_backend(P1)`) the
-               backend for polyhedral computations
-
-### Output
-
-The `HPolyhedron` (resp. `HPolytope`) obtained by the concrete convex hull of
-`P1` and `P2`.
-
-### Notes
-
-For performance reasons, it is suggested to use the `CDDLib.Library()` backend
-for the `convex_hull`.
-
-For further information on the supported backends see
-[Polyhedra's documentation](https://juliapolyhedra.github.io/).
-"""
-function convex_hull(P1::HPoly, P2::HPoly;
-                     backend=default_polyhedra_backend(P1))
-    require(@__MODULE__, :Polyhedra; fun_name="convex_hull")
-    Pch = Polyhedra.convexhull(polyhedron(P1; backend=backend),
-                               polyhedron(P2; backend=backend))
-    removehredundancy!(Pch)
-    return convert(basetype(P1), Pch)
-end
-
 @commutative function convex_hull(X::LazySet, ::EmptySet)
     return convex_hull(X)
 end
-
-"""
-    convex_hull(P1::SimpleSparsePolynomialZonotope,
-                P2::SimpleSparsePolynomialZonotope)
-
-Compute the convex hull of two simple sparse polynomial zonotopes.
-
-### Input
-
-- `P1` : simple sparse polynomial zonotopes
-- `P2` : simple sparse polynomial zonotopes
-
-### Output
-
-Tightest convex simple sparse polynomial zonotope containing `P1` and `P2`.
-"""
-function convex_hull(P1::SimpleSparsePolynomialZonotope, P2::SimpleSparsePolynomialZonotope)
-    return linear_combination(linear_combination(P1, P1), linear_combination(P2, P2))
-end