extractSolution

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.SimplexAlgorithm.extractSolution

Lean4

/-- Extracts target vector from the tableau, putting auxiliary variables aside (see `stateLP`). -/
def extractSolution (tableau : Tableau matType) : Array Rat :=
  Id.run
    (do
      let mut ans : Array Rat := Array.replicate (tableau.basic.size + tableau.free.size - 3) 0
      for h : i in [1:tableau.basic.size]do
        ans := ans.set! (tableau.basic[i] - 2) <| tableau.mat[(i, tableau.free.size - 1)]!
      return ans)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru