Skip to content

Commit

Permalink
Merge pull request #2596 from JuliaReach/schillic/1209_hyperplane
Browse files Browse the repository at this point in the history
#1209 - Concrete projection of Hyperplane & Line2D
  • Loading branch information
schillic authored Feb 26, 2021
2 parents a7e6cdc + 37ce92c commit 13fb587
Show file tree
Hide file tree
Showing 7 changed files with 56 additions and 3 deletions.
2 changes: 1 addition & 1 deletion docs/src/lib/sets/HalfSpace.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ tosimplehrep(::AbstractVector{LC}) where {N, LC<:LinearConstraint{N}}
remove_redundant_constraints
remove_redundant_constraints!
complement(::HalfSpace)
project(::HalfSpace, ::AbstractVector{Int})
project(::HalfSpace{N}, ::AbstractVector{Int}) where {N}
```
Inherited from [`LazySet`](@ref):
* [`norm`](@ref norm(::LazySet, ::Real))
Expand Down
4 changes: 2 additions & 2 deletions src/Sets/HalfSpace.jl
Original file line number Diff line number Diff line change
Expand Up @@ -756,10 +756,10 @@ julia> project(H, [1])
Universe{Float64}(1)
```
"""
function project(H::HalfSpace, block::AbstractVector{Int})
function project(H::HalfSpace{N}, block::AbstractVector{Int}) where {N}
if constrained_dimensions(H) block
return HalfSpace(H.a[block], H.b)
else
return Universe(length(block))
return Universe{N}(length(block))
end
end
8 changes: 8 additions & 0 deletions src/Sets/Hyperplane.jl
Original file line number Diff line number Diff line change
Expand Up @@ -478,6 +478,14 @@ function translate(hp::Hyperplane, v::AbstractVector; share::Bool=false)
return Hyperplane(a, b)
end

function project(hp::Hyperplane{N}, block::AbstractVector{Int}) where {N}
if constrained_dimensions(hp) block
return Hyperplane(hp.a[block], hp.b)
else
return Universe{N}(length(block))
end
end

# ============================================
# Functionality that requires ModelingToolkit
# ============================================
Expand Down
26 changes: 26 additions & 0 deletions src/Sets/Line2D.jl
Original file line number Diff line number Diff line change
Expand Up @@ -368,3 +368,29 @@ function translate(L::Line2D, v::AbstractVector; share::Bool=false)
b = L.b + dot(L.a, v)
return Line2D(a, b)
end

function project(L::Line2D{N}, block::AbstractVector{Int}) where {N}
m = length(block)
if m == 2
@assert ispermutation(block, 1:2) "invalid dimensions $block for projection"
return L # no projection
elseif m == 1
# projection to dimension i
cdims = constrained_dimensions(L)
if length(cdims) == 1
@inbounds if cdims[1] == block[1]
# L: aᵢxᵢ = b where aᵢ ≠ 0
return Singleton([L.b / L.a[cdims[1]]])
else
# L: aⱼxⱼ = b where i ≠ j
return Universe{N}(1)
end
else
# L is constrained in both dimensions
@assert length(cdims) == 2
return Universe{N}(1)
end
else
throw(ArgumentError("cannot project a two-dimensional line to $m dimensions"))
end
end
5 changes: 5 additions & 0 deletions test/unit_HalfSpace.jl
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,11 @@ for N in [Float64, Rational{Int}, Float32]
end
end

# projection
H = HalfSpace(N[1, -1], N(0)) # x <= y
@test project(H, [1]) == project(H, [2]) == Universe{N}(1)
@test project(H, [1, 2]) == H

# conversion of the normal vector
hs_sev = HalfSpace(SingleEntryVector(2, 3, N(1)), N(1))
hs_vec = convert(HalfSpace{N, Vector{N}}, hs_sev)
Expand Down
5 changes: 5 additions & 0 deletions test/unit_Hyperplane.jl
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,11 @@ for N in [Float64, Rational{Int}, Float32]
end
end

# projection
H = Hyperplane(N[1, -1], N(0)) # x = y
@test project(H, [1]) == project(H, [2]) == Universe{N}(1)
@test project(H, [1, 2]) == H

@test_throws ArgumentError linear_map(M, H, algorithm="inv")
M = N[2 2; 0 1] # invertible matrix

Expand Down
9 changes: 9 additions & 0 deletions test/unit_Line2D.jl
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,15 @@ for N in [Float64, Rational{Int}, Float32]
@test lm isa Line2D{N, Vector{N}}
@test lm.a N[1/2, -2] && lm.b N(0)

# projection
L = Line2D(N[1, -1], N(0)) # x = y
@test project(L, [1]) == project(L, [2]) == Universe{N}(1)
@test project(L, [1, 2]) == L
L = Line2D(N[2, 0], N(4)) # x = 2
@test project(L, [1]) == Singleton(N[2])
@test project(L, [2]) == Universe{N}(1)
@test project(L, [1, 2]) == L

# translation
@test translate(l1, N[1, 2]) == Line2D(a1, N(3))
end

0 comments on commit 13fb587

Please sign in to comment.