Subset Check

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

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.

Base.:⊆ — Function

⊆(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 ∖ H$

Algorithm

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

Base.:⊆ — Function

⊆(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 ∖ S$

Algorithm

"vertices":

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

Base.:⊆ — Function

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.

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

Base.:⊆ — Method

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.

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

Base.:⊆ — Function

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

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.

Base.:⊆ — Function

⊆(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 ∖ X$

Base.:⊆ — Function

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.

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

Base.:⊆ — Function

⊆(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 ∖ S2$

Base.:⊆ — Function

⊆(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 ∖ S$

Base.:⊆ — Function

⊆(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 ∖ S$

Algorithm

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

Base.:⊆ — Function

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.

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

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.

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.

Base.:⊆ — Function

⊆(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} ∖ X$

Base.:⊆ — Function

⊆(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} ∖ X$

Base.:⊆ — Function

⊆(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, [])

Base.:⊆ — Function

⊆(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 ∖ X$

Algorithm

We fall back to isuniversal(X).

Base.:⊆ — Function

⊆(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 ∖ C$

Algorithm

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

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

Base.:⊆ — Function

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

Base.:⊆ — Function

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

Base.:⊆ — Function

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

Base.:⊆ — Function

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

Strict subset check

LazySets.API.:⊂ — Function

⊂(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:

Algorithm

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