GitHub

Subset Check

The function ⊆ checks whether a set is a subset of another set. It can optionally produce a witness if the subset relation does not hold. The operator can be used in infix notation (X ⊆ Y).

Note

issubset can be used as an alternative name to ⊆.

Examples

We use the following four sets for illustration.

using LazySets, LazySets.Approximations, Plots
B1 = Ball1(-ones(2), 1.)
B2 = Ball2(ones(2), 1.)
BI = BallInf(zeros(2), 1.)
H = Hyperrectangle(ones(2), ones(2))
sets = [B1, B2, BI, H]

function plot_sets(sets)
    for S in sets
        println(S)
        plot!(S, 1e-2, fillalpha=0.1)
    end
end

function plot_points(points, prefix)
    for i in eachindex(points)
        p = points[i]
        num_occur = length(findfirst(x -> x == p, points[1:i]))
        x = p[1]
        y = p[2]
        if num_occur == 1
            x += 0.15
        elseif num_occur == 2
            y += 0.15
        elseif num_occur == 3
            x -= 0.15
        else
            y -= 0.15
        end
        plot!(Singleton(p))
        plot!(annotations=(x, y, text("$(prefix)$(i)")))
    end
end

plot1 = plot()
plot_sets(sets)
plot1
Example block output
println(B1 ⊆ B2)
w1 = ⊆(B1, B2, true)[2]
println(B1 ⊆ BI)
w2 = ⊆(B1, BI, true)[2]
println(B1 ⊆ H)
w3 = ⊆(B1, H, true)[2]
# 'B2 ⊆ B1' is not supported yet
# w11 = ⊆(B2, B1, true)[2]
println(B2 ⊆ BI)
w4 = ⊆(B2, BI, true)[2]
println(B2 ⊆ H)
println(BI ⊆ B1)
w5 = ⊆(BI, B1, true)[2]
println(BI ⊆ B2)
w6 = ⊆(BI, B2, true)[2]
println(BI ⊆ H)
w7 = ⊆(BI, H, true)[2]
println(H ⊆ B1)
w8 = ⊆(H, B1, true)[2]
println(H ⊆ B2)
w9 = ⊆(H, B2, true)[2]
println(H ⊆ BI)
w10 = ⊆(H, BI, true)[2];
2-element Vector{Float64}:
 2.0
 1.0
witnesses = [w1, w2, w3, w4, w5, w6, w7, w8, w9, w10]

plot1 = plot()
plot_sets(sets)
plot_points(witnesses, "w")
plot1
Example block output

Methods

Base.:⊆ — Method
⊆(X::LazySet, Y::LazySet, [witness]::Bool=false)

Check whether a set is a subset of another set, and optionally compute a witness.

Input

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

Output

  • If the witness option is deactivated: true iff $X ⊆ Y$
  • If the witness option is activated:
    • (true, []) iff $X ⊆ Y$
    • (false, v) iff $X ⊈ Y$ for some $v ∈ X ∖ Y$

Notes

The convenience alias issubset is also available.

source
Base.:⊆ — Function

Extended help

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

Algorithm

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

source
Base.:⊆ — Function

Extended help

⊆(X::LazySet, Y::LazySet, witness::Bool=false)

Algorithm

The default implementation assumes that Y is polyhedral, i.e., that constraints_list(Y) is available, and checks inclusion of X in every constraint of Y.

source

Extended help

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

Algorithm

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

source

Extended help

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

Input

  • 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

Notes

S is assumed to be convex, which is asserted via isconvextype.

Algorithm

  • "vertices":

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

