Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Outsource binary operations to set modules #3604

Merged
merged 8 commits into from
Jul 21, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions docs/make.jl
Original file line number Diff line number Diff line change
@@ -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",
3 changes: 0 additions & 3 deletions docs/src/lib/concrete_binary_operations/cartesian_product.md
Original file line number Diff line number Diff line change
@@ -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)
```
3 changes: 0 additions & 3 deletions docs/src/lib/concrete_binary_operations/convex_hull.md
Original file line number Diff line number Diff line change
@@ -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!
```
14 changes: 0 additions & 14 deletions docs/src/lib/concrete_binary_operations/exact_sum.md

This file was deleted.

2 changes: 0 additions & 2 deletions docs/src/lib/concrete_binary_operations/intersection.md
Original file line number Diff line number Diff line change
@@ -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)
14 changes: 0 additions & 14 deletions docs/src/lib/concrete_binary_operations/linear_combination.md

This file was deleted.

4 changes: 0 additions & 4 deletions docs/src/lib/concrete_binary_operations/minkowski_sum.md
Original file line number Diff line number Diff line change
@@ -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)
```
1 change: 1 addition & 0 deletions docs/src/lib/sets/Line2D.md
Original file line number Diff line number Diff line change
@@ -23,6 +23,7 @@ rand(::Type{Line2D})
project(::AbstractVector, ::Line2D)
σ(::AbstractVector, ::Line2D)
translate(::Line2D, ::AbstractVector)
intersection(::Line2D, ::Line2D)
```

```@meta
4 changes: 4 additions & 0 deletions docs/src/lib/sets/SimpleSparsePolynomialZonotope.md
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions docs/src/lib/sets/SparsePolynomialZonotope.md
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions docs/src/lib/sets/VPolygon.md
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions docs/src/lib/sets/VPolytope.md
Original file line number Diff line number Diff line change
@@ -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
105 changes: 0 additions & 105 deletions src/ConcreteOperations/cartesian_product.jl
Original file line number Diff line number Diff line change
@@ -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)

113 changes: 0 additions & 113 deletions src/ConcreteOperations/convex_hull.jl
Original file line number Diff line number Diff line change
@@ -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
Loading