Benchmarking

drs_benchmark.sh

@@ -5,10 +5,18 @@ TMPINPUT="tmp_$RANDOM$RANDOM.rs"
 CMD="./reactics -B"
 
 timelimit="$((30*60))" # 30 minutes
+timelimit="$((5*60))" # 5 minutes
 
-for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
+form_tgc_sc="`seq 1 3`"
+form_asm="`seq 1 2`"
 
-    for f in `seq 1 3`; do
+for benchmark in "tgc_sc" "asm"; do
+
+    eval formulae=\$form_${benchmark}
+
+    for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
+
+        for f in $formulae; do
 
             done=0
 
@@ -19,8 +27,8 @@ for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
                     continue
                 fi
 
-            echo "[i] n=$i; generating input file"
-            in/scripts/gen_tgc_sc.py $i > $TMPINPUT
+                echo "[i] n=$i; generating input file (${benchmark})"
+                in/scripts/gen_${benchmark}.py $i > $TMPINPUT
 
                 echo "[i] Testing formula f$f"
 
@@ -38,13 +46,14 @@ for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
                 res=$(timeout $timelimit $TMPCMD | grep STAT)
                 if [[ $? -ne 0 ]];then
                     done=1
+                    continue
                 fi
                 mem=$(echo $res | cut -d';' -f 5)
                 time=$(echo $res | cut -d';' -f 6)
 
                 echo "[.] Finished. time:$time, mem:$mem"
 
-            echo "$i $time $mem" >> bench_drs_tgc_${opt_str}_f$f.dat
+                echo "$i $time $mem" >> bench_drs_${benchmark}_${opt_str}_f$f.dat
 
             done
 
@@ -52,6 +61,8 @@ for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
             
         done
 
+    done
+
 done
 
 rm -f $TMPINPUT