Fix.Partition
This module offers a partition refinement data structure.
This data structure is useful in partition refinement algorithms, such as automata minimization algorithms. It is taken from Antti Valmari's 2012 paper, "Fast brief practical DFA minimization".
type 'n elt = 'n Indexing.index
An element is represented as an integer index in the range [0, n)
. See Indexing
for more information about type-level indices.
A data structure of type 'n t
represents a partition of a set of n
elements. The cardinal of this set is represented at the type level by 'n
. The elements are grouped into nonempty disjoint blocks. The data structure allows blocks to be split, so, over time, blocks become smaller: hence the name partition refinement.
The data structure allows elements to be temporarily marked; marks are used to determine how blocks must be split.
Furthermore, the data structure allows some elements to be permanently discarded. The discarded elements are set aside in a special block and no longer participate in the partition refinement process.
val create :
?partition:('n elt -> 'n elt -> int) ->
'n Indexing.cardinal ->
'n t
create ?partition n
creates a fresh partition data structure for a set of cardinal n
.
If the optional argument partition
is absent, then the partition initially has a single block, which contains all elements. In this case, the time complexity of this operation is O(n).
If the optional argument partition
is present, then partition
must be a function that implements a total order. Two elements x
and y
are placed in distinct blocks if and only if they are distinguished by this order, that is, if and only if partition x y
is nonzero. In this case, the time complexity of this operation is O(n.log n).
mark p elt
marks the element elt
. If this element was marked already, then this operation has no effect. If this element was discarded earlier, then this operation has no effect.
The time complexity of this operation is O(1).
val clear_marks : 'n t -> unit
clear_marks p
clears all marks, so, upon return, every element is unmarked.
The amortized time complexity of this operation is O(1).
val split : 'n t -> unit
split p
splits every block that has both marked and unmarked elements into two blocks: a block of the marked elements and a block of the unmarked elements. Then, all marks are cleared.
Whenever a block is split into two subblocks, the existing block index is re-used for the larger half, while a new block number is allocated and given to the smaller half.
The amortized time complexity of this operation is O(1).
val discard_unmarked : 'n t -> unit
discard_unmarked p
discards every unmarked element. Then, all marks are cleared, so, upon return, every element is unmarked.
If every element of a block is discarded, then this block disappears; so, this operation can cause the number of blocks to decrease.
The time complexity of this operation is O(n).
discard p f
discards every element x
such that f x
is true. discard
requires that no element is marked, and preserves this property.
If every element of a block is discarded, then this block disappears; so, this operation can cause the number of blocks to decrease.
The time complexity of this operation is O(n).
Blocks are identified by integer indices, comprised between 0
inclusive and block_count p
exclusive. Of course, the number of blocks, the mapping of elements to blocks, and the choice of a distinguished element within each block can change when the data structure is modified.
val block_count : 'n t -> int
block_count p
returns the current number of blocks. The special block that contains the discarded elements is not counted.
The time complexity of this operation is O(1).
find p elt
returns the index of the block that currently contains the element elt
. If this element has been discarded, the special index -1
is returned. Otherwise, a block index in the range [0, block_count p)
is returned.
The time complexity of this operation is O(1).
iter_block_elements p blk yield
applies yield
to each element that currently belongs to the block blk
.
The time complexity of this operation is linear in the size of the block blk
.
iter_all_elements p yield
applies yield
to every element of every block. The discarded elements are ignored.
The time complexity of this operation is O(n).
choose p blk
returns an arbitrary element of the block blk
.
The time complexity of this operation is O(1).
is_chosen p elt
returns true
if the element elt
has not been discarded and is the distinguished element of its block, that is, if choose p (find p elt)
is elt
.
The time complexity of this operation is O(1).
exhaust_marked_elements p blk yield
applies yield
to each marked element of the block blk
. The function yield
is allowed to mark new elements of this block or of other blocks. The iteration continues until every marked element of the block blk
has been yielded once.
The time complexity of this operation is linear in the number of yielded elements.