Commit 2024-06-11 19:39 e16925c9

refactor(Tactic/Linarith): introduce UsableInSimplexAlgorithm class to allow the use of sparse matrix types in the oracle (#13535) This is the first part of #12819, which I decided to split into two parts. The initial goal is to enable the use of sparse matrices in the linarith's oracle based on the Simplex Algorithm, which speeds up linarith, and especially nlinarith, in many cases.

• Introduce the UsableInSimplexAlgorithm class, which specifies the operations required from a matrix type for use in Gauss Elimination and the Simplex Algorithm within the corresponding oracle for the linarith tactic. Rewrite these algorithms to use this class, allowing any matrix type to be used.
• Make Matrix an instance of this class.