[SMT-COMP] Instruction to reproduce Unsat-core Track results

[Matthias Heizmann]

Dear SMT-COMP participants,

Please find attached instructions that should help you to reproduce the results 
of the Unsat-core Track more easily.

Best,
Matthias
-------------- next part --------------
// These are instruction that should help you to 
// reproduce Unsat-core Track results of SMT-COMP 2018
// 2018-07-10 Matthias Heizmann (heizmann at informatik.uni-freiburg.de)


// Step 1. Download the benchmark for which you want to reproduce the result.
// Option A: download the benchmark from StarExec
// https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=303893
// Option B: download the benchmark from the SMT-LIB repository.
// Note that the SMT-LIB repository might be changed over time whereas on
// StarExec we store exactly the benchmarks that were used in 2018.
wget https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_UFBV/raw/master/2018-Goel-hwbench/QF_UFBV_bv8_bv_fischer.1.prop1_ab_reg_max.smt2


// Step 2. Get the benchmark scrambler
// Since the Unsat-core Track used a slightly more recent version of the 
// scrambler as the other tools, we download the post-processor.
wget http://smtcomp.sourceforge.net/2018/SMT-COMP-2018-Unsat-Core-Track-Postprocessor.tgz
tar xf SMT-COMP-2018-Unsat-Core-Track-Postprocessor.tgz


// Step 3. Mimic the Unsat-core Track pre-processor
// Produce the solver input SMT script. 
// I.e., scramble, assert named terms, append get-unsat-core command
// Note that all three tasks are performed by the tool whose name is "scrambler"
/scrambler -seed 773027284 -generate_unsat_core_benchmark true < QF_UFBV_bv8_bv_fischer.1.prop1_ab_reg_max.smt2  > solverInput.smt2


// Step 4. Let your solver produce an unsatisfiable core
// Apply your solver to the just produced script solverInput.smt2 and 
// write the output to solverOutput.txt
mySolver solverInput.smt2 > solverOutput.txt


// Step 5. Mimic the generation of the validation script (first part of post-processing)
// Produce a copy of the input SMT script that asserts only the terms 
// that are in the unsatisfiable core of your solver
/scrambler -seed 0 -term_annot false -core ./solverOutput.txt < ./solverInput.smt2 > ./unsat-core-validation-script.smt2


// Step 6. Validate the unsatisfiable core (second part of post-processing)
// The "validationSolvers" folder in the post-processor contains the four 
// solvers that participated in the Main Track. We use the StarExec 
// configuration script to invoke them.
// First we make sure that the folder of the configuration script is 
// our working directory, then we run the solver on the validation script
// We repeat this step for each validation solver.
cd validationSolvers/myFavoriteValidationSolver/bin
/starexec_run_default ../../../unsat-core-validation-script.smt2
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part.
URL: </pipermail/smt-comp/attachments/20180712/b9d5a25d/attachment.asc>