Commit 2024-06-13 13:20 8c85ba7b

View on Github →

feat(Tactic/Linarith): use sparse matrices (#12819)

Introduce the SparseMatrix structure, which can be used in the Simplex Algorithm via class UsableInSimplexAlgorithm.
Use them in a default linarith's oracle. This should speed up linarith on sparse states. In particular, this affects nlinarith, because it typically passes very sparse matrices to the algorithm.

Estimated changes

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean

deleted def Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithm

added def Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmDense

added def Linarith.SimplexAlgorithm.CertificateOracle.simplexAlgorithmSparse

modified def Linarith.SimplexAlgorithm.preprocess

Modified Mathlib/Tactic/Linarith/SimplexAlgorithm/Datatypes.lean

added structure Linarith.SimplexAlgorithm.DenseMatrix

deleted structure Linarith.SimplexAlgorithm.Matrix

added structure Linarith.SimplexAlgorithm.SparseMatrix

Modified Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean

modified def Linarith.SimplexAlgorithm.Gauss.findNonzeroRow

Modified Mathlib/Tactic/Linarith/SimplexAlgorithm/PositiveVector.lean

modified def Linarith.SimplexAlgorithm.stateLP

Modified Mathlib/Tactic/Linarith/SimplexAlgorithm/SimplexAlgorithm.lean

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified test/linarith.lean