Merge pull request #4062 from JuliaReach/schillic/issubset_zonotope_witness

Add witness production in `⊆` for `AbstractZonotope`

Author: schillic

src/ConcreteOperations/issubset.jl

@@ -236,7 +236,9 @@ function _issubset_zonotope_in_polyhedron(Z::AbstractZonotope, P::LazySet,
     elseif !witness
         return false
     end
-    throw(ArgumentError("witness production is not supported yet"))
+    # fall back to default algorithm for witness production
+    # TODO more efficient implementation
+    return _issubset_constraints_list(Z, P, witness)
 end
 
 # for documentation see

test/ConcreteOperations/issubset.jl

@@ -80,8 +80,8 @@ for N in @tN([Float64, Float32, Rational{Int}])
     @test Z ⊆ P && res && w == N[]
     P = HPolyhedron([HalfSpace(N[1, 0], N(1)), HalfSpace(N[-1, 0], N(0)),
                      HalfSpace(N[0, 1], N(3)), HalfSpace(N[0, -1], N(0))])
-    @test !(Z ⊆ P)
-    @test_throws ArgumentError issubset(Z, P, true)  # not implemented; parser requires `issubset`
+    res, w = ⊆(Z, P, true)
+    @test !(Z ⊆ P) && !res && w isa Vector{N} && w ∈ Z && w ∉ P
     # corner case: no generator
     Z = Zonotope(N[2], zeros(N, 1, 0))
     P = convert(HPolytope, Interval(N(1), N(3)))

test/Sets/Zonotope.jl

@@ -674,18 +674,16 @@ for N in @tN([Float64, Float32, Rational{Int}])
 
     # isstrictsubset
     @test_throws DimensionMismatch Z ⊂ Z3
-    for Z2 in (Z, P)
-        @test !(Z2 ⊂ Z)
-        res, w = ⊂(Z2, Z, true)
+    Z2a = Zonotope(N[1, 2], N[1 0; 0 1])
+    for Z2b in (Z, P, Z2a)
+        @test !(Z2b ⊂ Z)
+        res, w = ⊂(Z2b, Z, true)
         @test !res && w isa Vector{N} && isempty(w)
     end
-    Z2 = Zonotope(N[1, 2], N[1 0; 0 1])
-    @test_broken ⊂(Z2, Z, true) isa Tuple  # TODO support witness production, then integrate in loop above
     Z2 = Zonotope(N[1, 2], N[4 0; 0 6])
     @test Z ⊂ Z2
-    @test_broken ⊂(Z, Z2, true) isa Tuple  # TODO support witness production
-    # res, w = ⊂(Z, Z2, true)
-    # @test res && w isa Vector{N} && w ∉ Z && w ∈ Z2
+    res, w = ⊂(Z, Z2, true)
+    @test res && w isa Vector{N} && w ∉ Z && w ∈ Z2
 
     # issubset
     @test_throws DimensionMismatch Z ⊆ Z3
@@ -696,9 +694,8 @@ for N in @tN([Float64, Float32, Rational{Int}])
     end
     Z2 = Zonotope(N[3, 0], N[1 0; 0 1])
     @test Z ⊈ Z2
-    @test_broken ⊆(Z, Z2, true) isa Tuple  # TODO this should work
-    # res, w = ⊆(Z, Z2, true)
-    # @test !res && w isa Vector{N} && w ∈ Z && w ∉ Z2
+    res, w = ⊆(Z, Z2, true)
+    @test !res && w isa Vector{N} && w ∈ Z && w ∉ Z2
 
     # linear_combination
     @test_throws DimensionMismatch linear_combination(Z, Z3)