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
def Linarith.SimplexAlgorithm.preprocess (matType : ℕ → ℕ → Type) [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (hyps : List Linarith.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 Linarith.SimplexAlgorithm.postprocess (vec : Array ℚ) :
    Batteries.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 Linarith.CertificateOracle.simplexAlgorithmSparse :
      Linarith.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 Linarith.CertificateOracle.simplexAlgorithmDense :
        Linarith.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