JuliaReach / LazySets.jl

Scalable symbolic-numeric set computations in Julia
https://juliareach.github.io/LazySets.jl/
Other
226 stars 32 forks source link

Polyhedra from lazy intersections of half-spaces #2353

Closed mforets closed 3 years ago

mforets commented 4 years ago

From a conversation on gitter:

H1 = HalfSpace([1.0, 1.0], 1.0) H2 = HalfSpace([-1.0, -1.0], 1.0)

H1 ∩ H2 HPolyhedron{Float64,Array{Float64,1}}(.....)

H3 = HalfSpace([1.0, 0.0], 3.0) H1 ∩ H2 ∩ H3 HPolyhedron{Float64,Array{Float64,1}}(......)

mforets commented 3 years ago

I have mixed feelings with regard to the proposed change. On one hand it is quite natural that H1 ∩ H2 creates an HPolyhedron because this makes the set much more "usable" than a lazy intersection of half-spaces; on the other hand, the change would let to not always mean a lazy intersection... but mixing concrete with lazy operations is perhaps the main feature of LazySets, so that is kind of against the current.


We should definitely add the missing conversions,

julia> H1 = HalfSpace([1.0, 1.0], 1.0)
HalfSpace{Float64,Array{Float64,1}}([1.0, 1.0], 1.0)

julia> H2 = HalfSpace([-1.0, -1.0], 1.0)
HalfSpace{Float64,Array{Float64,1}}([-1.0, -1.0], 1.0)

julia> H1 ∩ H2
Intersection{Float64,HalfSpace{Float64,Array{Float64,1}},HalfSpace{Float64,Array{Float64,1}}}(HalfSpace{Float64,Array{Float64,1}}([1.0, 1.0], 1.0), HalfSpace{Float64,Array{Float64,1}}([-1.0, -1.0], 1.0), LazySets.IntersectionCache(-1))

julia> convert(HPolyhedron, H1 ∩ H2)
ERROR: MethodError: Cannot `convert` an object of type 
  Intersection{Float64,HalfSpace{Float64,Array{Float64,1}},HalfSpace{Float64,Array{Float64,1}}} to an object of type 
  HPolyhedron
Closest candidates are:
  convert(::Type{HPolyhedron}, ::HPolyhedron) at /home/mforets/.julia/dev/LazySets/src/convert.jl:8
  convert(::Type{HPolyhedron}, ::HPolytope) at /home/mforets/.julia/dev/LazySets/src/convert.jl:1163
  convert(::Type{HPolyhedron}, ::AbstractPolytope) at /home/mforets/.julia/dev/LazySets/src/convert.jl:195
  ...
Stacktrace:
 [1] top-level scope at REPL[5]:1
schillic commented 3 years ago

I agreed that is and should stay lazy here. I do not mind a function to switch between lazy and concrete operations for math symbols. This would actually be not too hard to implement. But we should do this in a new issue.

However, HPolyhedron is not really concrete but rather a hybrid: there are no computations involved when you create them. So I also do not mind this simplification.

We should definitely add the missing conversions

:+1:

mforets commented 3 years ago

However, HPolyhedron is not really concrete but rather a hybrid: there are no computations involved when you create them. So I also do not mind this simplification.

This is an excellent point. This should be understood as a simplification, like the way the library chooses to deal (dispatch) with lazy intersection of halfspaces.