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.

def 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
    Instances For

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

      Equations
        Instances For

          An oracle that uses the Simplex Algorithm.

          Equations
            Instances For

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

              Equations
                Instances For