Fix issue when use script to run experiment for dsolve

README.md

@@ -91,9 +91,8 @@ python3 table.py comp_tools/unv > table.out
 ```
 The result will be stored in a `table.out` file.
 
-### Generate Tables for POPL paper:
+### Generate Tables for POPL 2021 paper:
 Inside the `scipts` folder, there is a script `benchs_popl21.sh` to run all experiments.
 ```bash
 ./benchs_popl21.sh
 ```
-TODO: For dsolve, you cannot run it under any other relative paths. Please run it under its own directory.

scripts/dsolve_runit.sh

@@ -1,10 +1,14 @@
 #!/bin/bash
 
 PROGDIR="../../dsolve" # Change directory here if you built it in another place
-
+DRIFTDIR="../drift"
+echo "Assume dsolve is built under relative path ../../dsolve"
+cp -a ../tests/benchmarks ${PROGDIR}/tests
+cp dsolve_table.py ${PROGDIR}
+pushd ${PROGDIR}
 # ./dsolve_runit.sh -set call/unv
-OUTDIR="../outputs/dsolve"
-PROG="./${PROGDIR}/dsolve.py"
+OUTDIR="outputs/dsolve"
+PROG="./dsolve.py"
 ARRAYSET="DRIFT"
 SET=$2
 echo "outdir=<$OUTDIR> prog=<$PROG>"
@@ -15,9 +19,9 @@ timeout="300"
 OUTPRE="out"
 
 if [ $SET = "call" ]; then
-    TESTDIR="../tests/benchmarks_call"
+    TESTDIR="tests/benchmarks_call"
 else
-    TESTDIR="../tests/benchmarks"
+    TESTDIR="tests/benchmarks"
 fi
 
 for dir in ${INS}; do
@@ -35,7 +39,10 @@ for hdir in ${DIRS}; do
             if [ ${dir} = "array" ] && [ ${hdir} != ${ARRAYSET} ]; then
                 continue
             fi 
-            for f in `find ${TESTDIR}/${hdir}/${dir} ! -iname "*annot*" -and ! -iname "*quals*" -and ! -iname ".DS_Store" -type f -execdir echo '{}' ';'`; do
+            for f in `find ${TESTDIR}/${hdir}/${dir} ! -iname "*annot*" -and ! -iname "*quals*" -and \
+                ! -iname ".DS_Store" -and ! -iname "*.json" -and ! -iname "*.status" -and ! -iname "*.horsat_out" \
+                -and ! -iname "*.hors" -and ! -iname "*.smt2" \
+                -type f -execdir echo '{}' ';'`; do
                 b=${f#*./}
                 ts=$(date +%s%N)
                     echo "${PROG} -v 0 ${TESTDIR}/${hdir}/${dir}/${b}"
@@ -54,4 +61,6 @@ done
 echo "Gnerate dsolve table results..."
 python3 dsolve_table.py  
 
-mv res-dsolve.csv ../result/comp_tools/unv
+mv res-dsolve.csv ${DRIFTDIR}/result/comp_tools/unv
+
+popd

scripts/dsolve_table.py

@@ -7,7 +7,7 @@
 import re
 import csv
 
-testdir = '../outputs/dsolve'
+testdir = 'outputs/dsolve'
 table_file = 'res-dsolve.csv'
 pattern = re.compile(".*ml$")
 attrs = ['subdir', 'file name', 'test class', 'timing (seconds)', 'res (true/false)']