Add special cases for disjointness and inclusion involving universe (#…

…2964) * add special cases for disjointness and inclusion involving universe * Update src/ConcreteOperations/issubset.jl Co-authored-by: Christian Schilling <[email protected]> * fix ambiguities Co-authored-by: Marcelo <[email protected]> Co-authored-by: Christian Schilling <[email protected]>
JuliaReach · May 14, 2022 · 508d38d · 508d38d
1 parent f390b6c
commit 508d38d
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 0 deletions.
diff --git a/src/ConcreteOperations/isdisjoint.jl b/src/ConcreteOperations/isdisjoint.jl
@@ -1373,3 +1373,22 @@ end
 @inline function _det(L1::Line2D, L2::Line2D)
     @inbounds det = L1.a[1] * L2.a[2] - L1.a[2] * L2.a[1]
 end
+
+for ST in (AbstractZonotope, AbstractSingleton)
+    @eval @commutative function isdisjoint(C::CartesianProduct{N, <:LazySet, <:Universe}, Z::$(ST)) where N
+        X = C.X
+        Zp = project(Z, 1:dim(X))
+        return isdisjoint(X, Zp)
+    end
+
+    @eval @commutative function isdisjoint(C::CartesianProduct{N, <:Universe, <:LazySet}, Z::$(ST)) where N
+        Y = C.Y
+        Zp = project(Z, dim(C.X)+1:dim(C))
+        return isdisjoint(Y, Zp)
+    end
+
+    # disambiguation
+    @eval @commutative function isdisjoint(C::CartesianProduct{N, <:Universe, <:Universe}, Z::$(ST)) where N
+        return false
+    end
+end
diff --git a/src/ConcreteOperations/issubset.jl b/src/ConcreteOperations/issubset.jl
@@ -1091,3 +1091,22 @@ function ⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, witness::Bool=false
     end
     return true
 end
+
+for ST in (AbstractZonotope, AbstractSingleton, LineSegment)
+    @eval function ⊆(Z::$(ST), C::CartesianProduct{N, <:LazySet, <:Universe}) where N
+        X = C.X
+        Zp = project(Z, 1:dim(X))
+        return ⊆(Zp, X)
+    end
+
+    @eval function ⊆(Z::$(ST), C::CartesianProduct{N, <:Universe, <:LazySet}) where N
+        Y = C.Y
+        Zp = project(Z, dim(C.X)+1:dim(C))
+        return ⊆(Zp, Y)
+    end
+
+    # disambiguation
+    @eval function ⊆(Z::$(ST), C::CartesianProduct{N, <:Universe, <:Universe}) where N
+        return true
+    end
+end