Merge pull request #166 from sisl/redo_constraints

Redo constraints

src/adversarial/dlv.jl

@@ -82,15 +82,16 @@ function backward_map(solver::DLV, y::Vector{Float64}, nnet::Network, bounds::Ve
     output = Hyperrectangle(y, zeros(size(y)))
     input = first(bounds)
     model = Model(solver)
-    neurons = init_neurons(model, nnet)
-    deltas  = init_deltas(model, nnet)
-    add_set_constraint!(model, input, first(neurons))
-    add_set_constraint!(model, output, last(neurons))
-    encode_network!(model, nnet, neurons, deltas, bounds, BoundedMixedIntegerLP())
-    o = max_disturbance!(model, first(neurons) - input.center)
+    model[:bounds] = bounds
+    z = init_vars(model, nnet, :z, with_input=true)
+    δ = init_vars(model, nnet, :δ, binary=true)
+    add_set_constraint!(model, input, first(z))
+    add_set_constraint!(model, output, last(z))
+    encode_network!(model, nnet, BoundedMixedIntegerLP())
+    o = max_disturbance!(model, first(z) - input.center)
     optimize!(model)
     if termination_status(model) == OPTIMAL
-        return (true, value(first(neurons)))
+        return (true, value(first(z)))
     else
         return (false, [])
     end

src/optimization/duality.jl

@@ -34,8 +34,8 @@ function solve(solver::Duality, problem::Problem)
     @assert length(d) == 1 "Duality only accepts HalfSpace output sets. Got a $(length(d))-d polytope."
     d = d[1]
 
-    λ = init_multipliers(model, problem.network, "λ")
-    μ = init_multipliers(model, problem.network, "μ")
+    λ = init_vars(model, problem.network, :λ)
+    μ = init_vars(model, problem.network, :μ)
     o = dual_value(solver, problem, model, λ, μ)
     @constraint(model, last(λ) .== -c)
     optimize!(model)

src/optimization/iLP.jl

@@ -36,29 +36,29 @@ function solve(solver::ILP, problem::Problem)
     nnet = problem.network
     x = problem.input.center
     model = Model(solver)
-    δ = get_activation(nnet, x)
-    neurons = init_neurons(model, nnet)
-    add_complementary_set_constraint!(model, problem.output, last(neurons))
-    o = max_disturbance!(model, first(neurons) - problem.input.center)
+    model[:δ] = δ = get_activation(nnet, x)
+    z = init_vars(model, nnet, :z, with_input=true)
+    add_complementary_set_constraint!(model, problem.output, last(z))
+    o = max_disturbance!(model, first(z) - problem.input.center)
 
     if !solver.iterative
-        encode_network!(model, nnet, neurons, δ, StandardLP())
+        encode_network!(model, nnet, StandardLP())
         optimize!(model)
         termination_status(model) != OPTIMAL && return AdversarialResult(:unknown)
-        x = value.(first(neurons))
+        x = value.(first(z))
         return interpret_result(solver, x, problem.input)
     end
 
-    encode_network!(model, nnet, neurons, δ, LinearRelaxedLP())
+    encode_network!(model, nnet, LinearRelaxedLP())
     while true
         optimize!(model)
         termination_status(model) != OPTIMAL && return AdversarialResult(:unknown)
-        x = value.(first(neurons))
+        x = value.(first(z))
         matched, index = match_activation(nnet, x, δ)
         if matched
             return interpret_result(solver, x, problem.input)
         end
-        add_constraint!(model, nnet, neurons, δ, index)
+        add_constraint!(model, nnet, z, δ, index)
     end
 end
 

src/optimization/mipVerify.jl

@@ -32,13 +32,16 @@ end
 
 function solve(solver::MIPVerify, problem::Problem)
     model = Model(solver)
-    neurons = init_neurons(model, problem.network)
-    deltas = init_deltas(model, problem.network)
-    add_set_constraint!(model, problem.input, first(neurons))
-    add_complementary_set_constraint!(model, problem.output, last(neurons))
-    bounds = get_bounds(problem)
-    encode_network!(model, problem.network, neurons, deltas, bounds, BoundedMixedIntegerLP())
-    o = max_disturbance!(model, first(neurons) - problem.input.center)
+    z = init_vars(model, problem.network, :z, with_input=true)
+    δ = init_vars(model, problem.network, :δ, binary=true)
+    # get the pre-activation bounds:
+    model[:bounds] = get_bounds(problem, false)
+    model[:before_act] = true
+
+    add_set_constraint!(model, problem.input, first(z))
+    add_complementary_set_constraint!(model, problem.output, last(z))
+    encode_network!(model, problem.network, BoundedMixedIntegerLP())
+    o = max_disturbance!(model, first(z) - problem.input.center)
     optimize!(model)
     if termination_status(model) == INFEASIBLE
         return AdversarialResult(:holds)

src/optimization/nsVerify.jl

@@ -29,30 +29,29 @@ Sound and complete.
 end
 
 function solve(solver::NSVerify, problem::Problem)
+    # Set up and solve the problem
+    model = Model(solver)
+    z = init_vars(model, problem.network, :z, with_input=true)
+    δ = init_vars(model, problem.network, :δ, binary=true)
     # Set M automatically if not already set.
     if isnothing(solver.m)
-        M = set_automatic_M(problem)
+        model[:M] = set_automatic_M(problem)
     else
         @warn "M should be chosen carefully. An M which is too small will cause
         the problem to be solved incorrectly. Not setting the `m` keyword, or setting
         it equal to `nothing` will cause a safe value to be calculated automatically.
         E.g. NSVerify()." maxlog = 1
-        M = solver.m
+        model[:M] = solver.m
     end
 
-    # Set up and solve the problem
-    model = Model(solver)
-    neurons = init_neurons(model, problem.network)
-    deltas = init_deltas(model, problem.network)
-    add_set_constraint!(model, problem.input, first(neurons))
-    add_complementary_set_constraint!(model, problem.output, last(neurons))
-    encode_network!(model, problem.network, neurons, deltas, MixedIntegerLP(M))
+    add_set_constraint!(model, problem.input, first(z))
+    add_complementary_set_constraint!(model, problem.output, last(z))
+    encode_network!(model, problem.network, MixedIntegerLP())
     feasibility_problem!(model)
     optimize!(model)
 
-
     if termination_status(model) == OPTIMAL
-        return CounterExampleResult(:violated, value.(first(neurons)))
+        return CounterExampleResult(:violated, value.(first(z)))
 
     elseif termination_status(model) == INFEASIBLE
         return CounterExampleResult(:holds)