#1267 - isdisjoint for Zonotopes

docs/src/lib/binary_functions.md

@@ -35,6 +35,7 @@ is_intersection_empty(::UnionSet{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
 is_intersection_empty(::UnionSetArray{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
 is_intersection_empty(::Universe{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
 is_intersection_empty(::Complement{N}, ::LazySet{N}, ::Bool=false) where {N<:Real}
+is_intersection_empty(::Zonotope{N}, ::Zonotope{N}, ::Bool=false) where {N<:Real}
 ```
 
 ## Convex hull

src/is_intersection_empty.jl

@@ -381,6 +381,47 @@ function is_intersection_empty(H::Hyperplane{N},
     return is_intersection_empty(Z, H, witness)
 end
 
+"""
+    is_intersection_empty(Z1::Zonotope{N}, Z2::Zonotope{N}, witness::Bool=false
+                         ) where {N<:Real}
+
+Check whether two zonotopes do not intersect, and otherwise optionally compute a
+witness.
+
+### Input
+
+- `Z1`      -- zonotope
+- `Z2`      -- zonotope
+- `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
+
+``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``.
+"""
+function is_intersection_empty(Z1::Zonotope{N}, Z2::Zonotope{N},
+                               witness::Bool=false) where {N<:Real}
+    n = dim(Z1)
+    @assert n == dim(Z2) "zonotopes need to have the same dimensions"
+    Z = Zonotope(zeros(N, n), hcat(Z1.generators, Z2.generators))
+    result = (center(Z1) - center(Z2)) ∈ Z
+    if result
+        return witness ? (true, N[]) : true
+    elseif witness
+        error("witness production is not supported yet")
+    else
+        return false
+    end
+end
+
 """
     is_intersection_empty(ls1::LineSegment{N},
                           ls2::LineSegment{N},

test/unit_Zonotope.jl

@@ -88,6 +88,13 @@ for N in [Float64, Rational{Int}, Float32]
     @test !is_intersection_empty(H1, Z1)
     @test is_intersection_empty(H2, Z1) && is_intersection_empty(H2, Z1, true)[1]
 
+    # isdisjoint
+    result, w = isdisjoint(Z1, Z2, true)
+    @test isdisjoint(Z1, Z2) && result && w == N[]
+    Z3 = Zonotope(N[2, 1], Matrix{N}(I, 2, 2))
+    @test_throws ErrorException isdisjoint(Z2, Z3, true)
+    @test !isdisjoint(Z2, Z3)
+
     # test number of generators
     Z = Zonotope(N[2, 1], N[-0.5 1.5 0.5 1; 0.5 1.5 1 0.5])
     @test ngens(Z) == 4