package grenier
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=04831d5c2ea783d4e32b356a8495e5481ce8919aa70f5eecee29baebbf6fa483
sha512=1199122ab70701ecd33bf9c6339a743d163a1ba3ef5d0db189cab6c6712386739031b66002bf48d4740112430a93780f82dc37f56688ee33f99da928186b8205
doc/grenier.valmari/Partition/index.html
Module Partition
Source
Each set is identified by an integer
A partitioning structure for a set of cardinal 'n \ (encoded as a Strong.Natural)
val create :
?partition:('n Strong.Finite.elt -> 'n Strong.Finite.elt -> int) ->
'n Strong.Finite.set ->
'n t
create ?partition n
create a fresh partitioning data structure for a set of cardinal n
. If partition
is not provided, the datastructure is initialized with a single subset that contains all elements. Otherwise, partition
must be a total ordering function and elements that can be distinguished are put in different subsets.
mark part elt
marks the element elt
as active. The datastructure manages an active set by marking a certain number of elements, and then applying an operation to all of them at once.
Put marked elements in different sets. That is, each input set is split in two subsets one with the marked and one with the unmarked elements. Active set is reset after (no elements are marked).
Elements that are not marked are removed from the partition (they will be ignored by future operations). In practice, they are considered as belonging to set -1
(which can be observed by set_of
function), and this -1
set is not counted by the set_count
function. Active set is reset after (no elements are marked).
discard part f
calls the function f
for each element in the set and discard it if the function returns true
. Active set must be empty before and is reset after (no elements are marked).
set_of part elt
returns the index of the set that contains element elt
. Result is between 0
and set_of part - 1
unless the element has been discarded, in which case it is -1
.
choose part set
returns an arbitrary element that belongs to set set
. set
must be between 0
and set_of part - 1
.
choose part set
returns an arbitrary element that belongs to set set
. set
must be between 0
and set_of part - 1
.
iter_elements part set f
applies function f
to each element that currently belongs to set set
.
iter_marked_elements part set f
applies function f
to each element that currently belongs to set set
and is marked.