Binary Functions on Sets

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.

cartesian_product(X::LazySet, Y::LazySet; [backend]=nothing,
                  [algorithm]::String="vrep")

Compute the Cartesian product of two sets.

Input

• X – set

• Y – set

• backend – (optional, default: nothing) backend for polyhedral computation

• algorithm – (optional, default: "hrep") the method used to transform the sets X and Y before taking the Cartesian product; choose between:

  • "vrep" (use the vertex representation)
  • "hrep" (use the constraint representation)
  • "hrep_polyhedra" (use the constraint representation and Polyhedra)

Output

The VPolytope (if "vrep" was used) or HPolytope/HPolyhedron (if "hrep" or "hrep_polyhedra" was used) obtained by the concrete Cartesian product of X and Y. The choice between HPolytope and HPolyhedron is made based on boundedness information deduced from the type.

Notes

For further information on the supported backends see Polyhedra's documentation.

If X can be converted to a one-dimensional interval and the vertices of Y are available, use algorithm="vrep".

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.

isdisjoint(X::LazySet, Y::LazySet, [witness]::Bool=false)

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

Input

• X – set
• Y – 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.

isdisjoint(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
           [witness]::Bool=false)

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

Input

• H1 – hyperrectangular set
• H2 – 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 ∩ 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.

isdisjoint(X::LazySet, S::AbstractSingleton, [witness]::Bool=false)

Check whether a set and a set with a single value do not intersect, and otherwise optionally compute a witness.

Input

• X – set
• S – set with a single value
• 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$.

isdisjoint(S1::AbstractSingleton, S2::AbstractSingleton,
           [witness]::Bool=false)

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

Input

• S1 – set with a single value
• S2 – set with a single value
• 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$.

isdisjoint(Z::AbstractZonotope, H::Hyperplane, [witness]::Bool=false)

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

Input

• Z – zonotopic set
• 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.

isdisjoint(B1::Ball2, B2::Ball2, [witness]::Bool=false)

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

Input

• B1 – ball in the 2-norm
• B2 – 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.

isdisjoint(L1::LineSegment, L2::LineSegment, [witness]::Bool=false)

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

Input

• L1 – line segment
• L2 – line segment
• witness – (optional, default: false) compute a witness if activated

Output

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

Algorithm

The algorithm is inspired from here, which again is the special 2D case of a 3D algorithm from [1].

We first check if the two line segments are parallel, and if so, if they are collinear. In the latter case, we check membership 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.

[1] Ronald Goldman. Intersection of two lines in three-space. Graphics Gems

isdisjoint(X::LazySet, hp::Hyperplane, [witness]::Bool=false)

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

Input

• X – convex 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$

Algorithm

A 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$:

\[-ρ(-a, X) ≤ b ≤ ρ(a, X)\]

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.

isdisjoint(X::LazySet, hs::HalfSpace, [witness]::Bool=false)

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

Input

• X – 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$

Algorithm

A set intersects with a half-space iff the support function in the negative direction of the half-space's normal vector $a$ is less than the constraint $b$ of the half-space: $-ρ(-a, X) ≤ b$.

For compact set X, we equivalently have that the support vector in the negative direction $-a$ is contained in the half-space: $σ(-a) ∈ hs$. The support vector is thus also a witness if the sets are not disjoint.

isdisjoint(H1::HalfSpace, H2::HalfSpace, [witness]::Bool=false)

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

Input

• H1 – half-space
• H2 – half-space
• 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

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 $H1 : a_1⋅x = b_1$ and $H2 : 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 $H1$. 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.

isdisjoint(P::AbstractPolyhedron, X::LazySet, [witness]::Bool=false;
           [solver]=nothing, [algorithm]="exact")

Check whether a polyhedral set and another set do not intersect, and otherwise optionally compute a witness.

Input

• P – polyhedral set
• X – set (see the Notes section below)
• witness – (optional, default: false) compute a witness if activated
• solver – (optional, default: nothing) the backend used to solve the linear program
• 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.

For solver == nothing, we fall back to default_lp_solver(N).

Algorithm

For algorithm == "exact", see isempty(P::HPoly, ::Bool).

For algorithm == "sufficient", we rely on the intersection check between the set X and each constraint in P. This requires one support-function evaluation of X for each constraint of P. With this algorithm, the method may return false even in the case where the intersection is empty. On the other hand, if the algorithm returns true, then it is guaranteed that the intersection is empty.

isdisjoint(U::UnionSet, X::LazySet, [witness]::Bool=false)

Check whether a union of two sets and another set do not intersect, and otherwise optionally compute a witness.

Input

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

Output

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

isdisjoint(U::UnionSetArray, X::LazySet, [witness]::Bool=false)

Check whether a union of a finite number of sets and another set do not intersect, and otherwise optionally compute a witness.

Input

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

Output

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

isdisjoint(U::Universe, X::LazySet, [witness]::Bool=false)

Check whether a universe and another set do not intersect, and otherwise optionally compute a witness.

Input

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

Output

true iff $X ≠ ∅$.

isdisjoint(C::Complement, X::LazySet, [witness]::Bool=false)

