Sparsification of Affine Equality Matrix

[GollokG]

This pull request contributes a sparsification of the AffineEqualityMatrix (affeq) and is based on the domain of @MartinWehking from this PR.

Following restructuring of the modules is introduced:

We added a second AffineEqualityDomain which exploits the sparsity of the affine equality matrices based on this observation by @DrMichaelPetter. A SparseMatrixFunctor and SparseVectorFunctor (as well as ArrayMatrixFunctor and ArrayVectorFunctor) were added for this purpose and replaced the general AbstractMatrix and AbstractVector. The AffineEqualityDomain is now implemented without relying on side effects.

The old AffineEqualityDomain using arrays was renamed to AffineEqualityDomainSideEffects which uses ArrayMatrixFunctor and ArrayVectorFunctor.
No new analysis was added to switch between versions. A description for how to switch between both implementations is provided in the affineEqualityAnalysis file.

The implementation of sparse matrix works as follows:

The sparse matrix is implemented in the ListMatrix module. Its type t is a list of sparseVectors representing the matrix' rows. sparseVector is implemented as an ordered list of tuples (index, value) for all non-zero entries.
Some functions are implemented for zero-preserving functions only. A function is zero-preserving iff it has a fixpoint at zero. These functions are implemented to gain performance when being used on sparseVectors.

This implementation is part of an assignment for the course Automated Bug Hunting and Beyond at TUM in the winter term 2024/25.

[DrMichaelPetter]

Given, that you could change the get_col.. . function to return not only the column, but also the last (idx,val) that is not zero, I think that you could get rid of a lot of calls to nth as well as rev. Especially in case_three.

[DrMichaelPetter]

The more I think about case three, the more I am convinced, that you do not even necessarily have to choose the column element with the largest row index - you might as well choose the one with the smallest index. That would be easy to change, and make case three considerably more easy to implement efficiently.

Although this is valid in terms of computing the disjunction, we lose rref, if we do not choose the largest index.

[jerhard]

Thanks for the PR. @GollokG To document this PR better for people who may look at it in the future , could you please add a few sentences in your top post to elaborate on your approach and what you have changed?