Merge pull request #117 from castrong/issue_107_debug

Redo Change for Bounds
sisl · Jul 17, 2020 · b8b7095 · b8b7095
2 parents a8acbf2 + fb3a97c
commit b8b7095
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/src/NeuralVerification.jl b/src/NeuralVerification.jl
@@ -90,4 +90,8 @@ include("adversarial/fastLip.jl")
 include("adversarial/dlv.jl")
 export ReluVal, FastLin, FastLip, DLV
 
+const TOL = Ref(sqrt(eps()))
+set_tolerance(x::Real) = (TOL[] = x)
+export set_tolerance
+
 end
diff --git a/src/satisfiability/reluplex.jl b/src/satisfiability/reluplex.jl
@@ -49,8 +49,9 @@ function find_relu_to_fix(ẑ, z)
     return (0, 0)
 end
 
-type_one_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ > 0.0)  && (zᵢⱼ != ẑᵢⱼ)  # TODO consider renaming to `inactive_broken` and `active_broken`
-type_two_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ == 0.0) && (ẑᵢⱼ > 0.0)
+ # TODO consider renaming to `inactive_broken` and `active_broken`
+type_one_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ > 0.0 + TOL[])  && (!(-TOL[] < ẑᵢⱼ - zᵢⱼ < TOL[])) # (zᵢⱼ > 0) && (ẑᵢⱼ != zᵢⱼ)
+type_two_broken(ẑᵢⱼ, zᵢⱼ) = (-TOL[] < zᵢⱼ < TOL[]) && (ẑᵢⱼ > 0.0 + TOL[]) # (zᵢⱼ == 0) && (ẑᵢⱼ > 0)
 
 # Corresponds to a ReLU that shouldn't be active but is
 function type_one_repair!(model, ẑᵢⱼ, zᵢⱼ)
@@ -91,9 +92,12 @@ function encode(solver::Reluplex, model::Model,  problem::Problem)
     bounds = get_bounds(problem)
     for (i, L) in enumerate(layers)
         @constraint(model, affine_map(L, z[i]) .== ẑ[i+1])
-        add_set_constraint!(model, bounds[i], ẑ[i])
+        add_set_constraint!(model, bounds[i], z[i])
         activation_constraint!(model, ẑ[i+1], z[i+1], L.activation)
     end
+    # Add the bounds on your output layer
+    add_set_constraint!(model, last(bounds), last(z))
+    # Add the complementary set defind as part of the problem
     add_complementary_set_constraint!(model, problem.output, last(z))
     feasibility_problem!(model)
     return ẑ, z