Skip to content

Commit

Permalink
Switch testing to use HiGHS.jl
Browse files Browse the repository at this point in the history
Cbc cannot be properly silenced (jump-dev/Cbc.jl#168); using HiGHS avoids the need for the workaround in #131 of using `optimize_silent!`.
  • Loading branch information
vtjeng committed Feb 17, 2023
1 parent 41b3805 commit 90245b0
Show file tree
Hide file tree
Showing 9 changed files with 58 additions and 74 deletions.
6 changes: 3 additions & 3 deletions Project.toml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Serialization = "9e88b42a-f829-5b0c-bbe9-9e923198166b"

[compat]
CSV = "0.7, 0.8, 0.9, 0.10"
Cbc = "0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 1.0"
HiGHS = "1.4"
DataFrames = "0.21, 0.22, 1"
DocStringExtensions = "0.8, 0.9"
IntervalArithmetic = "0.14, 0.15, 0.16, 0.17, 0.18, 0.19, 0.20"
Expand All @@ -32,10 +32,10 @@ TimerOutputs = "0.5"
julia = "1"

[extras]
Cbc = "9961bab8-2fa3-5c5a-9d89-47fab24efd76"
HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
TimerOutputs = "a759f4b9-e2f1-59dc-863e-4aeb61b1ea8f"

[targets]
test = ["Statistics", "Test", "Cbc", "TimerOutputs"]
test = ["Statistics", "Test", "HiGHS", "TimerOutputs"]
13 changes: 4 additions & 9 deletions src/MIPVerify.jl
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ function get_default_tightening_options(optimizer)::Dict
optimizer_type_name = string(typeof(optimizer()))
if optimizer_type_name == "Gurobi.Optimizer"
return Dict("OutputFlag" => 0, "TimeLimit" => 20)
elseif optimizer_type_name == "Cbc.Optimizer"
return Dict("logLevel" => 0, "seconds" => 20)
elseif optimizer_type_name == "HiGHS.Optimizer"
return Dict("output_flag" => false, "time_limit" => 20.0)
else
return Dict()
end
Expand Down Expand Up @@ -76,7 +76,7 @@ We guarantee that `y[j] - y[i] ≥ 0` for some `j ∈ target_selection` and for
+ `tightening_options`: Solver-specific options passed to optimizer when used to determine upper and
lower bounds for input to nonlinear units. Note that these are only used if the
`tightening_algorithm` is `lp` or `mip` (no solver is used when `interval_arithmetic` is used
to compute the bounds). Defaults for Gurobi and Cbc to a time limit of 20s per solve,
to compute the bounds). Defaults for Gurobi and HiGHS to a time limit of 20s per solve,
with output suppressed.
+ `solve_if_predicted_in_targeted`: Defaults to `true`. The prediction that `nn` makes for the
unperturbed `input` can be determined efficiently. If the predicted index is one of the indexes
Expand All @@ -98,7 +98,6 @@ function find_adversarial_example(
tightening_algorithm::TighteningAlgorithm = DEFAULT_TIGHTENING_ALGORITHM,
tightening_options::Dict = get_default_tightening_options(optimizer),
solve_if_predicted_in_targeted = true,
silence_solve_output::Bool = false,
)::Dict

