From a2be945bea3a00d708efcfbbf3a59a0b1556946f Mon Sep 17 00:00:00 2001 From: schillic Date: Sat, 20 Jul 2024 13:32:10 +0200 Subject: [PATCH] split Require functions for HalfSpace --- src/Sets/HalfSpace/HalfSpace.jl | 101 +++++++++ src/Sets/HalfSpace/HalfSpaceModule.jl | 301 +------------------------- src/Sets/HalfSpace/convert.jl | 83 +++++++ src/Sets/HalfSpace/init.jl | 4 +- src/Sets/HalfSpace/init_SymEngine.jl | 10 + src/Sets/HalfSpace/init_Symbolics.jl | 2 + src/Sets/HalfSpace/ishalfspace.jl | 113 ++++++++++ 7 files changed, 312 insertions(+), 302 deletions(-) create mode 100644 src/Sets/HalfSpace/init_SymEngine.jl create mode 100644 src/Sets/HalfSpace/init_Symbolics.jl create mode 100644 src/Sets/HalfSpace/ishalfspace.jl diff --git a/src/Sets/HalfSpace/HalfSpace.jl b/src/Sets/HalfSpace/HalfSpace.jl index 80ce013786..f790f38704 100644 --- a/src/Sets/HalfSpace/HalfSpace.jl +++ b/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 diff --git a/src/Sets/HalfSpace/HalfSpaceModule.jl b/src/Sets/HalfSpace/HalfSpaceModule.jl index 89f40d5a1c..7e438f1d18 100644 --- a/src/Sets/HalfSpace/HalfSpaceModule.jl +++ b/src/Sets/HalfSpace/HalfSpaceModule.jl @@ -48,6 +48,7 @@ include("constrained_dimensions.jl") include("halfspace_left.jl") include("halfspace_right.jl") include("iscomplement.jl") +include("ishalfspace.jl") include("normalize.jl") include("convert.jl") @@ -98,306 +99,6 @@ _normal_Vector(c::HalfSpace) = HalfSpace(convert(Vector, c.a), c.b) _normal_Vector(C::Vector{<:HalfSpace}) = [_normal_Vector(c) for c in C] _normal_Vector(P::LazySet) = _normal_Vector(constraints_list(P)) -# ============================================ -# Functionality that requires Symbolics -# ============================================ - -function load_symbolics_halfspace() - return quote - using .Symbolics: Symbolic, Num - using ..LazySets: _get_variables, _vec - - # returns `(true, sexpr)` if expr represents a half-space, - # where sexpr is the simplified expression sexpr := LHS - RHS <= 0 - # otherwise, returns `(false, expr)` - function _is_halfspace(expr::Symbolic) - got_halfspace = true - - # find sense and normalize - op = Symbolics.operation(expr) - args = Symbolics.arguments(expr) - if op in (<=, <) - a, b = args - sexpr = Symbolics.simplify(a - b) - - elseif op in (>=, >) - a, b = args - sexpr = Symbolics.simplify(b - a) - - elseif (op == |) && (Symbolics.operation(args[1]) == <) - a, b = Symbolics.arguments(args[1]) - sexpr = Symbolics.simplify(a - b) - - elseif (op == |) && (Symbolics.operation(args[2]) == <) - a, b = Symbolics.arguments(args[2]) - sexpr = Symbolics.simplify(a - b) - - elseif (op == |) && (Symbolics.operation(args[1]) == >) - a, b = Symbolics.arguments(args[1]) - sexpr = Symbolics.simplify(b - a) - - elseif (op == |) && (Symbolics.operation(args[2]) == >) - a, b = Symbolics.arguments(args[2]) - sexpr = Symbolics.simplify(b - a) - - else - got_halfspace = false - end - - return got_halfspace ? (true, sexpr) : (false, expr) - end - - """ - 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 # quote / load_symbolics_halfspace() - -# ===================================== -# Functionality that requires SymEngine -# ===================================== - -function load_symengine_halfspace() - return quote - using .SymEngine: Basic - import .SymEngine: free_symbols - using ..LazySets: _is_linearcombination - - """ - _is_halfspace(expr::Expr) - - Determine whether the given expression corresponds to a half-space. - - ### Input - - - `expr` -- a symbolic expression - - ### Output - - `true` if `expr` corresponds to a half-space or `false` otherwise. - - ### Examples - - ```jldoctest - julia> using LazySets: _is_halfspace - - julia> all(_is_halfspace.([:(x1 <= 0), :(x1 < 0), :(x1 > 0), :(x1 >= 0)])) - true - - julia> _is_halfspace(:(x1 = 0)) - false - - julia> _is_halfspace(:(2*x1 <= 4)) - true - - julia> _is_halfspace(:(6.1 <= 5.3*f - 0.1*g)) - true - - julia> _is_halfspace(:(2*x1^2 <= 4)) - false - - julia> _is_halfspace(:(x1^2 > 4*x2 - x3)) - false - - julia> _is_halfspace(:(x1 > 4*x2 - x3)) - true - ``` - """ - function _is_halfspace(expr::Expr)::Bool - - # check that there are three arguments - # these are the comparison symbol, the left hand side and the right hand side - if (length(expr.args) != 3) || !(expr.head == :call) - return false - end - - # check that this is an inequality - if !(expr.args[1] in [:(<=), :(<), :(>=), :(>)]) - return false - end - - # convert to symengine expressions - lhs, rhs = convert(Basic, expr.args[2]), convert(Basic, expr.args[3]) - - # check if the expression defines a half-space - return _is_linearcombination(lhs) && _is_linearcombination(rhs) - end - - """ - convert(::Type{HalfSpace{N}}, expr::Expr; vars=nothing) where {N} - - Return a `LazySet.HalfSpace` given a symbolic expression that represents a half-space. - - ### Input - - - `expr` -- a symbolic expression - - `vars` -- (optional, default: `nothing`): set of variables with respect to which - the gradient is taken; if nothing, it takes the free symbols in the given expression - - ### Output - - A `HalfSpace`, in the form `ax <= b`. - - ### Examples - - ```jldoctest convert_halfspace - julia> convert(HalfSpace, :(x1 <= -0.03)) - HalfSpace{Float64, Vector{Float64}}([1.0], -0.03) - - julia> convert(HalfSpace, :(x1 < -0.03)) - HalfSpace{Float64, Vector{Float64}}([1.0], -0.03) - - julia> convert(HalfSpace, :(x1 > -0.03)) - HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03) - - julia> convert(HalfSpace, :(x1 >= -0.03)) - HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03) - - julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6)) - HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0) - ``` - - You can also specify the set of "ambient" variables, even if not - all of them appear: - - ```jldoctest convert_halfspace - julia> using SymEngine: Basic - - julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4]) - HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0) - ``` - """ - function convert(::Type{HalfSpace{N}}, expr::Expr; vars::Vector{Basic}=Basic[]) where {N} - @assert _is_halfspace(expr) "the expression :(expr) does not correspond to a half-space" - - # check sense of the inequality, assuming < or <= by default - got_geq = expr.args[1] in [:(>=), :(>)] - - # get sides of the inequality - lhs, rhs = convert(Basic, expr.args[2]), convert(Basic, expr.args[3]) - - # a1 x1 + ... + an xn + K [cmp] 0 for cmp in <, <=, >, >= - eq = lhs - rhs - if isempty(vars) - vars = free_symbols(eq) - end - K = SymEngine.subs(eq, [vi => zero(N) for vi in vars]...) - a = convert(Basic, eq - K) - - # convert to numeric types - K = convert(N, K) - a = convert(Vector{N}, diff.(a, vars)) - - if got_geq - return HalfSpace(-a, K) - else - return HalfSpace(a, -K) - end - end - - # type-less default half-space conversion - function convert(::Type{HalfSpace}, expr::Expr; vars::Vector{Basic}=Basic[]) - return convert(HalfSpace{Float64}, expr; vars=vars) - end - - function free_symbols(expr::Expr, ::Type{<:HalfSpace}) - # get sides of the inequality - lhs, rhs = convert(Basic, expr.args[2]), convert(Basic, expr.args[3]) - return free_symbols(lhs - rhs) - end - end -end # quote / load_symengine_halfspace() - include("init.jl") end # module diff --git a/src/Sets/HalfSpace/convert.jl b/src/Sets/HalfSpace/convert.jl index 4c56be3c63..7c5ce7ad71 100644 --- a/src/Sets/HalfSpace/convert.jl +++ b/src/Sets/HalfSpace/convert.jl @@ -3,3 +3,86 @@ function convert(::Type{HalfSpace{N,Vector{N}}}, hs::HalfSpace{N,<:AbstractVector{N}}) where {N} return HalfSpace(Vector(hs.a), hs.b) end + +function load_SymEngine_convert_HalfSpace() + return quote + using .SymEngine: Basic + + """ + convert(::Type{HalfSpace{N}}, expr::Expr; vars=nothing) where {N} + + Return a `LazySet.HalfSpace` given a symbolic expression that represents a half-space. + + ### Input + + - `expr` -- a symbolic expression + - `vars` -- (optional, default: `nothing`): set of variables with respect to which + the gradient is taken; if nothing, it takes the free symbols in the given expression + + ### Output + + A `HalfSpace`, in the form `ax <= b`. + + ### Examples + + ```jldoctest convert_halfspace + julia> convert(HalfSpace, :(x1 <= -0.03)) + HalfSpace{Float64, Vector{Float64}}([1.0], -0.03) + + julia> convert(HalfSpace, :(x1 < -0.03)) + HalfSpace{Float64, Vector{Float64}}([1.0], -0.03) + + julia> convert(HalfSpace, :(x1 > -0.03)) + HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03) + + julia> convert(HalfSpace, :(x1 >= -0.03)) + HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03) + + julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6)) + HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0) + ``` + + You can also specify the set of "ambient" variables, even if not + all of them appear: + + ```jldoctest convert_halfspace + julia> using SymEngine: Basic + + julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4]) + HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0) + ``` + """ + function convert(::Type{HalfSpace{N}}, expr::Expr; vars::Vector{Basic}=Basic[]) where {N} + @assert _is_halfspace(expr) "the expression :(expr) does not correspond to a half-space" + + # check sense of the inequality, assuming < or <= by default + got_geq = expr.args[1] in [:(>=), :(>)] + + # get sides of the inequality + lhs, rhs = convert(Basic, expr.args[2]), convert(Basic, expr.args[3]) + + # a1 x1 + ... + an xn + K [cmp] 0 for cmp in <, <=, >, >= + eq = lhs - rhs + if isempty(vars) + vars = SymEngine.free_symbols(eq) + end + K = SymEngine.subs(eq, [vi => zero(N) for vi in vars]...) + a = convert(Basic, eq - K) + + # convert to numeric types + K = convert(N, K) + a = convert(Vector{N}, diff.(a, vars)) + + if got_geq + return HalfSpace(-a, K) + else + return HalfSpace(a, -K) + end + end + + # type-less default half-space conversion + function convert(::Type{HalfSpace}, expr::Expr; vars::Vector{Basic}=Basic[]) + return convert(HalfSpace{Float64}, expr; vars=vars) + end + end +end # load_SymEngine_convert_HalfSpace diff --git a/src/Sets/HalfSpace/init.jl b/src/Sets/HalfSpace/init.jl index 6b799e3c5c..d0892a2a4b 100644 --- a/src/Sets/HalfSpace/init.jl +++ b/src/Sets/HalfSpace/init.jl @@ -1,5 +1,5 @@ function __init__() @require LazySets = "b4f0291d-fe17-52bc-9479-3d1a343d9043" include("init_LazySets.jl") - @require SymEngine = "123dc426-2d89-5057-bbad-38513e3affd8" eval(load_symengine_halfspace()) - @require Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7" eval(load_symbolics_halfspace()) + @require SymEngine = "123dc426-2d89-5057-bbad-38513e3affd8" include("init_SymEngine.jl") + @require Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7" include("init_Symbolics.jl") end diff --git a/src/Sets/HalfSpace/init_SymEngine.jl b/src/Sets/HalfSpace/init_SymEngine.jl new file mode 100644 index 0000000000..a377e2ca27 --- /dev/null +++ b/src/Sets/HalfSpace/init_SymEngine.jl @@ -0,0 +1,10 @@ +import .SymEngine: free_symbols + +function free_symbols(expr::Expr, ::Type{<:HalfSpace}) + # get sides of the inequality + lhs, rhs = convert(SymEngine.Basic, expr.args[2]), convert(SymEngine.Basic, expr.args[3]) + return free_symbols(lhs - rhs) +end + +eval(load_SymEngine_ishalfspace()) +eval(load_SymEngine_convert_HalfSpace()) diff --git a/src/Sets/HalfSpace/init_Symbolics.jl b/src/Sets/HalfSpace/init_Symbolics.jl new file mode 100644 index 0000000000..34edc76331 --- /dev/null +++ b/src/Sets/HalfSpace/init_Symbolics.jl @@ -0,0 +1,2 @@ +eval(load_Symbolics_ishalfspace()) +eval(load_Symbolics_HalfSpace()) diff --git a/src/Sets/HalfSpace/ishalfspace.jl b/src/Sets/HalfSpace/ishalfspace.jl new file mode 100644 index 0000000000..34502a0592 --- /dev/null +++ b/src/Sets/HalfSpace/ishalfspace.jl @@ -0,0 +1,113 @@ +function load_SymEngine_ishalfspace() + return quote + using .SymEngine: Basic + import .SymEngine: free_symbols + using ..LazySets: _is_linearcombination + + """ + _is_halfspace(expr::Expr) + + Determine whether the given expression corresponds to a half-space. + + ### Input + + - `expr` -- a symbolic expression + + ### Output + + `true` if `expr` corresponds to a half-space or `false` otherwise. + + ### Examples + + ```jldoctest + julia> using LazySets: _is_halfspace + + julia> all(_is_halfspace.([:(x1 <= 0), :(x1 < 0), :(x1 > 0), :(x1 >= 0)])) + true + + julia> _is_halfspace(:(x1 = 0)) + false + + julia> _is_halfspace(:(2*x1 <= 4)) + true + + julia> _is_halfspace(:(6.1 <= 5.3*f - 0.1*g)) + true + + julia> _is_halfspace(:(2*x1^2 <= 4)) + false + + julia> _is_halfspace(:(x1^2 > 4*x2 - x3)) + false + + julia> _is_halfspace(:(x1 > 4*x2 - x3)) + true + ``` + """ + function _is_halfspace(expr::Expr)::Bool + + # check that there are three arguments + # these are the comparison symbol, the left hand side and the right hand side + if (length(expr.args) != 3) || !(expr.head == :call) + return false + end + + # check that this is an inequality + if !(expr.args[1] in [:(<=), :(<), :(>=), :(>)]) + return false + end + + # convert to symengine expressions + lhs, rhs = convert(Basic, expr.args[2]), convert(Basic, expr.args[3]) + + # check if the expression defines a half-space + return _is_linearcombination(lhs) && _is_linearcombination(rhs) + end + end +end # load_SymEngine_ishalfspace + +function load_Symbolics_ishalfspace() + return quote + using .Symbolics: Symbolic + + # returns `(true, sexpr)` if expr represents a half-space, + # where sexpr is the simplified expression sexpr := LHS - RHS <= 0 + # otherwise, returns `(false, expr)` + function _is_halfspace(expr::Symbolic) + got_halfspace = true + + # find sense and normalize + op = Symbolics.operation(expr) + args = Symbolics.arguments(expr) + if op in (<=, <) + a, b = args + sexpr = Symbolics.simplify(a - b) + + elseif op in (>=, >) + a, b = args + sexpr = Symbolics.simplify(b - a) + + elseif (op == |) && (Symbolics.operation(args[1]) == <) + a, b = Symbolics.arguments(args[1]) + sexpr = Symbolics.simplify(a - b) + + elseif (op == |) && (Symbolics.operation(args[2]) == <) + a, b = Symbolics.arguments(args[2]) + sexpr = Symbolics.simplify(a - b) + + elseif (op == |) && (Symbolics.operation(args[1]) == >) + a, b = Symbolics.arguments(args[1]) + sexpr = Symbolics.simplify(b - a) + + elseif (op == |) && (Symbolics.operation(args[2]) == >) + a, b = Symbolics.arguments(args[2]) + sexpr = Symbolics.simplify(b - a) + + else + got_halfspace = false + end + + return got_halfspace ? (true, sexpr) : (false, expr) + end + end +end # load_Symbolics_ishalfspace