Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm

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
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    def Mathlib.Tactic.Linarith.SimplexAlgorithm.postprocess (vec : Array â„š) :
    Std.HashMap â„• â„•

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

    Instances For
      source
      🔸 coverage
      def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmSparse :
      CertificateOracle

      An oracle that uses the Simplex Algorithm.

      Instances For
        source
        🔸 coverage
        def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmDense :
        CertificateOracle

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

        Instances For