Commit f0a3cf9b authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Clean up printer and tests

parent c1967cff
......@@ -5,6 +5,7 @@ extract: why3
why3 extract -D c -D mp.drv -o build/N.c -L . mp2.N
tests: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 tests.c build/N.c -I$(GMP_DIR) -lgmp -o tests
./tests
why3addbench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_ADD tests.c build/N.c -I$(GMP_DIR) -lgmp -o why3addbench
why3mulbench: extract check-gmp
......@@ -30,8 +31,7 @@ data: alltests
plots: data
./divplot
./fullrelative
./relative_noextremes
./divrelative
./mulrelative
./addrelative
......
#an bn t(s)
2 1 0.704004
2 2 0.767039
3 1 0.856312
3 2 0.963957
3 3 1.041644
4 1 0.862380
4 2 1.115684
4 3 1.226342
4 4 1.319345
5 1 0.850126
5 2 1.133145
5 3 1.386156
5 4 1.490561
5 5 1.597041
6 1 0.881402
6 2 1.123037
6 3 1.413522
6 4 1.654216
6 5 1.754929
6 6 1.880241
7 1 0.917437
7 2 1.156082
7 3 1.407971
7 4 1.691000
7 5 1.927504
7 6 2.030355
7 7 2.154608
8 1 0.937237
8 2 1.188003
8 3 1.436540
8 4 1.690123
8 5 1.967904
8 6 2.193819
8 7 2.294913
8 8 2.573332
9 1 0.934390
9 2 1.206959
9 3 1.473998
9 4 1.722001
9 5 1.971460
9 6 2.245232
9 7 2.461841
9 8 2.566012
9 9 2.713053
10 1 1.067195
10 2 1.216778
10 3 1.495716
10 4 1.760080
10 5 2.002989
10 6 2.254038
10 7 2.517203
10 8 2.731229
10 9 2.843845
10 10 2.995087
11 1 1.036081
11 2 1.288057
11 3 1.507325
11 4 1.780596
11 5 2.044580
11 6 2.286853
11 7 2.541158
11 8 2.792920
11 9 3.003020
11 10 3.118881
11 11 3.272000
12 1 1.057227
12 2 1.325909
12 3 1.573215
12 4 1.790573
12 5 2.063281
12 6 2.325924
12 7 2.564952
12 8 2.811257
12 9 3.065229
12 10 3.268730
12 11 3.412971
12 12 3.550496
13 1 1.077680
13 2 1.340040
13 3 1.618326
13 4 1.860378
13 5 2.076978
13 6 2.349487
13 7 2.610468
13 8 2.845325
13 9 3.091884
13 10 3.339462
13 11 3.542432
13 12 3.668044
13 13 3.832192
14 1 1.079897
14 2 1.353736
14 3 1.628944
14 4 1.895084
14 5 2.139063
14 6 2.364416
14 7 2.633916
14 8 2.891768
14 9 3.124213
14 10 3.367051
14 11 3.612620
14 12 3.814409
14 13 3.944502
14 14 4.110913
15 1 1.084846
15 2 1.366648
15 3 1.643708
15 4 1.914098
15 5 2.183454
15 6 2.427731
15 7 2.648170
15 8 2.915410
15 9 3.171932
15 10 3.406194
15 11 3.638970
15 12 3.885149
15 13 4.088371
15 14 4.225560
15 15 4.389310
16 1 1.092497
16 2 1.371500
16 3 1.654126
16 4 1.934951
16 5 2.204962
16 6 2.473238
16 7 2.713844
16 8 2.938615
16 9 3.202357
16 10 3.457740
16 11 3.683816
16 12 3.927341
16 13 4.159773
16 14 4.364571
16 15 4.512569
16 16 4.665957
17 1 1.099794
17 2 1.381838
17 3 1.664577
17 4 1.942136
17 5 2.220845
17 6 2.488188
17 7 2.756420
17 8 2.994732
17 9 3.220317
17 10 3.484894
17 11 3.736524
17 12 3.968917
17 13 4.195363
17 14 4.434144
17 15 4.639945
17 16 4.776893
17 17 4.945901
18 1 1.279268
18 2 1.389141
18 3 1.676328
18 4 1.957099
18 5 2.234260
18 6 2.507244
18 7 2.771167
18 8 3.037530
18 9 3.269933
18 10 3.498037
18 11 3.784929
18 12 4.014772
18 13 4.241274
18 14 4.477392
18 15 4.747171
18 16 5.054211
18 17 5.053722
18 18 5.231621
19 1 1.318796
19 2 1.505138
19 3 1.676245
19 4 1.964209
19 5 2.243710
19 6 2.519939
19 7 2.792005
19 8 3.055975
19 9 3.320424
19 10 3.553585
19 11 3.783330
19 12 4.048767
19 13 4.300445
19 14 4.520411
19 15 4.753391
19 16 4.983599
19 17 5.190714
19 18 5.334169
19 19 5.505564
20 1 1.348496
20 2 1.548956
20 3 1.790197
20 4 1.973200
20 5 2.250130
20 6 2.531995
20 7 2.806938
20 8 3.078427
20 9 3.356580
20 10 3.602790
20 11 3.839065
20 12 4.077655
20 13 4.337778
20 14 4.583526
20 15 4.911340
20 16 5.029044
20 17 5.260180
20 18 5.460390
20 19 5.626675
20 20 5.786055
2 1 0.079467
2 2 0.060877
3 1 0.094640
3 2 0.081266
3 3 0.059635
4 1 0.089383
4 2 0.099571
4 3 0.078243
4 4 0.059540
5 1 0.084238
5 2 0.098210
5 3 0.096763
5 4 0.080910
5 5 0.070140
6 1 0.093406
6 2 0.094459
6 3 0.093974
6 4 0.097817
6 5 0.085070
6 6 0.076898
7 1 0.094762
7 2 0.098427
7 3 0.094695
7 4 0.097634
7 5 0.100331
7 6 0.089650
7 7 0.086010
8 1 0.097797
8 2 0.104398
8 3 0.098424
8 4 0.095701
8 5 0.103645
8 6 0.107609
8 7 0.095698
8 8 0.083866
9 1 0.099413
9 2 0.106249
9 3 0.100785
9 4 0.100464
9 5 0.103021
9 6 0.110277
9 7 0.113445
9 8 0.095436
9 9 0.092269
10 1 0.103755
10 2 0.108328
10 3 0.101461
10 4 0.106431
10 5 0.110664
10 6 0.115347
10 7 0.119303
10 8 0.111763
10 9 0.103082
10 10 0.104693
11 1 0.107054
11 2 0.112648
11 3 0.103278
11 4 0.107135
11 5 0.109957
11 6 0.114993
11 7 0.119030
11 8 0.117005
11 9 0.118606
11 10 0.111979
11 11 0.112381
12 1 0.108282
12 2 0.115879
12 3 0.111298
12 4 0.111677
12 5 0.110954
12 6 0.118968
12 7 0.122954
12 8 0.122794
12 9 0.124443
12 10 0.126942
12 11 0.119923
12 12 0.110114
13 1 0.107629
13 2 0.115656
13 3 0.111833
13 4 0.115705
13 5 0.114747
13 6 0.124785
13 7 0.125491
13 8 0.122415
13 9 0.127197
13 10 0.132318
13 11 0.136054
13 12 0.122545
13 13 0.119053
14 1 0.110173
14 2 0.116350
14 3 0.114391
14 4 0.117406
14 5 0.119965
14 6 0.123538
14 7 0.130995
14 8 0.130843
14 9 0.130731
14 10 0.135399
14 11 0.140614
14 12 0.133722
14 13 0.126626
14 14 0.125747
15 1 0.109411
15 2 0.118324
15 3 0.115930
15 4 0.122063
15 5 0.127105
15 6 0.132441
15 7 0.131941
15 8 0.130355
15 9 0.138757
15 10 0.143413
15 11 0.148163
15 12 0.141343
15 13 0.140326
15 14 0.134765
15 15 0.134114
16 1 0.109747
16 2 0.121475
16 3 0.121154
16 4 0.123344
16 5 0.127820
16 6 0.131934
16 7 0.136007
16 8 0.133906
16 9 0.140128
16 10 0.144439
16 11 0.148485
16 12 0.146065
16 13 0.147621
16 14 0.148488
16 15 0.142898
16 16 0.134081
17 1 0.110933
17 2 0.119877
17 3 0.116384
17 4 0.121547
17 5 0.126154
17 6 0.134977
17 7 0.140126
17 8 0.134855
17 9 0.138751
17 10 0.146267
17 11 0.151862
17 12 0.147255
17 13 0.150891
17 14 0.156802
17 15 0.159461
17 16 0.142170
17 17 0.143547
18 1 0.128445
18 2 0.123796
18 3 0.120353
18 4 0.126107
18 5 0.128359
18 6 0.135965
18 7 0.144590
18 8 0.141012
18 9 0.143481
18 10 0.147114
18 11 0.159584
18 12 0.154038
18 13 0.158269
18 14 0.160255
18 15 0.163714
18 16 0.156013
18 17 0.150927
18 18 0.154707
19 1 0.133028
19 2 0.131021
19 3 0.123301
19 4 0.126381
19 5 0.132791
19 6 0.141111
19 7 0.143502
19 8 0.142804
19 9 0.149692
19 10 0.153453
19 11 0.156550
19 12 0.154729
19 13 0.161691
19 14 0.168451
19 15 0.171978
19 16 0.162821
19 17 0.165647
19 18 0.159678
19 19 0.159198
20 1 0.136727
20 2 0.134302
20 3 0.134061
20 4 0.126109
20 5 0.133479
20 6 0.139264
20 7 0.148553
20 8 0.146746
20 9 0.156501
20 10 0.162726
20 11 0.165067
20 12 0.158717
20 13 0.167729
20 14 0.175485
20 15 0.173620
20 16 0.167490
20 17 0.171069
20 18 0.172407
20 19 0.167107
20 20 0.159191
#an bn t(s)
2 1 0.437339
2 2 0.509746
3 1 0.517486
3 2 0.678138
3 3 0.481677
4 1 0.600554
4 2 0.846556
4 3 1.060539
4 4 0.499638
5 1 0.683074
5 2 1.001608
5 3 1.254160
5 4 1.250706
5 5 0.568078
6 1 0.765275
6 2 1.164116
6 3 1.401108
6 4 1.632845
6 5 1.306513
6 6 0.643751
7 1 0.842964
7 2 1.325636
7 3 1.602643
7 4 1.702600
7 5 1.802779
7 6 1.407048
7 7 0.746852
8 1 0.930004
8 2 1.498745
8 3 1.861463
8 4 1.894406
8 5 2.166974
8 6 2.000564
8 7 1.529775
8 8 0.800727
9 1 1.012236
9 2 1.655131
9 3 2.080765
9 4 2.116612
9 5 2.204114
9 6 2.387192
9 7 2.106474
9 8 1.640377
9 9 0.863482
10 1 1.088399
10 2 1.830060
10 3 2.328290
10 4 2.414314
10 5 2.417646
10 6 2.780448
10 7 2.595026
10 8 2.284352
10 9 1.763182
10 10 0.994418
11 1 1.173381
11 2 2.015509
11 3 2.549199
11 4 2.709287
11 5 2.752228
11 6 2.831046
11 7 3.065971
11 8 2.844468
11 9 2.448329
11 10 1.875630
11 11 1.063143
12 1 1.261231
12 2 2.173720
12 3 2.758261
12 4 3.003110
12 5 3.120796
12 6 3.126697
12 7 3.513561
12 8 3.321693
12 9 3.013909
12 10 2.600828
12 11 2.042058
12 12 1.177496
13 1 1.337767
13 2 2.336110
13 3 2.985548
13 4 3.275939
13 5 3.428079
13 6 3.521475
13 7 3.583931
13 8 3.854192
13 9 3.606378
13 10 3.246507
13 11 2.776279
13 12 2.142653
13 13 1.232431
14 1 1.417713
14 2 2.490813
14 3 3.215660
14 4 3.549173
14 5 3.738281
14 6 3.900586
14 7 3.916728
14 8 4.308727
14 9 4.176696
14 10 3.906379
14 11 3.440377
14 12 2.938988
14 13 2.291817
14 14 1.383833
15 1 1.501679
15 2 2.670758
15 3 3.460527
15 4 3.820841
15 5 4.087042
15 6 4.261879
15 7 4.355754
15 8 4.418510
15 9 4.684561
15 10 4.497998
15 11 4.121660
15 12 3.668749
15 13 3.156980
15 14 2.384129
15 15 1.377704
16 1 1.584621
16 2 2.827660
16 3 3.657064
16 4 4.090000
16 5 4.389941
16 6 4.660339
16 7 4.768594
16 8 4.776114
16 9 5.220904
16 10 5.041826
16 11 4.815634
16 12 4.383317
16 13 3.888748
16 14 3.296556
16 15 2.553493
16 16 1.588411
17 1 1.668304
17 2 2.995077
17 3 3.895473
17 4 4.382369
17 5 4.707583
17 6 5.014260
17 7 5.176013
17 8 5.268548
17 9 5.325769
17 10 5.645688
17 11 5.444816
17 12 5.133591
17 13 4.646217
17 14 4.131450
17 15 3.539627
17 16 2.701755
17 17 1.620451
18 1 1.745702
18 2 3.141227
18 3 4.074909
18 4 4.620624
18 5 5.019009
18 6 5.375486
18 7 5.590648
18 8 5.747268
18 9 5.732150
18 10 6.202145
18 11 6.061116
18 12 5.792638
18 13 5.434840
18 14 4.888842
18 15 4.367888
18 16 3.745866
18 17 2.825528
18 18 1.670484
19 1 1.825917
19 2 3.293024
19 3 4.268455
19 4 4.853045
19 5 5.313899
19 6 5.727552
19 7 5.955815
19 8 6.202871
19 9 6.227310
19 10 6.413466
19 11 6.712159
19 12 6.496179
19 13 6.152997
19 14 5.685231
19 15 5.181484
19 16 4.692840
19 17 3.803166
19 18 2.904441
19 19 1.801899
20 1 1.906144
20 2 3.461641
20 3 4.539049
20 4 5.183580
20 5 5.669835
20 6 6.116282
20 7 6.470186
20 8 6.723714
20 9 6.802896
20 10 6.935021
20 11 7.393492
20 12 7.178390
20 13 6.911021
20 14 6.542065
20 15 6.024770
20 16 5.457261
20 17 4.863276
20 18 3.956523
20 19 3.137017
20 20 1.954227
2 1 0.028907
2 2 0.020846
3 1 0.034066
3 2 0.038696
3 3 0.039679
4 1 0.039847
4 2 0.047367
4 3 0.077311
4 4 0.037603
5 1 0.045570
5 2 0.056152
5 3 0.082546
5 4 0.083905
5 5 0.039257
6 1 0.050825
6 2 0.066038
6 3 0.094025
6 4 0.106563
6 5 0.081958
6 6 0.041196
7 1 0.056767
7 2 0.073689
7 3 0.106005
7 4 0.105639
7 5 0.115044
7 6 0.084360
7 7 0.044313
8 1 0.062357
8 2 0.084776
8 3 0.117879
8 4 0.111655
8 5 0.130379
8 6 0.119339
8 7 0.087100
8 8 0.045674
9 1 0.067758