Seventeen provers under the hammer
, Martin, Petar Vukmirović, Jasmin Jasmin, Makarius Wenzel · Zenodo (CERN European Organization for Nuclear Research) · 2022
This archive contains used benchmarks, raw results, scripts to create tables from the paper and the provers used for all experiments in the the paper Seventeen provers under the hammer. The benchmarks used in the experiments are separated by the table in which they are used: Table Archive 4 baseline_probs.zip 6 max_facts_probs.zip 7 lam_trans_probs.zip 8 poly_enc_probs.zip 9 mono_enc_probs.zip Note that there are 5000 benchmarks in each subclass of benchmarks. Due to some technical issues we had to make sure our result collection scripts ignored classes of 100 benchmarks. Which benchmarks are ignored is specified below. Similarly, the raw results are separated by the benchmarks they are evaluated on Benchmarks Results baseline_probs.zip baseline_res.zip max_facts_probs.zip max_facts_res.zip lam_trans_probs.zip lam_trans_res.zip mono_enc_probs.zip mono_enc_res.zip poly_enc_probs.zip poly_enc_res.zip The archives with results further contain raw results obtained from our evaluation environment, StarExec. These files contain .csv files in which each row describes one run of a prover on one benchmark and contains information such as the used CPU time and memory resources, if the prover solved the problem and path to the benchmark. To create the tables used in paper from the raw results, extract all archives ending with _res in a directory (let's label it ) and extract contents of table_scripts.zip in a directory labelled . Then, use the following commands to create the tables: Table Generation command 4 python3 /get_table.py /baseline /baseline.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 5 python3 /get_table.py /running_time.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 --no-column-best --no-row-best 6 python3 /get_table.py /max_facts.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 7 python3 /get_table.py /lam_trans.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 8 python3 /get_table.py /poly_enc.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 9 python3 /get_table.py /mono_enc.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 10 python3 /get_greedy_seq.py /greedy.json --ignore-benchmarks Cauchy_00 Cauchy/00 LTL_to_GBA_00 LTL_to_GBA/00 --max-configurations 16 All provers, except for ENIGMA (which has several gigabyte installation) are stored in provers.zip. Note that due to library dependencies, and that they are packaged in StarExec-specific way, the best way to install them is by reuploading them to StarExec. ENIGMA is available at this link.