VeriFIT / mata

A fast and simple automata library
MIT License
14 stars 11 forks source link

Partition and ExtendableSquareMatrix data structures #399

Open kocotom opened 3 months ago

kocotom commented 3 months ago

I have implemented two data structures:

  1. Partition, an efficient representation of set partition with the ability to
    • matching carrier set elements with corresponding blocks in constant time
    • split blocks
    • easily access former blocks which had been split before and iterate through them efficiently
  2. ExtendableSquareMatrix, an abstract representation of binary relation over a set, a matrix of counters etc. with the ability to
    • assign a value to the matrix cell
    • read a value from the matrix cell
    • extend the n x n matrix to the (n+1) x (n+1) matrix (if n < capacity)
    • implement the exact inner representation of the matrix in various ways and choose the set/get/extend strategies depending on the context

I have also implemented three concrete representations of the ExtendableSquareMatrix which inherit from that structure and implement the virtual methods get, set and extend:

  1. CascadeSquareMatrix (I'm not sure whether the name is appropriate)
    • the matrix is represented as a single 1D vector which simulates some kind of "cascade" traversal of the matrix in respect to the way the matrix is iteratively extended
    • good for relations/matrices of counters over the sets which are not huge
  2. DynamicSquareMatrix
    • the matrix is represented as a vector of vectors
  3. HashedSquareMatrix
    • the matrix is represented as an unordered hashmap

These data structures are implemented in the file partition-relation-pair.hh. Soon there will be a data structure PartitionRelationPair which use combination of Partition and ExtendableSquareMatrix but it is not fully done yet so I have not included it.

I have also added a lot of tests which work with these data structures.

The code is massively commented to ease understanding.

codecov[bot] commented 3 months ago

Codecov Report

Attention: Patch coverage is 98.13433% with 5 lines in your changes missing coverage. Please review.

Project coverage is 73.90%. Comparing base (278a599) to head (9067a1f). Report is 17 commits behind head on devel.

:exclamation: Current head 9067a1f differs from pull request most recent head f37352b

Please upload reports for the commit f37352b to get more accurate results.

Files Patch % Lines
include/mata/utils/extendable-square-matrix.hh 96.80% 0 Missing and 3 partials :warning:
src/partition.cc 98.78% 0 Missing and 2 partials :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## devel #399 +/- ## ========================================== + Coverage 72.14% 73.90% +1.76% ========================================== Files 30 33 +3 Lines 3712 3982 +270 Branches 847 887 +40 ========================================== + Hits 2678 2943 +265 Misses 738 738 - Partials 296 301 +5 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

Adda0 commented 3 months ago

Thank you for the PR. I will be reviewing the PR throughout the week. Is that good enough for your needs?

kocotom commented 3 months ago

@Adda0 Thanks for your reaction, yes, that is ok!

I have just made few little changes:

kocotom commented 3 months ago

I have just made one more little change:

kocotom commented 3 months ago

I have just realized that I had passed several vectors to functions without using constant reference even though these vectors are not modified within corresponding functions, so I have fixed it. Namely:

Adda0 commented 3 months ago

Hey. Sorry for the delay. Still working on it. Things got in the way.

kocotom commented 3 months ago

I have just did one more little change. I have deleted the copy function which had cretead a deep copy of a given ExtendableSquareMatrix instance. Instead, I have replaced it with a pure virtual method clone which is a part of the ExtendableSquareMatrix structure. Each substructure reimplements it on its own. I think this is a better solution for this problem.

kocotom commented 3 months ago

Thanks for your suggestions. I have resolved several of them and I will continue later today. The last fix caused few unsuccessful checks but I have not discovered the cause yet, I will inspect it more thoroughly later today.

kocotom commented 2 months ago

I have made several changes in the Partition class inner logic to make it easier to manipulate with that data structure.

In the previous version, BlockItem, Block and Node were simple structures whose only purpose was to store various indices of partition vectors. The matching of the corresponding structures was done using several methods like get_node_idx_from_block_item_idx and so on.

In the current version, BlockItem, Block and Node are private classes defined inside of the Partition class. They still store indices of the partition vectors but they also contain methods which simplify manipulation with the partition.

The other methods were changed to reflect the current representation of the partition.

Adda0 commented 2 months ago

This looks beautiful. I will review the changes during this week. The description above looks great, though.