[m-rev.] for review: faster merging of varsets

[Julien Fischer]

Hi Zoltan,

On Wed, 23 Jan 2019, Zoltan Somogyi wrote:

> On Mon, 14 Jan 2019 06:38:53 +0000 (UTC), Julien Fischer <jfischer at opturion.com> wrote:
>>> If someone would undertake to run tuning benchmarks for me,
>>> I would write the required benchmarking code.
>>
>> I'm happy to run them for you.
>
> Thank you. The benchmark program is attached, as are the updated log file
> and diff.
>
> BTW, on my machine, the benchmark time went from about 920ms to about 170ms.

Here's an initial set of benchmarks on my machine; I've repeated each
benchmark 200 times.  The numbers in parenthesis give the numbers in
the heuristic in varset.use_simple_loop

rotd-2019-01-21: 1132.65
no-simple-loop: 134.50

   (5,2): 133.45
   (5,4): 135.00
   (5,8): 131.70
  (5,16): 117.80
  (5,32): 119.20
  (5,48): 115.75
  (5,64): 116.60
(5,128): 132.65

  (10,2): 131.45
  (10,4): 132.05
  (10,8): 133.25
(10,16): 117.90
(10,24): 116.90
(10,32): 116.90
(10,34): 117.40
(10,36): 115.90
(10,37): 117.15
(10,40): 118.20
(10,48): 118.45
(10,64): 117.70

  (15,2): 134.35
  (15,4): 132.10
  (15,8): 134.00
(15,16): 117.50
(15,32): 117.90
(15,64): 117.25

  (20,2): 133.35
  (20,4): 134.55
  (20,8): 132.45
(20,16): 117.75
(20,32): 116.90
(20,64): 119.10

  (100,2): 132.25
  (100,4): 133.60
  (100,8): 133.45
(100,16): 117.55
(100,32): 116.20
(100,64): 117.85

  (500,2): 132.05
  (500,4): 135.25
  (500,8): 132.45
(500,16): 116.85
(500,32): 116.15
(500,64): 116.95

  (1000,2): 134.65
  (1000,4): 134.25
  (1000,8): 135.00
(1000,16): 125.15
(1000,32): 125.00
(1000,64): 122.20