From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 10 Sep 2020 21:08:02 +0000 (-0700)
Subject: Dirk end to end analysis
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=inline;p=Benchmarks_CSolver.git
Dirk end to end analysis
---
diff --git a/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tuner b/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tuner
new file mode 100644
index 00000000..1a15e009
--- /dev/null
+++ b/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tuner
@@ -0,0 +1,13 @@
+0 0 0 6 0 1 1 1
+0 0 0 0 0 1 1 1
+0 0 0 1 0 1 1 1
+0 0 0 2 0 1 1 1
+0 0 0 3 0 1 1 1
+0 0 0 9 0 1 1 1
+0 0 0 5 0 1 0 0
+0 0 0 10 0 1 1 1
+0 0 0 12 0 1 1 1
+0 0 0 11 0 1 0 1
+0 0 0 16 0 2 2 2
+0 0 0 4 0 1 1 1
+0 0 0 13 1 5 2 2
diff --git a/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tunerused b/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tunerused
new file mode 100644
index 00000000..1a15e009
--- /dev/null
+++ b/dirk-new/endtoendeval/best-dirk-new-set0-bbuferwriter-best0.tunerused
@@ -0,0 +1,13 @@
+0 0 0 6 0 1 1 1
+0 0 0 0 0 1 1 1
+0 0 0 1 0 1 1 1
+0 0 0 2 0 1 1 1
+0 0 0 3 0 1 1 1
+0 0 0 9 0 1 1 1
+0 0 0 5 0 1 0 0
+0 0 0 10 0 1 1 1
+0 0 0 12 0 1 1 1
+0 0 0 11 0 1 0 1
+0 0 0 16 0 2 2 2
+0 0 0 4 0 1 1 1
+0 0 0 13 1 5 2 2
diff --git a/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tuner b/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tuner
new file mode 100644
index 00000000..8a0057fe
--- /dev/null
+++ b/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tuner
@@ -0,0 +1,25 @@
+0 0 0 15 1 3 3 3
+0 0 0 5 0 1 0 1
+0 0 0 6 0 1 1 1
+0 0 0 0 0 1 1 1
+0 0 0 10 0 1 1 1
+0 0 0 12 0 1 1 1
+0 0 0 11 0 1 1 1
+1 0 0 7 0 3 0 0
+1 1 0 7 0 3 0 0
+1 2 0 7 0 3 0 0
+0 0 0 16 0 2 2 2
+0 0 0 13 1 5 2 2
+1 0 0 1 0 1 1 1
+1 1 0 1 0 1 1 1
+1 2 0 1 0 1 1 1
+1 0 0 2 0 1 1 1
+1 1 0 2 0 1 1 1
+1 2 0 2 0 1 1 1
+1 0 0 3 0 1 1 1
+1 1 0 3 0 1 1 1
+1 2 0 3 0 1 1 1
+1 0 0 9 0 1 1 1
+1 1 0 9 0 1 1 1
+1 2 0 9 0 1 1 1
+0 0 0 4 0 1 1 1
diff --git a/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tunerused b/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tunerused
new file mode 100644
index 00000000..8a0057fe
--- /dev/null
+++ b/dirk-new/endtoendeval/best-dirk-new-set1-bbuffer-best0.tunerused
@@ -0,0 +1,25 @@
+0 0 0 15 1 3 3 3
+0 0 0 5 0 1 0 1
+0 0 0 6 0 1 1 1
+0 0 0 0 0 1 1 1
+0 0 0 10 0 1 1 1
+0 0 0 12 0 1 1 1
+0 0 0 11 0 1 1 1
+1 0 0 7 0 3 0 0
+1 1 0 7 0 3 0 0
+1 2 0 7 0 3 0 0
+0 0 0 16 0 2 2 2
+0 0 0 13 1 5 2 2
+1 0 0 1 0 1 1 1
+1 1 0 1 0 1 1 1
+1 2 0 1 0 1 1 1
+1 0 0 2 0 1 1 1
+1 1 0 2 0 1 1 1
+1 2 0 2 0 1 1 1
+1 0 0 3 0 1 1 1
+1 1 0 3 0 1 1 1
+1 2 0 3 0 1 1 1
+1 0 0 9 0 1 1 1
+1 1 0 9 0 1 1 1
+1 2 0 9 0 1 1 1
+0 0 0 4 0 1 1 1
diff --git a/dirk-new/endtoendeval/rundump.sh b/dirk-new/endtoendeval/rundump.sh
new file mode 100755
index 00000000..85c8a516
--- /dev/null
+++ b/dirk-new/endtoendeval/rundump.sh
@@ -0,0 +1,44 @@
+#!/bin/bash
+# run as the following:
+# ./runbench.sh [hexiom] [timeout] [tuner.conf]
+# ./runbench.sh [nqueens] [timeout] [tuner.conf]
+# ./runbench.sh [sudoku-csolver] [timeout] [tuner.conf]
+# ./runbench.sh [killerSudoku] [timeout] [tuner.conf]
+
+if [ "$#" -lt 1 ]; then
+ echo "Illegal number of argument"
+ echo "./runbench.sh [tuner.conf] [benchmark]"
+ exit 1
+fi
+
+SATUNE=/scratch/hamed/constraint_compiler/src
+BIN=$SATUNE/bin
+export CLASSPATH=$BIN/original.jar:$SATUNE:$CLASSPATH
+export LD_LIBRARY_PATH=$BIN
+# For Mac OSX
+export DYLD_LIBRARY_PATH=$BIN
+# For sat_solver
+export PATH=$SATUNE:$PATH
+
+
+maxtime=1800
+DUMPDIR=/scratch/hamed/end-to-end/dirk-new/dumps/
+cd $DUMPDIR
+
+DUMP=$(find . -name "*.dump")
+cd ..
+for d in $DUMP; do
+ if [[ $d = *$2* ]]; then
+ echo "Running: ./run.sh tunerrun "$DUMPDIR"$d $maxtime $1 out.out"
+ timeout $maxtime $BIN/tunerrun "$DUMPDIR"$d $maxtime $1 out.out
+ RETCODE=$?
+ echo "Return code: $RETCODE"
+ if [ $RETCODE -eq 141 ]; then #Dump info when SAT Solver gets killed by OS ....
+ echo "Satune got out of memory"
+ echo "deserializing $d ..."
+ echo "SAT Solving time: 400000000.0"
+ echo "CSOLVER solve time: 400000000.0"
+ fi
+ echo "Best tuner"
+ fi
+done
diff --git a/dirk-new/endtoendeval/satunetimecomputer.py b/dirk-new/endtoendeval/satunetimecomputer.py
new file mode 100644
index 00000000..3089e599
--- /dev/null
+++ b/dirk-new/endtoendeval/satunetimecomputer.py
@@ -0,0 +1,45 @@
+import os
+import sys
+import random
+import re
+
+import os
+
+
+myfile = ''
+
+def validateArgs():
+ global myfile;
+ if len(sys.argv) != 2:
+ print("Wrong argument! Usage: python satunetimecomputer.py satune_trace.log");
+ sys.exit(-1);
+ else:
+ myfile = sys.argv[1];
+
+
+def analyzeExecution():
+ solving=0;
+ total=0;
+ print(myfile);
+ with open(myfile, "r") as f:
+ line = f.readline()
+ while line:
+ if 'SAT Solving time' in line:
+ time =re.findall("\d+\.\d+", line)
+ solving = solving + float(time[0]);
+ elif 'CSOLVER solve time' in line:
+ time =re.findall("\d+\.\d+", line);
+ total = total + float(time[0]);
+
+ line = f.readline()
+
+ print("Total SAT Solving Time: " + str(solving));
+ print("Total SATTune Time: " + str(total));
+
+def main():
+ validateArgs();
+ analyzeExecution();
+
+if __name__ == "__main__":
+ main();
+