From c184f78eff077253758ee2134779c5f5bc31521f Mon Sep 17 00:00:00 2001
From: Vincent Tjeng <vincent.tjeng@gmail.com>
Date: Sun, 19 Jul 2020 10:02:01 -0700
Subject: [PATCH] fix tight_bound and maximum_ge (#56)

**Bugfix**: In tight_bound, getobjectivebound was empirically observed not to return the correct objective bound when the objective is an affine expression with a constant term (the constant term was ignored). This could lead to correctness issues with the solver where problems that are SAT are incorrectly determined to be UNSAT because (for example) the lower or upper bounds to some ReLU input are too tight.

We believe that this is what is causing the following error message, since expect even LP solves to provide a better answer than interval arithmetic. We will increase the warning message to an error that stops optimization in the future.

```
Tightening via interval_arithmetic gives a better result than lp; using best bound found.
```

As a short-term fix, we fall back to bounds determined by interval arithmetic if this is the case.

**Perf**: In maximum_ge, we created additional continuous and binary variables even when the array we were maximizing over consisted of only a single entry. We fix this, allowing us to save on extraneous variables.
---
 src/net_components/core_ops.jl | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/net_components/core_ops.jl b/src/net_components/core_ops.jl
index 42aff450..0ad7feb2 100644
--- a/src/net_components/core_ops.jl
+++ b/src/net_components/core_ops.jl
@@ -89,9 +89,17 @@ function tight_bound(
     status = solve(model, suppress_warnings = true, relaxation = relaxation)
     if status == :Optimal
         b = getobjectivevalue(model)
+        db = bound_delta_f[bound_type](b, b_0)
+        Memento.debug(MIPVerify.LOGGER, "  Δu = $(db)")
+        if db < 0
+            b = b_0
+            Memento.info(
+                MIPVerify.LOGGER,
+                "Tightening via interval_arithmetic gives a better result than $(tightening_algorithm); using best bound found.",
+            )
+        end
     elseif status == :UserLimit
-        b = getobjectivebound(model)
-        log_gap(model)
+        b = b_0
     else
         Memento.warn(
             MIPVerify.LOGGER,
@@ -99,15 +107,6 @@ function tight_bound(
         )
         b = b_0
     end
-    db = bound_delta_f[bound_type](b, b_0)
-    Memento.debug(MIPVerify.LOGGER, "  Δu = $(db)")
-    if db < 0
-        b = b_0
-        Memento.info(
-            MIPVerify.LOGGER,
-            "Tightening via interval_arithmetic gives a better result than $(tightening_algorithm); using best bound found.",
-        )
-    end
     return b
 end
 
@@ -416,6 +415,9 @@ function maximum_ge(xs::AbstractArray{T})::JuMPLinearType where {T<:JuMPLinearTy
     if all(is_constant.(xs))
         return maximum_of_constants(xs)
     end
+    if length(xs) == 1
+        return first(xs)
+    end
     # at least one of xs is not constant.
     model = MIPVerify.getmodel(xs)
     x_max = @variable(model)