Merge pull request #3603 from JuliaReach/schillic/load

Split Require functions for set modules

src/Sets/HPolyhedron/HPolyhedron.jl

@@ -48,6 +48,17 @@ function HPolyhedron(A::AbstractMatrix, b::AbstractVector)
     return HPolyhedron(constraints_list(A, b))
 end
 
+function load_Polyhedra_HPolyhedron()
+    return quote
+        using .Polyhedra: HRep
+
+        # convenience conversion method
+        function HPolyhedron(P::HRep{N}) where {N}
+            return convert(HPolyhedron, P)
+        end
+    end
+end  # load_Polyhedra_HPolyhedron
+
 function load_symbolics_hpolyhedron()
     return quote
         using .Symbolics: Num

src/Sets/HPolyhedron/HPolyhedronModule.jl

@@ -51,46 +51,6 @@ include("addconstraint.jl")
 
 include("convert.jl")
 
-function load_polyhedra_hpolyhedron() # function to be loaded by Requires
-    return quote
-        using .Polyhedra: HRep,
-                          polyhedron
-
-        """
-             convert(::Type{HPolyhedron}, P::HRep{N}) where {N}
-
-        Convert an `HRep` polyhedron from `Polyhedra.jl` to a polyhedron in constraint
-        representation .
-
-        ### Input
-
-        - `HPolyhedron` -- target type
-        - `P`           -- `HRep` polyhedron
-
-        ### Output
-
-        An `HPolyhedron`.
-        """
-        function convert(::Type{HPolyhedron}, P::HRep{N}) where {N}
-            VN = Polyhedra.hvectortype(P)
-            constraints = Vector{HalfSpace{N,VN}}()
-            for hi in Polyhedra.allhalfspaces(P)
-                a, b = hi.a, hi.β
-                if isapproxzero(norm(a))
-                    continue
-                end
-                push!(constraints, HalfSpace(a, b))
-            end
-            return HPolyhedron(constraints)
-        end
-
-        # convenience conversion method
-        function HPolyhedron(P::HRep{N}) where {N}
-            return convert(HPolyhedron, P)
-        end
-    end
-end  # quote / load_polyhedra_hpolyhedron()
-
 include("init.jl")
 
 end  # module

src/Sets/HPolyhedron/convert.jl

@@ -31,3 +31,37 @@ function convert(::Type{HPolyhedron{N,VT}}, X::LazySet) where {N,VT}
     end
     return HPolyhedron([HalfSpace(VT(c.a), N(c.b)) for c in constraints(X)])
 end
+
+function load_Polyhedra_convert_HPolyhedron()
+    return quote
+        using .Polyhedra: HRep
+
+        """
+             convert(::Type{HPolyhedron}, P::HRep{N}) where {N}
+
+        Convert an `HRep` polyhedron from `Polyhedra.jl` to a polyhedron in constraint
+        representation .
+
+        ### Input
+
+        - `HPolyhedron` -- target type
+        - `P`           -- `HRep` polyhedron
+
+        ### Output
+
+        An `HPolyhedron`.
+        """
+        function convert(::Type{HPolyhedron}, P::HRep{N}) where {N}
+            VN = Polyhedra.hvectortype(P)
+            constraints = Vector{HalfSpace{N,VN}}()
+            for hi in Polyhedra.allhalfspaces(P)
+                a, b = hi.a, hi.β
+                if isapproxzero(norm(a))
+                    continue
+                end
+                push!(constraints, HalfSpace(a, b))
+            end
+            return HPolyhedron(constraints)
+        end
+    end
+end  # load_Polyhedra_convert_HPolyhedron

src/Sets/HPolyhedron/init.jl

@@ -1,5 +1,5 @@
 function __init__()
     @require LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043" include("init_LazySets.jl")
-    @require Polyhedra = "67491407-f73d-577b-9b50-8179a7c68029" eval(load_polyhedra_hpolyhedron())
+    @require Polyhedra = "67491407-f73d-577b-9b50-8179a7c68029" include("init_Polyhedra.jl")
     @require Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7" eval(load_symbolics_hpolyhedron())
 end

src/Sets/HPolyhedron/init_Polyhedra.jl

@@ -0,0 +1,2 @@
+eval(load_Polyhedra_convert_HPolyhedron())
+eval(load_Polyhedra_HPolyhedron())

src/Sets/HPolyhedron/tovrep.jl

@@ -26,6 +26,6 @@ function tovrep(P::HPoly; backend=default_polyhedra_backend(P))
     require(@__MODULE__, :LazySets; fun_name="tovrep")
     require(@__MODULE__, :Polyhedra; fun_name="tovrep")
 
