Switch testing to use HiGHS.jl (#133)

Cbc cannot be properly silenced (jump-dev/Cbc.jl#168); using HiGHS avoids the need for the workaround in #131 of using `optimize_silent!`. This increases test times slightly, but is worth it to avoid the log spam without additional complexity.
vtjeng · Feb 17, 2023 · 9383d59 · 9383d59
1 parent 29c9f16
commit 9383d59
Show file tree

Hide file tree

Showing 9 changed files with 58 additions and 74 deletions.
diff --git a/Project.toml b/Project.toml
@@ -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"
@@ -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"]
diff --git a/src/MIPVerify.jl b/src/MIPVerify.jl
@@ -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
@@ -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 
@@ -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
@@ -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

diff --git a/src/net_components/core_ops.jl b/src/net_components/core_ops.jl
@@ -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},
@@ -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)

diff --git a/test/TestHelpers.jl b/test/TestHelpers.jl
@@ -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()
@@ -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 ||

diff --git a/test/net_components/core_ops.jl b/test/net_components/core_ops.jl
@@ -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)
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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]
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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

diff --git a/test/net_components/layers/conv2d.jl b/test/net_components/layers/conv2d.jl
@@ -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(
@@ -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)
@@ -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