Check whether the complement of a set and another set do not intersect, and otherwise optionally compute a witness.

Input

• C – complement of a set
• X – 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 ∩ C ≠ ∅$ and $v ∈ X ∩ C$

Algorithm

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

\[ X ∩ Y^C = ∅ ⟺ X ⊆ Y\]

isdisjoint(Z1::AbstractZonotope, Z2::AbstractZonotope,
           [witness]::Bool=false)

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

Input

• Z1 – zonotopic set
• Z2 – zonotopic set
• 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

The algorithm is taken from [1].

$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$.

[1] L. J. Guibas, A. T. Nguyen, L. Zhang: Zonotopes as bounding volumes. SODA

isdisjoint(I1::Interval, I2::Interval, [witness]::Bool=false)

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

Input

• I1 – interval
• I2 – interval
• witness – (optional, default: false) compute a witness if activated

Output

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

Algorithm

$I1 ∩ I2 ≠ ∅$ iff there is a gap between the left-most point of the second interval and the right-most point of the first interval, or vice-versa.

A witness is computed by taking the maximum over the left-most points of each interval, which is guaranteed to belong to the intersection.

isdisjoint(cpa::CartesianProductArray, P::AbstractPolyhedron,
           [witness]::Bool=false)

Check whether a polytopic Cartesian product array and a polyhedral set do not intersect, and otherwise optionally compute a witness.

Input

• cpa – Cartesian products of a finite number of polytopes
• P – polyhedral set
• witness – (optional, default: false) compute a witness if activated

Output

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

Algorithm

We first identify the blocks of cpa in which P is constrained. Then we project cpa to those blocks and convert the result to an HPolytope (or HPolyhedron if the set type is not known to be bounded) Q. Finally we determine whether Q and the projected P intersect.

isdisjoint(X::CartesianProductArray, Y::CartesianProductArray,
           [witness]::Bool=false)

Check whether two Cartesian products of a finite number of sets with the same block structure do not intersect, and otherwise optionally compute a witness.

Input

• X – Cartesian products of a finite number of sets
• Y – Cartesian products of a finite number of sets
• 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$

Notes

The implementation requires (and checks) that the Cartesian products have the same block structure.

Witness production is currently not supported.

isdisjoint(cpa::CartesianProductArray, H::AbstractHyperrectangle,
           [witness]::Bool=false)

Check whether a Cartesian product of a finite number of sets and a hyperrectangular set do not intersect, and otherwise optionally compute a witness.

Input

• cpa – Cartesian product of a finite number of sets
• H – hyperrectangular set
• witness – (optional, default: false) compute a witness if activated

Output

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

Algorithm

The sets cpa and H are disjoint if and only if at least one block of cpa and the corresponding projection of H are disjoint. We perform these checks sequentially.

isdisjoint(L1::Line2D, L2::Line2D, [witness]::Bool=false)

Check whether two two-dimensional lines do not intersect, and otherwise optionally compute a witness.

Input

• L1 – two-dimensional line
• L2 – two-dimensional line
• witness – (optional, default: false) compute a witness if activated

Output

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

convex_hull(X::LazySet, Y::LazySet; [algorithm]=nothing,
            [backend]=nothing, [solver]=nothing)

Compute the convex hull of two polytopic sets.

Input

• X – polytopic set
• Y – polytopic set
• algorithm – (optional, default: nothing) the convex-hull algorithm
• backend – (optional, default: nothing) backend for polyhedral computations (used for higher-dimensional sets)
• solver – (optional, default: nothing) the linear-programming solver used in the backend

Output

If the sets are empty, the result is an EmptySet. If the convex hull consists of a single point, the result is a Singleton. If the input sets are one-dimensional, the result is an Interval. If the input sets are two-dimensional, the result is a VPolygon. Otherwise the result is a VPolytope.

Algorithm

We compute the vertices of both X and Y using vertices_list and then compute the convex hull of the union of those vertices.

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.

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.

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.

convex_hull(points::Vector{VN}; [algorithm]=nothing, [backend]=nothing,
            [solver]=nothing) where {N, VN<:AbstractVector{N}}

Compute the convex hull of a list of points.

Input

• points – list of points
• algorithm – (optional, default: nothing) the convex-hull algorithm; see below for valid options
• backend – (optional, default: nothing) polyhedral computation backend for higher-dimensional point sets
• solver – (optional, default: nothing) the linear-programming solver used in the backend

Output

The convex hull as a list of points.

Algorithm

A pre-processing step treats the cases with up to two points for one dimension and up to four points for two dimensions. For more points in one resp. two dimensions, we use more general algorithms.

For the one-dimensional case, we return the minimum and maximum points, in that order.

The two-dimensional case is handled with a planar convex-hull algorithm. The following algorithms are available:

• "monotone_chain" – compute the convex hull of points in the plane using Andrew's monotone-chain method
• "monotone_chain_sorted" – the same as "monotone_chain" but assuming that the points are already sorted in counter-clockwise fashion

See the reference docstring of each of those algorithms for details.

