Half-space (HalfSpace)

HalfSpace{N, VN<:AbstractVector{N}} <: AbstractPolyhedron{N}

Type that represents a (closed) half-space of the form $a⋅x ≤ b$.

Fields

• a – normal direction (non-zero)
• b – constraint

Examples

The half-space $x + 2y - z ≤ 3$:

julia> HalfSpace([1, 2, -1.], 3.)
HalfSpace{Float64, Vector{Float64}}([1.0, 2.0, -1.0], 3.0)

To represent the set $y ≥ 0$ in the plane, we can rearrange the expression as $0x - y ≤ 0$:

julia> HalfSpace([0, -1.], 0.)
HalfSpace{Float64, Vector{Float64}}([0.0, -1.0], 0.0)

LinearConstraint

Alias for HalfSpace

convert(::Type{HalfSpace{N}}, expr::Expr; vars::Vector{Basic}=Basic[]) where {N}

Return a LazySet.HalfSpace given a symbolic expression that represents a half-space.

Input

• expr – a symbolic expression
• vars – (optional, default: nothing): set of variables with respect to which the gradient is taken; if empty, we take the free symbols in the given expression

Output

A HalfSpace, in the form ax <= b.

Examples

julia> convert(HalfSpace, :(x1 <= -0.03))
HalfSpace{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(HalfSpace, :(x1 < -0.03))
HalfSpace{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(HalfSpace, :(x1 > -0.03))
HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03)

julia> convert(HalfSpace, :(x1 >= -0.03))
HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03)

julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6))
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0)

You can also specify the set of "ambient" variables, even if not all of them appear:

julia> using SymEngine: Basic

julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4])
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0)

an_element(X::LazySet)

Return some element of a nonempty set.

Input

• X – set

Output

An element of X unless X is empty.

Extended help

an_element(hs::HalfSpace)

Output

This method returns an element on the defining hyperplane.

complement(X::LazySet)

Compute the complement of a set.

Input

• X – set

Output

A set representing the complement of X.

Extended help

complement(H::HalfSpace)

Algorithm

The result is the complementary half-space to H. If $H: ⟨ a, x ⟩ ≤ b$, then this method returns the half-space $H′: ⟨ a, x ⟩ ≥ b$. (Note that complementarity is understood in a relaxed sense, since the intersection of $H$ and $H′$ is non-empty).

constrained_dimensions(hs::HalfSpace)

Return the indices in which a half-space is constrained.

Input

• hs – half-space

Output

A vector of ascending indices i such that the half-space is constrained in dimension i.

Examples

A 2D half-space with constraint $x_1 ≥ 0$ is only constrained in dimension 1.

isuniversal(X::LazySet, witness::Bool=false)

Check whether a set is universal.

Input

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

Output

• If the witness option is deactivated: true iff $X = ℝ^n$
• If the witness option is activated:
  • (true, []) iff $X = ℝ^n$
  • (false, v) iff $X ≠ ℝ^n$ for some $v ∉ X$

Extended help

isuniversal(hs::HalfSpace, [witness]::Bool=false)

Algorithm

Witness production falls back to an_element(::Hyperplane).

normalize(hs::HalfSpace{N}, p::Real=N(2)) where {N}

Normalize a half-space.

Input

• hs – half-space
• p – (optional, default: 2) norm

Output

A new half-space whose normal direction $a$ is normalized, i.e., such that $‖a‖_p = 1$ holds.

rand(T::Type{<:LazySet}; [N]::Type{<:Real}=Float64, [dim]::Int=2,
     [rng]::AbstractRNG=GLOBAL_RNG, [seed]::Union{Int, Nothing}=nothing
    )

Create a random set of the given set type.

Input

• T – set type
• N – (optional, default: Float64) numeric type
• dim – (optional, default: 2) dimension
• rng – (optional, default: GLOBAL_RNG) random number generator
• seed – (optional, default: nothing) seed for reseeding

Output

A random set of the given set type.

Extended help

rand(::Type{HalfSpace}; [N]::Type{<:Real}=Float64, [dim]::Int=2,
     [rng]::AbstractRNG=GLOBAL_RNG, [seed]::Union{Int, Nothing}=nothing)

Algorithm

All numbers are normally distributed with mean 0 and standard deviation 1. Additionally, the constraint a is nonzero.

distance(x::AbstractVector, H::HalfSpace)

Compute the distance between point x and half-space H with respect to the Euclidean norm.

Input

• x – vector
• H – half-space

Output

A scalar representing the distance between point x and half-space H.

∈(x::AbstractVector, X::LazySet)

Check whether a point lies in a set.

Input

• x – point/vector
• X – set

Output

true iff $x ∈ X$.

Extended help

∈(x::AbstractVector, hs::HalfSpace)

Algorithm

This implementation checks whether $x$ satisfies $a⋅x ≤ b$.

project(X::LazySet, block::AbstractVector{Int})

Project a set to a given block by using a concrete linear map.

Input

• X – set
• block – block structure - a vector with the dimensions of interest

Output

A set representing the projection of X to block block.

Extended help

project(H::HalfSpace, block::AbstractVector{Int}; [kwargs...])

Algorithm

If the unconstrained dimensions of H are a subset of the block variables, the projection is applied to the normal direction of H. Otherwise, the projection results in the universal set.

The latter can be seen as follows. Without loss of generality consider projecting out a single and constrained dimension $xₖ$ (projecting out multiple dimensions can be modeled by repeatedly projecting out one dimension). We can write the projection as an existentially quantified linear constraint:

\[ ∃xₖ: a₁x₁ + … + aₖxₖ + … + aₙxₙ ≤ b\]

