Skip to content

Commit

Permalink
Merge pull request #3474 from JuliaReach/schillic/1193
Browse files Browse the repository at this point in the history
#1193 - Concrete translation of lazy operations
  • Loading branch information
schillic authored Mar 18, 2024
2 parents 79981c4 + ad3e284 commit a01c906
Show file tree
Hide file tree
Showing 13 changed files with 77 additions and 3 deletions.
9 changes: 8 additions & 1 deletion src/LazyOperations/AffineMap.jl
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ function AffineMap(M::AbstractMatrix, Z::ZeroSet, v::AbstractVector)
end

# EmptySet is absorbing for AffineMap
function AffineMap(M::AbstractMatrix, ∅::EmptySet, v::AbstractVector)
function AffineMap(::AbstractMatrix, ∅::EmptySet, ::AbstractVector)
return
end

Expand All @@ -167,3 +167,10 @@ end
function isboundedtype(::Type{<:AffineMap{N,S}}) where {N,S}
return isboundedtype(S)
end

function translate(am::AffineMap, x::AbstractVector)
M = matrix(am)
X = set(am)
v = vector(am)
return AffineMap(M, X, v + x)
end
4 changes: 4 additions & 0 deletions src/LazyOperations/Bloating.jl
Original file line number Diff line number Diff line change
Expand Up @@ -253,3 +253,7 @@ norm for bloating is either 1-norm or the infinity norm.
function is_polyhedral(B::Bloating)
return (B.p == 1 || B.p == Inf) && is_polyhedral(B.X)
end

function translate(B::Bloating, x::AbstractVector)
return Bloating(translate(B.X, x), B.ε, B.p)
end
8 changes: 8 additions & 0 deletions src/LazyOperations/CartesianProduct.jl
Original file line number Diff line number Diff line change
Expand Up @@ -509,3 +509,11 @@ The volume.
function volume(cp::CartesianProduct)
return volume(cp.X) * volume(cp.Y)
end

function translate(cp::CartesianProduct, x::AbstractVector)
X = first(cp)
n1 = dim(X)
X = translate(X, @view(x[1:n1]))
Y = translate(second(cp), @view(x[(n1 + 1):end]))
return CartesianProduct(X, Y)
end
11 changes: 11 additions & 0 deletions src/LazyOperations/CartesianProductArray.jl
Original file line number Diff line number Diff line change
Expand Up @@ -744,3 +744,14 @@ The volume.
function volume(cpa::CartesianProductArray)
return prod(volume, array(cpa))
end

function translate(cpa::CartesianProductArray, x::AbstractVector)
res = Vector{LazySet}(undef, length(array(cpa)))
s = 1
@inbounds for (j, Xj) in enumerate(array(cpa))
e = s + dim(Xj) - 1
res[j] = translate(Xj, @view(x[s:e]))
s = e + 1
end
return CartesianProductArray([X for X in res])
end
4 changes: 4 additions & 0 deletions src/LazyOperations/Complement.jl
Original file line number Diff line number Diff line change
Expand Up @@ -158,3 +158,7 @@ function constraints_list(C::Complement)
end
return out
end

function translate(C::Complement, x::AbstractVector)
return Complement(translate(C.X, x))
end
6 changes: 6 additions & 0 deletions src/LazyOperations/ConvexHull.jl
Original file line number Diff line number Diff line change
Expand Up @@ -217,3 +217,9 @@ function vertices_list(ch::ConvexHull;
end
return vlist
end

function translate(ch::ConvexHull, x::AbstractVector)
X = translate(first(ch), x)
Y = translate(second(ch), x)
return ConvexHull(X, Y)
end
4 changes: 4 additions & 0 deletions src/LazyOperations/ConvexHullArray.jl
Original file line number Diff line number Diff line change
Expand Up @@ -240,3 +240,7 @@ function concretize(cha::ConvexHullArray)
end
return X
end

function translate(cha::ConvexHullArray, x::AbstractVector)
return ConvexHullArray([translate(X, x) for X in array(cha)])
end
6 changes: 6 additions & 0 deletions src/LazyOperations/Intersection.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1001,3 +1001,9 @@ end
function volume(cap::Intersection)
return volume(intersection(cap.X, cap.Y))
end

function translate(cap::Intersection, x::AbstractVector)
X = translate(first(cap), x)
Y = translate(second(cap), x)
return Intersection(X, Y; cache=cap.cache)
end
4 changes: 4 additions & 0 deletions src/LazyOperations/IntersectionArray.jl
Original file line number Diff line number Diff line change
Expand Up @@ -222,3 +222,7 @@ function concretize(ia::IntersectionArray)
end
return X
end

function translate(ia::IntersectionArray, x::AbstractVector)
return IntersectionArray([translate(X, x) for X in array(ia)])
end
6 changes: 6 additions & 0 deletions src/LazyOperations/MinkowskiSum.jl
Original file line number Diff line number Diff line change
Expand Up @@ -295,3 +295,9 @@ We compute the concrete Minkowski sum (via `minkowski_sum`) and call
function vertices_list(ms::MinkowskiSum)
return vertices_list(minkowski_sum(ms.X, ms.Y))
end

function translate(ms::MinkowskiSum, x::AbstractVector)
X = translate(first(ms), x)
Y = translate(second(ms), x)
return MinkowskiSum(X, Y)
end
4 changes: 4 additions & 0 deletions src/LazyOperations/MinkowskiSumArray.jl
Original file line number Diff line number Diff line change
Expand Up @@ -220,3 +220,7 @@ function concretize(msa::MinkowskiSumArray)
end
return X
end

function translate(msa::MinkowskiSumArray, x::AbstractVector)
return MinkowskiSumArray([translate(X, x) for X in array(msa)])
end
4 changes: 4 additions & 0 deletions src/LazyOperations/Translation.jl
Original file line number Diff line number Diff line change
Expand Up @@ -386,3 +386,7 @@ The translation of the center of the wrapped set by the translation vector.
function center(tr::Translation)
return center(tr.X) + tr.v
end

function translate(tr::Translation, x::AbstractVector)
return Translation(translate(tr.X, x))
end
10 changes: 8 additions & 2 deletions src/LazyOperations/UnionSet.jl
Original file line number Diff line number Diff line change
Expand Up @@ -281,6 +281,12 @@ function volume(cup::UnionSet)
return volume(cup.X) + volume(cup.Y) - volume(Intersection(cup.X, cup.Y))
end

function convex_hull(X::UnionSet)
return convex_hull(X.X, X.Y)
function convex_hull(cup::UnionSet)
return convex_hull(cup.X, cup.Y)
end

function translate(cup::UnionSet, x::AbstractVector)
X = translate(first(cup), x)
Y = translate(second(cup), x)
return UnionSet(X, Y)
end

0 comments on commit a01c906

Please sign in to comment.