The higher-dimensional case is treated using the concrete polyhedra library Polyhedra, which gives access to libraries such as CDDLib and ConvexHull.jl. These libraries can be chosen via the backend argument.

Notes

For the in-place version use convex_hull! instead of convex_hull.

Examples

Compute the convex hull of a random set of points:

julia> points = [randn(2) for i in 1:30]; # 30 random points in 2D

julia> hull = convex_hull(points);

julia> typeof(hull)
Vector{Vector{Float64}} (alias for Array{Array{Float64, 1}, 1})

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.

monotone_chain!(points::Vector{VN}; sort::Bool=true
               ) where {N, VN<:AbstractVector{N}}

Compute the convex hull of a list of points in the plane using Andrew's monotone-chain method.

Input

• points – list of 2D vectors; will be sorted in-place inside this method
• sort – (optional, default: true) flag for sorting the vertices lexicographically; sortedness is required for correctness

Output

List of vectors containing the 2D coordinates of the corner points of the convex hull.

Notes

For large sets of points, it is convenient to use static vectors to get maximum performance. For information on how to convert usual vectors into static vectors, see the type SVector provided by the StaticArrays package.

Algorithm

This method implements Andrew's monotone-chain convex hull algorithm to construct the convex hull of a set of $n$ points in the plane in $O(n \log n)$ time. For further details see Monotone chain

⊞(X::LazySet, Y::LazySet)

Unicode alias constructor for the (concrete) exact_sum function.

Notes

Write \boxplus[TAB] to enter this symbol.

exact_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)

Compute the exact sum of sparse polyomial zonotopes $P₁$ and $P₂$.

Input

• P1 – sparse polynomial zonotope
• P2 – sparse polynomial zonotope

Output

A SparsePolynomialZonotope representing the exact sum $P₁ ⊞ P₂$.

intersection(S::AbstractSingleton, X::LazySet)

Compute the intersection of a set with a single point with another set.

Input

• S – set with a single point
• X – set

Output

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

intersection(L1::Line2D, L2::Line2D)

Compute the intersection of two two-dimensional lines.

Input

• L1 – line
• L2 – line

Output

Three outcomes are possible:

• 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 set with the unique intersection point.

Algorithm

We first check whether the lines are parallel. If not, we use Cramer's rule to compute the intersection point.

Examples

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

julia> intersection(Line2D([-1.0, 1], 0.0), Line2D([1.0, 1], 1.0))
Singleton{Float64, Vector{Float64}}([0.5, 0.5])

julia> intersection(Line2D([1.0, 1], 1.0), Line2D([1.0, 1], 1.0))
Line2D{Float64, Vector{Float64}}([1.0, 1.0], 1.0)

intersection(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle)

Compute the intersection of two hyperrectangular sets.

Input

• H1 – hyperrectangular set
• H2 – hyperrectangular set

Output

If the hyperrectangular sets 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 hyperrectangular sets. If these borders contradict, then the intersection is empty. Otherwise the resulting hyperrectangle uses these borders in each dimension.

intersection(x::Interval, y::Interval)

Compute the intersection of two intervals.

Input

• x – interval
• y – 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(X::Interval, hs::HalfSpace)

Compute the intersection of an interval and a half-space.

Input

• X – interval
• hs – half-space

Output

If the sets do not intersect, the result is the empty set. If the interval is fully contained in the half-space, the result is the original interval. Otherwise the result is the interval that describes the intersection.

Algorithm

We first handle the special case that the normal vector a of hs is close to zero. Then we distinguish the cases that hs is a lower or an upper bound.

intersection(X::Interval, hp::Hyperplane)

Compute the intersection of an interval and a hyperplane.

Input

• X – interval
• hp – hyperplane

Output

If the sets do not intersect, the result is the empty set. Otherwise the result is the singleton that describes the intersection.

intersection(X::Interval, Y::LazySet)

Compute the intersection of an interval and a convex set.

Input

• X – interval
• Y – convex set

Output

If the sets do not intersect, the result is the empty set. Otherwise the result is the interval that describes the intersection, which may be of type Singleton if the intersection is very small.

intersection(P1::AbstractHPolygon, P2::AbstractHPolygon; [prune]::Bool=true)

Compute the intersection of two polygons in constraint representation.

Input

• P1 – polygon in constraint representation
• P2 – polygon in constraint representation
• 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]=default_lp_solver(N), [prune]::Bool=true) where {N}

Compute the intersection of two polyhedra.

Input

• P1 – polyhedron
• P2 – polyhedron
• backend – (optional, default: default_lp_solver(N)) the LP solver used for the removal of redundant constraints; see the Notes section below for details
• prune – (optional, default: true) flag for removing redundant constraints

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 default_lp_solver(N) 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, use default_polyhedra_backend(P) for the default Polyhedra library, 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{VPolygon, VPolytope}, P2::Union{VPolygon, VPolytope};
             [backend]=nothing, [prunefunc]=nothing)

Compute the intersection of two polytopes in vertex representation.

Input

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

Output

A VPolytope.

Notes

