Merging + fixing memory bugs
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 5 Sep 2019 23:01:44 +0000 (16:01 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 5 Sep 2019 23:01:44 +0000 (16:01 -0700)
22 files changed:
deploy-cs.sh
src/Backend/satelemencoder.cc
src/SatuneJavaAPI.java
src/Scripts/autotunerparser.py [new file with mode: 0644]
src/Scripts/learnresultgen.sh [new file with mode: 0755]
src/Scripts/remotelearning.py [new file with mode: 0644]
src/Scripts/runbench.sh [new file with mode: 0755]
src/Scripts/runinterpreter.sh [new file with mode: 0755]
src/Scripts/serverstatus.py [new file with mode: 0644]
src/Test/analyzemultituner.cc
src/Test/dirkreader.cc
src/autotunerparser.py [deleted file]
src/ccsolver.cc
src/ccsolver.h
src/common.cc
src/csolver.cc
src/csolver.h
src/pycsolver.py
src/runbench.sh [deleted file]
src/runinterpreter.sh [deleted file]
src/satune_SatuneJavaAPI.cc
src/satune_SatuneJavaAPI.h

index 2f41b32..6eafd06 100755 (executable)
@@ -5,13 +5,14 @@ set -e
 
 BASE=../
 SERVERS="dc-4.calit2.uci.edu dc-5.calit2.uci.edu dc-6.calit2.uci.edu dc-7.calit2.uci.edu dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
+#SERVERS="dc-1.calit2.uci.edu dc-2.calit2.uci.edu dc-3.calit2.uci.edu"
 REMOTEDIR="/scratch/hamed/"
 INFILE="constraint_compiler/"
 SRC="constraint_compiler/src/"
 SHAREDDIR=~/
 OUTFILE=csolver.tar.gz
 USER=hamed
-
+BIN=${REMOTEDIR}${SRC}/bin
 cd $BASE
 
 rm -f $OUTFILE
@@ -19,5 +20,5 @@ tar -czvf $OUTFILE $INFILE
 
 cp $OUTFILE $SHAREDDIR
 for SERVER in $SERVERS; do
-       ssh $USER@$SERVER "cp $SHAREDDIR$OUTFILE $REMOTEDIR; cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
+       ssh $USER@$SERVER "cp $SHAREDDIR$OUTFILE $REMOTEDIR; cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh; find -iname csolver -exec rm '{}' \; -exec ln -s $BIN '{}' \;"
 done
index b380c3a..7687f35 100644 (file)
@@ -227,6 +227,15 @@ void SATEncoder::freezeElementVariables(ElementEncoding *encoding) {
                ASSERT(edgeIsVarConst(e));
                freezeVariable(cnf, e);
        }
+       for(uint i=0; i< encoding->encArraySize; i++){
+               if(encoding->isinUseElement(i) && encoding->encoding != EENC_NONE && encoding->numVars > 1){
+                       Edge e = encoding->edgeArray[i];
+                       if(!edgeIsNull(e)){
+                               ASSERT(edgeIsVarConst(e));
+                               freezeVariable(cnf, e);
+                       }
+               }
+       }
 }
 
 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
