Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm

Hooks to enable the use of the simplex algorithm in linarith #

source
def Linarith.SimplexAlgorithm.preprocess (hyps : List Linarith.Comp) (maxVar : ℕ) :
Linarith.SimplexAlgorithm.Matrix (maxVar + 1) hyps.length × List ℕ

Preprocess the goal to pass it to findPositiveVector.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Linarith.SimplexAlgorithm.postprocess (vec : Array ℚ) :
    Batteries.HashMap ℕ ℕ

    Extract the certificate from the vec found by findPositiveVector.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Linarith.CertificateOracle.simplexAlgorithm :
      Linarith.CertificateOracle

      An oracle that uses the simplex algorithm.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For