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.

constraints_list(A::AbstractMatrix{N}, b::AbstractVector)

Convert a matrix-vector representation to a linear-constraint representation.

Input

• A – matrix
• b – vector

Output

A list of linear constraints.

isfeasible(constraints::AbstractVector{<:HalfSpace}, [witness]::Bool=false;
           [solver]=nothing)

Check for feasibility of a list of linear constraints.

Input

• constraints – list of linear constraints
• witness – (optional; default: false) flag for witness production
• solver – (optional; default: nothing) LP solver

Output

If witness is false, the result is a Bool.

If witness is true, the result is a pair (res, w) where res is a Bool and w is a witness point/vector.

Algorithm

This implementation converts the constraints to matrix-vector form via tosimplehrep and then calls isfeasible on the result.

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.

remove_redundant_constraints(constraints::AbstractVector{<:HalfSpace}; backend=nothing)

Remove the redundant constraints of a given list of linear constraints.

Input

• constraints – list of constraints
• backend – (optional, default: nothing) the backend used to solve the linear program

Output

The list of constraints with the redundant ones removed, or an empty list if the constraints are infeasible.

Notes

If backend is nothing, it defaults to default_lp_solver(N).

Algorithm

See [remove_redundant_constraints!(::AbstractVector{<:HalfSpace})](@ref) for details.

remove_redundant_constraints!(constraints::AbstractVector{<:HalfSpace}; [backend]=nothing)

Remove the redundant constraints of a given list of linear constraints; the list is updated in-place.

Input

• constraints – list of constraints
• backend – (optional, default: nothing) the backend used to solve the linear program

Output

true if the removal was successful and the list of constraints constraints is modified by removing the redundant constraints, and false only if the constraints are infeasible.

Notes

Note that the result may be true even if the constraints are infeasible. For example, $x ≤ 0 && x ≥ 1$ will return true without removing any constraint. To check if the constraints are infeasible, use isempty(HPolyhedron(constraints)).

If backend is nothing, it defaults to default_lp_solver(N).

Algorithm

If there are m constraints in n dimensions, this function checks one by one if each of the m constraints is implied by the remaining ones.

To check if the k-th constraint is redundant, an LP is formulated using the constraints that have not yet been removed. If, at an intermediate step, it is detected that a subgroup of the constraints is infeasible, this function returns false. If the calculation finished successfully, this function returns true.

For details, see Fukuda's Polyhedra FAQ.

tosimplehrep(constraints::AbstractVector{<:HalfSpace}; [n]::Int=0)

Return the simple H-representation $Ax ≤ b$ from a list of linear constraints.

Input

• constraints – a list of linear constraints
• n – (optional; default: 0) dimension of the constraints

Output

The tuple (A, b) where A is the matrix of normal directions and b is the vector of offsets.

Notes

The parameter n can be used to create a matrix with no constraints but a non-zero dimension. If n ≤ 0, this method takes the dimension of the first constraint.

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.

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