Parametric benchmark management

[gaperez64]

Most action seems to be shifting to TLSF benchmarks. I spent a bit of time automating the benchmark-selection process using (Python) scripts @swenjacobs, @5nizza. The main idea is as follows:

• Benchmark-family directories where the names followed conventions such as file_N.tlsf or file_unreal_N_U.tlsf now have a subdirectory named `parametric' where two files are included. First, a tlsf template with a minimal value of N set and no tags. Second, a CSV containing values of all parameters (eg. N) and tag values for the file obtained by setting the parameters to the corresponding values.
• The original concrete benchmarks disappeared now, only for families that are not parameterized in their TLSF files did I leave files with different numbers.
• To change how many instances we get per family we only need to tweak the CSV files now!
• I have added all families to the current selection script `selectBenchmarks.py' and played with the CSV files to make sure not all instances of every family can be solved (I based this on the results from last year's SYNTCOMP) and so that we do not have too many instances no-one is able to solve (this was the case for unrealizable instances).

If you agree with the changes, we merge this into the main branch and keep that structure for TLSF benchmarks from now on. Then, I will take the current selection and launch the jobs for SYNTCOMP 2021.

[5nizza]

Just a note: the following folders contain parameterized benchmarks (either you missed them or intentionally left out):

• the folder tlsf/lift contains three specs, all are parameterized
• the folder tlsf/arbiters_zoo contains 4 more specs, each is parameterized
• the folder arbiters_s4 contain several benchmarks, all are parameterized
• the folder amba contains one parameterized benchmark

[gaperez64]

Ah yes, I missed those. Essentially, I had a script that diff'd files and if I found two that were identical except for the value of a parameter I placed that on the "to parameterize" list. While the ones you mention are indeed parametric, there was only a copy of them in the repo so I did not see them. How about we add this as a TODO for next year :D ?

As a side note, the choice of benchmark families is already visible here (everything non-parametric and all the parametric instances from the csv files in each benchdir will be included). This means that if arbiter_zoo/arbiter.tlsf and full_arbiter are merged this will work as well next year (but at the moment, even if the benchmarks are very similar, they will both be included).

[5nizza]

Those parameterized benchmarks seemed good to me (lift is hard, arbiters_zoo are hard), so it is a bit sad they will be missed this year, but OK, it is not crucial.