source
⊆(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 ∖ 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.

See Wetzlinger et al. [WKBA23], Proposition 7.

source
Base.:⊆ — Method

Extended help

⊆(X::LazySet, Y::LazySet, witness::Bool=false)

Algorithm

The default implementation assumes that Y is polyhedral, i.e., that constraints_list(Y) is available, and checks inclusion of X in every constraint of Y.

source

Extended help

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

Algorithm

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

source

Extended help

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

Input

  • 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

Notes

S is assumed to be convex, which is asserted via isconvextype.

Algorithm

  • "vertices":

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

source
⊆(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 ∖ 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.

See Wetzlinger et al. [WKBA23], Proposition 7.

source

Extended help

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

Algorithm

The algorithm is based on Mitchell et al. [MBB19], Lemma 3.1.

source
Base.:⊆ — Function
⊆(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 ∖ 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.

See Wetzlinger et al. [WKBA23], Proposition 7.

source
Base.:⊆ — Function

Extended help

⊆(X::LazySet, Y::LazySet, witness::Bool=false)

Algorithm

The default implementation assumes that Y is polyhedral, i.e., that constraints_list(Y) is available, and checks inclusion of X in every constraint of Y.

source

Extended help

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

Algorithm

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

source

Extended help

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

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.

source

Extended help

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

Input

  • 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

Notes

S is assumed to be convex, which is asserted via isconvextype.

Algorithm

  • "vertices":

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

source
⊆(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 ∖ 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.

See Wetzlinger et al. [WKBA23], Proposition 7.

source

Extended help

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

Algorithm

The algorithm is based on Mitchell et al. [MBB19], Lemma 3.1.

source
Base.:⊆ — Function

Extended help

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

Algorithm

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

source
Base.:⊆ — Function

Extended help

⊆(X::LazySet, Y::LazySet, witness::Bool=false)

Algorithm

The default implementation assumes that Y is polyhedral, i.e., that constraints_list(Y) is available, and checks inclusion of X in every constraint of Y.

source

Extended help

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

Algorithm

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

source

Extended help

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

Input

  • 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

Notes

S is assumed to be convex, which is asserted via isconvextype.

Algorithm

  • "vertices":

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

source
⊆(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 ∖ 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.

See Wetzlinger et al. [WKBA23], Proposition 7.

source

Extended help

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

Algorithm

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

source

Extended help

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

Algorithm

The algorithm is based on Mitchell et al. [MBB19], Lemma 3.1.

source
Base.:⊆ — Function
⊆(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.

source
Base.:⊆ — Function

Extended help

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

Algorithm

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

source
Base.:⊆ — Function

Extended help

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

Notes

This implementation assumes that the sets in the union U are convex.

source
Base.:⊆ — Function

Extended help

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

Notes

This implementation assumes that the sets in the union U are convex.

source
Base.:⊆ — Function

Extended help

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

Algorithm

We fall back to isuniversal(X).

source
Base.:⊆ — Function

Extended help

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

Algorithm

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

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

source
Base.:⊆ — Function

Extended help

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

Input

  • check_block_equality – (optional, default: true) flag for checking that the block structure of the two sets is identical

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.

source
Base.:⊆ — Function

Extended help

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

Input

  • check_block_equality – (optional, default: true) flag for checking that the block structure of the two sets is identical

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.

source
Base.:⊆ — Function

Extended help

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

Input

  • filter_redundant_sets – (optional, default: true) ignore sets in U that do not intersect with X

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.

source

Strict subset check

LazySets.API.:⊂ — Method
⊂(X::LazySet, Y::LazySet, [witness]::Bool=false)

Check whether a set is a strict subset of another set, and optionally compute a witness.

Input

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

Output

  • If the witness option is deactivated: true iff $X ⊂ Y$
  • If the witness option is activated:
    • (true, v) iff $X ⊂ Y$ for some $v ∈ Y ∖ X$
    • (false, []) iff $X ⊂ Y$ does not hold

Notes

Strict inclusion is sometimes written as ⊊. The following identity holds:

\[ X ⊂ Y ⇔ X ⊆ Y ∧ Y ⊈ X\]

Algorithm

The default implementation first checks inclusion of X in Y and then checks noninclusion of Y in X:

source
LazySets.API.:⊂ — Method

Extended help

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

Algorithm

The default implementation first checks inclusion of X in Y and then checks noninclusion of Y in X:

source