Since $aₖ ≠ 0$, there is always a value for $xₖ$ that satisfies the constraint for any valuation of the other variables.

Examples

Consider the half-space $x + y + 0⋅z ≤ 1$, whose ambient dimension is 3. The (trivial) projection in the three dimensions using the block of variables [1, 2, 3] is:

julia> H = HalfSpace([1.0, 1.0, 0.0], 1.0)
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0], 1.0)

julia> project(H, [1, 2, 3])
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0], 1.0)

Projecting along dimensions 1 and 2 only:

julia> project(H, [1, 2])
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0], 1.0)

For convenience, one can use project(H, constrained_dimensions(H)) to return the half-space projected on the dimensions where it is constrained:

julia> project(H, constrained_dimensions(H))
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0], 1.0)

If a constrained dimension is projected, we get the universal set of the dimension corresponding to the projection.

julia> project(H, [1, 3])
Universe{Float64}(2)

julia> project(H, [1])
Universe{Float64}(1)

ρ(d::AbstractVector, X::LazySet)

Evaluate the support function of a set in a given direction.

Input

• d – direction
• X – set

Output

The evaluation of the support function of X in direction d.

Notes

A convenience alias support_function is also available.

We have the following identity based on the support vector $σ$:

\[ ρ(d, X) = d ⋅ σ(d, X)\]

Extended help

ρ(d::AbstractVector, hs::HalfSpace)

Output

Unless the direction is (a multiple of) the normal direction of the half-space, the result is Inf.

σ(d::AbstractVector, X::LazySet)

Compute a support vector of a set in a given direction.

Input

• d – direction
• X – set

Output

A support vector of X in direction d.

Notes

A convenience alias support_vector is also available.

Extended help

σ(d::AbstractVector, hs::HalfSpace)

Output

The support vector in the given direction, which is only defined in the following two cases:

1. The direction has norm zero.
2. The direction is (a multiple of) the normal direction of the half-space.

In both cases the result is any point on the boundary (the defining hyperplane). Otherwise this function throws an error.

translate(X::LazySet, v::AbstractVector)

Compute the translation of a set with a vector.

Input

• X – set
• v – vector

Output

A set representing $X + \{v\}$.

Extended help

translate(hs::HalfSpace, v::AbstractVector; [share]::Bool=false)

Notes

The normal vector of the half-space (vector a in a⋅x ≤ b) is shared with the original half-space if share == true.

Algorithm

A half-space $a⋅x ≤ b$ is transformed to the half-space $a⋅x ≤ b + a⋅v$. In other words, we add the dot product $a⋅v$ to $b$.

iscomplement(H1::HalfSpace, H2::HalfSpace)

Check if two half-spaces complement each other.

Input

• H1 – half-space
• H2 – half-space

Output

true iff H1 and H2 are complementary, i.e., have opposite normal directions and identical boundaries (defining hyperplanes).

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

Check whether two sets are disjoint (i.e., do not intersect), 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 is_intersection_empty is also available.

Extended help

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

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

halfspace_left(p::AbstractVector, q::AbstractVector)

Return a half-space describing the 'left' of a two-dimensional line segment through two points.

Input

• p – first point
• q – second point

Output

The half-space whose boundary goes through the two points p and q and which describes the left-hand side of the directed line segment pq.

Algorithm

The half-space $a⋅x ≤ b$ is calculated as a = [dy, -dx], where $d = (dx, dy)$ denotes the line segment pq, i.e., $\vec{d} = \vec{p} - \vec{q}$, and b = dot(p, a).

Examples

The left half-space of the "east" and "west" directions in two-dimensions are the upper and lower half-spaces:

julia> using LazySets: halfspace_left

julia> halfspace_left([0.0, 0.0], [1.0, 0.0])
HalfSpace{Float64, Vector{Float64}}([0.0, -1.0], 0.0)

julia> halfspace_left([0.0, 0.0], [-1.0, 0.0])
HalfSpace{Float64, Vector{Float64}}([0.0, 1.0], 0.0)

We create a box from the sequence of line segments that describe its edges:

julia> H1 = halfspace_left([-1.0, -1.0], [1.0, -1.0]);

julia> H2 = halfspace_left([1.0, -1.0], [1.0, 1.0]);

julia> H3 = halfspace_left([1.0, 1.0], [-1.0, 1.0]);

julia> H4 = halfspace_left([-1.0, 1.0], [-1.0, -1.0]);

julia> H = HPolygon([H1, H2, H3, H4]);

julia> B = BallInf([0.0, 0.0], 1.0);

julia> B ⊆ H && H ⊆ B
true

halfspace_right(p::AbstractVector, q::AbstractVector)

Return a half-space describing the 'right' of a two-dimensional line segment through two points.

Input

• p – first point
• q – second point

Output

The half-space whose boundary goes through the two points p and q and which describes the right-hand side of the directed line segment pq.

Algorithm

See the documentation of halfspace_left.

_ishalfspace(expr::Expr)

Determine whether the given expression corresponds to a half-space.

Input

• expr – a symbolic expression

Output

true if expr corresponds to a half-space or false otherwise.

Examples

julia> using LazySets: _ishalfspace

julia> all(_ishalfspace.([:(x1 <= 0), :(x1 < 0), :(x1 > 0), :(x1 >= 0)]))
true

julia> _ishalfspace(:(x1 = 0))
false

julia> _ishalfspace(:(2*x1 <= 4))
true

julia> _ishalfspace(:(6.1 <= 5.3*f - 0.1*g))
true

julia> _ishalfspace(:(2*x1^2 <= 4))
false

julia> _ishalfspace(:(x1^2 > 4*x2 - x3))
false

julia> _ishalfspace(:(x1 > 4*x2 - x3))
true