If prunefunc is nothing, this implementation sets it to (X -> removevredundancy!(X; ztol=_ztol(eltype(P1)))).

intersection(P1::VPolygon, P2::VPolygon; apply_convex_hull::Bool=true)

Compute the intersection of two polygons in vertex representation.

Input

• P1 – polygon in vertex representation
• P2 – polygon in vertex representation
• apply_convex_hull – (default, optional: true) if false, skip the computation of the convex hull of the resulting polygon

Output

A VPolygon, or an EmptySet if the intersection is empty.

Algorithm

This function applies the Sutherland–Hodgman polygon clipping algorithm. The implementation is based on the one found in rosetta code.

intersection(cup::UnionSet, X::LazySet)

Compute the intersection of a union of two sets and another set.

Input

• cup – union of two sets
• X – 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, X::LazySet)

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

Input

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

Output

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

intersection(U::Universe, X::LazySet)

Compute the intersection of a universe and a set.

Input

• U – universe
• X – set

Output

The set X.

intersection(P::AbstractPolyhedron, rm::ResetMap)

Compute the intersection of a polyhedral set and a polyhedral reset map.

Input

• P – polyhedral set
• rm – polyhedral reset map

Output

A polyhedron.

Notes

This method assumes that rm is polyhedral, i.e., has a constraints_list method defined.

    intersection(X::CartesianProductArray, Y::CartesianProductArray)

Compute the intersection between Cartesian products of a finite number of sets with identical decomposition.

Input

• X – Cartesian product of a finite number of sets
• Y – Cartesian product of a finite number of sets

Output

The decomposed set that represents the concrete intersection of X and Y.

Algorithm

This algorithm intersects the corresponding blocks of the sets.

intersection(L::LinearMap, X::LazySet)

Compute the intersection of a lazy linear map and a set.

Input

• L – linear map
• X – set

Output

The set obtained by the computing the concrete linear map L.M * L.X and intersecting with X.

intersection(cpa::CartesianProductArray, P::AbstractPolyhedron)

Compute the intersection of a Cartesian product of a finite number of polyhedral sets with a polyhedron.

Input

• cpa – Cartesian product of a finite number of polyhedral sets
• P – polyhedron

Output

A Cartesian product of a finite number of polyhedral sets. See the Algorithm section below for details about the structure.

Notes

The restriction to polyhedral sets in cpa only applies to the blocks that are actually intersected with P (see the Algorithm section below for details). All other blocks are not considered by the intersection and remain identical.

Algorithm

The underlying idea of the algorithm is to exploit the unconstrained dimensions of P. Without loss of generality, assume that cpa has the structure $X × Y × Z$ such that only the dimensions of $Y$ are constrained in $P$. By denoting a suitable projection of $P$ to the dimensions of $Y$ with $P|_Y$, we have the following equivalence:

\[ (X × Y × Z) ∩ P = X × (Y ∩ P|_Y) × Z\]

Note that $Y$ may still consist of many blocks. However, due to the structural restriction of a Cartesian product, we cannot break down this set further even if $P|_Y$ is still unconstrained in some dimensions of blocks in $Y$. This would require a restructuring of the dimensions. Consider this example:

\[ Y := [0, 1] × [1, 2] × [2, 3] P|_Y := x₁ + x₃ ≤ 2 Y ∩ P|_Y = 0 ≤ x₁ ∧ 1 ≤ x₂ ≤ 2 ∧ 2 ≤ x₃ ∧ x₁ + x₃ ≤ 2\]

Even though the constraints of dimension $x₂$ are decoupled from the rest, due to the last constraint, the Cartesian product cannot be broken down further. In particular, the result $Y ∩ P|_Y$ is a polyhedron in this implementation.

Now we explain the implementation of the above idea. We first identify the dimensions in which P is constrained. Then we identify the block dimensions of $X × Y × Z$ such that $Y$ has minimal dimension. Finally, we convert $Y$ to a polyhedron and intersect it with a suitable projection of P.

intersection(LS::LineSegment, L2::Line2D)

Compute the intersection of a line segment and a line in two dimensions.

Input

• LS – line segment
• L2 – two-dimensional line

Output

If the sets do not intersect, the result is the empty set. Otherwise the result is the singleton or line segment that describes the intersection.

intersection(LS1::LineSegment, LS2::LineSegment)

Compute the intersection of two line segments.

Input

• LS1 – line segment
• LS2 – line segment

Output

A singleton, line segment, or the empty set depending on the result of the intersection.

Notes

• If the line segments cross, or are parallel and have one point in common, that point is returned.

• If the line segments are parallel and have a line segment in common, that segment is returned.

• Otherwise, if there is no intersection, an empty set is returned.

intersection(Z::AbstractZonotope{N}, H::HalfSpace{N};
             [backend]=default_lp_solver(N), [prune]::Bool=true) where {N}

Compute the intersection between a zonotopic set and a half-space.

Input

• Z – zonotopic set
• H – half-space
• backend – (optional, default: default_lp_solver(N)) the LP solver used for the removal of redundant constraints
• prune – (optional, default: true) flag for removing redundant constraints

Output

