# The oracle based on Simplex Algorithm #

This file contains hooks to enable the use of the Simplex Algorithm in `linarith`. The algorithm's entry point is the function `Linarith.SimplexAlgorithm.findPositiveVector`. See the file `PositiveVector.lean` for details of how the procedure works.

source
def Mathlib.Tactic.Linarith.SimplexAlgorithm.preprocess (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matType] (hyps : List Comp) (maxVar : ℕ) :
matType (maxVar + 1) hyps.length × List ℕ

Preprocess the goal to pass it to `Linarith.SimplexAlgorithm.findPositiveVector`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Linarith.SimplexAlgorithm.postprocess (vec : Array ℚ) :
Std.HashMap ℕ ℕ

Extract the certificate from the `vec` found by `Linarith.SimplexAlgorithm.findPositiveVector`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmSparse :
CertificateOracle

An oracle that uses the Simplex Algorithm.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmDense :
CertificateOracle

The same oracle as `CertificateOracle.simplexAlgorithmSparse`, but uses dense matrices. Works faster on dense states.

Equations

- One or more equations did not get rendered due to their size.

Instances For