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.

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.

Calculates the lower_bound only if u is positive; otherwise, returns u (since we expect) the ReLU to be fixed to zero anyway.

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)

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.

tight_bound_helper(m, bound_type, objective, b_0)

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

• If an optimal solution is reached, we return the objective value. We also verify that the objective found is better than the bound b_0 provided; if this is not the case, we throw an error.
• If we reach the user-defined time limit, we compute the best objective bound found. We compare this to b_0 and return the better result.
• For all other solve statuses, we warn the user and report b_0.