Core Operations

abs_ge(x)

Expresses a one-sided absolute-value constraint: output is constrained to be at least as large as |x|.

Only use when you are minimizing over the output in the objective.

consistent_relu_bounds(x, l, u) -> (lower, upper)

Choose the bounds on the ReLU input x to use when formulating relu(x).

If u < l, the candidate bounds contradict each other. Log a warning and replace both with the interval-arithmetic bounds computed from x; otherwise, return (l, u) unchanged. This fallback handles numerical errors in solver-derived bounds.

Only u < l is considered inconsistent. Ordered candidates are not checked against x, and the interval-arithmetic fallback is returned without another ordering check.

is_constant(x)

Checks whether a JuMPLinearType is constant (and thus has no model associated) with it. This can only be true if it is an affine expression with no stored variables.

masked_relu(x, m; nta)

Expresses a masked rectified-linearity constraint, with three possibilities depending on the value of the mask. Output is constrained to be:

1) max(x, 0) if m=0,
2) 0 if m<0
3) x if m>0

maximum(xs)

Expresses a maximization constraint: output is constrained to be equal to max(xs).

maximum_ge(xs)

Expresses a one-sided maximization constraint: output is constrained to be at least max(xs).

Only use when you are minimizing over the output in the objective.

NB: If all of xs are constant, we simply return the largest of them.

relax_integrality_context(
    f,
    model,
    should_relax_integrality
)

Context manager for running f on model. If should_relax_integrality is true, the integrality constraints are relaxed before f is run and re-imposed after.

relu(x)
relu(x; nta, stats)

Expresses a rectified-linearity constraint: output is constrained to be equal to max(x, 0).

set_max_indexes(model, xs, target_indexes; margin)

Imposes constraints ensuring that one of the elements at the targetindexes is (tied for) the largest element of the array x. More specifically, we require x[j] - x[i] ≥ margin for some `j ∈ targetindexesand for alli ∉ target_indexes`.

Calculates a tight bound of type bound_type on the variable x using the specified tightening algorithm nta.

If an upper bound is proven to be below cutoff, or a lower bound is proven to above cutoff, the algorithm returns early with whatever value was found. MIP tightening first tries the LP relaxation and passes its certified result to the MIP solve.

tight_bound_helper(
    m,
    bound_type,
    objective,
    b_0,
    tightening_algorithm,
    stats
)

Optimizes the value of objective based on bound_type, with b_0, computed via interval arithmetic, as a backup.

• If an optimal LP solution is reached and row duals are available, validate them and return the resulting certified Lagrangian bound. The certificate is re-verified here with outward rounding, so its validity does not depend on the solver's duals being exactly feasible. Otherwise, return b_0.
• If an optimal MIP solution is reached, return the solver's objective bound (its dual bound). In exact arithmetic, weak duality places the objective bound on the valid side of the true optimum, overshooting it by at most the achieved gap (objective bound minus incumbent objective value), and OPTIMAL termination keeps that gap within the solver's gap tolerance. The incumbent objective value can sit on the invalid side by up to the same gap, which is why it is not used here. Two claims are trusted rather than verified: (1) the reported bound is assembled from floating-point node relaxation bounds without directed rounding, so its validity is subject to the solver's numerics; (2) the incumbent is feasible only up to the solver's feasibility and integrality tolerances, so the true conservatism can exceed the reported gap by a tolerance-scale amount (this weakens the tightness claim, but a super-optimal incumbent cannot invalidate the bound). Solvers expose no independently checkable MIP certificate through JuMP, so neither claim can be re-verified the way the LP certificate is.
• If we reach the user-defined time limit, return b_0.
• For all other solve statuses, we warn the user and report b_0.

Whenever an optimal solution is reported, its objective value is cross-checked against b_0. The solution is a feasible point of the model, so its value can never lie outside a bound that interval arithmetic computed for the same model; if it does (beyond solver feasibility tolerances), the solver and our view of the model disagree — solver numerics have failed or the model plumbing is desynced — and no bound computed by this run can be trusted, so we raise an error rather than continue.