If the sets do not intersect, the output is the empty set. If the zonotopic set is fully contained in the half-space, the zonotopic set is returned. Otherwise, the output is the concrete intersection between Z and H.

Algorithm

First there is a disjointness test. If that is negative, there is an inclusion test. If that is negative, then the concrete intersection is computed.

intersection(X::Star, H::HalfSpace)

Compute the intersection between a star and a half-space.

Input

• X – star
• H – half-space

Output

A star set representing the intersection between a star and a half-space.

intersection!(X::Star, H::HalfSpace)

Compute the intersection between a star set and a half-space, in-place.

Input

• X – star set
• H – half-space

Output

The modified star set.

linear_combination(P1::SimpleSparsePolynomialZonotope,
                   P2::SimpleSparsePolynomialZonotope)

Compute the linear combination of two simple sparse polynomial zonotopes.

Input

• P1 – simple sparse polynomial zonotope
• P2 – simple sparse polynomial zonotope

Output

Linear combination of P1 and P2.

Notes

The linear combination of two sets $P₁$ and $P₂$ is defined as

\[\{1/2(1+λ)p₁ + 1/2(1-λ)p₂ | p₁ ∈ P₁, p₂ ∈ P₂, λ ∈ [-1, 1]\}.\]

This method implements the algorithm described in Proposition 3.1.25 of [1].

[1] N. Kochdumper. Extensions of polynomial zonotopes and their application to verification of cyber-physical systems. 2021.

minkowski_sum(P::LazySet, Q::LazySet;
              [backend]=nothing, [algorithm]=nothing, [prune]=true)

Compute the Minkowski sum of two polyhedral sets.

Input

• P – set
• Q – set
• backend – (optional, default: nothing) polyhedral computations backend
• algorithm – (optional, default: nothing) algorithm to eliminate variables; available options are Polyhedra.FourierMotzkin, Polyhedra.BlockElimination, and Polyhedra.ProjectGenerators
• prune – (optional, default: true) if true, apply a post-processing to remove redundant constraints or vertices

Output

In two dimensions, if the sets are polygons, the result is a VPolygon. In higher dimensions, the result is an HPolytope if both P and Q are known to be bounded by their types, and an HPolyhedron otherwise.

Notes

This function requires that the list of constraints of both sets P and Q can be obtained. After obtaining the respective lists of constraints, the minkowski_sum method for polyhedral sets is used.

minkowski_sum(P::AbstractPolyhedron, Q::AbstractPolyhedron;
              [backend]=nothing, [algorithm]=nothing, [prune]=true)

Compute the Minkowski sum of two polyhedra in constraint representation.

Input

• P – polyhedron in constraint representation
• Q – polyhedron in constraint representation
• backend – (optional, default: nothing) polyhedral computations backend
• algorithm – (optional, default: nothing) algorithm to eliminate variables; available options are Polyhedra.FourierMotzkin, Polyhedra.BlockElimination, and Polyhedra.ProjectGenerators
• prune – (optional, default: true) if true, apply a post-processing to remove redundant constraints

Output

A polyhedron in H-representation that corresponds to the Minkowski sum of P and Q.

Algorithm

This function implements the concrete Minkowski sum by projection and variable elimination as detailed in [1]. The idea is that if we write $P$ and $Q$ in simple H-representation, that is, $P = \{x ∈ \mathbb{R}^n : Ax ≤ b \}$ and $Q = \{x ∈ \mathbb{R}^n : Cx ≤ d \}$, then their Minkowski sum can be seen as the projection onto the first $n$-dimensional coordinates of the polyhedron:

\[ \begin{pmatrix} 0 & A \ C & -C \end{pmatrix} \binom{x}{y} ≤ inom{b}{d}\]

This is seen by noting that $P ⊕ Q$ corresponds to the set of points $x ∈ \mathbb{R}^n$ such that $x = y + z$ with $Ay ≤ b$ and $Cz ≤ d$; hence it follows that $Ay ≤ b$ and $C(x-y) ≤ d$, and the inequality above follows by considering the $2n$-dimensional space $\binom{x}{y}$. The reduction from $2n$ to $n$ variables is performed using an elimination algorithm as described next.

The elimination of variables depends on the polyhedra library Polyhedra, which itself uses CDDLib for variable elimination. The available algorithms are:

• Polyhedra.FourierMotzkin – projection by computing the H-representation and applying the Fourier-Motzkin elimination algorithm to it

• Polyhedra.BlockElimination – projection by computing the H-representation and applying the block elimination algorithm to it

• Polyhedra.ProjectGenerators – projection by computing the V-representation

[1] Kvasnica, Michal. "Minkowski addition of convex polytopes." (2005): 1-10.

minkowski_sum(P1::VPolytope, P2::VPolytope;
              [apply_convex_hull]=true,
              [backend]=nothing,
              [solver]=nothing)

Compute the Minkowski sum of two polytopes in vertex representation.

Input

