add scripts to produce smtlib brenchmarks
ADD
scripts/filter-bench.php
+<?php
+
+// filter out benchmarks:
+// 1) remove duplicated files
+// 2) remove files that use lambdas (non-smtlib compliant)
+// 3) remove trivial benchmarks
+
+$files = glob('bench_*/*.smt2');
+$hashes = [];
+
+foreach ($files as $f) {
+ $hash = md5_file($f);
+ if (isset($hashes[$hash])) {
+ //echo "remove dup file $f\n";
+ unlink($f);
+ continue;
+ }
+ $hashes[$hash] = $f;
+}
+
+foreach ($hashes as $h => $f) {
+ if (`grep -c '(lambda' $f` > 0) {
+ //echo "remove file with lambdas $f\n";
+ unlink($f);
+ continue;
+ }
+
+ $z3 = `z3 -T:1 $f 2>&1`;
+ if ($z3 == "sat\n" || $z3 == "unsat\n") {
+ //echo "remove trivial file $f\n";
+ unlink($f);
+ } else if ($z3 != "timeout\n" &&
+ $z3 != "unknown\n" &&
+ $z3 != "unknown\ntimeout\n") {
+ echo "CRASH: $f\n$z3\n\n";
+ }
+}

ADD
scripts/pick-random-bench.php
+<?php
+
+// pick x benchmarks randomly
+$dstdir = 'alive2_bench';
+
+if ($argc !== 2)
+ die("Usage: php $argv[0] <num bench>\n");
+
+$files = glob('bench_*/*.smt2');
+
+`mkdir -p $dstdir`;
+
+$i = 0;
+foreach (array_rand($files, $argv[1]) as $n) {
+ $f = $files[$n];
+ $dst = preg_replace('@bench_(.*)/.*\.smt2@S',
+ "$dstdir/" . str_pad($i++, 3, '0', STR_PAD_LEFT) .
+ "_\\1.smt2", $f);
+ copy($f, $dst);
+}
+
+`tar c $dstdir | xz -9 -e -T0 > $dstdir.tar.xz`;

add scripts to produce smtlib brenchmarks