Skip to content

GitLab

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

Add tentative optimisation, fix graphs, beautify extraction

parent 63347968
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1454 additions and 1466 deletions
examples/in_progress/multiprecision/Makefile
View file @ 6caec053
......@@ -2,17 +2,17 @@ all: why3 extract
why3:
make -C ../../..
extract: why3
why3 extract -D c -o build mp2.mlw -T N
why3 extract -D c -D mp.drv -o build -L . -T mp2.N
tests: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 tests.c build/mp2.mlw__N.c -I$(GMP_DIR) -lgmp -o tests
gcc -O3 -Wall -g -std=gnu99 tests.c build/N.c -I$(GMP_DIR) -lgmp -o tests
why3mulbench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_MUL tests.c build/mp2.mlw__N.c -I$(GMP_DIR) -lgmp -o why3mulbench
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_MUL tests.c build/N.c -I$(GMP_DIR) -lgmp -o why3mulbench
why3divbench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_DIV tests.c build/mp2.mlw__N.c -I$(GMP_DIR) -lgmp -o why3divbench
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_DIV tests.c build/N.c -I$(GMP_DIR) -lgmp -o why3divbench
gmpmulbench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_GMP -DTEST_MUL tests.c build/mp2.mlw__N.c -I$(GMP_DIR) -lgmp -o gmpmulbench
gcc -O3 -Wall -g -std=gnu99 -DTEST_GMP -DTEST_MUL tests.c build/N.c -I$(GMP_DIR) -lgmp -o gmpmulbench
gmpdivbench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_GMP -DTEST_DIV tests.c build/mp2.mlw__N.c -I$(GMP_DIR) -lgmp -o gmpdivbench
gcc -O3 -Wall -g -std=gnu99 -DTEST_GMP -DTEST_DIV tests.c build/N.c -I$(GMP_DIR) -lgmp -o gmpdivbench
alltests: tests why3mulbench why3divbench gmpmulbench gmpdivbench
......
examples/in_progress/multiprecision/bench/gmpdiv
View file @ 6caec053
#an bn t(s)
2 1 0.004439
2 2 0.005499
3 1 0.005775
3 2 0.007117
3 3 0.004297
4 1 0.006066
4 2 0.008271
4 3 0.010690
4 4 0.004766
5 1 0.006802
5 2 0.010133
5 3 0.012442
5 4 0.012794
5 5 0.005587
6 1 0.007720
6 2 0.011777
6 3 0.013942
6 4 0.016551
6 5 0.013114
6 6 0.005933
7 1 0.008528
7 2 0.013144
7 3 0.016217
7 4 0.016897
7 5 0.018005
7 6 0.013568
7 7 0.008467
8 1 0.009286
8 2 0.014930
8 3 0.018620
8 4 0.018852
8 5 0.021474
8 6 0.019939
8 7 0.015468
8 8 0.007486
9 1 0.010351
9 2 0.016507
9 3 0.020792
9 4 0.021369
9 5 0.022122
9 6 0.024109
9 7 0.020956
9 8 0.016326
9 9 0.009614
10 1 0.010892
2 1 0.004442
2 2 0.005566
3 1 0.005776
3 2 0.007039
3 3 0.004306
4 1 0.006037
4 2 0.008275
4 3 0.010696
4 4 0.004770
5 1 0.006792
5 2 0.010140
5 3 0.012459
5 4 0.012894
5 5 0.005598
6 1 0.007715
6 2 0.011779
6 3 0.013940
6 4 0.016549
6 5 0.013069
6 6 0.005935
7 1 0.008510
7 2 0.013130
7 3 0.016212
7 4 0.016885
7 5 0.017999
7 6 0.013555
7 7 0.008463
8 1 0.009292
8 2 0.014826
8 3 0.018351
8 4 0.019234
8 5 0.030451
8 6 0.028759
8 7 0.022356
8 8 0.011177
9 1 0.011274
9 2 0.020737
9 3 0.029074
9 4 0.021376
9 5 0.022134
9 6 0.024088
9 7 0.020975
9 8 0.016347
9 9 0.009745
10 1 0.010891
10 2 0.018228
10 3 0.022521
10 4 0.023824
10 5 0.023810
10 6 0.027816
10 7 0.025915
10 8 0.022576
10 9 0.017192
10 10 0.010074
11 1 0.011597
11 2 0.019924
11 3 0.024960
11 4 0.026783
11 5 0.027147
11 6 0.028512
11 7 0.030302
11 8 0.028309
11 9 0.024031
11 10 0.019114
11 11 0.010289
12 1 0.012418
12 2 0.021671
12 3 0.027220
12 4 0.029347
12 5 0.030648
12 6 0.031233
12 7 0.034341
12 8 0.033002
12 9 0.030142
12 10 0.025740
12 11 0.020480
12 12 0.011960
13 1 0.013435
13 2 0.023332
13 3 0.029530
13 4 0.032408
13 5 0.033829
13 6 0.034417
13 7 0.035314
13 8 0.037599
13 9 0.036718
13 10 0.032619
13 11 0.027649
13 12 0.022041
13 13 0.013410
14 1 0.014047
14 2 0.024591
14 3 0.031363
14 4 0.034691
14 5 0.037016
14 6 0.038421
14 7 0.038728
14 8 0.043094
14 9 0.041193
14 10 0.038431
14 11 0.034443
14 12 0.028942
14 13 0.021816
14 14 0.013147
15 1 0.014910
15 2 0.026159
15 3 0.033954
15 4 0.037666
15 5 0.040321
15 6 0.041759
15 7 0.042385
15 8 0.043955
15 9 0.046109
15 10 0.043921
15 11 0.042280
15 12 0.036454
15 13 0.031005
15 14 0.023847
15 15 0.014091
16 1 0.015732
16 2 0.027835
16 3 0.036372
16 4 0.040386
16 5 0.043081
16 6 0.046116
16 7 0.046938
16 8 0.047397
16 9 0.051499
16 10 0.050052
16 11 0.047154
16 12 0.043103
16 13 0.038821
16 14 0.032434
16 15 0.025040
16 16 0.015439
17 1 0.016812
17 2 0.030016
17 3 0.038207
17 4 0.042983
17 5 0.046803
17 6 0.049575
17 7 0.051213
17 8 0.052147
17 9 0.053032
17 10 0.056041
17 11 0.054389
17 12 0.050354
17 13 0.046221
17 14 0.040925
17 15 0.034794
17 16 0.025879
17 17 0.015507
18 1 0.017202
18 2 0.031369
18 3 0.040394
18 4 0.046321
18 5 0.049916
18 6 0.053218
18 7 0.056060
18 8 0.057012
18 9 0.056780
18 10 0.062270
18 11 0.060491
18 12 0.057650
18 13 0.053612
18 14 0.049040
18 15 0.042833
18 16 0.036393
18 17 0.027947
18 18 0.017035
19 1 0.018215
19 2 0.032914
19 3 0.042703
19 4 0.048785
19 5 0.053078
19 6 0.056765
19 7 0.059732
19 8 0.061922
19 9 0.062343
19 10 0.064348
19 11 0.066924
19 12 0.065165
19 13 0.061209
19 14 0.055828
19 15 0.051189
19 16 0.046103
19 17 0.037882
19 18 0.029081
19 19 0.017190
20 1 0.018992
20 2 0.034321
20 3 0.045068
20 4 0.051448
20 5 0.057655
20 6 0.060897
20 7 0.063999
20 8 0.066394
20 9 0.067761
20 10 0.068117
20 11 0.073596
20 12 0.071476
20 13 0.069213
20 14 0.064567
20 15 0.059769
20 16 0.054225
20 17 0.046759
20 18 0.038948
20 19 0.030428
20 20 0.018993
10 3 0.022600
10 4 0.023821
10 5 0.023831
10 6 0.027682
10 7 0.025862
10 8 0.022561
10 9 0.017216
10 10 0.010069
11 1 0.011608
11 2 0.019913
11 3 0.024966
11 4 0.026717
11 5 0.027144
11 6 0.028310
11 7 0.030268
11 8 0.028378
11 9 0.024021
11 10 0.019205
11 11 0.010279
12 1 0.012421
12 2 0.021713
12 3 0.027218
12 4 0.029367
12 5 0.030640
12 6 0.031062
12 7 0.034282
12 8 0.033116
12 9 0.030400
12 10 0.025768
12 11 0.020435
12 12 0.011772
13 1 0.013441
13 2 0.023339
13 3 0.029560
13 4 0.032331
13 5 0.033821
13 6 0.034323
13 7 0.035227
13 8 0.037770
13 9 0.036771
13 10 0.032614
13 11 0.027669
13 12 0.022012
13 13 0.013342
14 1 0.014092
14 2 0.024670
14 3 0.031517
14 4 0.034877
14 5 0.037158
14 6 0.038593
14 7 0.038729
14 8 0.043726
14 9 0.042057
14 10 0.038931
14 11 0.034890
14 12 0.028791
14 13 0.021833
14 14 0.013177
15 1 0.014936
15 2 0.026174
15 3 0.034040
15 4 0.037661
15 5 0.040386
15 6 0.041716
15 7 0.042399
15 8 0.043753
15 9 0.046099
15 10 0.043854
15 11 0.041620
15 12 0.036570
15 13 0.031080
15 14 0.023895
15 15 0.014130
16 1 0.015706
16 2 0.027638
16 3 0.036247
16 4 0.040371
16 5 0.043040
16 6 0.046073
16 7 0.046862
16 8 0.047543
16 9 0.051473
16 10 0.050162
16 11 0.047403
16 12 0.043057
16 13 0.038784
16 14 0.032444
16 15 0.024959
16 16 0.015448
17 1 0.016696
17 2 0.029680
17 3 0.038334
17 4 0.043621
17 5 0.046683
17 6 0.049539
17 7 0.051309
17 8 0.052118
17 9 0.052925
17 10 0.055956
17 11 0.054558
17 12 0.050665
17 13 0.046766
17 14 0.040460
17 15 0.035033
17 16 0.025931
17 17 0.015521
18 1 0.017267
18 2 0.031322
18 3 0.040381
18 4 0.046072
18 5 0.049940
18 6 0.053248
18 7 0.056064
18 8 0.057322
18 9 0.056726
18 10 0.061928
18 11 0.060397
18 12 0.057675
18 13 0.053566
18 14 0.048545
18 15 0.042997
18 16 0.036479
18 17 0.027945
18 18 0.017129
19 1 0.018237
19 2 0.032873
19 3 0.042678
19 4 0.048612
19 5 0.053098
19 6 0.056772
19 7 0.059667
19 8 0.061728
19 9 0.062311
19 10 0.064421
19 11 0.066724
19 12 0.065068
19 13 0.061166
19 14 0.055715
19 15 0.051299
19 16 0.046214
19 17 0.037872
19 18 0.028903
19 19 0.017179
20 1 0.018976
20 2 0.034590
20 3 0.045676
20 4 0.051391
20 5 0.056411
20 6 0.060904
20 7 0.064198
20 8 0.066562
20 9 0.067804
20 10 0.068147
20 11 0.073546
20 12 0.071454
20 13 0.069289
20 14 0.064537
20 15 0.059889
20 16 0.054516
20 17 0.046838
20 18 0.039020
20 19 0.030495
20 20 0.019054
examples/in_progress/multiprecision/bench/gmpmul
View file @ 6caec053
#an bn t(s)
2 1 0.000195
2 2 0.000346
2 3 0.000411
2 4 0.000519
2 5 0.000652
2 6 0.000806
2 7 0.000840
2 8 0.000953
2 9 0.001064
2 10 0.001149
2 11 0.001278
2 12 0.001465
2 13 0.001671
2 14 0.001792
2 15 0.001938
2 16 0.002064
2 17 0.002176
2 18 0.002292
2 19 0.002154
2 20 0.002543
3 1 0.000222
3 2 0.000387
3 3 0.000625
3 4 0.000742
3 5 0.000912
3 6 0.001074
3 7 0.001146
3 8 0.001450
3 9 0.001473
3 10 0.001632
3 11 0.001784
3 12 0.001932
3 13 0.002097
3 14 0.002278
3 15 0.002378
3 16 0.002576
3 17 0.002704
3 18 0.002891
3 19 0.003024
3 20 0.003192
4 1 0.000267
4 2 0.000482
4 3 0.000672
4 4 0.000920
4 5 0.001126
4 6 0.001280
4 7 0.001480
4 8 0.001700
4 9 0.001873
4 10 0.002076
4 11 0.002233
4 12 0.002479
4 13 0.002684
4 14 0.002852
4 15 0.003091
4 16 0.003274
4 17 0.003483
4 18 0.003648
4 19 0.003847
4 20 0.004046
5 1 0.000315
5 2 0.000570
5 3 0.000794
5 4 0.001082
5 5 0.001341
5 6 0.001530
5 7 0.001791
5 8 0.002031
5 9 0.002275
5 10 0.002532
5 11 0.002767
5 12 0.003019
5 13 0.003277
5 14 0.003512
5 15 0.003752
5 16 0.003988
5 17 0.004211
5 18 0.004443
5 19 0.004745
5 20 0.004994
6 1 0.000361
6 2 0.000636
6 3 0.000961
6 4 0.001223
6 5 0.001526
6 6 0.001846
6 7 0.002117
6 8 0.002432
6 9 0.002674
6 10 0.002998
6 11 0.003266
6 12 0.003554
6 13 0.003860
6 14 0.004077
6 15 0.004403
6 16 0.004705
6 17 0.005022
6 18 0.005264
6 19 0.005556
6 20 0.005894
7 1 0.000402
7 2 0.000739
7 3 0.001057
7 4 0.001481
7 5 0.001749
7 6 0.002094
7 7 0.002442
7 8 0.002768
7 9 0.003101
7 10 0.003430
7 11 0.003773
7 12 0.004076
7 13 0.004443
7 14 0.004770
7 15 0.005106
7 16 0.005449
7 17 0.005822
7 18 0.006136
7 19 0.006499
7 20 0.006792
8 1 0.000445
8 2 0.000830
8 3 0.001211
8 4 0.001654
8 5 0.001985
8 6 0.002384
8 7 0.002776
8 8 0.003178
8 9 0.003545
8 10 0.003889
8 11 0.004309
8 12 0.004674
8 13 0.005049
8 14 0.005440
8 15 0.005807
8 16 0.006239
8 17 0.006593
8 18 0.006942
8 19 0.007412
8 20 0.007702
2 1 0.000204
2 2 0.000347
3 1 0.000228
3 2 0.000386
3 3 0.000549
4 1 0.000274
4 2 0.000464
4 3 0.000677
4 4 0.000935
5 1 0.000310
5 2 0.000572
5 3 0.000806
5 4 0.001063
5 5 0.001495
6 1 0.000423
6 2 0.000766
6 3 0.001099
6 4 0.001484
6 5 0.001867
6 6 0.002169
7 1 0.000472
7 2 0.000867
7 3 0.001239