• P1 – polytope
• P2 – polytope
• apply_convex_hull – (optional, default: true) if true, post-process the pairwise sums using a convex-hull algorithm
• backend – (optional, default: nothing) the backend for polyhedral computations used to post-process with a convex hull; see default_polyhedra_backend(P1)
• solver – (optional, default: nothing) the backend used to solve the linear program; see default_lp_solver_polyhedra(N)

Output

A new polytope in vertex representation whose vertices are the convex hull of the sum of all possible sums of vertices of P1 and P2.

minkowski_sum(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle)

Concrete Minkowski sum of a pair of hyperrectangular sets.

Input

• H1 – hyperrectangular set
• H2 – hyperrectangular set

Output

A Hyperrectangle corresponding to the Minkowski sum of H1 and H2.

Algorithm

The resulting hyperrectangle is obtained by summing up the centers and radii.

minkowski_sum(Z1::AbstractZonotope, Z2::AbstractZonotope)

Concrete Minkowski sum of a pair of zonotopic sets.

Input

• Z1 – zonotopic set
• Z2 – zonotopic set

Output

A Zonotope corresponding to the Minkowski sum of Z1 and Z2.

Algorithm

The resulting zonotope is obtained by summing up the centers and concatenating the generators of Z1 and Z2.

minkowski_sum(P::VPolygon, Q::VPolygon)

The Minkowski Sum of two polygons in vertex representation.

Input

• P – polygon in vertex representation
• Q – polygon in vertex representation

Output

A polygon in vertex representation.

Algorithm

We treat each edge of the polygons as a vector, attaching them in polar order (attaching the tail of the next vector to the head of the previous vector). The resulting polygonal chain will be a polygon, which is the Minkowski sum of the given polygons. This algorithm assumes that the vertices of P and Q are sorted in counter-clockwise fashion and has linear complexity $O(m+n)$, where $m$ and $n$ are the number of vertices of P and Q, respectively.

minkowski_sum(PZ::DensePolynomialZonotope, Z::AbstractZonotope)

Compute the Minkowski sum of a polynomial zonotope and a zonotopic set.

Input

• PZ – polynomial zonotope
• Z – zonotopic set

Output

A polynomial zonotope whose center is the sum of the centers of PZ and Z and whose generators are the concatenation of the generators of PZ and Z.

minkowski_sum(x::Interval, y::Interval)

Concrete Minkowski sum of a pair of intervals.

Input

• x – interval
• y – interval

Output

An Interval corresponding to the Minkowski sum of x and y.

Algorithm

The implementation takes the sum of x and y following the rules of interval arithmetic.

minkowski_sum(X::AbstractSingleton, Y::AbstractSingleton)

Concrete Minkowski sum of a pair of singletons.

Input

• X – singleton
• Y – singleton

Output

A singleton

Algorithm

The singleton obtained by summing the elements in X and Y.

minkowski_sum(P1::SimpleSparsePolynomialZonotope,
              P2::SimpleSparsePolynomialZonotope)

Compute the Minkowski sum of two simple sparse polynomial zonotopes.

Input

• P1 – simple sparse polynomial zonotope
• P2 – simple sparse polynomial zonotope

Output

The Minkowski sum of P1 and P2.

minkowski_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)

Compute the Minkowski sum of two sparse polyomial zonotopes.

Input

• P1 – sparse polynomial zonotope
• P2 – sparse polynomial zonotope

Output

The Minkowski sum of P1 and P2.

pontryagin_difference(X::LazySet, Y::LazySet)

An alias for the function minkowski_difference.

Notes

There is some inconsistency in the literature regarding the naming conventions. In this library, both the names Minkowski difference and Pontryagin difference refer to the geometric difference of two sets. Mathematically:

\[ X ⊖ Y = \{z ∈ ℝ^n: z + v ∈ X ~∀~v ∈ Y\}\]

minkowski_difference(P::LazySet, Q::LazySet)

Concrete Minkowski difference (geometric difference) of a polytopic set and a compact convex set.

Input

• P – polytopic set
• Q – compact convex set that is subtracted from P

Output

An HPolytope that corresponds to the Minkowski difference of P minus Q if P is bounded, and an HPolyhedron if P is unbounded.

Notes

This implementation requires that the set P is polyhedral and that the set Q is bounded.

Algorithm

This method implements Theorem 2.3 in [1]:

Suppose $P$ is a polyhedron

\[P = \{z ∈ ℝ^n: sᵢᵀz ≤ rᵢ,~i = 1, …, N\}.\]

where $sᵢ ∈ ℝ^n, sᵢ ≠ 0$, and $rᵢ ∈ ℝ$. Assume $ρ(sᵢ,Q)$ is defined for $i = 1, …, N$. Then the Minkowski difference is

\[\{z ∈ ℝ^n: sᵢᵀz ≤ rᵢ - ρ(sᵢ,Q),~i = 1, …, N\}.\]

[1] Ilya Kolmanovsky and Elmer G. Gilbert (1997). Theory and computation of disturbance invariant sets for discrete-time linear systems. Mathematical Problems in Engineering Volume 4, Issue 4, Pages 317-367.

minkowski_difference(Z1::AbstractZonotope, Z2::AbstractZonotope)

