postprocess

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm

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

Lean4

/-- Extract the certificate from the `vec` found by `Linarith.SimplexAlgorithm.findPositiveVector`.
-/
def postprocess (vec : Array ℚ) : Std.HashMap ℕ ℕ :=
  let common_den : ℕ := vec.foldl (fun acc item => acc.lcm item.den) 1
  let vecNat : Array ℕ := vec.map (fun x : ℚ => (x * common_den).floor.toNat)
  (∅ : Std.HashMap Nat Nat).insertMany <|
    vecNat.zipIdx.filterMap fun ⟨item, idx⟩ => if item != 0 then some (idx, item) else none

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

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

Разделы

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

Аффилиация

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