[m-rev.] for review: improve the worst case of sparse bitset list_to_set

[Julien Fischer]

On Mon, 23 Jan 2023, Zoltan Somogyi wrote:

> For very small bitsets, e.g. those that contain only values
> in the range 0-63, the old implementation is probably a bit faster.
> Is this important enough to keep the old implementation alongside the new?
> And if so, should the old one be list_to_set, and the new one
> something like long_list_to_set, or should the new one be
> list_to_set, with the old one being short_list_to_set?

What impact does this change have on the compiler?  (Since set_of_var
is implemented using sparse_bitsets and list_to_set is called during
things like quantification.)

> Improve the worst case of list_to_set on sparse bitsets.
> 
> library/sparse_bitset.m:
>     Replace the old algorithm, which had O(N^2) worst-case behavior,
>     with a modified form of natural merge sort, whose worst-case complexity
>     is O(NlogN).
> 
> diff --git a/library/sparse_bitset.m b/library/sparse_bitset.m
> index 1f96de33f..6126d6271 100644
> --- a/library/sparse_bitset.m
> +++ b/library/sparse_bitset.m
> @@ -1319,78 +1319,143 @@ divide_bits_by_set(DivideByBits, Size, Offset, Bits, !In, !Out) :-

...

> +list_to_set(ItemList, Set) :-
> +    % The algorithm we use is a modified version of natural merge sort.
> +    %
> +    % Unlike with the usual version of natural merge sort, the enum values
> +    % of the items in a run don't have to be strictly ascending, because
> +    % the order in which the bits of a given bitset_elem are set does not
> +    % matter. For the purposes of finding ascending runs, the defining
> +    % characteristic of a run is that the *offsets* of the bitset_elems
> +    % to which the enum values of the items belong should not decrease.
> +    % Likewise, the criterion for descending runs is that the offsets
> +    % should not increase.
> +    %
> +    % This means that the typical runs discovered by list_to_set_get_runs
> +    % can be expected to be longer than the runs of a conventional
> +    % natural merge sort, unless the number of bits set in each bitset_elem
> +    % in each run is at, or just above, one.
> +    list_to_set_get_runs(ItemList, [], Runs),
> +    % Once we have a list of runs, union them all together using the
> +    % usual implementation of union_list, which is effectively a merge sort.
> +    % It can be significantly faster than usual merge sort, because a single
> +    % logical OE operation can merge up to ubits_per_uint items, though again,

s/OE/OR/

> +    % this advantage goes away if the number of bits set in each bitset_elem
> +    % in the final result is at, or just above, one.
> +    union_list(Runs, Set).

That looks fine otherwise.

Julien