package acgtk
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=5d380a947658fb1201895cb4cb449b1f60f54914c563e85181d628a89f045c1dd7b5b2226bb7865dd090f87caa9187e0ea6c7a4ee3dc3dda340d404c4e76c7c2
doc/acgtk.datalogLib/DatalogLib/UnionFind/Make/index.html
Module UnionFind.MakeSource
This (functor) module implements a UnionFind data structure. The S parameter is used to try different implementations of indexed data structure, in particular eventually persistent arrays as described in "A Persistent Union-Find Data Structure" (Sylvain Conchon and Jean-Chrisophe Filliâtre
Parameters
Signature
The type of the indexed data structure
The type of the values (content) that are indexed. It is either an actual value of type 'a or a link to another indexed value. If a content at an index i points to i, it is meant that to be a variable.
Exception raised when a the union of to indexed value can not happen. It should be raised by the union function when it amounts to make the union between to actual values Value a and Value b and a != b.
create l returns the corresponding indexed storage data structure where each value (or link) is indexed by its position in l (starting at 1). d is a data that may or may not be used to fill at init the indexed data structure.
extract ~start:s i t returns a list of the i first elements of t starting from position s (default is 1, first position). It is ensured that the results only contain the values of representatives (i.e it follows the Link_to links until the value of the representative before returning it).
find i h returns not only the index of the representative and the values it indexes, but also the storage data structure, so that the find algorithm can modify it, in particular with path compression. If the returned content is a Link_to j then j=i.
union i j h returns a new indexed storage data structure where values indexed by i and j have been unified (ie one of the two is now linked to the index of the representative of the other. It fails and raises the Union_Failure exception if both i and j representatives index actual values Value a and Value b and a != b.
instantiate i t h returns a new indexed storage data structure where the value indexed by i and t have been unified. It fails and raises the Union_Failure exception if i's representative indexes an actual values Value a such that a differs from t.
cyclic i h returns a pair (b,h') where b is true if h has a cycle (following the Link_to links) containing i and false otherwise, and where h' contains the same information as h (possibly differently stored, for instance using path compression while checking h cyclicity.