Merge b7734bd into 2949ebe

src/NeuralVerification.jl

@@ -40,8 +40,6 @@ export
     Solver,
     Network,
     AbstractActivation,
-    PolytopeComplement,
-    complement,
     # NOTE: not sure if exporting these is a good idea as far as namespace conflicts go:
     # ReLU,
     # Max,

src/optimization/utils/constraints.jl

@@ -208,8 +208,8 @@ function add_complementary_set_constraint!(m::Model, H::HalfSpace, z::Vector{Var
     @constraint(m, a * z .>= b)
     return nothing
 end
-function add_complementary_set_constraint!(m::Model, PC::PolytopeComplement, z::Vector{VariableRef})
-    add_set_constraint!(m, PC.P, z)
+function add_complementary_set_constraint!(m::Model, PC::Complement, z::Vector{VariableRef})
+    add_set_constraint!(m, PC.X, z)
     return nothing
 end
 
@@ -225,7 +225,7 @@ function add_set_constraint!(m::Model, set::Hyperrectangle, z::Vector{VariableRe
     return nothing
 end
 
-function add_set_constraint!(m::Model, PC::PolytopeComplement, z::Vector{VariableRef})
-    add_complementary_set_constraint!(m, PC.P, z)
+function add_set_constraint!(m::Model, PC::Complement, z::Vector{VariableRef})
+    add_complementary_set_constraint!(m, PC.X, z)
     return nothing
 end

src/utils/problem.jl

@@ -1,41 +1,3 @@
-
-"""
-    PolytopeComplement
-
-The complement to a given set. Note that in general, a `PolytopeComplement` is not necessarily a convex set.
-Also note that `PolytopeComplement`s are open by definition.
-
-### Examples
-```julia
-julia> H = Hyperrectangle([0,0], [1,1])
-Hyperrectangle{Int64}([0, 0], [1, 1])
-
-julia> PC = complement(H)
-PolytopeComplement of:
-  Hyperrectangle{Int64}([0, 0], [1, 1])
-
-julia> center(H) ∈ PC
-false
-
-julia> high(H).+[1,1] ∈ PC
-true
-```
-"""
-struct PolytopeComplement{S<:LazySet}
-    P::S
-end
-
-Base.show(io::IO, PC::PolytopeComplement) = (println(io, "PolytopeComplement of:"), println(io, "  ", PC.P))
-LazySets.issubset(s, PC::PolytopeComplement) = LazySets.is_intersection_empty(s, PC.P)
-LazySets.is_intersection_empty(s, PC::PolytopeComplement) = LazySets.issubset(s, PC.P)
-LazySets.tohrep(PC::PolytopeComplement) = PolytopeComplement(convert(HPolytope, PC.P))
-Base.in(pt, PC::PolytopeComplement) = pt ∉ PC.P
-complement(PC::PolytopeComplement)  = PC.P
-complement(P::LazySet) = PolytopeComplement(P)
-Base.:(==)(pc1::PolytopeComplement, pc2::PolytopeComplement) = pc1.P == pc2.P
-# etc.
-
-
 """
     Problem{P, Q}(network::Network, input::P, output::Q)
 

test/complements.jl

@@ -4,13 +4,13 @@
     @testset "Basic" begin
 
         HS = HalfSpace([-1.0, -1.0], 0.0)
-        PC = PolytopeComplement(HS)
+        PC = Complement(HS)
 
         @test [5.0, 5.0]   ∈ HS && [5.0, 5.0]   ∉ PC
         @test [-1.0, -1.0] ∉ HS && [-1.0, -1.0] ∈ PC
 
-        @test complement(PC) == HS
-        @test complement(HS) == PC
+        @test Complement(PC) == HS
+        # @test Complement(HS) == PC
 
         # Hyperrectangle contained in HS
         hr = Hyperrectangle(low = [1.0, 1.0], high = [2.0, 2.0])
@@ -28,11 +28,11 @@
         @test !(hr ⊆ HS)
 
         # Test some other sets
-        @test @no_error complement(Hyperrectangle(ones(2), ones(2)))
-        @test @no_error complement(Ball2(ones(2), 1.0))
-        @test @no_error complement(Ball1(ones(3), 1.0))
-        @test @no_error complement(Zonotope(ones(4), ones(4, 2)))
-        @test @no_error complement(convert(HPolytope, hr))
+        @test @no_error Complement(Hyperrectangle(ones(2), ones(2)))
+        @test @no_error Complement(Ball2(ones(2), 1.0))
+        @test @no_error Complement(Ball1(ones(3), 1.0))
+        @test @no_error Complement(Zonotope(ones(4), ones(4, 2)))
+        @test @no_error Complement(convert(HPolytope, hr))
     end
 
     @testset "Solvers with PCs" begin
@@ -41,8 +41,8 @@
         in_hyper  = Hyperrectangle(low = [-0.9], high = [0.9])
 
         # Output sets that are the PolytopeComplements of the complements of the output sets used in the regular tests.
-        problem_holds    = Problem(small_nnet, in_hyper, PolytopeComplement(HPolytope([HalfSpace([-1.0], 10.0)])))
-        problem_violated = Problem(small_nnet, in_hyper, PolytopeComplement(HPolytope([HalfSpace([1.0], -20.0)])))
+        problem_holds    = Problem(small_nnet, in_hyper, Complement(HPolytope([HalfSpace([-1.0], 10.0)])))
+        problem_violated = Problem(small_nnet, in_hyper, Complement(HPolytope([HalfSpace([1.0], -20.0)])))
 
         for solver in [NSVerify(), MIPVerify(), ILP(), Reluplex(), Planet()]
             holds    = solve(solver, problem_holds)