-    P = polyhedron(P; backend=backend)
+    P = LazySets.polyhedron(P; backend=backend)
     return VPolytope(P)
 end

src/Sets/HPolytope/HPolytope.jl

@@ -77,6 +77,30 @@ function HPolytope(A::AbstractMatrix, b::AbstractVector;
     return HPolytope(constraints_list(A, b); check_boundedness=check_boundedness)
 end
 
+function load_Polyhedra_HPolytope()
+    return quote
+        using .Polyhedra: HRep
+
+        """
+            HPolytope(P::HRep)
+
+        Return a polytope in constraint representation given an `HRep` polyhedron from
+        `Polyhedra.jl`.
+
+        ### Input
+
+        - `P` -- `HRep` polyhedron
+
+        ### Output
+
+        An `HPolytope`.
+        """
+        function HPolytope(P::HRep)
+            return convert(HPolytope, P)
+        end
+    end
+end  # load_Polyhedra_HPolytope
+
 function load_symbolics_hpolytope()
     return quote
         using .Symbolics: Num

src/Sets/HPolytope/HPolytopeModule.jl

@@ -28,45 +28,6 @@ include("linear_map.jl")
 
 include("convert.jl")
 
-function load_polyhedra_hpolytope() # function to be loaded by Requires
-    return quote
-        using .Polyhedra: HRep
-
-        function convert(::Type{HPolytope}, P::HRep{N}) where {N}
-            VT = Polyhedra.hvectortype(P)
-            constraints = Vector{HalfSpace{N,VT}}()
-            for hi in Polyhedra.allhalfspaces(P)
-                a, b = hi.a, hi.β
-                if isapproxzero(norm(a))
-                    @assert b >= zero(N) "the half-space is inconsistent since it " *
-                                         "has a zero normal direction but the constraint is negative"
-                    continue
-                end
-                push!(constraints, HalfSpace(hi.a, hi.β))
-            end
-            return HPolytope(constraints)
-        end
-
-        """
-            HPolytope(P::HRep)
-
-        Return a polytope in constraint representation given an `HRep` polyhedron from
-        `Polyhedra.jl`.
-
-        ### Input
-
-        - `P` -- `HRep` polyhedron
-
-        ### Output
-
-        An `HPolytope`.
-        """
-        function HPolytope(P::HRep)
-            return convert(HPolytope, P)
-        end
-    end
-end  # quote / load_polyhedra_hpolytope()
-
 include("init.jl")
 
 end  # module

src/Sets/HPolytope/convert.jl

@@ -31,3 +31,24 @@ function convert(::Type{HPolytope{N,VT}}, X::LazySet) where {N,VT}
     end
     return HPolytope([HalfSpace(VT(c.a), N(c.b)) for c in constraints_list(X)])
 end
+
+function load_Polyhedra_convert_HPolytope()
+    return quote
+        using .Polyhedra: HRep
+
+        function convert(::Type{HPolytope}, P::HRep{N}) where {N}
+            VT = Polyhedra.hvectortype(P)
+            constraints = Vector{HalfSpace{N,VT}}()
+            for hi in Polyhedra.allhalfspaces(P)
+                a, b = hi.a, hi.β
+                if isapproxzero(norm(a))
+                    @assert b >= zero(N) "the half-space is inconsistent since it " *
+                                         "has a zero normal direction but the constraint is negative"
+                    continue
+                end
+                push!(constraints, HalfSpace(hi.a, hi.β))
+            end
+            return HPolytope(constraints)
+        end
+    end
+end  # load_Polyhedra_convert_HPolytope

src/Sets/HPolytope/init.jl

@@ -1,5 +1,5 @@
 function __init__()
     @require LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043" include("init_LazySets.jl")
-    @require Polyhedra = "67491407-f73d-577b-9b50-8179a7c68029" eval(load_polyhedra_hpolytope())
+    @require Polyhedra = "67491407-f73d-577b-9b50-8179a7c68029" include("init_Polyhedra.jl")
     @require Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7" eval(load_symbolics_hpolytope())
 end

src/Sets/HPolytope/init_Polyhedra.jl

@@ -0,0 +1,2 @@
+eval(load_Polyhedra_convert_HPolytope())
+eval(load_Polyhedra_HPolytope())

src/Sets/HalfSpace/HalfSpace.jl

@@ -34,3 +34,104 @@ struct HalfSpace{N,VN<:AbstractVector{N}} <: AbstractPolyhedron{N}
         return new{N,VN}(a, b)
     end
 end
+
+function load_Symbolics_HalfSpace()
+    return quote
+        using .Symbolics: Num
+        using ..LazySets: _get_variables, _vec
+
+        """
+            HalfSpace(expr::Num, vars=_get_variables(expr); [N]::Type{<:Real}=Float64)
+
+        Return the half-space given by a symbolic expression.
+
+        ### Input
+
+        - `expr` -- symbolic expression that describes a half-space
+        - `vars` -- (optional, default: `get_variables(expr)`) if an array of variables
+                    is given, use those as the ambient variables in the set with respect
+                    to which derivations take place; otherwise, use only the variables
+                    that appear in the given expression (but be careful because the
+                    order may be incorrect; it is advised to always pass `vars`
+                    explicitly; see the examples below for details)
+        - `N`    -- (optional, default: `Float64`) the numeric type of the half-space
+
+        ### Output
+
+        A `HalfSpace`.
+
+        ### Examples
+
+        ```jldoctest halfspace_symbolics
+        julia> using Symbolics
+
+        julia> vars = @variables x y
+        2-element Vector{Num}:
+         x
+         y
+
+        julia> HalfSpace(x - y <= 2, vars)
+        HalfSpace{Float64, Vector{Float64}}([1.0, -1.0], 2.0)
+
+        julia> HalfSpace(x >= y, vars)
+        HalfSpace{Float64, Vector{Float64}}([-1.0, 1.0], -0.0)
+
+        julia> vars = @variables x[1:4]
+        1-element Vector{Symbolics.Arr{Num, 1}}:
+         x[1:4]
+
+        julia> HalfSpace(x[1] >= x[2], x)
+        HalfSpace{Float64, Vector{Float64}}([-1.0, 1.0, 0.0, 0.0], -0.0)
+        ```
+
+        Be careful with using the default `vars` value because it may introduce a wrong
+        order.
+
+        ```@example halfspace_symbolics  # doctest deactivated due to downgrade of Symbolics
+        julia> HalfSpace(2x ≥ 5y - 1) # correct
+        HalfSpace{Float64, Vector{Float64}}([-2.0, 5.0], 1.0)
+
+        julia> HalfSpace(2x ≥ 5y - 1, vars) # correct
+        HalfSpace{Float64, Vector{Float64}}([-2.0, 5.0], 1.0)
+
+        julia> HalfSpace(y - x ≥ 1) # incorrect
+        HalfSpace{Float64, Vector{Float64}}([-1.0, 1.0], -1.0)
+
+        julia> HalfSpace(y - x ≥ 1, vars) # correct
+        HalfSpace{Float64, Vector{Float64}}([1.0, -1.0], -1.0)
+        julia> nothing  # hide
+        ```
+
+        ### Algorithm
+
+        It is assumed that the expression is of the form
+        `α*x1 + ⋯ + α*xn + γ CMP β*x1 + ⋯ + β*xn + δ`,
+        where `CMP` is one among `<`, `<=`, `≤`, `>`, `>=` or `≥`.
+        This expression is transformed, by rearrangement and substitution, into the
+        canonical form `a1 * x1 + ⋯ + an * xn ≤ b`. The method used to identify the
+        coefficients is to take derivatives with respect to the ambient variables `vars`.
+        Therefore, the order in which the variables appear in `vars` affects the final
+        result. Note in particular that strict inequalities are relaxed as being
+        smaller-or-equal. Finally, the returned set is the half-space with normal vector
+        `[a1, …, an]` and displacement `b`.
+        """
+        function HalfSpace(expr::Num, vars::AbstractVector{Num}; N::Type{<:Real}=Float64)
+            valid, sexpr = _is_halfspace(Symbolics.value(expr))
+            if !valid
+                throw(ArgumentError("expected an expression describing a half-space, got $expr"))
+            end
+
+            # compute the linear coefficients by taking first-order derivatives
+            coeffs = [N(α.val) for α in Symbolics.gradient(sexpr, collect(vars))]
+
+            # get the constant term by expression substitution
+            zeroed_vars = Dict(v => zero(N) for v in vars)
+            β = -N(Symbolics.substitute(sexpr, zeroed_vars))
+
+            return HalfSpace(coeffs, β)
+        end
+
+        HalfSpace(expr::Num; N::Type{<:Real}=Float64) = HalfSpace(expr, _get_variables(expr); N=N)
+        HalfSpace(expr::Num, vars; N::Type{<:Real}=Float64) = HalfSpace(expr, _vec(vars); N=N)
+    end
+end  # load_Symbolics_HalfSpace