Binary Functions on Sets

isdisjoint(X, Y)

An alternative name for is_intersection_empty(X, Y).

is_intersection_empty(X::LazySet{N},
                      Y::LazySet{N},
                      witness::Bool=false
                      )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two sets do not intersect, and otherwise optionally compute a witness.

Input

• X – set
• Y – another set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $X ∩ Y = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ Y = ∅$
  • (false, v) iff $X ∩ Y ≠ ∅$ and $v ∈ X ∩ Y$

Algorithm

This is a fallback implementation that computes the concrete intersection, intersection, of the given sets.

A witness is constructed using the an_element implementation of the result.

is_intersection_empty(H1::AbstractHyperrectangle{N},
                      H2::AbstractHyperrectangle{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two hyperrectangles do not intersect, and otherwise optionally compute a witness.

Input

• H1 – first hyperrectangle
• H2 – second hyperrectangle
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $H1 ∩ H2 = ∅$
• If witness option is activated:
  • (true, []) iff $H1 ∩ H2 = ∅$
  • (false, v) iff $H1 ∩ H2 ≠ ∅$ and $v ∈ H1 ∩ H2$

Algorithm

$H1 ∩ H2 ≠ ∅$ iff $|c_2 - c_1| ≤ r_1 + r_2$, where $≤$ is taken component-wise.

A witness is computed by starting in one center and moving toward the other center for as long as the minimum of the radius and the center distance. In other words, the witness is the point in H1 that is closest to the center of H2.

is_intersection_empty(X::LazySet{N},
                      S::AbstractSingleton{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a convex set and a singleton do not intersect, and otherwise optionally compute a witness.

Input

• X – convex set
• S – singleton
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S ∩ X = ∅$
• If witness option is activated:
  • (true, []) iff $S ∩ X = ∅$
  • (false, v) iff $S ∩ X ≠ ∅$ and v = element(S) $∈ S ∩ X$

Algorithm

$S ∩ X = ∅$ iff element(S) $∉ X$.

is_intersection_empty(H::AbstractHyperrectangle{N},
                      S::AbstractSingleton{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a hyperrectangle and a singleton do not intersect, and otherwise optionally compute a witness.

Input

• H – hyperrectangle
• S – singleton
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $H ∩ S = ∅$
• If witness option is activated:
  • (true, []) iff $H ∩ S = ∅$
  • (false, v) iff $H ∩ S ≠ ∅$ and v = element(S) $∈ H ∩ S$

Algorithm

$H ∩ S = ∅$ iff element(S) $∉ H$.

is_intersection_empty(S1::AbstractSingleton{N},
                      S2::AbstractSingleton{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two singletons do not intersect, and otherwise optionally compute a witness.

Input

• S1 – first singleton
• S2 – second singleton
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S1 ∩ S2 = ∅$
• If witness option is activated:
  • (true, []) iff $S1 ∩ S2 = ∅$
  • (false, v) iff $S1 ∩ S2 ≠ ∅$ and v = element(S1) $∈ S1 ∩ S2$

Algorithm

$S1 ∩ S2 = ∅$ iff $S1 ≠ S2$.

is_intersection_empty(Z::Zonotope{N}, H::Hyperplane{N}, witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a zonotope and a hyperplane do not intersect, and otherwise optionally compute a witness.

Input

• Z – zonotope
• H – hyperplane
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $Z ∩ H = ∅$
• If witness option is activated:
  • (true, []) iff $Z ∩ H = ∅$
  • (false, v) iff $Z ∩ H ≠ ∅$ and $v ∈ Z ∩ H$

Algorithm

$Z ∩ H = ∅$ iff $(b - a⋅c) ∉ \left[ ± ∑_{i=1}^p |a⋅g_i| \right]$, where $a$, $b$ are the hyperplane coefficients, $c$ is the zonotope's center, and $g_i$ are the zonotope's generators.

For witness production we fall back to a less efficient implementation for general sets as the first argument.

is_intersection_empty(B1::Ball2{N},
                      B2::Ball2{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:AbstractFloat}

Check whether two balls in the 2-norm do not intersect, and otherwise optionally compute a witness.

Input

• B1 – first ball in the 2-norm
• B2 – second ball in the 2-norm
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $B1 ∩ B2 = ∅$
• If witness option is activated:
  • (true, []) iff $B1 ∩ B2 = ∅$
  • (false, v) iff $B1 ∩ B2 ≠ ∅$ and $v ∈ B1 ∩ B2$

Algorithm

$B1 ∩ B2 = ∅$ iff $‖ c_2 - c_1 ‖_2 > r_1 + r_2$.

A witness is computed depending on the smaller/bigger ball (to break ties, choose B1 for the smaller ball) as follows.

• If the smaller ball's center is contained in the bigger ball, we return it.
• Otherwise start in the smaller ball's center and move toward the other center until hitting the smaller ball's border. In other words, the witness is the point in the smaller ball that is closest to the center of the bigger ball.

is_intersection_empty(ls1::LineSegment{N},
                      ls2::LineSegment{N},
                      witness::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two line segments do not intersect, and otherwise optionally compute a witness.

Input

• ls1 – first line segment
• ls2 – second line segment
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $ls1 ∩ ls2 = ∅$
• If witness option is activated:
  • (true, []) iff $ls1 ∩ ls2 = ∅$
  • (false, v) iff $ls1 ∩ ls2 ≠ ∅$ and $v ∈ ls1 ∩ ls2$

Algorithm

The algorithm is inspired from here, which again is the special 2D case of a 3D algorithm by Ronald Goldman's article on the Intersection of two lines in three-space in Graphics Gems, Andrew S. (ed.), 1990.

We first check if the two line segments are parallel, and if so, if they are collinear. In the latter case, we check containment of any of the end points in the other line segment. Otherwise the lines are not parallel, so we can solve an equation of the intersection point, if it exists.

is_intersection_empty(X::LazySet{N},
                      hp::Union{Hyperplane{N}, Line{N}},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a compact set an a hyperplane do not intersect, and otherwise optionally compute a witness.

Input

• X – compact set
• hp – hyperplane
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $X ∩ hp = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ hp = ∅$
  • (false, v) iff $X ∩ hp ≠ ∅$ and $v ∈ X ∩ hp$

Notes

We assume that X is compact. Otherwise, the support vector queries may fail.

Algorithm

A compact convex set intersects with a hyperplane iff the support function in the negative resp. positive direction of the hyperplane's normal vector $a$ is to the left resp. right of the hyperplane's constraint $b$:

For witness generation, we compute a line connecting the support vectors to the left and right, and then take the intersection of the line with the hyperplane. We follow this algorithm for the line-hyperplane intersection.

is_intersection_empty(X::LazySet{N},
                      hs::HalfSpace{N},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a compact set an a half-space do not intersect, and otherwise optionally compute a witness.

Input

• X – compact set
• hs – half-space
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $X ∩ hs = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ hs = ∅$
  • (false, v) iff $X ∩ hs ≠ ∅$ and $v ∈ X ∩ hs$

Notes

We assume that X is compact. Otherwise, the support vector queries may fail.

Algorithm

A compact convex set intersects with a half-space iff the support vector in the negative direction of the half-space's normal vector $a$ is contained in the half-space: $σ(-a) ∈ hs$. The support vector is thus also a witness.

Optional keyword arguments can be passed to the ρ function. In particular, if X is a lazy intersection, options can be passed to the line search algorithm.

is_intersection_empty(hs1::HalfSpace{N},
                      hs2::HalfSpace{N},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two half-spaces do not intersect, and otherwise optionally compute a witness.

Input

• hs1 – half-space
• hs2 – half-space
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $hs1 ∩ hs2 = ∅$
• If witness option is activated:
  • (true, []) iff $hs1 ∩ hs2 = ∅$
  • (false, v) iff $hs1 ∩ hs2 ≠ ∅$ and $v ∈ hs1 ∩ hs2$

Algorithm

Two half-spaces do not intersect if and only if their normal vectors point in the opposite direction and there is a gap between the two defining hyperplanes.

The latter can be checked as follows: Let $hs_1 : a_1⋅x = b_1$ and $hs2 : a_2⋅x = b_2$. Then we already know that $a_2 = -k⋅a_1$ for some positive scaling factor $k$. Let $x_1$ be a point on the defining hyperplane of $hs_1$. We construct a line segment from $x_1$ to the point $x_2$ on the defining hyperplane of $hs_2$ by shooting a ray from $x_1$ with direction $a_1$. Thus we look for a factor $s$ such that $(x_1 + s⋅a_1)⋅a_2 = b_2$. This gives us $s = (b_2 - x_1⋅a_2) / (-k a_1⋅a_1)$. The gap exists if and only if $s$ is positive.

If the normal vectors do not point in opposite directions, then the defining hyperplanes intersect and we can produce a witness as follows. All points $x$ in this intersection satisfy $a_1⋅x = b_1$ and $a_2⋅x = b_2$. Thus we have $(a_1 + a_2)⋅x = b_1+b_2$. We now find a dimension where $a_1 + a_2$ is non-zero, say, $i$. Then the result is a vector with one non-zero entry in dimension $i$, defined as $[0, …, 0, (b_1 + b_2)/(a_1[i] + a_2[i]), 0, …, 0]$. Such a dimension $i$ always exists.

is_intersection_empty(P::Union{HPolyhedron{N}, AbstractPolytope{N}},
                      X::LazySet{N},
                      witness::Bool=false;
                      solver=GLPKSolverLP(method=:Simplex)
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two polyhedra do not intersect.

Input

• P – polyhedron
• X – another set (see the Notes section below)
• witness – (optional, default: false) compute a witness if activated
• solver – (optional, default: GLPKSolverLP(method=:Simplex)) LP solver backend
• algorithm – (optional, default: "exact") algorithm keyword, one of: * "exact" (exact, uses a feasibility LP) *"sufficient" (sufficient, uses half-space checks)

Output

• If witness option is deactivated: true iff $P ∩ X = ∅$
• If witness option is activated:
  • (true, []) iff $P ∩ X = ∅$
  • (false, v) iff $P ∩ X ≠ ∅$ and $v ∈ P ∩ X$

Notes

For algorithm == "exact", we assume that constraints_list(X) is defined. For algorithm == "sufficient", witness production is not supported.

Algorithm

For algorithm == "exact", see @ref(isempty(P::HPoly{N}, ::Bool)).

For algorithm == "sufficient", we rely on the intersection check between the set X and each constraint in P. This means one support function evaluation of X for each constraint of P.

is_intersection_empty(X::LazySet{N},
                      Y::LazySet{N},
                      witness::Bool=false
                      )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two sets do not intersect, and otherwise optionally compute a witness.

Input

• X – set
• Y – another set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $X ∩ Y = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ Y = ∅$
  • (false, v) iff $X ∩ Y ≠ ∅$ and $v ∈ X ∩ Y$

Algorithm

This is a fallback implementation that computes the concrete intersection, intersection, of the given sets.

A witness is constructed using the an_element implementation of the result.

is_intersection_empty(P::Union{HPolyhedron{N}, AbstractPolytope{N}},
                      X::LazySet{N},
                      witness::Bool=false;
                      solver=GLPKSolverLP(method=:Simplex)
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether two polyhedra do not intersect.

Input

• P – polyhedron
• X – another set (see the Notes section below)
• witness – (optional, default: false) compute a witness if activated
• solver – (optional, default: GLPKSolverLP(method=:Simplex)) LP solver backend
• algorithm – (optional, default: "exact") algorithm keyword, one of: * "exact" (exact, uses a feasibility LP) *"sufficient" (sufficient, uses half-space checks)

Output

• If witness option is deactivated: true iff $P ∩ X = ∅$
• If witness option is activated:
  • (true, []) iff $P ∩ X = ∅$
  • (false, v) iff $P ∩ X ≠ ∅$ and $v ∈ P ∩ X$

Notes

For algorithm == "exact", we assume that constraints_list(X) is defined. For algorithm == "sufficient", witness production is not supported.

Algorithm

For algorithm == "exact", see @ref(isempty(P::HPoly{N}, ::Bool)).

For algorithm == "sufficient", we rely on the intersection check between the set X and each constraint in P. This means one support function evaluation of X for each constraint of P.

is_intersection_empty(cup::UnionSet{N}, X::LazySet{N}, [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a union of two convex sets and another set do not intersect.

Input

• cup – union of two convex sets
• X – another set

Output

true iff $\text{cup} ∩ X = ∅$.

is_intersection_empty(cup::UnionSetArray{N},
                      X::LazySet{N},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a union of a finite number of convex sets and another set do not intersect.

Input

• cup – union of a finite number of convex sets
• X – another set

Output

true iff $\text{cup} ∩ X = ∅$.

is_intersection_empty(U::Universe{N},
                      X::LazySet{N},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a universe and another set do not intersect.

Input

• U – universe
• X – another set

Output

true iff $X ≠ ∅$.

is_intersection_empty(C::Complement{N},
                      X::LazySet{N},
                      [witness]::Bool=false
                     )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether the complement of a convex set and another set do not intersect.

Input

• C – complement of a convex set
• X – convex set

Output

• If witness option is deactivated: true iff $X ∩ C = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ C = ∅$
  • (false, v) iff $X ∩ C ≠ ∅$ and $v ∈ X ∩ C$

Algorithm

We fall back to X ⊆ C.X, which can be justified as follows:

is_intersection_empty(Z1::Zonotope{N}, Z2::Zonotope{N}, witness::Bool=false
                     ) where {N<:Real}

Check whether two zonotopes do not intersect, and otherwise optionally compute a witness.

Input

• Z1 – zonotope
• Z2 – zonotope
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $Z1 ∩ Z2 = ∅$
• If witness option is activated:
  • (true, []) iff $Z1 ∩ Z2 = ∅$
  • (false, v) iff $Z1 ∩ Z2 ≠ ∅$ and $v ∈ Z1 ∩ Z2$

Algorithm

$Z1 ∩ Z2 ≠ ∅$ iff $c_1 - c_2 ∈ Z(0, (g_1, g_2))$ where $c_i$ and $g_i$ are the center and generators of zonotope Zi and $Z(c, g)$ represents the zonotope with center $c$ and generators $g$.

convex_hull(P1::HPoly{N}, P2::HPoly{N};
           [backend]=default_polyhedra_backend(P1, N)) where {N}

Compute the convex hull of the set union of two polyhedra in H-representation.

Input

• P1 – polyhedron
• P2 – another polyhedron
• backend – (optional, default: default_polyhedra_backend(P1, N)) the polyhedral computations backend

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.

convex_hull(P1::VPolytope{N}, P2::VPolytope{N};
            [backend]=default_polyhedra_backend(P1, N)) where {N}

Compute the convex hull of the set union of two polytopes in V-representation.

Input

• P1 – polytope
• P2 – another polytope
• backend – (optional, default: default_polyhedra_backend(P1, N)) the polyhedral computations backend, see Polyhedra's documentation for further information

Output

The VPolytope 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.

convex_hull(P::VPolygon{N}, Q::VPolygon{N};
            [algorithm]::String="monotone_chain")::VPolygon{N} where {N<:Real}

Return the convex hull of two polygons in vertex representation.

Input

• P – polygon in vertex representation
• Q – another 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 given two polygons.

Algorithm

A convex hull algorithm is used to compute the convex hull of the vertices of the given input polygons P and Q; see ?convex_hull for details on the available algorithms. The vertices of the output polygon are sorted in counter-clockwise fashion.

intersection(S::AbstractSingleton{N},
             X::LazySet{N}
            )::Union{Singleton{N}, EmptySet{N}} where {N<:Real}

Return the intersection of a singleton with another set.

Input

• S – singleton
• X – another set

Output

If the sets intersect, the result is S. Otherwise, the result is the empty set.

intersection(L1::Line{N}, L2::Line{N}
            )::Union{Singleton{N}, Line{N}, EmptySet{N}} where {N<:Real}

Return the intersection of two 2D lines.

Input

• L1 – first line
• L2 – second line

Output

If the lines are identical, the result is the first line. If the lines are parallel and not identical, the result is the empty set. Otherwise the result is the only intersection point.

Examples

The line $y = -x + 1$ intersected with the line $y = x$:

julia> intersection(Line([-1., 1.], 0.), Line([1., 1.], 1.))
Singleton{Float64,Array{Float64,1}}([0.5, 0.5])

julia> intersection(Line([1., 1.], 1.), Line([1., 1.], 1.))
Line{Float64,Array{Float64,1}}([1.0, 1.0], 1.0)

intersection(H1::AbstractHyperrectangle{N},
             H2::AbstractHyperrectangle{N}
            )::Union{<:Hyperrectangle{N}, EmptySet{N}} where {N<:Real}

Return the intersection of two hyperrectangles.

Input

• H1 – first hyperrectangle
• H2 – second hyperrectangle

Output

If the hyperrectangles do not intersect, the result is the empty set. Otherwise the result is the hyperrectangle that describes the intersection.

Algorithm

In each isolated direction i we compute the rightmost left border and the leftmost right border of the hyperrectangles. If these borders contradict, then the intersection is empty. Otherwise the result uses these borders in each dimension.

intersection(x::Interval{N},
             y::Interval{N}
             )::Union{Interval{N}, EmptySet{N}} where {N<:Real}

Return the intersection of two intervals.

Input

• x – first interval
• y – second interval

Output

If the intervals do not intersect, the result is the empty set. Otherwise the result is the interval that describes the intersection.

intersection(P1::AbstractHPolygon{N},
             P2::AbstractHPolygon{N}
            )::Union{HPolygon{N}, EmptySet{N}} where {N<:Real}

Return the intersection of two polygons in constraint representation.

Input

• P1 – first polygon
• P2 – second polygon
• prune – (optional, default: true) flag for removing redundant constraints

Output

If the polygons do not intersect, the result is the empty set. Otherwise the result is the polygon that describes the intersection.

Algorithm

We just combine the constraints of both polygons. To obtain a linear-time algorithm, we interleave the constraints. If there are two constraints with the same normal vector, we choose the tighter one.

Redundancy of constraints is checked with remove_redundant_constraints!(::AbstractHPolygon).

intersection(P1::AbstractPolyhedron{N},
             P2::AbstractPolyhedron{N};
             backend=GLPKSolverLP()) where {N<:Real}

Compute the intersection of two polyhedra.

Input

• P1 – polyhedron
• P2 – polyhedron
• backend – (optional, default: nothing) the solver backend used for the removal of redundant constraints, see the notes below for details

Output

An HPolyhedron resulting from the intersection of P1 and P2, with the redundant constraints removed, or an empty set if the intersection is empty. If one of the arguments is a polytope, the result is an HPolytope instead.

Notes

The default value of the solver backend is GLPKSolverLP() and it is used to run a feasiblity LP to remove the redundant constraints of the intersection.

If you want to use the Polyhedra library, pass an appropriate backend. For example, to use the default Polyhedra library use default_polyhedra_backend(P, N) or use CDDLib.Library() for the CDD library.

There are some shortcomings of the removal of constraints using the default Polyhedra library; see e.g. #1038 and Polyhedra#146. It is safer to check for emptiness of intersection before calling this function in those cases.

Algorithm

This implementation unifies the constraints of the two sets obtained from the constraints_list method.

intersection(P1::Union{VPolytope{N}, VPolygon{N}},
             P2::Union{VPolytope{N}, VPolygon{N}};
             [backend]=default_polyhedra_backend(P1, N),
             [prunefunc]=removevredundancy!) where {N<:Real}

Compute the intersection of two polytopes in vertex representation.

Input

• P1 – polytope in vertex representation
• P2 – polytope in vertex representation
• backend – (optional, default: default_polyhedra_backend(P1, N)) the backend for polyhedral computations
• prunefunc – (optional, default: removevredundancy!) function to prune the vertices of the result

Output

A VPolygon if both arguments are VPolygons, and a VPolytope otherwise.

intersection(cup::UnionSet{N}, X::LazySet{N}) where {N<:Real}

Return the intersection of a union of two convex sets and another convex set.

Input

• cup – union of two convex sets
• X – convex set

Output

The union of the pairwise intersections, expressed as a UnionSet. If one of those sets is empty, only the other set is returned.

intersection(cup::UnionSetArray{N}, X::LazySet{N}) where {N<:Real}

Return the intersection of a union of a finite number of convex sets and another convex set.

Input

• cup – union of a finite number of convex sets
• X – convex set

Output

The union of the pairwise intersections, expressed as a UnionSetArray.

intersection(U::Universe{N}, X::LazySet{N}) where {N<:Real}

Return the intersection of a universe and a convex set.

Input

• U – universe
• X – convex set

Output

The set X.

intersection(P::AbstractPolyhedron{N}, rm::ResetMap{N}) where {N<:Real}

Return the intersection of a polyhedron and a polyhedral reset map.

Input

• P – polyhedron
• rm – polyhedral reset map

Output

A polyhedron.

Notes

We assume that rm is polyhedral, i.e., has a constraints_list method defined.

⊆(S::LazySet{N}, H::AbstractHyperrectangle{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a convex set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

• S – inner convex set
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S ⊆ H$
• If witness option is activated:
  • (true, []) iff $S ⊆ H$
  • (false, v) iff $S ⊈ H$ and $v ∈ S \setminus H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval hull operator.

⊆(P::AbstractPolytope{N}, S::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a polytope is contained in a convex set, and if not, optionally compute a witness.

Input

• P – inner polytope
• S – outer convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $P ⊆ S$
• If witness option is activated:
  • (true, []) iff $P ⊆ S$
  • (false, v) iff $P ⊈ S$ and $v ∈ P \setminus S$

Algorithm

Since $S$ is convex, $P ⊆ S$ iff $v_i ∈ S$ for all vertices $v_i$ of $P$.

⊆(P::AbstractPolytope{N}, H::AbstractHyperrectangle, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a polytope is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

• P – inner polytope
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $P ⊆ H$
• If witness option is activated:
  • (true, []) iff $P ⊆ H$
  • (false, v) iff $P ⊈ H$ and $v ∈ P \setminus H$

Notes

This copy-pasted method just exists to avoid method ambiguities.

Algorithm

Since $H$ is convex, $P ⊆ H$ iff $v_i ∈ H$ for all vertices $v_i$ of $P$.

⊆(H1::AbstractHyperrectangle{N},
  H2::AbstractHyperrectangle{N},
  [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a given hyperrectangular set is contained in another hyperrectangular set, and if not, optionally compute a witness.

Input

• H1 – inner hyperrectangular set
• H2 – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $H1 ⊆ H2$
• If witness option is activated:
  • (true, []) iff $H1 ⊆ H2$
  • (false, v) iff $H1 ⊈ H2$ and $v ∈ H1 \setminus H2$

Algorithm

$H1 ⊆ H2$ iff $c_1 + r_1 ≤ c_2 + r_2 ∧ c_1 - r_1 ≥ c_2 - r_2$ iff $r_1 - r_2 ≤ c_1 - c_2 ≤ -(r_1 - r_2)$, where $≤$ is taken component-wise.

⊆(S::LazySet{N},
  P::AbstractPolyhedron{N},
  witness::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a convex set is contained in a polyhedron, and if not, optionally compute a witness.

Input

• S – inner convex set
• P – outer polyhedron (including a half-space)
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S ⊆ P$
• If witness option is activated:
  • (true, []) iff $S ⊆ P$
  • (false, v) iff $S ⊈ P$ and $v ∈ P \setminus S$

Algorithm

Since $S$ is convex, we can compare the support function of $S$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use the support vector in the first direction where the above check fails.

⊆(S::AbstractSingleton{N}, set::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a given set with a single value is contained in a convex set, and if not, optionally compute a witness.

Input

• S – inner set with a single value
• set – outer convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S ⊆ \text{set}$
• If witness option is activated:
  • (true, []) iff $S ⊆ \text{set}$
  • (false, v) iff $S ⊈ \text{set}$ and $v ∈ S \setminus \text{set}$

⊆(S::AbstractSingleton{N},
  H::AbstractHyperrectangle{N},
  [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a given set with a single value is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

• S – inner set with a single value
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S ⊆ H$
• If witness option is activated:
  • (true, []) iff $S ⊆ H$
  • (false, v) iff $S ⊈ H$ and $v ∈ S \setminus H$

Notes

This copy-pasted method just exists to avoid method ambiguities.

⊆(S1::AbstractSingleton{N},
  S2::AbstractSingleton{N},
  [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a given set with a single value is contained in another set with a single value, and if not, optionally compute a witness.

Input

• S1 – inner set with a single value
• S2 – outer set with a single value
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $S1 ⊆ S2$ iff $S1 == S2$
• If witness option is activated:
  • (true, []) iff $S1 ⊆ S2$
  • (false, v) iff $S1 ⊈ S2$ and $v ∈ S1 \setminus S2$

⊆(B1::Ball2{N}, B2::Ball2{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:AbstractFloat}

Check whether a ball in the 2-norm is contained in another ball in the 2-norm, and if not, optionally compute a witness.

Input

• B1 – inner ball in the 2-norm
• B2 – outer ball in the 2-norm
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $B1 ⊆ B2$
• If witness option is activated:
  • (true, []) iff $B1 ⊆ B2$
  • (false, v) iff $B1 ⊈ B2$ and $v ∈ B1 \setminus B2$

Algorithm

$B1 ⊆ B2$ iff $‖ c_1 - c_2 ‖_2 + r_1 ≤ r_2$

⊆(B::Union{Ball2{N}, Ballp{N}},
  S::AbstractSingleton{N},
  [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:AbstractFloat}

Check whether a ball in the 2-norm or p-norm is contained in a set with a single value, and if not, optionally compute a witness.

Input

• B – inner ball in the 2-norm or p-norm
• S – outer set with a single value
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $B ⊆ S$
• If witness option is activated:
  • (true, []) iff $B ⊆ S$
  • (false, v) iff $B ⊈ S$ and $v ∈ B \setminus S$

⊆(L::LineSegment{N}, S::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a line segment is contained in a convex set, and if not, optionally compute a witness.

Input

• L – inner line segment
• S – outer convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $L ⊆ S$
• If witness option is activated:
  • (true, []) iff $L ⊆ S$
  • (false, v) iff $L ⊈ S$ and $v ∈ L \setminus S$

Algorithm

Since $S$ is convex, $L ⊆ S$ iff $p ∈ S$ and $q ∈ S$, where $p, q$ are the end points of $L$.

⊆(L::LineSegment{N}, H::AbstractHyperrectangle{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a line segment is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

• L – inner line segment
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $L ⊆ H$
• If witness option is activated:
  • (true, []) iff $L ⊆ H$
  • (false, v) iff $L ⊈ H$ and $v ∈ L \setminus H$

Notes

This copy-pasted method just exists to avoid method ambiguities.

Algorithm

Since $H$ is convex, $L ⊆ H$ iff $p ∈ H$ and $q ∈ H$, where $p, q$ are the end points of $L$.

⊆(x::Interval, y::Interval)

Check whether an interval is contained in another interval.

Input

• x – interval
• y – interval

Output

true iff $x ⊆ y$.

⊆(∅::EmptySet{N}, X::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether an empty set is contained in another set.

Input

• ∅ – empty set
• X – another set
• witness – (optional, default: false) compute a witness if activated (ignored, just kept for interface reasons)

Output

true.

⊆(X::LazySet{N}, ∅::EmptySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a set is contained in an empty set.

Input

• X – another set
• ∅ – empty set
• witness – (optional, default: false) compute a witness if activated

Output

true iff X is empty.

Algorithm

We rely on isempty(X) for the emptiness check and on an_element(X) for witness production.

⊆(cup::UnionSet{N}, X::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a union of two convex sets is contained in another set.

Input

• cup – union of two convex sets
• X – another set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $\text{cup} ⊆ X$
• If witness option is activated:
  • (true, []) iff $\text{cup} ⊆ X$
  • (false, v) iff $\text{cup} \not\subseteq X$ and $v ∈ \text{cup} \setminus X$

⊆(cup::UnionSetArray{N}, X::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a union of a finite number of convex sets is contained in another set.

Input

• cup – union of a finite number of convex sets
• X – another set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $\text{cup} ⊆ X$
• If witness option is activated:
  • (true, []) iff $\text{cup} ⊆ X$
  • (false, v) iff $\text{cup} \not\subseteq X$ and $v ∈ \text{cup} \setminus X$

⊆(X::LazySet{N}, U::Universe{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a convex set is contained in a universe.

Input

• U – universe
• X – convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true
• If witness option is activated: (true, [])

⊆(U::Universe{N}, X::LazySet{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a universe is contained in another convex set, and otherwise optionally compute a witness.

Input

• U – universe
• X – convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $U ⊆ X$
• If witness option is activated:
  • (true, []) iff $U ⊆ X$
  • (false, v) iff $U \not\subseteq X$ and $v ∈ U \setminus X$

Algorithm

We fall back to isuniversal(X).

⊆(X::LazySet{N}, C::Complement{N}, [witness]::Bool=false
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a convex set is contained in the complement of another convex set, and otherwise optionally compute a witness.

Input

• X – convex set
• C – complement of a convex set
• witness – (optional, default: false) compute a witness if activated

Output

• If witness option is deactivated: true iff $X ⊆ C$
• If witness option is activated:
  • (true, []) iff $X ⊆ C$
  • (false, v) iff $X \not\subseteq C$ and $v ∈ X \setminus C$

Algorithm

We fall back to isdisjoint(X, C.X), which can be justified as follows.

⊆(X::CartesianProductArray{N}, Y::CartesianProductArray{N},
  witness::Bool=false; check_block_equality::Bool=true
 )::Union{Bool, Tuple{Bool, Vector{N}}} where {N<:Real}

Check whether a Cartesian product of finitely many convex sets is contained in another Cartesian product of finitely many convex sets, and otherwise optionally compute a witness.

Input

• X – Cartesian product of finitely many convex sets
• Y – Cartesian product of finitely many convex sets
• witness – (optional, default: false) compute a witness if activated
• check_block_equality – (optional, default: true) flag for checking that the block structure of the two sets is identical

Output

• If witness option is deactivated: true iff $X ⊆ Y$
• If witness option is activated:
  • (true, []) iff $X ⊆ Y$
  • (false, v) iff $X \not\subseteq Y$ and $v ∈ X \setminus Y$

Notes

This algorithm requires that the two Cartesian products share the same block structure. Depending on the value of check_block_equality, we check this property.

Algorithm

We check for inclusion for each block of the Cartesian products.

For witness production, we obtain a witness in one of the blocks. We then construct a high-dimensional witness by obtaining any point in the other blocks (using an_element) and concatenating these points.