chooseEnteringVar — Mathlib

Lean4
/-- Chooses an entering variable: among the variables with a positive coefficient in the objective
function, the one with the smallest index (in the initial indexing).
-/
def chooseEnteringVar : SimplexAlgorithmM matType Nat := do
  let mut enterIdxOpt : Option Nat := none
  let mut minIdx := 0
  for i in [:(← get).free.size - 1]do
    if (← get).mat[(0, i)]! > 0 && (enterIdxOpt.isNone || (← get).free[i]! < minIdx) then
      enterIdxOpt := i
      minIdx :=
        (← get).free[i]!
          /- If there is no such variable the solution does not exist for sure. -/

  match enterIdxOpt with
  | none =>
    throwThe SimplexAlgorithmException SimplexAlgorithmException.infeasible
  | some enterIdx =>
    return enterIdx
Похожие утверждения