Compute the Minkowski difference of two zonotopic sets.

Input

• Z1 – zonotopic set
• Z2 – zonotopic set

Output

An HPolytope that corresponds to the Minkowski difference of Z1 minus Z2.

Algorithm

This method implements Theorem 3 in [1].

[1] M. Althoff: On computing the Minkowski difference of zonotopes. 2016.

issubset(X::LazySet, Y::LazySet, [witness]::Bool=false, args...)

Alias for ⊆ (inclusion check).

Input

• X – set
• Y – 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 \setminus Y$

Notes

For more documentation see ⊆.

⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

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

Input

• S – inner 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, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

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

Input

• P – inner polytopic set

• S – outer convex set

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

• algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

  • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

  • "vertices", using the list of vertices of P and membership evaluations of S

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

• "vertices":

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

⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

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

Input

• S – inner 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, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

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

Input

• P – inner polytopic set

• S – outer convex set

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

• algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

  • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

  • "vertices", using the list of vertices of P and membership evaluations of S

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

• "vertices":

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

⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

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

Input

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

Output

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

Algorithm

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

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

⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

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

Input

• S – inner 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, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

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

Input

• P – inner polytopic set

• S – outer convex set

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

• algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

  • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

  • "vertices", using the list of vertices of P and membership evaluations of S

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

• "vertices":

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

⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

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

Input

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

Output

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

Algorithm

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

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

⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

• Z – inner zonotopic set
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
  [witness]::Bool=false)

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.

⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

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

Input

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

Output

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

Algorithm

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

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

⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)

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

Input

• S – inner set with a single value
• X – outer set
• 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 ∈ S \setminus X$

⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

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

Input

• S – inner 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.

⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
  [witness]::Bool=false)

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.

⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

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

Input

• P – inner polytopic set

• S – outer convex set

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

• algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

  • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

  • "vertices", using the list of vertices of P and membership evaluations of S

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

• "vertices":

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

⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

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

Input

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

Output

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

Algorithm

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

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

⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)

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

Input

• S – inner set with a single value
• X – outer set
• 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 ∈ S \setminus X$

⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

• Z – inner zonotopic set
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

⊆(S1::AbstractSingleton, S2::AbstractSingleton, witness::Bool=false)

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, B2::Ball2, [witness]::Bool=false)

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, Ballp}, S::AbstractSingleton, witness::Bool=false)

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, S::LazySet, witness::Bool=false)

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$.

⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

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

Input

• S – inner 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, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

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

Input

• P – inner polytopic set

• S – outer convex set

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

• algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

  • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

  • "vertices", using the list of vertices of P and membership evaluations of S

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

• "vertices":

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

⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

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

Input

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

Output

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

Algorithm

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

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

⊆(L::LineSegment, S::LazySet, witness::Bool=false)

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$.

⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

• Z – inner zonotopic set
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

⊆(x::Interval, y::Interval, [witness]::Bool=false)

Check whether an interval is contained in another interval.

Input

• x – inner interval
• y – outer interval
• witness – (optional, default: false) compute a witness if activated

Output

true iff $x ⊆ y$.

⊆(x::Interval, U::UnionSet, [witness]::Bool=false)

Check whether an interval is contained in the union of two convex sets.

Input

• x – inner interval
• U – outer union of two convex sets

Output

true iff x ⊆ U.

Notes

This implementation assumes that U is a union of one-dimensional convex sets. Since these are equivalent to intervals, we convert to Intervals.

Algorithm

Let $U = a ∪ b$ where $a$ and $b$ are intervals and assume that the lower bound of $a$ is to the left of $b$. If the lower bound of $x$ is to the left of $a$, we have a counterexample. Otherwise we compute the set difference $y = x \ a$ and check whether $y ⊆ b$ holds.

⊆(∅::EmptySet, X::LazySet, witness::Bool=false)

Check whether the empty set is contained in another set.

Input

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

Output

true.

⊆(X::LazySet, ∅::EmptySet, [witness]::Bool=false)

Check whether a set is contained in the empty set.

Input

• X – inner set
• ∅ – outer 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.

⊆(U::UnionSet, X::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

⊆(U::UnionSetArray, X::LazySet, [witness]::Bool=false)

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

Input

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

Output

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

⊆(X::LazySet, U::Universe, [witness]::Bool=false)

Check whether a set is contained in a universe.

Input

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

Output

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

⊆(U::Universe, X::LazySet, [witness]::Bool=false)

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

Input

• U – inner universe
• X – outer 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, C::Complement, [witness]::Bool=false)

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

Input

• X – inner set
• C – outer complement of a 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 ⊆ Y^C ⟺ X ∩ Y = ∅\]

⊆(X::CartesianProduct, Y::CartesianProduct, [witness]::Bool=false;
  check_block_equality::Bool=true)

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

Input

• X – inner Cartesian product of two sets
• Y – outer Cartesian product of two 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. If check_block_equality is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

Algorithm

We check 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 (lower-dimensional) points.

⊆(X::CartesianProductArray, Y::CartesianProductArray, [witness]::Bool=false;
  check_block_equality::Bool=true)

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

