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