From 252af97897a61e5b3a1820853f694dca41a06240 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 25 Nov 2018 14:47:21 +0000 Subject: [PATCH] Benchmarking --- drs_benchmark.sh | 71 ++++++++++++++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 30 deletions(-) diff --git a/drs_benchmark.sh b/drs_benchmark.sh index 87760d6..a925c62 100755 --- a/drs_benchmark.sh +++ b/drs_benchmark.sh @@ -5,51 +5,62 @@ 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 - done=0 + eval formulae=\$form_${benchmark} - for i in `seq 2 20`;do + for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do - if [[ $done -eq 1 ]];then - echo "Skipping f=$f i=$i for $opt" - continue - fi + for f in $formulae; do - echo "[i] n=$i; generating input file" - in/scripts/gen_tgc_sc.py $i > $TMPINPUT + done=0 - echo "[i] Testing formula f$f" + for i in `seq 2 20`;do - if [[ "$opt" = "" ]];then - opt_str="NoOpt" - CMDOPT="" - else - opt_str="$opt" - CMDOPT="-$opt" - fi + if [[ $done -eq 1 ]];then + echo "Skipping f=$f i=$i for $opt" + continue + fi - TMPCMD="$CMD $CMDOPT -c f$f $TMPINPUT" - echo "[i] running reactics: $TMPCMD" + echo "[i] n=$i; generating input file (${benchmark})" + in/scripts/gen_${benchmark}.py $i > $TMPINPUT - res=$(timeout $timelimit $TMPCMD | grep STAT) - if [[ $? -ne 0 ]];then - done=1 - fi - mem=$(echo $res | cut -d';' -f 5) - time=$(echo $res | cut -d';' -f 6) + echo "[i] Testing formula f$f" - echo "[.] Finished. time:$time, mem:$mem" + if [[ "$opt" = "" ]];then + opt_str="NoOpt" + CMDOPT="" + else + opt_str="$opt" + CMDOPT="-$opt" + fi - echo "$i $time $mem" >> bench_drs_tgc_${opt_str}_f$f.dat + TMPCMD="$CMD $CMDOPT -c f$f $TMPINPUT" + echo "[i] running reactics: $TMPCMD" + 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_${benchmark}_${opt_str}_f$f.dat + + done + + echo + done - echo - done done