benchmarks: Distribute results over different directories

Allows benchmarks of two formula series to be performed in parallel
without interfering with each other.

benchmarks/aconjunctive_mu/bench_one_formula.sh

@@ -47,7 +47,9 @@ FORMULA=$1
 COOL_LOGIC=$2
 MLSOLVER_LOGIC=$3
 
-mkdir -p "${OUTPUT_BASE}"
+OUTPUT_DIR="${OUTPUT_BASE}/${FORMULA}/"
+
+mkdir -p "${OUTPUT_DIR}"
 
 echo "# ${FORMULA}:"
 
@@ -56,14 +58,14 @@ function bench {
 
     echo -n "  - ${FORMULA}-${1}: "
 
-    while timeout ${TIMEOUT} perf stat -o "${OUTPUT_BASE}/tmp.time" -r ${REPEATS} "$2" "$3" "$i" "${@:4}" > "${OUTPUT_BASE}/tmp.out" 2>&1; do
-	mv "${OUTPUT_BASE}/tmp.time" "${OUTPUT_BASE}/${FORMULA}-${i}-${1}.time";
-	mv "${OUTPUT_BASE}/tmp.out" "${OUTPUT_BASE}/${FORMULA}-${i}-${1}.out";
+    while timeout ${TIMEOUT} perf stat -o "${OUTPUT_DIR}/tmp.time" -r ${REPEATS} "$2" "$3" "$i" "${@:4}" > "${OUTPUT_DIR}/tmp.out" 2>&1; do
+	mv "${OUTPUT_DIR}/tmp.time" "${OUTPUT_DIR}/${FORMULA}-${i}-${1}.time";
+	mv "${OUTPUT_DIR}/tmp.out" "${OUTPUT_DIR}/${FORMULA}-${i}-${1}.out";
 	i=$(($i+1))
 	echo -n "."
     done
     
-    rm "${OUTPUT_BASE}/tmp."{time,out}
+    rm "${OUTPUT_DIR}/tmp."{time,out}
     echo ""
 }
 

benchmarks/aconjunctive_mu/collect_output.pl

@@ -10,8 +10,9 @@ use File::Basename;
 
 print "family; index; variant; time (seconds); stddev (percent); result; states\n";
 
-foreach my $timefile (<*.time>) {
+foreach my $timefile (<*/*.time>) {
     my $base = basename($timefile, ".time");
+    my $outfile = $timefile =~ s/time$/out/r;
 
     my ($family, $index, $variant);
 
@@ -33,7 +34,7 @@ foreach my $timefile (<*.time>) {
 
     my ($result, $states, $cores);
 
-    open (FILE, '<', "$base.out") or die;
+    open (FILE, '<', "$outfile") or die;
     while (<FILE>) {
 	if (/Query is not satisfiable/ or /Formula is unsatisfiable/) {
 	    $result = "unsat";