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

Add example data and example data generator. 

The data will be used in the HOWTO/tutorial.  It might not yet
be appropiate, and hence change in the future.
parent f6435925
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
contrib/example_data.csv 0 → 100644
+ 156
− 0
View file @ 5a2c5a8f
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
contrib/gen_example_data.py 0 → 100755
+ 55
− 0
View file @ 5a2c5a8f
#!/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. """
import csv
import random
with open("example_data.csv", "w") as example:
writer = csv.DictWriter(
example, ["benchmark", "logic", "strategy", "solved", "time"], delimiter=";"
)
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,
}
)
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,
}
)
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(
{
"benchmark": benchmark_name,
"logic": "UF",
"strategy": strategy_name,
"solved": "yes",
"time": time,
}
)
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