From e85b7df8f710bc1ffba95e78eaf50074b3c239ec Mon Sep 17 00:00:00 2001 From: Marcelo Date: Fri, 13 May 2022 23:00:53 +0200 Subject: [PATCH 1/3] add special cases for disjointness and inclusion involving universe --- src/ConcreteOperations/isdisjoint.jl | 6 ++++++ src/ConcreteOperations/issubset.jl | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/src/ConcreteOperations/isdisjoint.jl b/src/ConcreteOperations/isdisjoint.jl index 3503738df4..8b99279e67 100644 --- a/src/ConcreteOperations/isdisjoint.jl +++ b/src/ConcreteOperations/isdisjoint.jl @@ -1373,3 +1373,9 @@ end @inline function _det(L1::Line2D, L2::Line2D) @inbounds det = L1.a[1] * L2.a[2] - L1.a[2] * L2.a[1] end + +@commutative function isdisjoint(C::CartesianProduct{N, <:LazySet, <:Universe}, Z::AbstractZonotope) where N + X = C.X + Zp = project(Z, 1:dim(X)) + return isdisjoint(X, Zp) +end diff --git a/src/ConcreteOperations/issubset.jl b/src/ConcreteOperations/issubset.jl index e11abe9394..f480dd2ae7 100644 --- a/src/ConcreteOperations/issubset.jl +++ b/src/ConcreteOperations/issubset.jl @@ -1091,3 +1091,9 @@ function ⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, witness::Bool=false end return true end + +function ⊆(Z::AbstractZonotope, C::CartesianProduct{N, <:LazySet, <:Universe}) where N + X = C.X + Zp = project(Z, 1:dim(X)) + return ⊆(Zp, X) +end From e0bd90a2edd06c78d9d88c0300c17aec21d2e4e0 Mon Sep 17 00:00:00 2001 From: Marcelo Forets Date: Fri, 13 May 2022 14:28:45 -0700 Subject: [PATCH 2/3] Update src/ConcreteOperations/issubset.jl Co-authored-by: Christian Schilling --- src/ConcreteOperations/issubset.jl | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ConcreteOperations/issubset.jl b/src/ConcreteOperations/issubset.jl index f480dd2ae7..0ff88d9c3e 100644 --- a/src/ConcreteOperations/issubset.jl +++ b/src/ConcreteOperations/issubset.jl @@ -1097,3 +1097,9 @@ function ⊆(Z::AbstractZonotope, C::CartesianProduct{N, <:LazySet, <:Universe}) Zp = project(Z, 1:dim(X)) return ⊆(Zp, X) end + +function ⊆(Z::AbstractZonotope, C::CartesianProduct{N, <:Universe, <:LazySet}) where N + Y = C.Y + Zp = project(Z, dim(C.X)+1:dim(C)) + return ⊆(Zp, Y) +end From 4b4b839f9595923d8aba770baee27b1d2f20d881 Mon Sep 17 00:00:00 2001 From: schillic Date: Sat, 14 May 2022 09:46:53 +0200 Subject: [PATCH 3/3] fix ambiguities --- src/ConcreteOperations/isdisjoint.jl | 21 +++++++++++++++++---- src/ConcreteOperations/issubset.jl | 25 ++++++++++++++++--------- 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/src/ConcreteOperations/isdisjoint.jl b/src/ConcreteOperations/isdisjoint.jl index 8b99279e67..4d54c607f6 100644 --- a/src/ConcreteOperations/isdisjoint.jl +++ b/src/ConcreteOperations/isdisjoint.jl @@ -1374,8 +1374,21 @@ end @inbounds det = L1.a[1] * L2.a[2] - L1.a[2] * L2.a[1] end -@commutative function isdisjoint(C::CartesianProduct{N, <:LazySet, <:Universe}, Z::AbstractZonotope) where N - X = C.X - Zp = project(Z, 1:dim(X)) - return isdisjoint(X, Zp) +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 index 0ff88d9c3e..62dffc7d86 100644 --- a/src/ConcreteOperations/issubset.jl +++ b/src/ConcreteOperations/issubset.jl @@ -1092,14 +1092,21 @@ function ⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, witness::Bool=false return true end -function ⊆(Z::AbstractZonotope, C::CartesianProduct{N, <:LazySet, <:Universe}) where N - X = C.X - Zp = project(Z, 1:dim(X)) - return ⊆(Zp, X) -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 -function ⊆(Z::AbstractZonotope, C::CartesianProduct{N, <:Universe, <:LazySet}) where N - Y = C.Y - Zp = project(Z, dim(C.X)+1:dim(C)) - return ⊆(Zp, Y) + # disambiguation + @eval function ⊆(Z::$(ST), C::CartesianProduct{N, <:Universe, <:Universe}) where N + return true + end end