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

[Zoltan Somogyi]

2023-01-24 02:09 GMT+11:00 "Julien Fischer" <jfischer at opturion.com>:
> 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? 

It speeds it up very slightly; the difference (56.14s vs 56.23s on
my speedtest) is in the noise.

> (Since set_of_var
> is implemented using sparse_bitsets and list_to_set is called during
> things like quantification.)

Most of those lists are very short, and thus the improved worst-case
behavior of the new list_to_set is irrelevant for them.

>> +    % 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/

Fixed. Thanks for the review.

Zoltan.