total_time = @elapsed begin
Expand Down Expand Up @@ -151,11 +150,7 @@ function find_adversarial_example(
end
set_optimizer(m, optimizer)
set_optimizer_attributes(m, main_solve_options...)
if silence_solve_output
optimize_silent!(m)
else
optimize!(m)
end
optimize!(m)
d[:SolveStatus] = JuMP.termination_status(m)
d[:SolveTime] = JuMP.solve_time(m)
end
Expand Down
10 changes: 1 addition & 9 deletions src/net_components/core_ops.jl
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,6 @@ function is_constant(x::JuMP.VariableRef)
false
end

function optimize_silent!(m)
redirect_stdout(devnull) do
optimize!(m)
# Required, per https://discourse.julialang.org/t/consistent-way-to-suppress-solver-output/20437/9
Base.Libc.flush_cstdio()
end
end

function get_tightening_algorithm(
x::JuMPLinearType,
nta::Union{TighteningAlgorithm,Nothing},
Expand Down Expand Up @@ -94,7 +86,7 @@ arithmetic, as a backup.
"""
function tight_bound_helper(m::Model, bound_type::BoundType, objective::JuMPLinearType, b_0::Number)
@objective(m, bound_obj[bound_type], objective)
optimize_silent!(m)
optimize!(m)
status = JuMP.termination_status(m)
if status == MathOptInterface.OPTIMAL
b = JuMP.objective_value(m)
Expand Down
9 changes: 4 additions & 5 deletions test/TestHelpers.jl
Original file line number Diff line number Diff line change
Expand Up @@ -25,10 +25,10 @@ end
const TEST_DEFAULT_TIGHTENING_ALGORITHM = lp

if Base.find_package("Gurobi") === nothing
using Cbc
optimizer = Cbc.Optimizer
main_solve_options = Dict("logLevel" => 0)
tightening_options = Dict("logLevel" => 0, "seconds" => 20)
using HiGHS
optimizer = HiGHS.Optimizer
main_solve_options = Dict("output_flag" => false)
tightening_options = Dict("output_flag" => false, "time_limit" => 20.0)
else
using Gurobi
env = Gurobi.Env()
Expand Down Expand Up @@ -75,7 +75,6 @@ function test_find_adversarial_example(
tightening_options = get_tightening_options(),
tightening_algorithm = TEST_DEFAULT_TIGHTENING_ALGORITHM,
invert_target_selection = invert_target_selection,
silence_solve_output = true,
)
if isnan(expected_objective_value)
@test d[:SolveStatus] == MathOptInterface.INFEASIBLE ||
Expand Down
61 changes: 30 additions & 31 deletions test/net_components/core_ops.jl
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@ using MIPVerify:
TighteningAlgorithm,
MIPVerifyExt,
upper_bound,
lower_bound,
optimize_silent!
lower_bound
@isdefined(TestHelpers) || include("../TestHelpers.jl")

function count_binary_variables(m::Model)
Expand Down Expand Up @@ -103,7 +102,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, x1)
optimize_silent!(m)
optimize!(m)
solve_output = JuMP.value(xmax)
@test solve_output 3
end
Expand All @@ -122,7 +121,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin

# elements of the input array are made to take their maximum value
@objective(m, Max, x1 + x2 + x3 + x4 + x5)
optimize_silent!(m)
optimize!(m)

solve_output = JuMP.value(xmax)
@test solve_output 7
Expand Down Expand Up @@ -162,7 +161,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin

# elements of the input array are made to take their maximum value
@objective(m, Max, xmax)
optimize_silent!(m)
optimize!(m)

solve_output = JuMP.value(xmax)
@test solve_output 100
Expand All @@ -177,7 +176,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
# no binary variables need to be introduced
@test count_binary_variables(m) == 0

optimize_silent!(m)
optimize!(m)

solve_output = JuMP.value(xmax)
@test solve_output 2
Expand All @@ -194,7 +193,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, x1)
optimize_silent!(m)
optimize!(m)
solve_output = JuMP.value(xmax)
@test solve_output 3
end
Expand Down Expand Up @@ -267,7 +266,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 1
end
@testset "strictly non-positive" begin
Expand All @@ -279,7 +278,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 1
end
@testset "regular" begin
Expand All @@ -291,7 +290,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) <= 1

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 2
end
end
Expand All @@ -306,7 +305,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 0
end
@testset "strictly non-positive" begin
Expand Down Expand Up @@ -349,13 +348,13 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 1
@test JuMP.value(x) -1
@test JuMP.value(x_r) 0

@objective(m, Min, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) -2
@test JuMP.value(x) 2
@test JuMP.value(x_r) 0
Expand All @@ -369,13 +368,13 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) <= 1

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 2
@test JuMP.value(x) 2
@test JuMP.value(x_r) 2

@objective(m, Min, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 0
@test JuMP.value(x) 0
@test JuMP.value(x_r) 0
Expand All @@ -389,13 +388,13 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 2
@test JuMP.value(x) 2
@test JuMP.value(x_r) 2

@objective(m, Min, 2 * x_r - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) -1
@test JuMP.value(x) -1
@test JuMP.value(x_r) -1
Expand All @@ -416,13 +415,13 @@ TestHelpers.@timed_testset "core_ops.jl" begin
x_r = masked_relu(x, [-1, 0, 1])

@objective(m, Max, sum(2 * x_r - x))
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 5
@test JuMP.value.(x) [-1, 2, 2]
@test JuMP.value.(x_r) [0, 2, 2]

@objective(m, Min, sum(2 * x_r - x))
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) -3
@test JuMP.value.(x) [2, 0, -1]
@test JuMP.value.(x_r) [0, 0, -1]
Expand All @@ -440,7 +439,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_a - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 1
end
@testset "strictly non-positive" begin
Expand All @@ -452,7 +451,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_a - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 3
end
@testset "regular" begin
Expand All @@ -464,7 +463,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Max, 2 * x_a - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 6
end
@testset "abs_ge is not strict" begin
Expand All @@ -477,7 +476,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@test count_binary_variables(m) == 0

@objective(m, Min, x_a - x)
optimize_silent!(m)
optimize!(m)
@test JuMP.objective_value(m) 0
end
end
Expand All @@ -500,7 +499,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@constraint(m, x[3] == 1)
set_max_indexes(m, x, [1])
@objective(m, Min, x[1])
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x[1]) 5
end
@testset "with margin" begin
Expand All @@ -511,7 +510,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
@constraint(m, x[3] == 1)
set_max_indexes(m, x, [1], margin = margin)
@objective(m, Min, x[1])
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x[1]) 5 + margin
end
end
Expand All @@ -526,7 +525,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
set_upper_bound(x[3], 10)
set_max_indexes(m, x, [2, 3])
@objective(m, Min, x[2] + x[3])
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x[2]) 5
@test JuMP.value(x[3]) -1
end
Expand All @@ -541,7 +540,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
set_upper_bound(x[3], 10)
set_max_indexes(m, x, [2, 3], margin = margin)
@objective(m, Min, x[2] + x[3])
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x[2]) 5 + margin
@test JuMP.value(x[3]) -1
end
Expand All @@ -552,7 +551,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
x2 = @variable(m, lower_bound = 4, upper_bound = 5)
set_max_indexes(m, [x1, x2], [2])
@objective(m, Min, x2)
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x2) 4
end
@testset "selected variable has non-constant value, and cannot take the maximum value" begin
Expand All @@ -561,7 +560,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
x2 = @variable(m, lower_bound = -5, upper_bound = -4)
set_max_indexes(m, [x1, x2], [2])
@objective(m, Min, x2)
optimize_silent!(m)
optimize!(m)
solve_status = JuMP.termination_status(m)
@test (
solve_status in
Expand All @@ -574,7 +573,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
x2 = @variable(m, lower_bound = -5, upper_bound = -4)
set_max_indexes(m, [x1, x2], [1])
@objective(m, Min, x2)
optimize_silent!(m)
optimize!(m)
@test JuMP.value(x2) -5
end
@testset "selected variable has constant value, and cannot take the maximum value" begin
Expand All @@ -583,7 +582,7 @@ TestHelpers.@timed_testset "core_ops.jl" begin
x2 = @variable(m, lower_bound = 4, upper_bound = 5)
set_max_indexes(m, [x1, x2], [1])
@objective(m, Min, x2)
optimize_silent!(m)
optimize!(m)
solve_status = JuMP.termination_status(m)
@test (
solve_status in
Expand Down
6 changes: 3 additions & 3 deletions test/net_components/layers/conv2d.jl
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
using Test
using JuMP
using MIPVerify
using MIPVerify: check_size, optimize_silent!
using MIPVerify: check_size
@isdefined(TestHelpers) || include("../../TestHelpers.jl")

function test_convolution_layer(
Expand Down Expand Up @@ -53,7 +53,7 @@ function test_convolution_layer(
p_v = MIPVerify.Conv2d(filter_v, bias_v, p.stride, p.padding)
output_v = MIPVerify.conv2d(input, p_v)
@constraint(m, output_v .== expected_output)
optimize_silent!(m)
optimize!(m)

p_solve = MIPVerify.Conv2d(JuMP.value.(filter_v), JuMP.value.(bias_v), p.stride, p.padding)
solve_output = MIPVerify.conv2d(input, p_solve)
Expand All @@ -64,7 +64,7 @@ function test_convolution_layer(
input_v = map(_ -> @variable(m), CartesianIndices(input_size))
output_v = MIPVerify.conv2d(input_v, p)
@constraint(m, output_v .== expected_output)
optimize_silent!(m)
optimize!(m)

solve_output = MIPVerify.conv2d(JuMP.value.(input_v), p)
@test solve_output expected_output
Expand Down
Loading

0 comments on commit 90245b0

Please sign in to comment.