Setting up a post-analysis count of the share of elements in a matrix that are equal to 0, we come to the following histogram:
the x-axis is the percentage of 0-elements in relation to all matrix elements of an analysis
the y-axis is the number of SV-Comp input files of which the average share of 0 entries
Since we explicitly represent those 0 entries in our current affine-equality array, representation a sparse representation would have some potential for runtime and memory consumption savings.
In former legacy implementations for older analyzers, sparse affine equality implementations where quite successful.
Implementation
Although there is an interface of abstract vectors and matrices are already present in the code, this was not designed with the idea of sparsely represented data in mind. All in all, this is an initial idea of the complications:
Especially fold/map style interfaces need to be carefully either implemented with a artificially dense behaviour, or its call-sites need to be checked for compatibility with the sparsity of the representation.
Liberal conversion to lists/arrays is now costly
Representation must decide on a row-based or column-based representation; non representation-conforming accesses may be costly and are maybe candidates for caching?
Setting up a post-analysis count of the share of elements in a matrix that are equal to 0, we come to the following histogram:
Since we explicitly represent those 0 entries in our current affine-equality array, representation a sparse representation would have some potential for runtime and memory consumption savings.
In former legacy implementations for older analyzers, sparse affine equality implementations where quite successful.
Implementation
Although there is an interface of abstract vectors and matrices are already present in the code, this was not designed with the idea of sparsely represented data in mind. All in all, this is an initial idea of the complications: