Mentions légales du service

Skip to content

Add refinement algorithm (to merge after the clean-ijkstra-prepare request)

BOUR Frederic requested to merge fbour/menhir:clean-ijkstra-refinement into faster-reachability

The computation of refined partitions is done by assuming a total order on the element of the sets (the index of a bit for bit sets).

Sets are then seen as an ordered sequence of element. They are ordered by their minimum elements, and then repeatedly split to extract the unique prefix and the common prefix.

A few dedicated primitives help making this operation much more efficient than if naively implemented on top of set interface.

The primitives are:

  • quick_subset: a faster computation of subset that assumes the arguments are either in a subset relation or disjoint.

  • compare_minimum: order sets by comparing their minimum elements

  • extract_common: extract the common prefix of two sets seen as sequences and also return the remainders.

  • extract_prefix: [extract_prefix s1 s2] extracts all elements of [s1] that are strictly smaller than all elements of [s2], and also returns the remainder.

  • interval_union: computes the union of a list of sets that does not overlap when seen as sequence (the intervals formed by [min s ... max s] do not overlap). This primitive helps working around the case where a sequence of [SparseBitSet.union] can become quadratic when the arguments are ordered (always appending at the end).

Finding better names

  • quick_subset: "quick" does not reflect the peculiarity of this function, and that it is "unsound" in general (it won't compute the subset relation for two arbitrary sets)

  • extract_common: extract_shared_prefix? (the prefix sequence common to s1 and s2)

  • extract_prefix: extract_unique_prefix? This is not ideal either. For instance:

    extract_prefix [1; 2; 4] [3; 5] = ([1; 2], [4])

    because even if the sets are disjoints, [1; 2] is the prefix of [1; 2; 4] that is strictly smaller than min [3; 5] = 3

  • interval_union: does not reflect that the list should be ordered, and that the arguments are not really intervals, but that their intervals does not overlap. Maybe ordered_union is better: the invariant expected is that, for a sequence of sets S_n, i < j => max(S_i) < min (S_j)

Implementation for patricia

These primitives are not implemented for patricia sets (implemented by Patricia.Domain). I didn't bother... Right now the implementation raises an exception.

An alternative solution is to split [GSet.S] in two: leaving [S] for the unchanged, traditional, Set interface and adding, say, [Partitionable] for the "partition" friendly interface.

A third solution is to implement the primitives for [Patricia.Domain]. In this case, and if performance matters, it might also be worth considering to borrow a bit from [SparseBitSet] and represent a [Patricia.Domain] as a map of sparse addresses to AtomicBitSet. This is significantly more compact that a normal PatriciaSet (especially for terminals and non-terminals which are quite compact finite sets).

This new bitset implementation should probably be quite competitive compared to the existing specialized ones (~ a constant factor slower for small bit sets, and asymptotically faster for large ones).

Edited by BOUR Frederic

Merge request reports