@@ -294,6 +303,9 @@ void SATEncoder::generateElementEncoding(Element *element) {
 }
 
 int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+       if(encoding->encArraySize == 1){
+               return 1;
+       }
        for (int i = encoding->encArraySize - 1; i >= 0; i--) {
                if (encoding->isinUseElement(i))
                        return i + 1;
index 2b6baea..a5e71d3 100644 (file)
@@ -43,6 +43,10 @@ public class SatuneJavaAPI{
             printConstraints(satune);
         }
        
+        public void turnoffOptimizations(){
+            turnoffOptimizations(satune);
+        }
+       
         public int solve(){
             return solve(satune);
         }
@@ -81,6 +85,7 @@ public class SatuneJavaAPI{
        private native int getBooleanValue(long solver,long bool);
        private native int getOrderConstraintValue(long solver,long order, long first, long second);
        private native void printConstraints(long solver);
+       private native void turnoffOptimizations(long solver);
        private native void serialize(long solver);
        private native void mustHaveValue(long solver, long element);
        private native void setInterpreter(long solver, int type);
diff --git a/src/Scripts/autotunerparser.py b/src/Scripts/autotunerparser.py
new file mode 100644 (file)
index 0000000..618fcd6
--- /dev/null
@@ -0,0 +1,97 @@
+import re
+import argparse
+import sys
+
+
+class AutoTunerArgParser:
+    def __init__(self):
+        self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...')
+        self.parser.add_argument('--file', '-f', metavar='out.log', type=str, nargs=1,help='output log of running the autotuner ...')
+        self.args = self.parser.parse_args()
+        
+    def getFileName(self):
+        return self.args.file[0]
+
+HEADER = ["TESTCASE", "SATTIME", "EXECTIME", "PREPROCESS", "ELEMENTOPT", "ELEMENTOPTSETS", "PROXYVARIABLE", "#SubGraph", "NODEENCODING", "EDGEENCODING", "NAIVEENCODER", "ENCODINGGRAPHOPT"]
+
+configs = {"EXECTIME": "-",
+               "SATTIME":"-",
+               "TESTCASE":"-",
+               "PREPROCESS" : "-",
+               "ELEMENTOPT" : "-",
+               "ELEMENTOPTSETS" : "-",
+               "PROXYVARIABLE" : "-",
+               "#SubGraph" : "-",
+               "NODEENCODING" : "-",
+               "EDGEENCODING" : "-",
+               "NAIVEENCODER" :"-",
+               "ENCODINGGRAPHOPT" : "-"
+               }
+
+REGEXES = {"EXECTIME": "CSOLVER solve time: (.*)",
+               "SATTIME":"SAT Solving time: (.*)",
+               "TESTCASE": "deserializing (.+) ...",
+               "PREPROCESS" : "Param PREPROCESS = (.*)range=\[0,1\]",
+               "ELEMENTOPT" : "Param ELEMENTOPT = (.*)range=\[0,1\]",
+               "ELEMENTOPTSETS" : "Param ELEMENTOPTSETS = (.*)range=\[0,1\]",
+               "PROXYVARIABLE" : "Param PROXYVARIABLE = (.*)range=\[1,5\]",
+               "#SubGraph" : "#SubGraph = (.*)",
+               "NODEENCODING" : "Param NODEENCODING = (.*)range=\[0,3\](.*)",
+               "EDGEENCODING" : "Param EDGEENCODING = (.*)range=\[0,2\](.*)",
+               "NAIVEENCODER" : "Param NAIVEENCODER = (.*)range=\[1,3\](.*)",
+               "ENCODINGGRAPHOPT" : "Param ENCODINGGRAPHOPT = (.*)range=\[0,1\]"
+               }
+def reorderEntry(entry):
+       global HEADER
+       result = []
+       for key in HEADER:
+               result.append(entry[key])
+       return result
+
+
+def printHeader(file):
+       global HEADER
+       mystr=""
+       for key in HEADER:
+                mystr+=key+","
+       print >>file, mystr
+       
+def printConfig(file, data):
+       print data
+       mystr=""
+       for val  in data:
+                mystr+=str(val)+","
+       print >> file, mystr
+
+
+def main():
+       global configs
+       argprocess = AutoTunerArgParser()
+       output = open("tuner.csv", "w")
+       printHeader(output)
+       result = []
+       with open(argprocess.getFileName()) as file:
+               for line in file:
+                       if line.startswith("Mutating"):
+                               result.append(reorderEntry(configs))
+                       elif line.startswith("Best tuner"):
+                               result.append(reorderEntry(configs))
+                       else :
+                               for regex in REGEXES:
+                                       p = re.compile(REGEXES[regex])
+                                       token = p.search(line)
+                                       if token is not None:
+                                               if regex == "TESTCASE":
+                                                       configs[regex] = re.search(REGEXES[regex], line).group(1)
+                                               else:
+                                                       configs[regex] = re.findall("\d+\.?\d*", line)[0]
+
+       #configs["EXECTIME"] = "BEST TUNE:"
+       result.append(reorderEntry(configs))
+       result.sort(key = lambda entry: entry[0])
+       for entry in result:
+               printConfig(output, entry)
+       print "Done with parsing " + argprocess.getFileName()
+
+if __name__ == "__main__":
+       main()
diff --git a/src/Scripts/learnresultgen.sh b/src/Scripts/learnresultgen.sh
new file mode 100755 (executable)
index 0000000..d34f090
--- /dev/null
@@ -0,0 +1,30 @@
+#!/bin/bash
+# ./learnresultgen.sh [sypet] [learning set = 1, 2, 3, etc.] [algorithm= 1, 2, 3, 4]
+set -e
+
+if [ "$#" -lt 3 ]; then
+        echo "Illegal number of argument"
+        echo "./learnresultgen.sh [sypet] [learning set = 0, 1, 2, 3, etc.] [algorithm = Known Tuner Types: Random Tuner=1, Comp Tuner=2, Kmeans Tuner=3, Simulated Annealing Tuner=4]"
+        exit 1
+fi
+
+SATUNEDIR=$PWD
+BENCHDIR=$SATUNEDIR/Benchmarks/$1
+BIN=$SATUNEDIR/bin
+
+source $SATUNEDIR/Benchmarks/common.sh
+cd $BENCHDIR
+./learn.sh $2 $3
+cd $BIN
+./run.sh analyzemultituner
+cd $SATUNEDIR
+TUNERS=$(find "$BIN" -name "*.tuner")
+for T in $TUNERS; do
+       TUNER=$(basename $T)
+       echo "Running tuner "$TUNER
+       ./Scripts/runbench.sh $1 $TIMEOUT $TUNER &> $BIN/$1"-set"$2"-"$TUNER".log"
+       python ./Scripts/autotunerparser.py -f $BIN/$1"-set"$2"-"$TUNER".log"
+       mv tuner.csv $1"-set"$2"-"$TUNER".csv"
+done
+
+mv ./bin ./"bin-"$1"-set"$2"-alg"$3
diff --git a/src/Scripts/remotelearning.py b/src/Scripts/remotelearning.py
new file mode 100644 (file)
index 0000000..dccee9c
--- /dev/null
@@ -0,0 +1,117 @@
+import re
+import argparse
+import sys
+from threading import Thread
+import subprocess
+import os
+
+# 1) Deploy on all the servers
+# 2) Based on the benchmark selection, run each learning set on a server
+# 3) After being done with that, it sshould calculate the first best 3
+# 4) Run them indivisually
+# 5) Generate the excel sheet!
+SRCDIR="/scratch/hamed/constraint_compiler/src"
+LOCALSRCDIR="/scratch/satcheck/satproject/constraint_compiler/src"
+class ArgParser:
+    def __init__(self):
+        self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...')
+        self.parser.add_argument('--bench', '-b', metavar='sudoku', type=str, nargs=1,help='Benchmark that you want to learn on')
+        self.args = self.parser.parse_args()
+        
+    def getBenchmarkName(self):
+        return self.args.bench[0]
+       
+def deploy():
+       os.system("cd ../; ./deploy-cs.sh")
+
+def getServerNeeded(benchmark):
+       variable = ""
+       with open("./Benchmarks/" + benchmark + "/learn.sh") as f:
+               line = f.readline()
+               while "declare -a LearningSet=" not in line:
+                       line = f.readline()
+               while ")" not in line:
+                       variable = variable + line
+                       line = f.readline()
+               variable = variable + line
+       return variable.count("\"")/2
+
+def getAvailableServerList(needed):
+       global SRCDIR
+       available = []
+       for i in range(4,12):
+               print ("Checking availability for server " + str(i))
+               HOST="dc-"+ str(i) + ".calit2.uci.edu"
+               COMMAND="cd "+SRCDIR+"; python ./Scripts/serverstatus.py"
+               ssh = subprocess.Popen(["ssh", "%s" % HOST, COMMAND],
+                       shell=False,
+                       stdout=subprocess.PIPE,
+                       stderr=subprocess.PIPE)
+               result = ssh.stdout.readlines()
+               if result == []:
+                       error = ssh.stderr.readlines()
+                       print >>sys.stderr, "ERROR: %s" % error
+               else:
+                       print ("Result of running serverStatus: ")
+                       print result
+                       if "AVAILABLE\n" in result:
+                               available.append(i)
+                               if len(available) >= needed:
+                                       break
+       return available
+
+def startLearningProcess(benchmark, server, learningSet):
+       global SRCDIR
+       HOST="dc-"+ str(server) + ".calit2.uci.edu"
+       ALGORITHM = "2"
+       LOGFILE= benchmark + "-" + str(learningSet) + ".log"
+       print("Running benchmark " + benchmark + "(Set="+ str(learningSet)+") on server")
+       COMMAND=("cd "+SRCDIR+"; ./Scripts/learnresultgen.sh " +
+               benchmark + " " + str(learningSet) + " " + ALGORITHM + " &> " + LOGFILE + "; mv *.csv ~/; echo 'SUCCESS'")
+       print("Calling the following command:\n" + COMMAND)
+       ssh = subprocess.Popen(["ssh", "%s" % HOST, COMMAND],
+               shell=False,
+               stdout=subprocess.PIPE,
+               stderr=subprocess.PIPE)
+       result = ssh.stdout.readlines()
+       if result == []:
+               error = ssh.stderr.readlines()
+               print >>sys.stderr, "ERROR: %s" % error
+       else:
+               print ("Result of running serverStatus: ") 
+               print result
+
+def moveCSVFiles():
+       global LOCALSRCDIR
+       os.system("mv ~/*.csv "+ LOCALSRCDIR)
+
+
+def main():
+       benchmark = ArgParser().getBenchmarkName()
+#      print("Deploying on all the servers ...")
+#      deploy()
+       serverNumber = getServerNeeded(benchmark)
+       print("Learning on " + benchmark + " needs " + str(serverNumber) + " servers.")
+       availableServers = getAvailableServerList(serverNumber)
+       print ("Available Server:" + str(availableServers))
+       if serverNumber > len(availableServers):
+               print("Servers are busy. We don't have enough server available for learning ...")
+               sys.exit(1)
+       try:
+               threads = []
+               for i in range(serverNumber):
+                       t = Thread(target=startLearningProcess, args=(benchmark, availableServers[i], i, ))
+                       t.start()
+                       threads.append(t)
+               
+               for t in threads:
+                       t.join()
+               moveCSVFiles()
+       except:
+               print("Exception in creating learning thread ...")
+               sys.exit(1)
+
+
+
+if __name__ == "__main__":
+       main()
diff --git a/src/Scripts/runbench.sh b/src/Scripts/runbench.sh
new file mode 100755 (executable)
index 0000000..ed66315
--- /dev/null
@@ -0,0 +1,24 @@
+#!/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 3 ]; then
+        echo "Illegal number of argument"
+        echo "./runbench.sh [benchmark] [timeout] [tuner.conf]"
+        exit 1
+fi
+
+
+BIN=./bin
+DUMP=$(find . -name "*.dump")
+cd $BIN
+for d in $DUMP; do
+       if [[ $d = *$1* ]]; then
+               echo $d
+               ./run.sh tunerrun "."$d $2 "../"$3 out.out
+               echo "Best tuner"
+       fi
+done
diff --git a/src/Scripts/runinterpreter.sh b/src/Scripts/runinterpreter.sh
new file mode 100755 (executable)
index 0000000..759b957
--- /dev/null
@@ -0,0 +1,32 @@
+#!/bin/bash
+# run as the following:
+# ./runalloy.sh [hexiom] [--alloy]
+# ./runalloy.sh [nqueens] [--alloy]
+# ./runalloy.sh [sudoku-csolver] [--alloy]
+# ./runalloy.sh [killerSudoku] [--alloy]
+
+#./run.sh deserializealloytest ../Benchmarks/sudoku-csolver/4x4.dump --alloy
+#./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz satune.als > solution.log
+
+if [ "$#" -lt 2 ]; then
+        echo "Illegal number of argument"
+        echo "./runinterpreter.sh [benchmark] [--alloy/--z3/--smtrat/--mathsat] [timeout]"
+        exit 1
+fi
+
+
+BIN=./bin
+DUMP=$(find . -name "*.dump")
+cd $BIN
+for d in $DUMP; do
+       if [[ $d = *$1* ]]; then
+               echo $d
+               START=$(date +%s.%N)
+               ./run.sh deserializealloytest "."$d $2 $3
+               END=$(date +%s.%N)
+               DIFF=$(echo "$END - $START" | bc)
+               echo "CSOLVER solve time: $DIFF"
+               cat solution.sol
+               echo "Best tuner"
+       fi
+done
diff --git a/src/Scripts/serverstatus.py b/src/Scripts/serverstatus.py
new file mode 100644 (file)
index 0000000..3f6ffd4
--- /dev/null
@@ -0,0 +1,15 @@
+import psutil
+from time import sleep
+# gives a single float value
+avg = 0.0
+count = 0
+for i in range(350):
+       avg = (psutil.cpu_percent() + avg*count)/(count+1)
+       count = count + 1
+       sleep(0.1)
+
+
+if avg> 15:
+       print "BUSY"
+else:
+       print "AVAILABLE"
index effe965..f132e74 100644 (file)
@@ -1,15 +1,30 @@
 #include "csolver.h"
 #include "comptuner.h"
 #include "searchtuner.h"
+#include "dirent.h"
 
-int main(int argc, char **argv) {
-       if (argc < 2) {
-               printf("You should specify number of runs\n");
-               exit(-1);
+uint getNumberOfRuns(){
+       uint runs = 0;
+       DIR *dir;
+       struct dirent *ent;
+       if ((dir = opendir ("./")) != NULL) {
+               /* print all the files and directories within directory */
+               while ((ent = readdir (dir)) != NULL) {
+                       if(strstr(ent->d_name, "result") != NULL){
+                               runs++;
+                       }
+               }
+               closedir (dir);
+       } else {
+               perror ("Unable to open the directory\n");
+               exit(1);
        }
-       uint numruns;
-       sscanf(argv[1], "%u", &numruns);
+       return runs;
+}
 
+int main(int argc, char **argv) {
+       uint numruns = getNumberOfRuns();
+       printf("Number of Runs: %u\n", numruns);
        CompTuner *multituner = new CompTuner(0, 0);
        multituner->readData(numruns);
        multituner->findBestThreeTuners();
index 60b4aee..56393fb 100644 (file)
@@ -51,34 +51,49 @@ public:
 
 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
-
+Vector<OrderRec*> * orderRecVector = NULL;
 HashtableIW * ordertable = NULL;
 HashtableBV * vartable = new HashtableBV();
 
+void cleanAndFreeOrderRecVector(){
+       for(uint i=0; i< orderRecVector->getSize(); i++){
+               delete orderRecVector->get(i);
+       }
+       orderRecVector->clear();
+}
+
 int main(int numargs, char ** argv) {
   file = new std::ifstream(argv[1]);
   char * assert = NULL;
   char * sat = NULL;
+  Vector<OrderRec*> orderRecs;
+  orderRecVector = &orderRecs;
   while(true) {
     int retval = skipahead(assertstart, satstart);
     printf("%d\n", retval);
-    if (retval == 0)
+    if (retval == 0){
       break;
+    }
     if (retval == 1) {
-      if (assert != NULL)
+      if (assert != NULL){
        free(assert);
+       assert = NULL;
+      }
       assert = readuntilend(assertend);
       printf("[%s]\n", assert);
     } else if (retval == 2) {
       if (sat != NULL) {
        free(sat);
+       sat = NULL;
        vartable->resetAndDeleteKeys();
-       ordertable->resetAndDeleteVals();
+       ordertable->reset();
+       cleanAndFreeOrderRecVector();
       } else {
        ordertable = new HashtableIW();
       }
       sat = readuntilend(satend);
       CSolver *solver = new CSolver();
+      solver->turnoffOptimizations();
       set = solver->createMutableSet(1);
       order = solver->createOrder(SATC_TOTAL, (Set *) set);
       int offset = 0;
@@ -96,8 +111,21 @@ int main(int numargs, char ** argv) {
       delete solver;
     }
   }
-  
+
+  cleanAndFreeOrderRecVector();
+  if(ordertable != NULL){
+       delete ordertable;
+  }
+  if(assert != NULL){
+       free(assert);
+  }
+  if(sat != NULL){
+       free(sat);
+  }
+  vartable->resetAndDeleteKeys();
+  delete vartable;
   file->close();
+  delete file;
 }
 
 void skipwhitespace(char * constraint, int & offset) {
@@ -160,6 +188,7 @@ void mergeVars(int32_t value1, int32_t value2) {
   if (r1 == r2) {
     if (r1 == NULL) {
       OrderRec * r = new OrderRec();
+      orderRecVector->push(r);
       r->value = value1;
       r->set = new HashsetIW();
       intwrapper * k1 = new intwrapper(v1);
@@ -197,7 +226,10 @@ int32_t checkordervar(CSolver * solver, int32_t value) {
   if (rec == NULL) {
     intwrapper * k = new intwrapper(value);
     rec = new OrderRec();
+    orderRecVector->push(rec);
     rec->value = value;
+    rec->set = new HashsetIW();
+    rec->set->add(k);
     ordertable->put(k, rec);
   }
   if (!rec->alloced) {
diff --git a/src/autotunerparser.py b/src/autotunerparser.py
deleted file mode 100644 (file)
index 1632f4b..0000000
+++ /dev/null
@@ -1,83 +0,0 @@
-import re
-import argparse
-import sys
-
-
-class AutoTunerArgParser:
-    def __init__(self):
-        self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...')
-        self.parser.add_argument('--file', '-f', metavar='out.log', type=str, nargs=1,help='output log of running the autotuner ...')
-        self.args = self.parser.parse_args()
-        
-    def getFileName(self):
-        return self.args.file[0]
-       
-configs = {"EXECTIME": "-",
-               "SATTIME":"-",
-               "TESTCASE":"-",
-               "PREPROCESS" : "-",
-               "ELEMENTOPT" : "-",
-               "ELEMENTOPTSETS" : "-",
-               "PROXYVARIABLE" : "-",
-               "#SubGraph" : "-",
-               "NODEENCODING" : "-",
-               "EDGEENCODING" : "-",
-               "NAIVEENCODER" :"-",
-               "ENCODINGGRAPHOPT" : "-"
-               }
-
-REGEXES = {"EXECTIME": "CSOLVER solve time: (.*)",
-               "SATTIME":"SAT Solving time: (.*)",
-               "TESTCASE": "deserializing (.+) ...",
-               "PREPROCESS" : "Param PREPROCESS = (.*)range=\[0,1\]",
-               "ELEMENTOPT" : "Param ELEMENTOPT = (.*)range=\[0,1\]",
-               "ELEMENTOPTSETS" : "Param ELEMENTOPTSETS = (.*)range=\[0,1\]",
-               "PROXYVARIABLE" : "Param PROXYVARIABLE = (.*)range=\[1,5\]",
-               "#SubGraph" : "#SubGraph = (.*)",
-               "NODEENCODING" : "Param NODEENCODING = (.*)range=\[0,3\](.*)",
-               "EDGEENCODING" : "Param EDGEENCODING = (.*)range=\[0,2\](.*)",
-               "NAIVEENCODER" : "Param NAIVEENCODER = (.*)range=\[1,3\](.*)",
-               "ENCODINGGRAPHOPT" : "Param ENCODINGGRAPHOPT = (.*)range=\[0,1\]"
-               }
-
-def printHeader(file):
-       global configs
-       mystr=""
-       for config in configs:
-                mystr+=str(config)+","
-       print >>file, mystr
-       
-def printConfig(file, data):
-       print data
-       mystr=""
-       for config in data:
-                mystr+=str(data[config])+","
-       print >> file, mystr
-
-def main():
-       global configs
-       argprocess = AutoTunerArgParser()
-       output = open("tuner.csv", "w")
-       printHeader(output)
-       with open(argprocess.getFileName()) as file:
-               for line in file:
-                       if line.startswith("Mutating"):
-                               printConfig(output,configs)
-                       elif line.startswith("Best tuner"):
-                               printConfig(output,configs);
-                       else :
-                               for regex in REGEXES:
-                                       p = re.compile(REGEXES[regex])
-                                       token = p.search(line)
-                                       if token is not None:
-                                               if regex == "TESTCASE":
-                                                       configs[regex] = re.search(REGEXES[regex], line).group(1)
-                                               else:
-                                                       configs[regex] = re.findall("\d+\.?\d*", line)[0]
-
-       configs["EXECTIME"] = "BEST TUNE:"
-       printConfig(output, configs)
-       print "Done with parsing " + argprocess.getFileName()
-
-if __name__ == "__main__":
-       main()
index aea2161..aca46a5 100644 (file)
@@ -146,10 +146,18 @@ int solve(void *solver) {
        return CCSOLVER(solver)->solve();
 }
 
+int solveIncremental(void *solver) {
+       return CCSOLVER(solver)->solveIncremental();
+}
+
 long getElementValue(void *solver,void *element) {
        return (long) CCSOLVER(solver)->getElementValue((Element *)element);
 }
 
+void freezeElement(void *solver,void *element) {
+       CCSOLVER(solver)->freezeElement((Element *)element);
+}
+
 int getBooleanValue(void *solver, void *boolean) {
        return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
 }
@@ -162,6 +170,10 @@ void printConstraints(void *solver) {
        CCSOLVER(solver)->printConstraints();
 }
 
+void turnoffOptimizations(void *solver) {
+       CCSOLVER(solver)->turnoffOptimizations();
+}
+
 
 void serialize(void *solver) {
        CCSOLVER(solver)->serialize();
index 86d5a46..8e708b8 100644 (file)
@@ -40,10 +40,13 @@ void printConstraint(void *solver,void *constraint);
 void *createOrder(void *solver,unsigned int type, void *set);
 void *orderConstraint(void *solver,void *order, long first, long second);
 int solve(void *solver);
+int solveIncremental(void *solver);
 long getElementValue(void *solver,void *element);
+void freezeElement(void *solver,void *element);
 int getBooleanValue(void *solver,void *boolean);
 int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);
+void turnoffOptimizations(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
 void setInterpreter(void *solver, unsigned int type);
index f54756b..b66fc44 100644 (file)
@@ -1,6 +1,18 @@
 #include "common.h"
+#include <stdio.h>
+#include <execinfo.h>
+#include <signal.h>
+#include <stdlib.h>
+#include <unistd.h>
 
 void assert_hook(void)
 {
        model_print("Add breakpoint to line %u in file %s.\n", __LINE__, __FILE__);
 }
+
+void print_trace(void){
+       void *array[10];
+       size_t size;
+       size = backtrace(array, 10);
+       backtrace_symbols_fd(array, size, STDERR_FILENO);       
+}
index 17b3dc3..17e2378 100644 (file)
@@ -40,6 +40,7 @@ CSolver::CSolver() :
        unsat(false),
        booleanVarUsed(false),
        incrementalMode(false),
+       optimizationsOff(false),
        tuner(NULL),
        elapsedTime(0),
        satsolverTimeout(NOTIMEOUT),
@@ -566,7 +567,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if (!useInterpreter()) {
+       if (!useInterpreter() && !optimizationsOff) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
@@ -650,8 +651,9 @@ int CSolver::solveIncremental() {
        }
        int result = IS_INDETER;
        ASSERT (!useInterpreter());
-
-       computePolarities(this);
+       if(!optimizationsOff){
+               computePolarities(this);
+       }
 //     long long time1 = getTimeNano();
 //     model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 //     Preprocess pp(this);
@@ -733,36 +735,39 @@ int CSolver::solve() {
                        }
                        delete orderit;
                }
+               long long time1, time2;
+               
                computePolarities(this);
-               long long time1 = getTimeNano();
-               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
-               Preprocess pp(this);
-               pp.doTransform();
-               long long time2 = getTimeNano();
-               model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
-
-               DecomposeOrderTransform dot(this);
-               dot.doTransform();
                time1 = getTimeNano();
-               model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+               if(!optimizationsOff){
+                       Preprocess pp(this);
+                       pp.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 
-               IntegerEncodingTransform iet(this);
-               iet.doTransform();
+                       DecomposeOrderTransform dot(this);
+                       dot.doTransform();
+                       time1 = getTimeNano();
+                       model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
-               ElementOpt eop(this);
-               eop.doTransform();
+                       IntegerEncodingTransform iet(this);
+                       iet.doTransform();
 
-               EncodingGraph eg(this);
-               eg.encode();
+                       ElementOpt eop(this);
+                       eop.doTransform();
 
+                       EncodingGraph eg(this);
+                       eg.encode();
+               }
                naiveEncodingDecision(this);
                //      eg.validate();
-
-               VarOrderingOpt bor(this, satEncoder);
-               bor.doTransform();
-
-               time2 = getTimeNano();
-               model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               if(!optimizationsOff){
+                       VarOrderingOpt bor(this, satEncoder);
+                       bor.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               }
 
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
index b27e3c0..eba7b3c 100644 (file)
@@ -141,7 +141,7 @@ public:
        uint64_t getElementValue(Element *element);
 
        void freezeElement(Element *e);
-
+       void turnoffOptimizations(){optimizationsOff = true;}
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 
@@ -237,10 +237,12 @@ private:
        bool unsat;
        bool booleanVarUsed;
        bool incrementalMode;
+       bool optimizationsOff;
        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;
+       bool noOptimization;
        friend class ElementOpt;
        friend class VarOrderingOpt;
 };
index 461a859..a3e0f11 100644 (file)
@@ -101,16 +101,22 @@ def loadCSolver():
        csolverlb.orderConstraint.restype = c_void_p
        csolverlb.solve.argtypes = [c_void_p]
        csolverlb.solve.restype = c_int
+       csolverlb.solveIncremental.argtypes = [c_void_p]
+       csolverlb.solveIncremental.restype = c_int
         csolverlb.mustHaveValue.argtypes = [c_void_p, c_void_p]
        csolverlb.mustHaveValue.restype = c_void_p
        csolverlb.getElementValue.argtypes = [c_void_p, c_void_p]
-       csolverlb.getElementValue.restype = c_long
+       csolverlb.getElementValue.restype = c_void_p
+       csolverlb.freezeElement.argtypes = [c_void_p, c_void_p]
+       csolverlb.freezeElement.restype = c_long
        csolverlb.getBooleanValue.argtypes = [c_void_p, c_void_p]
        csolverlb.getBooleanValue.restype = c_int
        csolverlb.getOrderConstraintValue.argtypes = [c_void_p, c_void_p, c_long, c_long]
        csolverlb.getOrderConstraintValue.restype = c_int
        csolverlb.printConstraints.argtypes = [c_void_p]
        csolverlb.printConstraints.restype = None
+       csolverlb.turnoffOptimizations.argtypes = [c_void_p]
+       csolverlb.turnoffOptimizations.restype = None
         csolverlb.clone.argtypes = [c_void_p]
        csolverlb.clone.restype = c_void_p
        csolverlb.serialize.argtypes = [c_void_p]
diff --git a/src/runbench.sh b/src/runbench.sh
deleted file mode 100755 (executable)
index ed66315..0000000
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/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 3 ]; then
-        echo "Illegal number of argument"
-        echo "./runbench.sh [benchmark] [timeout] [tuner.conf]"
-        exit 1
-fi
-
-
-BIN=./bin
-DUMP=$(find . -name "*.dump")
-cd $BIN
-for d in $DUMP; do
-       if [[ $d = *$1* ]]; then
-               echo $d
-               ./run.sh tunerrun "."$d $2 "../"$3 out.out
-               echo "Best tuner"
-       fi
-done
diff --git a/src/runinterpreter.sh b/src/runinterpreter.sh
deleted file mode 100755 (executable)
index 759b957..0000000
+++ /dev/null
@@ -1,32 +0,0 @@
-#!/bin/bash
-# run as the following:
-# ./runalloy.sh [hexiom] [--alloy]
-# ./runalloy.sh [nqueens] [--alloy]
-# ./runalloy.sh [sudoku-csolver] [--alloy]
-# ./runalloy.sh [killerSudoku] [--alloy]
-
-#./run.sh deserializealloytest ../Benchmarks/sudoku-csolver/4x4.dump --alloy
-#./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz satune.als > solution.log
-
-if [ "$#" -lt 2 ]; then
-        echo "Illegal number of argument"
-        echo "./runinterpreter.sh [benchmark] [--alloy/--z3/--smtrat/--mathsat] [timeout]"
-        exit 1
-fi
-
-
-BIN=./bin
-DUMP=$(find . -name "*.dump")
-cd $BIN
-for d in $DUMP; do
-       if [[ $d = *$1* ]]; then
-               echo $d
-               START=$(date +%s.%N)
-               ./run.sh deserializealloytest "."$d $2 $3
-               END=$(date +%s.%N)
-               DIFF=$(echo "$END - $START" | bc)
-               echo "CSOLVER solve time: $DIFF"
-               cat solution.sol
-               echo "Best tuner"
-       fi
-done
index 37bfba4..0a7d672 100644 (file)
@@ -391,6 +391,17 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
        return (jint) solve((void *)solver);
 }
 
+/*
+ * Class:     SatuneJavaAPI
+ * Method:    solveIncremental
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solveIncremental
+       (JNIEnv *env, jobject obj, jlong solver)
+{
+       return (jint) solveIncremental((void *)solver);
+}
+
 /*
  * Class:     SatuneJavaAPI
  * Method:    getElementValue
@@ -402,6 +413,17 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
        return (jlong) getElementValue((void *)solver,(void *)element);
 }
 
+/*
+ * Class:     SatuneJavaAPI
+ * Method:    freezeElement
+ * Signature: (JJ)J
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_freezeElement
+       (JNIEnv *env, jobject obj, jlong solver, jlong element)
+{
+       freezeElement((void *)solver,(void *)element);
+}
+
 /*
  * Class:     SatuneJavaAPI
  * Method:    getBooleanValue
@@ -435,6 +457,17 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        printConstraints((void *)solver);
 }
 
+/*
+ * Class:     SatuneJavaAPI
+ * Method:    turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+       (JNIEnv *env, jobject obj, jlong solver)
+{
+       turnoffOptimizations((void *)solver);
+}
+
 /*
  * Class:     SatuneJavaAPI
  * Method:    serialize
index 93a386d..0a0b6e5 100644 (file)
@@ -280,6 +280,14 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
        (JNIEnv *, jobject, jlong);
 
+/*
+ * Class:     satune_SatuneJavaAPI
+ * Method:    solveIncremental
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solveIncremental
+       (JNIEnv *, jobject, jlong);
+
 /*
  * Class:     satune_SatuneJavaAPI
  * Method:    getElementValue
@@ -288,6 +296,15 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
        (JNIEnv *, jobject, jlong, jlong);
 
+
+/*
+ * Class:     satune_SatuneJavaAPI
+ * Method:    getElementValue
+ * Signature: (JJ)J
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_freezeElement
+       (JNIEnv *, jobject, jlong, jlong);
+
 /*
  * Class:     satune_SatuneJavaAPI
  * Method:    getBooleanValue
@@ -312,6 +329,14 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        (JNIEnv *, jobject, jlong);
 
+/*
+ * Class:     satune_SatuneJavaAPI
+ * Method:    turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+       (JNIEnv *, jobject, jlong);
+
 /*
  * Class:     satune_SatuneJavaAPI
  * Method:    serialize