From 4c7319472ab821e95a4837169d9be441d1a085a3 Mon Sep 17 00:00:00 2001 From: schillic Date: Mon, 17 Jun 2024 21:52:22 +0200 Subject: [PATCH 1/2] outsource SymEngine code to LazySets --- Project.toml | 2 +- docs/Project.toml | 2 +- docs/src/lib/methods.md | 10 -- src/SpaceExParser.jl | 9 +- src/convert.jl | 358 ---------------------------------------- src/symbolic.jl | 6 +- test/Project.toml | 2 +- 7 files changed, 10 insertions(+), 379 deletions(-) delete mode 100644 src/convert.jl diff --git a/Project.toml b/Project.toml index 5da7843..a8a1ac7 100644 --- a/Project.toml +++ b/Project.toml @@ -14,7 +14,7 @@ SymEngine = "123dc426-2d89-5057-bbad-38513e3affd8" DataStructures = "0" EzXML = "1" HybridSystems = "0.4" -LazySets = "1, 2" +LazySets = "2.14" MathematicalSystems = "0.11, 0.12, 0.13" SymEngine = "0.7, 0.8, 0.9, 0.10, 0.11, 0.12" julia = "1.2" diff --git a/docs/Project.toml b/docs/Project.toml index a58d2f6..3a99411 100644 --- a/docs/Project.toml +++ b/docs/Project.toml @@ -5,5 +5,5 @@ SymEngine = "123dc426-2d89-5057-bbad-38513e3affd8" [compat] Documenter = "1" -LazySets = "2" +LazySets = "2.14" SymEngine = "0.11, 0.12" diff --git a/docs/src/lib/methods.md b/docs/src/lib/methods.md index e99056b..00bd5bd 100644 --- a/docs/src/lib/methods.md +++ b/docs/src/lib/methods.md @@ -29,13 +29,3 @@ add_transition_label! parse_location parse_transition ``` - -### Conversion of symbolic expressions into sets - -```@docs -convert -free_symbols -is_halfspace -is_hyperplane -is_linearcombination -``` diff --git a/src/SpaceExParser.jl b/src/SpaceExParser.jl index 7cfde31..719fca5 100644 --- a/src/SpaceExParser.jl +++ b/src/SpaceExParser.jl @@ -20,8 +20,8 @@ using MathematicalSystems: AbstractSystem, AbstractContinuousSystem, ConstrainedAffineControlContinuousSystem using EzXML: readxml, root, eachelement, nodename, nodecontent using SymEngine: Basic, subs + import Base: convert -import SymEngine: convert, free_symbols #========================= Input/Output functions @@ -33,10 +33,9 @@ Parsing SpaceEx files =====================# include("parse.jl") -#================================================ -Converting symbolic expressions and systems types -=================================================# -include("convert.jl") +#=============================================== +Converting symbolic expressions and system types +================================================# include("symbolic.jl") #========================== diff --git a/src/convert.jl b/src/convert.jl deleted file mode 100644 index c15c5b0..0000000 --- a/src/convert.jl +++ /dev/null @@ -1,358 +0,0 @@ -""" - is_linearcombination(L::Basic) - -Determine whether the expression `L` is a linear combination of its symbols. - -### Input - -- `L` -- expression - -### Output - -`true` if `L` is a linear combination or false otherwise. - -### Examples - -```jldoctest -julia> using SpaceExParser: is_linearcombination - -julia> is_linearcombination(:(2*x1 - 4)) -true - -julia> is_linearcombination(:(6.1 - 5.3*f - 0.1*g)) -true - -julia> is_linearcombination(:(2*x1^2)) -false - -julia> is_linearcombination(:(x1^2 - 4*x2 + x3 + 2)) -false -``` -""" -function is_linearcombination(L::Basic) - return all(isempty.(free_symbols.(diff.(L, free_symbols(L))))) -end - -is_linearcombination(L::Expr) = is_linearcombination(convert(Basic, L)) - -""" - 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 SpaceExParser: is_halfspace - -julia> all(is_halfspace.([:(x1 <= 0), :(x1 < 0), :(x1 > 0), :(x1 >= 0)])) -true - -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 - -""" - is_hyperplane(expr::Expr) - -Determine whether the given expression corresponds to a hyperplane. - -### Input - -- `expr` -- a symbolic expression - -### Output - -`true` if `expr` corresponds to a half-space or `false` otherwise. - -### Examples - -```jldoctest -julia> using SpaceExParser: is_hyperplane - -julia> is_hyperplane(:(x1 = 0)) -true - -julia> is_hyperplane(:(2*x1 = 4)) -true - -julia> is_hyperplane(:(6.1 = 5.3*f - 0.1*g)) -true - -julia> is_hyperplane(:(2*x1^2 = 4)) -false - -julia> is_hyperplane(:(x1^2 = 4*x2 - x3)) -false - -julia> is_hyperplane(:(x1 = 4*x2 - x3)) -true -``` -""" -function is_hyperplane(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) != 2) || !(expr.head == :(=)) - return false - end - - # convert to symengine expressions - lhs = convert(Basic, expr.args[1]) - - if :args in fieldnames(typeof(expr.args[2])) - # treats the 4 in :(2*x1 = 4) - rhs = convert(Basic, expr.args[2].args[2]) - else - rhs = convert(Basic, expr.args[2]) - end - - # check if the expression defines a hyperplane - 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> using LazySets: 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 = 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 - -""" - convert(::Type{Hyperplane{N}}, expr::Expr; vars=nothing) where {N} - -Return a `LazySet.Hyperplane` given a symbolic expression that represents a hyperplane. - -### 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 `Hyperplane`, in the form `ax = b`. - -### Examples - -```jldoctest convert_hyperplane -julia> using LazySets: Hyperplane - -julia> convert(Hyperplane, :(x1 = -0.03)) -Hyperplane{Float64, Vector{Float64}}([1.0], -0.03) - -julia> convert(Hyperplane, :(x1 + 0.03 = 0)) -Hyperplane{Float64, Vector{Float64}}([1.0], -0.03) - -julia> convert(Hyperplane, :(x1 + x2 = 2*x4 + 6)) -Hyperplane{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0) -``` - -You can also specify the set of "ambient" variables in the hyperplane, even if not -all of them appear: - -```jldoctest convert_hyperplane -julia> using SymEngine: Basic - -julia> convert(Hyperplane, :(x1 + x2 = 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4]) -Hyperplane{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0) -``` -""" -function convert(::Type{Hyperplane{N}}, expr::Expr; vars::Vector{Basic}=Basic[]) where {N} - @assert is_hyperplane(expr) "the expression :(expr) does not correspond to a Hyperplane" - - # get sides of the inequality - lhs = convert(Basic, expr.args[1]) - - # treats the 4 in :(2*x1 = 4) - rhs = :args in fieldnames(typeof(expr.args[2])) ? convert(Basic, expr.args[2].args[2]) : - convert(Basic, expr.args[2]) - - # a1 x1 + ... + an xn + K = 0 - eq = lhs - rhs - if isempty(vars) - vars = free_symbols(eq) - end - K = 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)) - - return Hyperplane(a, -K) -end - -# type-less default Hyperplane conversion -function convert(::Type{Hyperplane}, expr::Expr; vars::Vector{Basic}=Basic[]) - return convert(Hyperplane{Float64}, expr; vars=vars) -end - -""" - free_symbols(expr::Expr, set_type::Type{LazySet}) - -Return the free symbols in an expression that represents a given set type. - -### Input - -- `expr` -- symbolic expression - -### Output - -A list of symbols, in the form of SymEngine `Basic` objects. - -### Examples - -```jldoctest -julia> using SpaceExParser: free_symbols - -julia> using LazySets: HalfSpace - -julia> free_symbols(:(x1 <= -0.03), HalfSpace) -1-element Vector{SymEngine.Basic}: - x1 - -julia> free_symbols(:(x1 + x2 <= 2*x4 + 6), HalfSpace) -3-element Vector{SymEngine.Basic}: - x2 - x1 - x4 -``` -""" -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 - -function free_symbols(expr::Expr, ::Type{<:Hyperplane}) - # get sides of the equality - lhs = convert(Basic, expr.args[1]) - - # treats the 4 in :(2*x1 = 4) - rhs = :args in fieldnames(typeof(expr.args[2])) ? convert(Basic, expr.args[2].args[2]) : - convert(Basic, expr.args[2]) - return free_symbols(lhs - rhs) -end - -function free_symbols(expr::Expr) - if is_hyperplane(expr) - return free_symbols(expr, HyperPlane) - elseif is_halfspace(expr) - return free_symbols(expr, Halfspace) - else - error("the free symbols for the expression $(expr) is not implemented") - end -end diff --git a/src/symbolic.jl b/src/symbolic.jl index 5dd03a7..6445cc9 100644 --- a/src/symbolic.jl +++ b/src/symbolic.jl @@ -208,16 +208,16 @@ end # ref_tuple is used for the error message function _add_invariants!(X, U, invariants, state_variables, input_variables, ref_tuple) for invi in invariants - if is_hyperplane(invi) + if LazySets._is_hyperplane(invi) set_type = Hyperplane{NUM} - elseif is_halfspace(invi) + elseif LazySets._is_halfspace(invi) set_type = HalfSpace{NUM} else loc_or_trans, id = ref_tuple error_msg_set(loc_or_trans, invi, id) end - vars = free_symbols(invi, set_type) + vars = LazySets.free_symbols(invi, set_type) got_state_invariant = all(si in state_variables for si in vars) got_input_invariant = all(si in input_variables for si in vars) if got_state_invariant diff --git a/test/Project.toml b/test/Project.toml index 3b945c7..57da407 100644 --- a/test/Project.toml +++ b/test/Project.toml @@ -10,5 +10,5 @@ Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" Aqua = "0.8" EzXML = "1" HybridSystems = "0.4" -LazySets = "1, 2" +LazySets = "2.14" MathematicalSystems = "0.11, 0.12, 0.13" From ed1a2280afe0d4b25f8911988e08215b02f2309d Mon Sep 17 00:00:00 2001 From: schillic Date: Fri, 28 Jun 2024 07:51:27 +0200 Subject: [PATCH 2/2] require Julia v1.6 --- .github/workflows/test-pull-request.yml | 2 +- Project.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-pull-request.yml b/.github/workflows/test-pull-request.yml index 2b8f1d2..1036e83 100644 --- a/.github/workflows/test-pull-request.yml +++ b/.github/workflows/test-pull-request.yml @@ -26,7 +26,7 @@ jobs: arch: - x64 include: - - version: '1.2' # test on oldest supported version + - version: '1.6' # test on oldest supported version arch: x64 os: ubuntu-latest env: diff --git a/Project.toml b/Project.toml index a8a1ac7..e4d94a0 100644 --- a/Project.toml +++ b/Project.toml @@ -17,4 +17,4 @@ HybridSystems = "0.4" LazySets = "2.14" MathematicalSystems = "0.11, 0.12, 0.13" SymEngine = "0.7, 0.8, 0.9, 0.10, 0.11, 0.12" -julia = "1.2" +julia = "1.6"