Skip to content

GitLab

why3
why3
Commit 2cb47409 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft
Browse files
Options

Improve addition

parent f6974ad7
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 380739 additions and 437227 deletions
examples/in_progress/multiprecision/bench/gmpadd 0 → 100644
View file @ 2cb47409
#an bn t(s)
2 1 0.007612
2 2 0.008347
3 1 0.008706
3 2 0.009808
3 3 0.010550
4 1 0.008798
4 2 0.011303
4 3 0.012280
4 4 0.013217
5 1 0.008525
5 2 0.011310
5 3 0.013939
5 4 0.014983
5 5 0.015953
6 1 0.008804
6 2 0.011209
6 3 0.014072
6 4 0.016534
6 5 0.017613
6 6 0.018735
7 1 0.009149
7 2 0.011512
7 3 0.014120
7 4 0.016943
7 5 0.019190
7 6 0.020239
7 7 0.021518
8 1 0.009210
8 2 0.011898
8 3 0.014391
8 4 0.016876
8 5 0.019705
8 6 0.021952
8 7 0.022920
8 8 0.024306
9 1 0.009378
9 2 0.012079
9 3 0.015107
9 4 0.017830
9 5 0.019848
9 6 0.022382
9 7 0.024802
9 8 0.025645
9 9 0.027107
10 1 0.010062
10 2 0.012115
10 3 0.014905
10 4 0.017594
10 5 0.020003
10 6 0.022510
10 7 0.025175
10 8 0.027331
10 9 0.028408
10 10 0.029857
11 1 0.010397
11 2 0.012920
11 3 0.015061
11 4 0.017879
11 5 0.020378
11 6 0.022789
11 7 0.025375
11 8 0.028946
11 9 0.030413
11 10 0.031147
11 11 0.032668
12 1 0.010557
12 2 0.013218
12 3 0.015744
12 4 0.017855
12 5 0.020641
12 6 0.023267
12 7 0.025645
12 8 0.028325
12 9 0.030610
12 10 0.032694
12 11 0.033824
12 12 0.035450
13 1 0.010735
13 2 0.013485
13 3 0.016074
13 4 0.018905
13 5 0.021226
13 6 0.024127
13 7 0.026170
13 8 0.028705
13 9 0.030943
13 10 0.033304
13 11 0.035615
13 12 0.036713
13 13 0.038216
14 1 0.010832
14 2 0.013706
14 3 0.016509
14 4 0.019011
14 5 0.021465
14 6 0.023606
14 7 0.026607
14 8 0.030035
14 9 0.031389
14 10 0.033623
14 11 0.036363
14 12 0.038273
14 13 0.040744
14 14 0.046934
15 1 0.011565
15 2 0.014034
15 3 0.016841
15 4 0.019569
15 5 0.022162
15 6 0.024552
15 7 0.026545
15 8 0.032112
15 9 0.034781
15 10 0.038561
15 11 0.040088
15 12 0.040039
15 13 0.044708
15 14 0.042742
15 15 0.044063
16 1 0.010859
16 2 0.013735
16 3 0.016625
16 4 0.019297
16 5 0.022109
16 6 0.024702
16 7 0.027116
16 8 0.030395
16 9 0.032287
16 10 0.034723
16 11 0.038429
16 12 0.049697
16 13 0.041607
16 14 0.043606
16 15 0.045224
16 16 0.046773
17 1 0.011024
17 2 0.013809
17 3 0.016635
17 4 0.019555
17 5 0.022191
17 6 0.025515
17 7 0.028115
17 8 0.030532
17 9 0.032131
17 10 0.034856
17 11 0.037644
17 12 0.039548
17 13 0.041875
17 14 0.044973
17 15 0.046762
17 16 0.056693
17 17 0.050506
18 1 0.012815
18 2 0.014093
18 3 0.017173
18 4 0.020352
18 5 0.022746
18 6 0.025036
18 7 0.027715
18 8 0.030510
18 9 0.032674
18 10 0.034918
18 11 0.037673
18 12 0.040151
18 13 0.042613
18 14 0.044712
18 15 0.047185
18 16 0.049299
18 17 0.050511
18 18 0.052211
19 1 0.013199
19 2 0.015068
19 3 0.016812
19 4 0.019629
19 5 0.022906
19 6 0.025354
19 7 0.027845
19 8 0.030553
19 9 0.033186
19 10 0.036029
19 11 0.038023
19 12 0.040483
19 13 0.042920
19 14 0.045187
19 15 0.047424
19 16 0.050128
19 17 0.051815
19 18 0.053386
19 19 0.054986
20 1 0.013538
20 2 0.015556
20 3 0.018324
20 4 0.020611
20 5 0.022951
20 6 0.025488
20 7 0.028389
20 8 0.030651
20 9 0.033384
20 10 0.035949
20 11 0.038327
20 12 0.040623
20 13 0.043241
20 14 0.045804
20 15 0.048935
20 16 0.050220
20 17 0.052658
20 18 0.054675
20 19 0.056212
20 20 0.057761
examples/in_progress/multiprecision/bench/gmpdiv
View file @ 2cb47409
#an bn t(s)
2 1 0.005016
2 2 0.005734
3 1 0.005421
3 2 0.006790
3 3 0.004319
4 1 0.006068
4 2 0.008277
4 3 0.010722
4 4 0.004772
5 1 0.006798
5 2 0.010132
5 3 0.012493
5 4 0.012807
5 5 0.005586
6 1 0.007727
6 2 0.011840
6 3 0.013949
6 4 0.016527
6 5 0.013075
6 6 0.005934
7 1 0.008498
7 2 0.013162
7 3 0.016220
7 4 0.016888
7 5 0.018007
7 6 0.013541
7 7 0.008505
8 1 0.009278
8 2 0.014843
8 3 0.018344
8 4 0.019098
8 5 0.021520
8 6 0.019925
8 7 0.015462
8 8 0.007485
9 1 0.010169
9 2 0.016384
9 3 0.020759
9 4 0.021383
9 5 0.022123
9 6 0.024119
9 7 0.021004
9 8 0.016336
9 9 0.009619
10 1 0.010874
10 2 0.018220
10 3 0.022553
10 4 0.024159
10 5 0.023808
10 6 0.027794
10 7 0.025853
10 8 0.022585
10 9 0.017189
10 10 0.010061
11 1 0.011586
11 2 0.019902
11 3 0.024970
11 4 0.026994
11 5 0.027123
11 6 0.028354
11 7 0.030151
11 8 0.028378
11 9 0.024019
11 10 0.019109
11 11 0.010300
12 1 0.012473
12 2 0.021655
12 3 0.027146
12 4 0.029412
12 5 0.030639
12 6 0.031058
12 7 0.034298
12 8 0.033475
12 9 0.030157
12 10 0.025800
12 11 0.020438
12 12 0.011758
13 1 0.013571
13 2 0.023322
13 3 0.029531
13 4 0.032356
13 5 0.033817
13 6 0.034315
13 7 0.035241
13 8 0.037582
13 9 0.036424
13 10 0.033001
13 11 0.027648
13 12 0.022019
13 13 0.013321
14 1 0.014079
14 2 0.024581
14 3 0.031390
14 4 0.034697
14 5 0.037551
14 6 0.038432
14 7 0.038640
14 8 0.043101
14 9 0.041245
14 10 0.038259
14 11 0.034351
14 12 0.028757
14 13 0.021979
14 14 0.013144
15 1 0.014901
15 2 0.026138
15 3 0.033936
15 4 0.037609
15 5 0.040277
15 6 0.042060
15 7 0.042295
15 8 0.044062
15 9 0.046096
15 10 0.043832
15 11 0.041666
15 12 0.036437
15 13 0.031640
15 14 0.023828
15 15 0.014109
16 1 0.015700
16 2 0.027644
16 3 0.036276
16 4 0.040402
2 1 0.004482
2 2 0.005710
3 1 0.005761
3 2 0.006844
3 3 0.004424
4 1 0.006069
4 2 0.008290
4 3 0.010668
4 4 0.004841
5 1 0.006804
5 2 0.010156
5 3 0.012433
5 4 0.012875
5 5 0.005575
6 1 0.007718
6 2 0.011801
6 3 0.013934
6 4 0.016520
6 5 0.013381
6 6 0.005949
7 1 0.008506
7 2 0.013149
7 3 0.016218
7 4 0.017119
7 5 0.018091
7 6 0.013822
7 7 0.008716
8 1 0.009295
8 2 0.014908
8 3 0.018465
8 4 0.018758
8 5 0.021518
8 6 0.020081
8 7 0.015732
8 8 0.007759
9 1 0.010174
9 2 0.016390
9 3 0.020761
9 4 0.021376
9 5 0.022118
9 6 0.024093
9 7 0.021152
9 8 0.016417
9 9 0.009659
10 1 0.010891
10 2 0.018247
10 3 0.022535
10 4 0.023859
10 5 0.023807
10 6 0.027932
10 7 0.025905
10 8 0.022694
10 9 0.017366
10 10 0.010009
11 1 0.011710
11 2 0.019904
11 3 0.024956
11 4 0.026706
11 5 0.027161
11 6 0.028288
11 7 0.030199
11 8 0.028388
11 9 0.024095
11 10 0.019368
11 11 0.010277
12 1 0.012464
12 2 0.021642
12 3 0.027175
12 4 0.029329
12 5 0.030673
12 6 0.031219
12 7 0.034441
12 8 0.033202
12 9 0.030833
12 10 0.025845
12 11 0.020655
12 12 0.011726
13 1 0.013646
13 2 0.023342
13 3 0.029536
13 4 0.032335
13 5 0.033807
13 6 0.034336
13 7 0.035336
13 8 0.037882
13 9 0.036530
13 10 0.032474
13 11 0.027569
13 12 0.022309
13 13 0.013294
14 1 0.014063
14 2 0.024577
14 3 0.031353
14 4 0.034701
14 5 0.037496
14 6 0.038408
14 7 0.038607
14 8 0.043107
14 9 0.041218
14 10 0.038318
14 11 0.034388
14 12 0.028747
14 13 0.021773
14 14 0.013135
15 1 0.015022
15 2 0.026359
15 3 0.033931
15 4 0.037988
15 5 0.040300
15 6 0.041619
15 7 0.042401
15 8 0.043758
15 9 0.046212
15 10 0.044212
15 11 0.041924
15 12 0.036469
15 13 0.031207
15 14 0.023945
15 15 0.014123
16 1 0.015885
16 2 0.027631
16 3 0.036283
16 4 0.040663
16 5 0.042999
16 6 0.046398
16 7 0.046812
16 8 0.047419
16 9 0.051448
16 10 0.050120
16 11 0.047026
16 12 0.043101
16 13 0.038904
16 14 0.032975
16 15 0.024982
16 16 0.015986
17 1 0.016693
17 2 0.029596
17 3 0.038395
17 4 0.042968
17 5 0.046636
17 6 0.049549
17 7 0.051330
17 8 0.052133
17 9 0.052961
17 10 0.055924
17 11 0.054375
17 12 0.050357
17 13 0.046826
17 14 0.040937
17 15 0.034158
17 16 0.026076
17 17 0.015483
18 1 0.017193
18 2 0.031324
18 3 0.040439
18 4 0.046520
18 5 0.050172
18 6 0.053554
18 7 0.056421
18 8 0.057378
18 9 0.057366
18 10 0.061900
18 11 0.060235
18 12 0.057651
18 13 0.053572
18 14 0.048578
18 15 0.043460
18 16 0.036359
18 17 0.028018
18 18 0.017020
19 1 0.018217
19 2 0.033067
19 3 0.043532
19 4 0.048756
19 5 0.053108
19 6 0.056895
19 7 0.059704
19 8 0.061764
19 9 0.062303
19 10 0.064343
19 11 0.066938
19 12 0.065012
19 13 0.061178
19 14 0.055746
19 15 0.051335
19 16 0.045880
19 17 0.037872
19 18 0.028903
19 19 0.017178
20 1 0.018982
20 2 0.034319
20 3 0.045110
20 4 0.051793
20 5 0.056397
20 6 0.060883
20 7 0.064933
20 8 0.066664
20 9 0.067779
20 10 0.068119
20 11 0.073337
20 12 0.071523
20 13 0.069029
20 14 0.064570
20 15 0.059830
20 16 0.054649
20 17 0.046724
20 18 0.038923
20 19 0.030442
20 20 0.018974
16 6 0.046060
16 7 0.046825
16 8 0.047451
16 9 0.051467
16 10 0.050045
16 11 0.047306
16 12 0.042999
16 13 0.039053
16 14 0.032953
16 15 0.025136
16 16 0.015600
17 1 0.016702
17 2 0.029598
17 3 0.038438
17 4 0.043060
17 5 0.046618
17 6 0.049514
17 7 0.051156
17 8 0.052097
17 9 0.053224
17 10 0.056671
17 11 0.056248
17 12 0.050362
17 13 0.046133
17 14 0.040551
17 15 0.034497
17 16 0.026320
17 17 0.015538
18 1 0.017198
18 2 0.031310
18 3 0.040401
18 4 0.046038
18 5 0.049816
18 6 0.053620
18 7 0.056138
18 8 0.056961
18 9 0.056670
18 10 0.062173
18 11 0.060207
18 12 0.057732
18 13 0.053763
18 14 0.048513
18 15 0.042832
18 16 0.036563
18 17 0.028179
18 18 0.017067
19 1 0.018216
19 2 0.033005
19 3 0.042695
19 4 0.048599
19 5 0.053083
19 6 0.056908
19 7 0.059629
19 8 0.061968
19 9 0.062484