Lazy intersection of lazyset and polytope

[mforets]

See #375.

[mforets]

We want to compute ρ(d, cap::Intersection{N, <:LazySet, HPolytope}...). Can be used for any AbstractPolytope so long as we have the constraints_list method, but this method is not part of the interface API though, so i would suggest to be used as

X = ... # lazy set
Y = convert(HPolytope, P::AbstractPolytope) # efficiency depends on the concrete type of P
ρ(d, X ∩ Y)

In Frehse & Ray, two strategies are outlined to compute ρ(d, X ∩ Y):

1 - if Y has m constraints, consider the optimization problem in the domain R^m with the f to be f(lambda_1, ..., lambda_n) = rho_X(l - sum_i lambda_i a_i) + sum_i lambda_i b_i.

2 - consider the intersection of each constraint in Y with the set X separately.

2 has the advantage that each problem is a univariate optimization problem and we can make use of the function

function ρ(d::AbstractVector{N},
           cap::Intersection{N, <:LazySet, S};
           algorithm::String="line_search",
           check_intersection::Bool=true,
           kwargs...) where {N<:AbstractFloat, S<:Union{HalfSpace, Hyperplane}}

Let g_i = rho_{X \cap {a_i^T x <= bi} (d) be the result of each intersection. They are combined as min_{i=1, ..., m} g_i do give rho_{X \cap Y}(d)^+. The number rho_{X \cap Y}(d)^+ is not necessarily the exact support function, though. But it is an overapproximation: rho_{X \cap Y}(d)^+ >= rho_{X \cap Y}(d). Indeed, since X cap Y is contained in all of the sets X \cap {a_i^T x <= b_i, the inequality follows.

Important! An outer approximation copmuted with rho_{X \cap Y}(d)^+ may be non-empty even though X \cap Y is empty.

[mforets]

🤔 option 2 is more properly a dispatch on overapproximate.

[schillic]

Agreed. I would keep overapproximations out of the play for the default functions such as ρ. Otherwise we never know if the result that we compute is exact or approximate (if we nest operations). I was thinking about a lazy operation Overapproximation once where we allow such things, but this brings a lot of other troubles.

[schillic]

constraints_list will be added in #188.