Skip to content
Snippets Groups Projects
Commit 2a424add authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Update example data and generation script 

- Add an unsolved benchmark
- Add a bad strategy
parent 957c8286
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
contrib/example_data.csv
+ 163
− 155
View file @ 2a424add
benchmark;logic;strategy;solved;time
base01.smt2;UF;base-strategy;yes;0.5
base02.smt2;UF;base-strategy;yes;0.5
base03.smt2;UF;base-strategy;yes;0.5
base04.smt2;UF;base-strategy;yes;0.5
base05.smt2;UF;base-strategy;yes;0.5
base06.smt2;UF;base-strategy;yes;0.5
base07.smt2;UF;base-strategy;yes;0.5
base08.smt2;UF;base-strategy;yes;0.5
base09.smt2;UF;base-strategy;yes;0.5
base10.smt2;UF;base-strategy;yes;0.5
base11.smt2;UF;base-strategy;yes;0.5
base12.smt2;UF;base-strategy;yes;0.5
base13.smt2;UF;base-strategy;yes;0.5
base14.smt2;UF;base-strategy;yes;0.5
base15.smt2;UF;base-strategy;yes;0.5
base16.smt2;UF;base-strategy;yes;0.5
base17.smt2;UF;base-strategy;yes;0.5
base18.smt2;UF;base-strategy;yes;0.5
base19.smt2;UF;base-strategy;yes;0.5
base20.smt2;UF;base-strategy;yes;0.5
base01.smt2;UF;extra01;yes;1.5
base02.smt2;UF;extra01;yes;1.5
base03.smt2;UF;extra01;yes;1.5
base04.smt2;UF;extra01;yes;1.5
base05.smt2;UF;extra01;yes;1.5
base06.smt2;UF;extra01;yes;1.5
base07.smt2;UF;extra01;yes;1.5
base08.smt2;UF;extra01;yes;1.5
base09.smt2;UF;extra01;yes;1.5
base10.smt2;UF;extra01;yes;1.5
base11.smt2;UF;extra01;yes;1.5
base12.smt2;UF;extra01;yes;1.5
base13.smt2;UF;extra01;yes;1.5
base14.smt2;UF;extra01;yes;1.5
base15.smt2;UF;extra01;yes;1.5
base16.smt2;UF;extra01;yes;1.5
base17.smt2;UF;extra01;yes;1.5
base18.smt2;UF;extra01;yes;1.5
base19.smt2;UF;extra01;yes;1.5
base20.smt2;UF;extra01;yes;1.5
extra01_01.smt2;UF;extra01;yes;0.5
extra01_02.smt2;UF;extra01;yes;0.5
extra01_03.smt2;UF;extra01;yes;0.5
extra01_04.smt2;UF;extra01;yes;0.5
extra01_05.smt2;UF;extra01;yes;0.5
base01.smt2;UF;extra02;yes;1.5
base02.smt2;UF;extra02;yes;1.5
base03.smt2;UF;extra02;yes;1.5
base04.smt2;UF;extra02;yes;1.5
base05.smt2;UF;extra02;yes;1.5
base06.smt2;UF;extra02;yes;1.5
base07.smt2;UF;extra02;yes;1.5
base08.smt2;UF;extra02;yes;1.5
base09.smt2;UF;extra02;yes;1.5
base10.smt2;UF;extra02;yes;1.5
base11.smt2;UF;extra02;yes;1.5
base12.smt2;UF;extra02;yes;1.5
base13.smt2;UF;extra02;yes;1.5
base14.smt2;UF;extra02;yes;1.5
base15.smt2;UF;extra02;yes;1.5
base16.smt2;UF;extra02;yes;1.5
base17.smt2;UF;extra02;yes;1.5
base18.smt2;UF;extra02;yes;1.5
base19.smt2;UF;extra02;yes;1.5
base20.smt2;UF;extra02;yes;1.5
extra02_01.smt2;UF;extra02;yes;0.5
extra02_02.smt2;UF;extra02;yes;0.5
extra02_03.smt2;UF;extra02;yes;0.5
extra02_04.smt2;UF;extra02;yes;0.5
base01.smt2;UF;extra03;yes;1.5
base02.smt2;UF;extra03;yes;1.5
base03.smt2;UF;extra03;yes;1.5
base04.smt2;UF;extra03;yes;1.5
base05.smt2;UF;extra03;yes;1.5
base06.smt2;UF;extra03;yes;1.5
base07.smt2;UF;extra03;yes;1.5
base08.smt2;UF;extra03;yes;1.5
base09.smt2;UF;extra03;yes;1.5
base10.smt2;UF;extra03;yes;1.5
base11.smt2;UF;extra03;yes;1.5
base12.smt2;UF;extra03;yes;1.5
base13.smt2;UF;extra03;yes;1.5
base14.smt2;UF;extra03;yes;1.5
base15.smt2;UF;extra03;yes;1.5
base16.smt2;UF;extra03;yes;1.5
base17.smt2;UF;extra03;yes;1.5
base18.smt2;UF;extra03;yes;1.5
base19.smt2;UF;extra03;yes;1.5
base20.smt2;UF;extra03;yes;1.5
extra03_01.smt2;UF;extra03;yes;0.5
extra03_02.smt2;UF;extra03;yes;0.5
extra03_03.smt2;UF;extra03;yes;0.5
base01.smt2;UF;extra04;yes;1.5
base02.smt2;UF;extra04;yes;1.5
base03.smt2;UF;extra04;yes;1.5
base04.smt2;UF;extra04;yes;1.5
base05.smt2;UF;extra04;yes;1.5
base06.smt2;UF;extra04;yes;1.5
base07.smt2;UF;extra04;yes;1.5
base08.smt2;UF;extra04;yes;1.5
base09.smt2;UF;extra04;yes;1.5
base10.smt2;UF;extra04;yes;1.5
base11.smt2;UF;extra04;yes;1.5
base12.smt2;UF;extra04;yes;1.5
base13.smt2;UF;extra04;yes;1.5
base14.smt2;UF;extra04;yes;1.5
base15.smt2;UF;extra04;yes;1.5
base16.smt2;UF;extra04;yes;1.5
base17.smt2;UF;extra04;yes;1.5
base18.smt2;UF;extra04;yes;1.5
base19.smt2;UF;extra04;yes;1.5
base20.smt2;UF;extra04;yes;1.5
extra04_01.smt2;UF;extra04;yes;0.5
extra04_02.smt2;UF;extra04;yes;0.5
base01.smt2;UF;extra05;yes;1.5
base02.smt2;UF;extra05;yes;1.5
base03.smt2;UF;extra05;yes;1.5
base04.smt2;UF;extra05;yes;1.5
base05.smt2;UF;extra05;yes;1.5
base06.smt2;UF;extra05;yes;1.5
base07.smt2;UF;extra05;yes;1.5
base08.smt2;UF;extra05;yes;1.5
base09.smt2;UF;extra05;yes;1.5
base10.smt2;UF;extra05;yes;1.5
base11.smt2;UF;extra05;yes;1.5
base12.smt2;UF;extra05;yes;1.5
base13.smt2;UF;extra05;yes;1.5
base14.smt2;UF;extra05;yes;1.5
base15.smt2;UF;extra05;yes;1.5
base16.smt2;UF;extra05;yes;1.5
base17.smt2;UF;extra05;yes;1.5
base18.smt2;UF;extra05;yes;1.5
base19.smt2;UF;extra05;yes;1.5
base20.smt2;UF;extra05;yes;1.5
extra05_01.smt2;UF;extra05;yes;0.5
base01.smt2;UF;extra06;yes;1.5
base02.smt2;UF;extra06;yes;1.5
base03.smt2;UF;extra06;yes;1.5
base04.smt2;UF;extra06;yes;1.5
base05.smt2;UF;extra06;yes;1.5
base06.smt2;UF;extra06;yes;1.5
base07.smt2;UF;extra06;yes;1.5
base08.smt2;UF;extra06;yes;1.5
base09.smt2;UF;extra06;yes;1.5
base10.smt2;UF;extra06;yes;1.5
base11.smt2;UF;extra06;yes;1.5
base12.smt2;UF;extra06;yes;1.5
base13.smt2;UF;extra06;yes;1.5
base14.smt2;UF;extra06;yes;1.5
base15.smt2;UF;extra06;yes;1.5
base16.smt2;UF;extra06;yes;1.5
base17.smt2;UF;extra06;yes;1.5
base18.smt2;UF;extra06;yes;1.5
base19.smt2;UF;extra06;yes;1.5
base20.smt2;UF;extra06;yes;1.5
base01.smt2;UF;base-strategy;yes;0.5189
base02.smt2;UF;base-strategy;yes;0.2164
base03.smt2;UF;base-strategy;yes;0.1754
base04.smt2;UF;base-strategy;yes;0.2658
base05.smt2;UF;base-strategy;yes;0.02813
base06.smt2;UF;base-strategy;yes;0.6898
base07.smt2;UF;base-strategy;yes;0.8723
base08.smt2;UF;base-strategy;yes;0.4137
base09.smt2;UF;base-strategy;yes;0.4554
base10.smt2;UF;base-strategy;yes;0.898
base11.smt2;UF;base-strategy;yes;0.4704
base12.smt2;UF;base-strategy;yes;0.3552
base13.smt2;UF;base-strategy;yes;0.7022
base14.smt2;UF;base-strategy;yes;0.3421
base15.smt2;UF;base-strategy;yes;0.1686
base16.smt2;UF;base-strategy;yes;0.5768
base17.smt2;UF;base-strategy;yes;0.5904
base18.smt2;UF;base-strategy;yes;0.8163
base19.smt2;UF;base-strategy;yes;0.4209
base20.smt2;UF;base-strategy;yes;0.4729
unsolved.smt2;UF;base-strategy;no;0.6347
base01.smt2;UF;extra01;yes;1.29
base02.smt2;UF;extra01;yes;1.255
base03.smt2;UF;extra01;yes;1.004
base04.smt2;UF;extra01;yes;1.523
base05.smt2;UF;extra01;yes;1.315
base06.smt2;UF;extra01;yes;1.627
base07.smt2;UF;extra01;yes;1.63
base08.smt2;UF;extra01;yes;1.587
base09.smt2;UF;extra01;yes;1.393
base10.smt2;UF;extra01;yes;1.702
base11.smt2;UF;extra01;yes;1.355
base12.smt2;UF;extra01;yes;1.469
base13.smt2;UF;extra01;yes;1.265
base14.smt2;UF;extra01;yes;1.666
base15.smt2;UF;extra01;yes;1.427
base16.smt2;UF;extra01;yes;1.431
base17.smt2;UF;extra01;yes;1.356
base18.smt2;UF;extra01;yes;1.461
base19.smt2;UF;extra01;yes;1.47
base20.smt2;UF;extra01;yes;1.863
extra01_01.smt2;UF;extra01;yes;0.4127
extra01_02.smt2;UF;extra01;yes;0.5314
extra01_03.smt2;UF;extra01;yes;0.664
extra01_04.smt2;UF;extra01;yes;0.389
extra01_05.smt2;UF;extra01;yes;0.2684
unsolved.smt2;UF;extra01;yes;0.5983
base01.smt2;UF;extra02;yes;1.474
base02.smt2;UF;extra02;yes;1.21
base03.smt2;UF;extra02;yes;1.591
base04.smt2;UF;extra02;yes;1.151
base05.smt2;UF;extra02;yes;1.628
base06.smt2;UF;extra02;yes;1.289
base07.smt2;UF;extra02;yes;1.916
base08.smt2;UF;extra02;yes;1.422
base09.smt2;UF;extra02;yes;1.816
base10.smt2;UF;extra02;yes;1.552
base11.smt2;UF;extra02;yes;1.405
base12.smt2;UF;extra02;yes;1.681
base13.smt2;UF;extra02;yes;1.411
base14.smt2;UF;extra02;yes;1.613
base15.smt2;UF;extra02;yes;1.913
base16.smt2;UF;extra02;yes;1.331
base17.smt2;UF;extra02;yes;1.92
base18.smt2;UF;extra02;yes;1.755
base19.smt2;UF;extra02;yes;1.276
base20.smt2;UF;extra02;yes;1.579
extra02_01.smt2;UF;extra02;yes;0.6712
extra02_02.smt2;UF;extra02;yes;0.3699
extra02_03.smt2;UF;extra02;yes;0.6082
extra02_04.smt2;UF;extra02;yes;0.5594
unsolved.smt2;UF;extra02;yes;0.6376
base01.smt2;UF;extra03;yes;1.427
base02.smt2;UF;extra03;yes;1.277
base03.smt2;UF;extra03;yes;1.89
base04.smt2;UF;extra03;yes;1.647
base05.smt2;UF;extra03;yes;1.652
base06.smt2;UF;extra03;yes;1.632
base07.smt2;UF;extra03;yes;1.607
base08.smt2;UF;extra03;yes;1.542
base09.smt2;UF;extra03;yes;1.352
base10.smt2;UF;extra03;yes;1.546
base11.smt2;UF;extra03;yes;1.19
base12.smt2;UF;extra03;yes;1.377
base13.smt2;UF;extra03;yes;1.399
base14.smt2;UF;extra03;yes;1.611
base15.smt2;UF;extra03;yes;1.566
base16.smt2;UF;extra03;yes;1.275
base17.smt2;UF;extra03;yes;1.418
base18.smt2;UF;extra03;yes;1.629
base19.smt2;UF;extra03;yes;1.422
base20.smt2;UF;extra03;yes;1.512
extra03_01.smt2;UF;extra03;yes;0.4896
extra03_02.smt2;UF;extra03;yes;0.3624
extra03_03.smt2;UF;extra03;yes;0.4418
unsolved.smt2;UF;extra03;yes;0.5025
base01.smt2;UF;extra04;yes;1.746
base02.smt2;UF;extra04;yes;1.486
base03.smt2;UF;extra04;yes;1.556
base04.smt2;UF;extra04;yes;1.827
base05.smt2;UF;extra04;yes;1.32
base06.smt2;UF;extra04;yes;1.391
base07.smt2;UF;extra04;yes;1.045
base08.smt2;UF;extra04;yes;1.594
base09.smt2;UF;extra04;yes;1.513
base10.smt2;UF;extra04;yes;1.623
base11.smt2;UF;extra04;yes;1.429
base12.smt2;UF;extra04;yes;1.699
base13.smt2;UF;extra04;yes;1.477
base14.smt2;UF;extra04;yes;1.699
base15.smt2;UF;extra04;yes;1.498
base16.smt2;UF;extra04;yes;1.899
base17.smt2;UF;extra04;yes;1.625
base18.smt2;UF;extra04;yes;1.817
base19.smt2;UF;extra04;yes;1.475
base20.smt2;UF;extra04;yes;1.502
extra04_01.smt2;UF;extra04;yes;0.1238
extra04_02.smt2;UF;extra04;yes;0.4929
unsolved.smt2;UF;extra04;yes;0.3676
base01.smt2;UF;extra05;yes;1.608
base02.smt2;UF;extra05;yes;1.471
base03.smt2;UF;extra05;yes;1.303
base04.smt2;UF;extra05;yes;1.238
base05.smt2;UF;extra05;yes;1.126
base06.smt2;UF;extra05;yes;1.173
base07.smt2;UF;extra05;yes;1.491
base08.smt2;UF;extra05;yes;1.722
base09.smt2;UF;extra05;yes;1.883
base10.smt2;UF;extra05;yes;1.566
base11.smt2;UF;extra05;yes;1.217
base12.smt2;UF;extra05;yes;1.262
base13.smt2;UF;extra05;yes;1.353
base14.smt2;UF;extra05;yes;1.888
base15.smt2;UF;extra05;yes;1.422
base16.smt2;UF;extra05;yes;1.883
base17.smt2;UF;extra05;yes;1.795
base18.smt2;UF;extra05;yes;1.471
base19.smt2;UF;extra05;yes;1.988
base20.smt2;UF;extra05;yes;1.002
extra05_01.smt2;UF;extra05;yes;0.7602
unsolved.smt2;UF;extra05;yes;1.014
base01.smt2;UF;extra06;yes;1.489
base02.smt2;UF;extra06;yes;1.151
base03.smt2;UF;extra06;yes;1.517
base04.smt2;UF;extra06;yes;1.341
base05.smt2;UF;extra06;yes;1.74
base06.smt2;UF;extra06;yes;1.47
base07.smt2;UF;extra06;yes;1.516
base08.smt2;UF;extra06;yes;1.575
base09.smt2;UF;extra06;yes;1.483
base10.smt2;UF;extra06;yes;1.539
base11.smt2;UF;extra06;yes;1.339
base12.smt2;UF;extra06;yes;1.731
base13.smt2;UF;extra06;yes;1.576
base14.smt2;UF;extra06;yes;1.346
base15.smt2;UF;extra06;yes;1.575
base16.smt2;UF;extra06;yes;1.71
base17.smt2;UF;extra06;yes;1.261
base18.smt2;UF;extra06;yes;1.581
base19.smt2;UF;extra06;yes;1.534
base20.smt2;UF;extra06;yes;1.642
unsolved.smt2;UF;extra06;yes;0.4478
special01.smt2;UF;bad-strategy;yes;1.689
contrib/gen_example_data.py
+ 31
− 11
View file @ 2a424add
#!/usr/bin/env python3
""" This script generates example data in a CSV file as used by the tutorial.
It might enerate invalid data, i.e., negative solving time. """
# This script generates example data in a CSV file as used by the tutorial.
import csv
import random
......@@ -13,36 +12,39 @@ with open("example_data.csv", "w") as example:
writer.writeheader()
base_names = list(map(lambda x: f"base{x:02}.smt2", range(1, 20+1)))
for name in base_names:
time = f"{abs(random.gauss(0.5, 0.2)):.4}"
time = "0.5"
writer.writerow(
{
"benchmark": name,
"logic": "UF",
"strategy": "base-strategy",
"solved": "yes",
"time": time,
"time": f"{abs(random.gauss(0.5, 0.2)):.4}"
}
)
writer.writerow(
{
"benchmark": "unsolved.smt2",
"logic": "UF",
"strategy": "base-strategy",
"solved": "no",
"time": f"{abs(random.gauss(0.5, 0.2)):.4}",
}
)
for i in range(1, 7):
print(i)
strategy_name = f"extra{i:02}"
for name in base_names:
time = f"{abs(random.gauss(1.5, 0.2)):.4}"
time = "1.5"
writer.writerow(
{
"benchmark": name,
"logic": "UF",
"strategy": strategy_name,
"solved": "yes",
"time": time,
"time": f"{abs(random.gauss(1.5, 0.2)):.4}",
}
)
for j in range(1, 7 - i):
time = f"{abs(random.gauss(0.5, 0.2)):.4}"
time = "0.5"
benchmark_name = f"extra{i:02}_{j:02}.smt2"
writer.writerow(
{
......@@ -50,6 +52,24 @@ with open("example_data.csv", "w") as example:
"logic": "UF",
"strategy": strategy_name,
"solved": "yes",
"time": time,
"time": f"{abs(random.gauss(0.5, 0.2)):.4}",
}
)
writer.writerow(
{
"benchmark": "unsolved.smt2",
"logic": "UF",
"strategy": strategy_name,
"solved": "yes",
"time": f"{abs(random.gauss(0.5, 0.2)):.4}",
}
)
writer.writerow(
{
"benchmark": "special01.smt2",
"logic": "UF",
"strategy": "bad-strategy",
"solved": "yes",
"time": f"{abs(random.gauss(1.5, 0.2)):.4}",
}
)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment