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 classUsableInSimplexAlgorithm
. - Use them in a default
linarith
's oracle. This should speed uplinarith
on sparse states. In particular, this affectsnlinarith
, because it typically passes very sparse matrices to the algorithm.