Input

• X – inner Cartesian product of finitely many sets
• Y – outer Cartesian product of finitely many 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. If check_block_equality is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

Algorithm

We check 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 (lower-dimensional) points.

⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

• Z – inner zonotopic set
• H – outer hyperrectangular set
• witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

⊆(X::LazySet{N}, U::UnionSetArray, witness::Bool=false;
  filter_redundant_sets::Bool=true) where {N}

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

Input

• X – inner set
• U – outer union of a finite number of sets
• witness – (optional, default: false) compute a witness if activated
• filter_redundant_sets – (optional, default: true) ignore sets in U that do not intersect with X

Output

true iff $X ⊆ U$.

Algorithm

This implementation is general and successively removes parts from X that are covered by the sets in the union $U$ using the difference function. For the resulting subsets, this implementation relies on the methods isdisjoint, ⊆, and intersection.

As a preprocessing, this implementation checks if X is contained in any of the sets in U.

The filter_redundant_sets option controls whether sets in U that do not intersect with X should be ignored.

⊂(X::LazySet{N}, Y::LazySet, [witness]::Bool=false) where {N}

Strict inclusion check of a set in another set.

Input

• X – first set
• Y – second 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, v) iff $X ⊂ Y$ and $v ∈ Y \setminus X$
  • (false, []) iff not $X ⊂ Y$

Algorithm

We check inclusion of X in Y and then check inclusion of Y in X:

\[X ⊂ Y \Leftrightarrow X ⊆ Y \land ¬ (Y ⊆ X)\]

\(X::LazySet, Y::LazySet)

Convenience alias for set difference.

Input

• X – first set
• Y – second set

Output

The set difference between X and Y.

Notes

If X and Y are intervals, X \ Y is used in some libraries to denote the left division, as the example below shows. However, it should not be confused with the set difference. For example,

julia> X = Interval(0, 2); Y = Interval(1, 4);

julia> X \ Y  # computing the set difference
Interval{Float64, IntervalArithmetic.Interval{Float64}}([0, 1])

julia> X.dat \ Y.dat  # computing the left division
[0.5, ∞]

difference(X::Interval{N}, Y::Interval) where {N}

Compute the set difference between two intervals.

The set difference is defined as:

\[ X \setminus Y = \{x: x ∈ X \text{ and } x ∉ Y \}\]

The backslash symbol, \, can be used as an alias.

Input

• X – first interval
• Y – second interval

Output

Depending on the position of the intervals, the output is one of the following:

• An EmptySet.
• An Interval.
• A UnionSet of two Interval sets.

Algorithm

Let $X = [a, b]$ and $Y = [c, d]$ be intervals. Their set difference is $X \setminus Y = \{x: x ∈ X \text{ and } x ∉ Y \}$ and, depending on their position, three different results may occur:

• If $X$ and $Y$ do not overlap, i.e., if their intersection is empty, then the set difference is just $X$.
• Otherwise, let $Z = X ∩ Y ≠ ∅$, then $Z$ splits $X$ into either one or two intervals. The latter case happens when the bounds of $Y$ are strictly contained in $X$.

To check for strict inclusion, we assume that the inclusion is strict and then check if the resulting intervals that cover $X$ (one to its left and one to its right, let them be L and R), obtained by intersection with $Y$, are flat or not. Three cases may arise:

• If both L and R are flat then $X = Y$ and the result is the empty set.
• If only L is flat, then the result is R, the remaining interval not covered by $Y$. Similarly, if only R is flat, then the result is L.
• Finally, if none of the intervals is flat, then $Y$ is strictly contained in $X$ and the set union of L and R is returned.

difference(X::AbstractHyperrectangle{N}, Y::AbstractHyperrectangle) where {N}

Compute the set difference between two hyperrectangular sets.

Input

• X – first hyperrectangular set
• Y – second hyperrectangular set

The set difference is defined as:

\[ X \setminus Y = \{x: x ∈ X \text{ and } x ∉ Y \}\]

Output

A UnionSetArray consisting of the union of hyperrectangles. Note that this union is in general not convex.

Algorithm

This implementation uses IntervalArithmetic.setdiff.

distance(S::AbstractSingleton, X::LazySet; [p]::Real=2.0)

Compute the distance between the singleton S and the set X with respect to the given p-norm.

Input

• S – singleton, i.e., a set with one element
• X – set
• p – (optional, default: 2.0) the p-norm used; p = 2.0 corresponds to the usual Euclidean norm

Output

A scalar representing the distance between the element wrapped by S and the set X.

distance(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle;
         [p]::Real=2)

Compute the standard distance between two hyperrectangular sets, defined as

\[ \inf_{x \in H_1, y \in H_2} \{ d(x, y) \}.\]

Input

• H1 – hyperrectangular set
• H2 – hyperrectangular set
• p – (optional; default: 2) value of the $p$-norm

Output

The distance, which is zero if the sets intersect and otherwise the $p$-norm of the shortest line segment between any pair of points.

Notes

See also hausdorff_distance for an alternative distance notion.