Namespace conflict error when using alongside Flux

[rlipkis]

Hi,

I've run into a bit of an issue when using your package. The @requires statement causes Flux to be loaded in full inside NeuralVerification if it's used in Main at any point. This causes a conflict with the symbol σ, which is exported by both LazySets and Flux.

A MWE is Flux + the script given in the README, used with a reachability-based solver,

using NeuralVerification
using NeuralVerification: Hyperrectangle
using Flux

solver = ReluVal()
nnet = read_nnet("test/networks/small_nnet.nnet")
input_set  = Hyperrectangle(low = [-1.0], high = [1.0])
output_set = Hyperrectangle(low = [-1.0], high = [70.0])
problem = Problem(nnet, input_set, output_set)

solve(solver, problem)

which errors with the message

WARNING: both Flux and LazySets export "σ"; uses of it in module NeuralVerification must be qualified
ERROR: UndefVarError: σ not defined
Stacktrace:
 [1] upper_bound(a::LazySets.Arrays.SingleEntryVector{Float64}, set::LazySets.AffineMap{Float64, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Float64, SubArray{Float64, 2, Matrix{Float64}, Tuple{Base.Slice{Base.OneTo{Int64}}, UnitRange{Int64}}, true}, SubArray{Float64, 1, Matrix{Float64}, Tuple{Base.Slice{Base.OneTo{Int64}}, Int64}, true}})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:141
 [2] upper_bound
   @ ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:145 [inlined]
 [3] forward_act(#unused#::ReluVal, L::NeuralVerification.Layer{NeuralVerification.ReLU, Float64}, input::NeuralVerification.SymbolicIntervalGradient{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Bool})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\reluVal.jl:107
 [4] forward_layer(solver::ReluVal, layer::NeuralVerification.Layer{NeuralVerification.ReLU, Float64}, reach::NeuralVerification.SymbolicIntervalGradient{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Bool})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:59
 [5] _forward_network(solver::ReluVal, nnet::Network, input::NeuralVerification.SymbolicIntervalGradient{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Bool})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:26
 [6] #forward_network#78
   @ ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:18 [inlined]
 [7] forward_network(solver::ReluVal, nnet::Network, input::NeuralVerification.SymbolicIntervalGradient{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Bool})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\utils\reachability.jl:13
 [8] solve(solver::ReluVal, problem::Problem{Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}, Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}}})
   @ NeuralVerification ~\.julia\packages\NeuralVerification\zWjPO\src\reachability\reluVal.jl:44
 [9] top-level scope
   @ REPL[9]:1

I think if the using statement in utils/flux.jl were qualified with only the required names, it would avert the conflict.