Merging with Tuner branch
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 22 Feb 2019 00:31:39 +0000 (16:31 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Fri, 22 Feb 2019 00:31:39 +0000 (16:31 -0800)
86 files changed:
deploy-cs.sh
src/AST/astops.h
src/AST/ops.h
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Encoding/encodinggraph.h
src/ASTAnalyses/Encoding/subgraph.cc
src/ASTAnalyses/Encoding/subgraph.h
src/ASTTransform/elementopt.cc
src/ASTTransform/preprocess.cc
src/ASTTransform/varorderingopt.cc
src/ASTTransform/varorderingopt.h
src/Backend/inc_solver.cc
src/Backend/inc_solver.h
src/Backend/satelemencoder.cc
src/Backend/satencoder.h
src/Collections/cppvector.h
src/Collections/structs.cc
src/Collections/structs.h
src/Encoders/naiveencoder.cc
src/Interpreter/alloyinterpreter.cc [new file with mode: 0644]
src/Interpreter/alloyinterpreter.h [new file with mode: 0644]
src/Interpreter/alloysig.cc [new file with mode: 0644]
src/Interpreter/alloysig.h [new file with mode: 0644]
src/Interpreter/interpreter.cc [new file with mode: 0644]
src/Interpreter/interpreter.h [new file with mode: 0644]
src/Interpreter/mathsatinterpreter.cc [new file with mode: 0644]
src/Interpreter/mathsatinterpreter.h [new file with mode: 0644]
src/Interpreter/signature.cc [new file with mode: 0644]
src/Interpreter/signature.h [new file with mode: 0644]
src/Interpreter/signatureenc.cc [new file with mode: 0644]
src/Interpreter/signatureenc.h [new file with mode: 0644]
src/Interpreter/smtinterpreter.cc [new file with mode: 0644]
src/Interpreter/smtinterpreter.h [new file with mode: 0644]
src/Interpreter/smtratinterpreter.cc [new file with mode: 0644]
src/Interpreter/smtratinterpreter.h [new file with mode: 0644]
src/Interpreter/smtsig.cc [new file with mode: 0644]
src/Interpreter/smtsig.h [new file with mode: 0644]
src/Makefile
src/Serialize/deserializer.cc
src/Serialize/deserializer.h
src/Test/analyzemultituner.cc [new file with mode: 0644]
src/Test/deserializealloytest.cc [new file with mode: 0644]
src/Test/deserializertest.cc [deleted file]
src/Test/deserializerun.cc [new file with mode: 0644]
src/Test/printtuner.cc [new file with mode: 0644]
src/Test/run.sh
src/Test/runmultituner.cc [new file with mode: 0644]
src/Test/serializestatictuner.cc [new file with mode: 0644]
src/Test/tunerrun.cc [new file with mode: 0644]
src/Tuner/autotuner.cc
src/Tuner/autotuner.h
src/Tuner/basictuner.cc [new file with mode: 0644]
src/Tuner/basictuner.h [new file with mode: 0644]
src/Tuner/comptuner.cc [new file with mode: 0644]
src/Tuner/comptuner.h [new file with mode: 0644]
src/Tuner/kmeanstuner.cc [new file with mode: 0644]
src/Tuner/kmeanstuner.h [new file with mode: 0644]
src/Tuner/randomtuner.cc [new file with mode: 0644]
src/Tuner/randomtuner.h [new file with mode: 0644]
src/Tuner/satuner.cc [new file with mode: 0644]
src/Tuner/satuner.h [new file with mode: 0644]
src/Tuner/searchtuner.cc
src/Tuner/searchtuner.h
src/Tuner/serializetuner.cc [new file with mode: 0644]
src/Tuner/serializetuner.h [new file with mode: 0644]
src/Tuner/tunable.cc
src/Tuner/tunable.h
src/analyzer/analyze.sh [new file with mode: 0755]
src/analyzer/plot.py [new file with mode: 0644]
src/analyzer/report/makefile [new file with mode: 0644]
src/analyzer/report/paper.bib [new file with mode: 0644]
src/analyzer/report/paper.tex [new file with mode: 0644]
src/analyzer/report/tech.tex [new file with mode: 0644]
src/analyzer/tunerloganalyzer.py [new file with mode: 0644]
src/ccsolver.cc
src/ccsolver.h
src/classes.h
src/classlist.h
src/common.h
src/config.h
src/csolver.cc
src/csolver.h
src/learn.sh [deleted file]
src/pycsolver.py
src/runbench.sh [new file with mode: 0755]
tunermonitor.sh [new file with mode: 0755]

index bafb92a..2f41b32 100755 (executable)
@@ -4,7 +4,7 @@
 set -e
 
 BASE=../
-SERVERS="dc-5.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-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"
 REMOTEDIR="/scratch/hamed/"
 INFILE="constraint_compiler/"
 SRC="constraint_compiler/src/"
@@ -17,7 +17,7 @@ cd $BASE
 rm -f $OUTFILE
 tar -czvf $OUTFILE $INFILE
 
+cp $OUTFILE $SHAREDDIR
 for SERVER in $SERVERS; do
-       cp $OUTFILE $SHAREDDIR
-       ssh $USER@$SERVER "mv $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"
 done
index a451c5f..04b4c83 100644 (file)
@@ -25,7 +25,7 @@ enum ElementEncodingType {
 
 typedef enum ElementEncodingType ElementEncodingType;
 
-enum BooleanVarOrdering {CONSTRAINTORDERING=0, CHORONOLOGICALORDERING=1, REVERSEORDERING=2};
+enum BooleanVarOrdering {CONSTRAINTORDERING=0, ELEMENTORDERING=1, REVERSEORDERING=2};
 typedef enum BooleanVarOrdering BooleanVarOrdering;
 
 Polarity negatePolarity(Polarity This);
index 8b08202..6d6fd97 100644 (file)
@@ -26,4 +26,8 @@ typedef enum OverFlowBehavior OverFlowBehavior;
 enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED};
 typedef enum UndefinedBehavior UndefinedBehavior;
 
+enum InterpreterType {SATUNE, ALLOY, Z3, MATHSAT, SMTRAT};
+typedef enum InterpreterType InterpreterType;
+
+
 #endif
index 957fea3..66d8606 100644 (file)
@@ -305,7 +305,6 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) {
 }
 
 uint convertSize(uint cost) {
-       cost = FUDGEFACTOR * cost;// fudge factor
        return NEXTPOW2(cost);
 }
 
@@ -333,8 +332,8 @@ void EncodingGraph::decideEdges() {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
-               
-               uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
+
+               uint leftSize = 0, rightSize = 0, newSize = 0, min = 0;
                bool merge = false;
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
@@ -342,26 +341,28 @@ void EncodingGraph::decideEdges() {
                        newSize = convertSize(left->s->getUnionSize(right->s));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = left->measureSimilarity(right) > 1.5 || min == newSize;
                } else if (leftGraph != NULL && rightGraph == NULL) {
-                       leftSize = convertSize(leftGraph->encodingSize);
+                       leftSize = convertSize(leftGraph->numValues());
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       max = rightSize > leftSize? rightSize : leftSize;
-//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
-                       merge = left->measureSimilarity(right) > 1.5 || max == newSize;
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = leftGraph->measureSimilarity(right) > 1.5 || min == newSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
                } else {
                        //Neither are null
-                       leftSize = convertSize(leftGraph->encodingSize);
-                       rightSize = convertSize(rightGraph->encodingSize);
+                       leftSize = convertSize(leftGraph->numValues());
+                       rightSize = convertSize(rightGraph->numValues());
                        newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
 //                     model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       max = rightSize > leftSize? rightSize : leftSize;
-//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
-                       merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = leftGraph->measureSimilarity(rightGraph) > 1.5 || min == newSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
                }
                if (merge) {
                        //add the edge
@@ -419,7 +420,7 @@ uint EncodingNode::getSize() const {
        return s->getSize();
 }
 
-uint64_t EncodingNode::getIndex(uint index){
+uint64_t EncodingNode::getIndex(uint index) {
        return s->getElement(index);
 }
 
@@ -427,24 +428,23 @@ VarType EncodingNode::getType() const {
        return s->getType();
 }
 
-bool EncodingNode::itemExists(uint64_t item){
-       for(uint i=0; i< s->getSize(); i++){
-               if(item == s->getElement(i))
-                       return true;
-       }
-       return false;
-}
-
-double EncodingNode::measureSimilarity(EncodingNode *node){
+double EncodingNode::measureSimilarity(EncodingNode *node) {
        uint common = 0;
-       for(uint i=0; i < s->getSize(); i++){
+       for (uint i = 0, j = 0; i < s->getSize() && j < node->s->getSize(); ) {
                uint64_t item = s->getElement(i);
-               if(node->itemExists(item)){
+               uint64_t item2 = node->s->getElement(j);
+               if (item < item2)
+                       i++;
+               else if (item2 > item)
+                       j++;
+               else {
+                       i++;
+                       j++;
                        common++;
                }
        }
-//     model_print("common=%u\tsize1=%u\tsize2=%u\tsim1=%f\tsim2=%f\n", common, s->getSize(), node->getSize(), 1.0*common/s->getSize(), 1.0*common/node->getSize());
-       return common*1.0/s->getSize() + common*1.0/node->getSize();
+
+       return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
 }
 
 EncodingNode *EncodingGraph::createNode(Element *e) {
index ae330b8..b53568e 100644 (file)
@@ -4,8 +4,6 @@
 #include "structs.h"
 #include "graphstructs.h"
 
-#define FUDGEFACTOR 1.2
-#define CONVERSIONFACTOR  0.5
 
 class EncodingGraph {
 public:
@@ -44,10 +42,9 @@ public:
        uint getSize() const;
        uint64_t getIndex(uint index);
        VarType getType() const;
-        double measureSimilarity(EncodingNode *node);
+       double measureSimilarity(EncodingNode *node);
        void setEncoding(ElementEncodingType e) {encoding = e;}
        ElementEncodingType getEncoding() {return encoding;}
-        bool itemExists(uint64_t item);
        bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
        CMEMALLOC;
 private:
index de76e4d..b36b8c0 100644 (file)
@@ -4,8 +4,6 @@
 #include "qsort.h"
 
 EncodingSubGraph::EncodingSubGraph() :
-       encodingSize(0),
-       numElements(0),
        maxEncodingVal(0) {
 }
 
@@ -109,101 +107,61 @@ void EncodingSubGraph::solveComparisons() {
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
-       uint newSize = 0;
-       SetIteratorEncodingNode *nit = sg->nodes.iterator();
-       while (nit->hasNext()) {
-               EncodingNode *en = nit->next();
-               uint size = estimateNewSize(en);
-               if (size > newSize)
-                       newSize = size;
+       uint newSize = sg->allValues.getSize() + allValues.getSize();
+       SetIterator64Int *it = sg->allValues.iterator();
+
+       while (it->hasNext()) {
+               uint64_t val = it->next();
+               if (allValues.contains(val))
+                       newSize--;
        }
-       delete nit;
+       delete it;
        return newSize;
 }
 
 double EncodingSubGraph::measureSimilarity(EncodingNode *node) {
        uint common = 0;
-       Hashset64Int intSet;
-       SetIteratorEncodingNode *nit = nodes.iterator();
-       while (nit->hasNext()) {
-               EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
-                       intSet.add(en->getIndex(i));
-               }
-       }
-       for(uint i=0; i < node->getSize(); i++){
-               if(intSet.contains( node->getIndex(i) )){
+       uint size = node->getSize();
+       for (uint i = 0; i < size; i++) {
+               uint64_t val = node->getIndex(i);
+               if (allValues.contains(val))
                        common++;
-               }
        }
-//     model_print("measureSimilarity:139: common=%u\t GraphSize=%u\tnodeSize=%u\tGraphSim=%f\tnodeSim=%f\n", common, intSet.getSize(), node->getSize(), 1.0*common/intSet.getSize(), 1.0*common/node->getSize());
-       delete nit;
-       return common*1.0/intSet.getSize() + common*1.0/node->getSize();
+       return common * 1.0 / allValues.getSize() + common * 1.0 / node->getSize();
 }
 
 double EncodingSubGraph::measureSimilarity(EncodingSubGraph *sg) {
        uint common = 0;
-       Hashset64Int set1;
-       Hashset64Int set2;
-       SetIteratorEncodingNode *nit = nodes.iterator();
-       while (nit->hasNext()) {
-               EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
-                       set1.add(en->getIndex(i));
-               }
-       }
-       delete nit;
-       nit = sg->nodes.iterator();
-       while (nit->hasNext()) {
-               EncodingNode *en = nit->next();
-               for(uint i=0; i < en->getSize(); i++){
-                       set2.add(en->getIndex(i));
-               }
-       }
-       delete nit;
-       SetIterator64Int *setIter1 = set1.iterator();
-       while(setIter1->hasNext()){
+       SetIterator64Int *setIter1 = allValues.iterator();
+       while (setIter1->hasNext()) {
                uint64_t item1 = setIter1->next();
-               if( set2.contains(item1)){
+               if ( sg->allValues.contains(item1)) {
                        common++;
                }
        }
        delete setIter1;
-//     model_print("measureSimilarity:139: common=%u\tGraphSize1=%u\tGraphSize2=%u\tGraphSize1=%f\tGraphSize2=%f\n", common, set1.getSize(), set2.getSize(), 1.0*common/set1.getSize(), 1.0*common/set2.getSize());
-       return common*1.0/set1.getSize() + common*1.0/set2.getSize();
+       return common * 1.0 / allValues.getSize() + common * 1.0 / sg->allValues.getSize();
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
-       SetIteratorEncodingEdge *eeit = n->edges.iterator();
-       uint newsize = n->getSize();
-       while (eeit->hasNext()) {
-               EncodingEdge *ee = eeit->next();
-               if (ee->left != NULL && ee->left != n && nodes.contains(ee->left)) {
-                       uint intersectSize = n->s->getUnionSize(ee->left->s);
-                       if (intersectSize > newsize)
-                               newsize = intersectSize;
-               }
-               if (ee->right != NULL && ee->right != n && nodes.contains(ee->right)) {
-                       uint intersectSize = n->s->getUnionSize(ee->right->s);
-                       if (intersectSize > newsize)
-                               newsize = intersectSize;
-               }
-               if (ee->dst != NULL && ee->dst != n && nodes.contains(ee->dst)) {
-                       uint intersectSize = n->s->getUnionSize(ee->dst->s);
-                       if (intersectSize > newsize)
-                               newsize = intersectSize;
-               }
+       uint nSize = n->getSize();
+       uint newSize = allValues.getSize() + nSize;
+       for (uint i = 0; i < nSize; i++) {
+               if (allValues.contains(n->getIndex(i)))
+                       newSize--;
        }
-       delete eeit;
-       return newsize;
+       return newSize;
+}
+
+uint EncodingSubGraph::numValues() {
+       return allValues.getSize();
 }
 
 void EncodingSubGraph::addNode(EncodingNode *n) {
        nodes.add(n);
-       uint newSize = estimateNewSize(n);
-       numElements += n->elements.getSize();
-       if (newSize > encodingSize)
-               encodingSize = newSize;
+       uint size = n->getSize();
+       for (uint i = 0; i < size; i++)
+               allValues.add(n->getIndex(i));
 }
 
 SetIteratorEncodingNode *EncodingSubGraph::nodeIterator() {
index 1392dba..00264a6 100644 (file)
@@ -45,8 +45,9 @@ public:
        void encode();
        uint getEncoding(EncodingNode *n, uint64_t val);
        uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
-        double measureSimilarity(EncodingNode *n);
-        double measureSimilarity(EncodingSubGraph *sg);
+       double measureSimilarity(EncodingNode *n);
+       double measureSimilarity(EncodingSubGraph *sg);
+       uint numValues();
        CMEMALLOC;
 private:
        uint estimateNewSize(EncodingNode *n);
@@ -64,10 +65,8 @@ private:
        HashsetEncodingValue values;
        HashsetEncodingNode nodes;
        NVPMap map;
-       uint encodingSize;
-       uint numElements;
        uint maxEncodingVal;
-
+       Hashset64Int allValues;
        friend class EncodingGraph;
 };
 
index b0866ed..96ca8f6 100644 (file)
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
        : Transform(_solver),
-       updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+         updateSets(false)
 {
 }
 
@@ -20,6 +20,9 @@ void ElementOpt::doTransform() {
        if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
 
+       //Set once we know we are going to use it.
+       updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
+       
        SetIteratorBooleanEdge *iterator = solver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
index 1e60c19..c0e3571 100644 (file)
@@ -13,7 +13,7 @@ Preprocess::~Preprocess() {
 }
 
 void Preprocess::doTransform() {
-       if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+       if (!solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
                return;
 
        BooleanIterator bit(solver);
index 41f3edb..890afd9 100644 (file)
@@ -4,10 +4,10 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   VarOrderingOpt.cpp
  * Author: hamed
- * 
+ *
  * Created on October 11, 2018, 5:31 PM
  */
 
 #include "elementencoding.h"
 #include "element.h"
 
-VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder): Transform(_solver){
+VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder) : Transform(_solver) {
        satencoder = _satencoder;
 }
 
 VarOrderingOpt::~VarOrderingOpt() {
 }
 
-void VarOrderingOpt::doTransform(){
+void VarOrderingOpt::doTransform() {
        BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
-       if ( direction == CONSTRAINTORDERING ){
+       if ( direction == CONSTRAINTORDERING ) {
                return;
        }
-       
+
        uint size = solver->allElements.getSize();
-       if(direction == CHORONOLOGICALORDERING){
+       if (direction == ELEMENTORDERING) {
                for (uint i = 0; i < size; i++) {
                        Element *el = solver->allElements.get(i);
                        ElementEncoding *encoding = el->getElementEncoding();
@@ -40,8 +40,8 @@ void VarOrderingOpt::doTransform(){
                                continue;
                        satencoder->encodeElementSATEncoder(el);
                }
-       }else{
-               for (int i = size-1; i>0; i--) {
+       } else {
+               for (int i = size - 1; i > 0; i--) {
                        Element *el = solver->allElements.get(i);
                        ElementEncoding *encoding = el->getElementEncoding();
                        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
index efb0152..ed134d7 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   VarOrderingOpt.h
  * Author: hamed
  *
 #include "transform.h"
 
 
-class VarOrderingOpt :Transform {
+class VarOrderingOpt : Transform {
 public:
-        VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
-        void doTransform();
-        virtual ~VarOrderingOpt();
+       VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
+       void doTransform();
+       virtual ~VarOrderingOpt();
 private:
-        SATEncoder* satencoder;
+       SATEncoder *satencoder;
 };
 
-#endif /* VARORDERINGOPT_H */
+#endif/* VARORDERINGOPT_H */
 
index c1bebb8..2d6b8a4 100644 (file)
@@ -117,23 +117,23 @@ int readStatus(IncrementalSolver *This) {
        fd_set rfds;
        FD_ZERO(&rfds);
        FD_SET(This->from_solver_fd, &rfds);
-       fd_set * temp;
-       if(This->timeout == NOTIMEOUT){
-               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, NULL);
-       }else {
+       fd_set *temp;
+       if (This->timeout == NOTIMEOUT) {
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, NULL);
+       } else {
                struct timeval tv;
                tv.tv_sec = This->timeout;
                tv.tv_usec = 0;
-               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, &tv);
+               retval = select(This->from_solver_fd + 1, &rfds, NULL, NULL, &tv);
        }
-       if(retval == -1){
+       if (retval == -1) {
                perror("Error in select()");
                exit(EXIT_FAILURE);
        }
-       else if (retval){
+       else if (retval) {
                printf("Data is available now.\n");
                return readIntSolver(This);
-       }else{
+       } else {
                printf("Timeout for the solver\n");
                return IS_INDETER;
        }
index 4692cfe..3562a42 100644 (file)
@@ -28,7 +28,7 @@ struct IncrementalSolver {
        pid_t solver_pid;
        int to_solver_fd;
        int from_solver_fd;
-        long timeout;
+       long timeout;
 };
 
 IncrementalSolver *allocIncrementalSolver();
index 8f06eec..3f26b5c 100644 (file)
@@ -7,6 +7,7 @@
 #include "predicate.h"
 #include "csolver.h"
 #include "tunable.h"
+#include <cmath>
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
@@ -223,10 +224,15 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->element->anyValue){
+       if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
-               uint encArraySize = encoding->encArraySize;
-               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+               int maxIndex = getMaximumUsedSize(encoding);
+               if (setSize == encoding->encArraySize && maxIndex == (int)setSize) {
+                       return;
+               }
+               double ratio = (setSize * (1 + 2 * encoding->numVars)) / (encoding->numVars * (encoding->numVars + maxIndex * 1.0 - setSize));
+//             model_print("encArraySize=%u\tmaxIndex=%d\tsetSize=%u\tmetric=%f\tnumBits=%u\n", encoding->encArraySize, maxIndex, setSize, ratio, encoding->numVars);
+               if ( ratio <  pow(2, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 3)) {
                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);
@@ -278,23 +284,23 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+       for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+               if (encoding->isinUseElement(i))
+                       return i + 1;
+       }
+       ASSERT(false);
+       return -1;
+}
+
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
        if (encoding->numVars == 0)
                return;
-       int index = -1;
-       for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
-               if (encoding->isinUseElement(i)) {
-                       if (i + 1 < encoding->encArraySize) {
-                               index = i + 1;
-                       }
-                       break;
-               }
-       }
-       if ( index != -1 ) {
+       int index = getMaximumUsedSize(encoding);
+       if ( index != (int)encoding->encArraySize ) {
                addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
        }
-       index = index == -1 ? encoding->encArraySize - 1 : index - 1;
-       for (int i = index; i >= 0; i--) {
+       for (int i = index - 1; i >= 0; i--) {
                if (!encoding->isinUseElement(i)) {
                        addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
                }
index 827a904..63b5a61 100644 (file)
@@ -63,13 +63,14 @@ private:
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+       int getMaximumUsedSize(ElementEncoding *encoding);
        void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;
        CSolver *solver;
        BooleanToEdgeMap booledgeMap;
        VectorEdge *vector;
-        friend class VarOrderingOpt;
+       friend class VarOrderingOpt;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
index b8497d9..b4822ef 100644 (file)
@@ -20,6 +20,12 @@ public:
                memcpy(array, _array, capacity * sizeof(type));
        }
 
+       Vector(Vector<type> *v) :
+               size(v->size),
+               capacity(v->capacity),
+               array((type *) ourmalloc(sizeof(type) * v->capacity)) {
+               memcpy(array, v->array, capacity * sizeof(type));
+       }
        void pop() {
                size--;
        }
@@ -63,6 +69,21 @@ public:
                array[index] = item;
        }
 
+       void insertAt(uint index, type item) {
+               setSize(size + 1);
+               for (uint i = size - 1; i > index; i--) {
+                       set(i, get(i - 1));
+               }
+               array[index] = item;
+       }
+
+       void removeAt(uint index) {
+               for (uint i = index; (i + 1) < size; i++) {
+                       set(i, get(i + 1));
+               }
+               setSize(size - 1);
+       }
+
        inline uint getSize() const {
                return size;
        }
index 7bff7eb..0744a35 100644 (file)
@@ -7,7 +7,7 @@
 #include "orderelement.h"
 #include "structs.h"
 #include "decomposeorderresolver.h"
-#include "tunabledependent.h"
+#include "searchtuner.h"
 
 #define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
 #define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
@@ -30,14 +30,6 @@ bool table_entry_equals(TableEntry *key1, TableEntry *key2) {
        return true;
 }
 
-unsigned int tunable_dependent_hash_function(TunableDependent *This){
-       return (uint)This->dependent;
-}
-
-bool tunable_dependent_equals(TunableDependent *key1, TunableDependent *key2){
-       return key1->dependent == key2->dependent;
-}
-
 unsigned int order_node_hash_function(OrderNodeKey *This) {
        return (uint) This->id;
 }
@@ -90,3 +82,14 @@ bool doredge_equals(DOREdge *key1, DOREdge *key2) {
        return key1->newfirst == key2->newfirst &&
                                 key1->newsecond == key2->newsecond;
 }
+
+unsigned int tunableSettingHash(TunableSetting *setting) {
+       return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
+}
+
+bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
+       return setting1->hasVar == setting2->hasVar &&
+                                setting1->type1 == setting2->type1 &&
+                                setting1->type2 == setting2->type2 &&
+                                setting1->param == setting2->param;
+}
index 747d82c..6540b5a 100644 (file)
@@ -12,44 +12,41 @@ unsigned int table_entry_hash_function(TableEntry *This);
 bool table_entry_equals(TableEntry *key1, TableEntry *key2);
 unsigned int order_node_hash_function(OrderNodeKey *This);
 bool order_node_equals(OrderNodeKey *key1, OrderNodeKey *key2);
-unsigned int tunable_dependent_hash_function(TunableDependent *This);
-bool tunable_dependent_equals(TunableDependent *key1, TunableDependent *key2);
 unsigned int order_edge_hash_function(OrderEdge *This);
 bool order_edge_equals(OrderEdge *key1, OrderEdge *key2);
 unsigned int order_element_hash_function(OrderElement *This);
 bool order_element_equals(OrderElement *key1, OrderElement *key2);
 unsigned int order_pair_hash_function(OrderPair *This);
 bool order_pair_equals(OrderPair *key1, OrderPair *key2);
-
+unsigned int tunableSettingHash(TunableSetting *setting);
+bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
 unsigned int doredge_hash_function(DOREdge *key);
 bool doredge_equals(DOREdge *key1, DOREdge *key2);
 
 
 typedef Hashset<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
 typedef Hashset<OrderNodeKey *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> HashsetOrderNode;
-typedef Hashset<TunableDependent *, uintptr_t, PTRSHIFT, tunable_dependent_hash_function, tunable_dependent_equals> HashsetTunableDep;
 typedef Hashset<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> HashsetOrderElement;
 typedef Hashset<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> HashsetDOREdge;
 typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
 typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
-typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
 typedef Hashset<uint64_t, uint64_t, 0> Hashset64Int;
-typedef SetIterator<uint64_t, uint64_t, 0> SetIterator64Int;
+typedef Hashset<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> HashsetTunableSetting;
 
 
 typedef Hashtable<OrderNodeKey *, HashsetOrderNode *, uintptr_t, PTRSHIFT> HashtableNodeToNodeSet;
 typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, PTRSHIFT, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
 typedef Hashtable<void *, void *, uintptr_t, PTRSHIFT> CloneMap;
-
-
 typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashtableEncoding;
 
 
 typedef SetIterator<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
 typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
 typedef SetIterator<OrderNodeKey *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
-typedef SetIterator<TunableDependent *, uintptr_t, PTRSHIFT, tunable_dependent_hash_function, tunable_dependent_equals> SetIteratorTunableDep;
 typedef SetIterator<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
 typedef SetIterator<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> SetIteratorDOREdge;
+typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
+typedef SetIterator<uint64_t, uint64_t, 0> SetIterator64Int;
+typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> SetIteratorTunableSetting;
 #endif
index 3f9e44e..63ec82f 100644 (file)
@@ -69,7 +69,10 @@ void naiveEncodingElement(CSolver *csolver, Element *This) {
                if (This->type != ELEMCONST) {
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
-               encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
+               uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
+               if (enc == ELEM_UNASSIGNED)
+                       enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
+               encoding->setElementEncodingType((ElementEncodingType)enc);
                encoding->encodingArrayInitialization();
        }
 
diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
new file mode 100644 (file)
index 0000000..c0e4a60
--- /dev/null
@@ -0,0 +1,212 @@
+#include "alloyinterpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "alloysig.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+#include "cppvector.h"
+#include "math.h"
+
+using namespace std;
+
+#define ALLOYFILENAME "satune.als"
+#define ALLOYSOLUTIONFILE "solution.sol"
+
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver): 
+       Interpreter(_solver) 
+{
+       output.open(ALLOYFILENAME);
+       if(!output.is_open()){
+               model_print("AlloyEnc:Error in opening the dump file satune.als\n");
+               exit(-1);
+       }
+}
+
+AlloyInterpreter::~AlloyInterpreter(){
+       if(output.is_open()){
+               output.close();
+       }
+}
+
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+       return new AlloyBoolSig(id);
+}
+
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+       return new AlloyElementSig(id, ssig);
+}
+
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+       return new AlloySetSig(id, set);
+}
+
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
+       output << "fact {" << endl;
+       for(uint i=0; i< facts.getSize(); i++){
+               char *cstr = facts.get(i);
+               writeToFile(cstr);
+       }
+       output << "}" << endl;
+}
+
+
+int AlloyInterpreter::getResult(){
+       ifstream input(ALLOYSOLUTIONFILE, ios::in);
+       string line;
+       while(getline(input, line)){
+               if(line.find("Unsatisfiable.")== 0){
+                       return IS_UNSAT;
+               }
+               if(line.find("univ") == 0){
+                       continue;
+               }
+               if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+                       const char delim [2] = ",";
+                       char cline [line.size()+1];
+                       strcpy ( cline, line.c_str() );
+                       char *token = strtok(cline, delim);
+                       while( token != NULL ) {
+                               uint i1, i2, i3;
+                               if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+                                       model_print("Signature%u = %u\n", i1, i3);
+                                       sigEnc.setValue(i1, i3);
+                               }
+                               token = strtok(NULL, delim);
+                       }
+               }
+       }
+       return IS_SAT;
+}
+
+
+int AlloyInterpreter::getAlloyIntScope(){
+       double mylog = log2(sigEnc.getMaxValue() + 1);
+       return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
+void AlloyInterpreter::dumpFooter(){
+       output << "pred show {}" << endl;
+       output << "run show for " << getAlloyIntScope() << " int" << endl;
+}
+
+void AlloyInterpreter::dumpHeader(){
+       output << "open util/integer" << endl;
+}
+
+void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+       snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
+}
+
+string AlloyInterpreter::negateConstraint(string constr){
+       return "not ( " + constr + " )";
+}
+
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+       uint size = bl->inputs.getSize();
+       string array[size];
+       for (uint i = 0; i < size; i++)
+               array[i] = encodeConstraint(bl->inputs.get(i));
+       string op;
+       switch (bl->op){
+               case SATC_OR:
+                       op = " or ";
+                       break;
+               case SATC_AND:
+                       op = " and ";
+                       break;
+               case SATC_NOT:
+                       op = " not ";
+                       break;
+               case SATC_IFF:
+                       op = " iff ";
+                       break;
+               case SATC_IMPLIES:
+                       op = " implies ";
+                       break;
+               case SATC_XOR:
+               default:
+                       ASSERT(0);
+       }
+       switch (bl->op) {
+               case SATC_OR:
+               case SATC_AND:{
+                       ASSERT(size >= 2);
+                       string res = "( ";
+                       res += array[0];
+                       for( uint i=1; i< size; i++){
+                               res += op + array[i];
+                       }
+                       res += " )";
+                       return res;
+               }
+               case SATC_NOT:{
+                       return "not ( " + array[0] + " )";
+               }
+               case SATC_IMPLIES:
+               case SATC_IFF:
+                       return "( " + array[0] + op + array[1] + " )";
+               case SATC_XOR:
+               default:
+                       ASSERT(0);
+
+       }
+}
+
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
+       ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+       return *boolSig + " = 1";
+}
+
+string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+       FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+       uint numDomains = elemFunc->inputs.getSize();
+       ASSERT(numDomains > 1);
+       ValuedSignature *inputs[numDomains];
+       string result;
+       for (uint i = 0; i < numDomains; i++) {
+               Element *elem = elemFunc->inputs.get(i);
+               inputs[i] = sigEnc.getElementSignature(elem);
+               if(elem->type == ELEMFUNCRETURN){
+                       result += processElementFunction((ElementFunction *) elem, inputs[i]);
+               }
+       }
+       string op;
+       switch(function->op){
+               case SATC_ADD:
+                       op = ".add";
+                       break;
+               case SATC_SUB:
+                       op = ".sub";
+                       break;
+               default:
+                       ASSERT(0);
+       }
+       result += *signature + " = " + *inputs[0];
+       for (uint i = 1; i < numDomains; i++) {
+               result += op + "["+ *inputs[i] +"]";
+       }
+       result += "\n";
+       return result;
+}
+
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+       switch (op) {
+               case SATC_EQUALS:
+                       return *elemSig1 + " = " + *elemSig2;
+               case SATC_LT:
+                       return *elemSig1 + " < " + *elemSig2;
+               case SATC_GT:
+                       return *elemSig1 + " > " + *elemSig2;
+               default:
+                       ASSERT(0);
+       }
+}
+
+
diff --git a/src/Interpreter/alloyinterpreter.h b/src/Interpreter/alloyinterpreter.h
new file mode 100644 (file)
index 0000000..e4a1e3b
--- /dev/null
@@ -0,0 +1,32 @@
+#ifndef ALLOYINTERPRETER_H
+#define ALLOYINTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+class AlloyInterpreter: public Interpreter{
+public:
+       AlloyInterpreter(CSolver *solver);
+       virtual ValuedSignature *getBooleanSignature(uint id);
+       virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
+       virtual Signature *getSetSignature(uint id, Set *set);
+       virtual ~AlloyInterpreter();
+protected:
+       virtual void dumpFooter();
+       virtual void dumpHeader();
+       int getAlloyIntScope();
+       virtual void compileRunCommand(char * command , size_t size);
+       virtual int getResult();
+       virtual void dumpAllConstraints(Vector<char *> &facts);
+       virtual string negateConstraint(string constr);
+       virtual string encodeBooleanLogic( BooleanLogic *bl);
+       virtual string encodeBooleanVar( BooleanVar *bv);
+       string encodeOperatorPredicate(BooleanPredicate *constraint);
+       virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
+       virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
+};
+
+#endif
diff --git a/src/Interpreter/alloysig.cc b/src/Interpreter/alloysig.cc
new file mode 100644 (file)
index 0000000..1b98cd8
--- /dev/null
@@ -0,0 +1,104 @@
+#include "alloysig.h"
+#include "set.h"
+
+bool AlloyBoolSig::encodeAbs = true;
+bool AlloySetSig::encodeAbs = true;
+bool AlloyElementSig::encodeAbs = true;
+
+AlloyBoolSig::AlloyBoolSig(uint id):
+       ValuedSignature(id)
+{
+}
+
+string AlloyBoolSig::toString() const{
+       return "Boolean" + to_string(id) + ".value";
+}
+
+string AlloyBoolSig::getSignature() const{
+       string str;
+       if(encodeAbs){
+               encodeAbs = false;
+               str += getAbsSignature();
+       }
+       str += "one sig Boolean" + to_string(id) + " extends AbsBool {}";
+       return str;
+}
+
+string AlloyBoolSig::getAbsSignature() const{
+       string str;
+       if(AlloySetSig::encodeAbs){
+               AlloySetSig::encodeAbs = false;
+               str += "abstract sig AbsSet {\
+               domain: set Int\
+               }\n";
+       }
+       str +="one sig BooleanSet extends AbsSet {}{\n\
+       domain = 0 + 1 \n\
+       }\n\
+       abstract sig AbsBool {\
+       value: Int\
+       }{\n\
+       value in BooleanSet.domain\n\
+       }\n";
+       return str;
+}
+
+AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig): 
+       ValuedSignature(id),
+       ssig(_ssig)
+{
+}
+
+string AlloyElementSig::toString() const{
+       return "Element" + to_string(id) + ".value";
+}
+
+string AlloyElementSig::getSignature() const{
+       string str;
+       if(encodeAbs){
+               encodeAbs = false;
+               str += getAbsSignature();
+       }
+       str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\
+               value in " + *ssig + "\n\
+               }";
+       return str;
+}
+
+string AlloyElementSig::getAbsSignature() const{
+       return "abstract sig AbsElement {\n\
+               value: Int\n\
+               }\n";
+       
+}
+
+AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
+       ASSERT(set->getSize() > 0);
+       domain = to_string(set->getElement(0));
+       for(uint i=1; i< set->getSize(); i++){
+               domain += " + " + to_string(set->getElement(i));
+       }
+}
+
+string AlloySetSig::toString() const{
+       return "Set" + to_string(id) + ".domain";
+}
+
+string AlloySetSig::getSignature() const{
+       string str;
+       if(encodeAbs){
+               encodeAbs = false;
+               str += getAbsSignature();
+       }
+       str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\
+               domain = " + domain + "\n\
+               }";
+       return str;
+}
+
+string AlloySetSig::getAbsSignature() const{
+       return "abstract sig AbsSet {\n\
+               domain: set Int\n\
+               }\n";
+       
+}
diff --git a/src/Interpreter/alloysig.h b/src/Interpreter/alloysig.h
new file mode 100644 (file)
index 0000000..3fb2d10
--- /dev/null
@@ -0,0 +1,44 @@
+#ifndef ALLOYSIG_H
+#define ALLOYSIG_H
+#include <string>
+#include <iostream>
+#include "signature.h"
+#include "classlist.h"
+using namespace std;
+
+class AlloyBoolSig: public ValuedSignature{
+public:
+       AlloyBoolSig(uint id);
+       virtual ~AlloyBoolSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+private:
+       static bool encodeAbs;
+};
+
+class AlloySetSig: public Signature{
+public:
+       AlloySetSig(uint id, Set *set);
+       virtual ~AlloySetSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+       static bool encodeAbs;
+private:
+       string domain;
+};
+
+class AlloyElementSig: public ValuedSignature{
+public:
+       AlloyElementSig(uint id, Signature *ssig);
+       virtual ~AlloyElementSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+private:
+       Signature *ssig;
+       static bool encodeAbs;
+};
+
+#endif
diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc
new file mode 100644 (file)
index 0000000..a5927f7
--- /dev/null
@@ -0,0 +1,138 @@
+#include "interpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "signature.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+
+using namespace std;
+
+Interpreter::Interpreter(CSolver *_solver): 
+       csolver(_solver),
+       sigEnc(this)
+{
+}
+
+Interpreter::~Interpreter(){
+}
+
+void Interpreter::encode(){
+       dumpHeader();
+       SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+       Vector<char *> facts;
+       while(iterator->hasNext()){
+               BooleanEdge constraint = iterator->next();
+               string constr = encodeConstraint(constraint);
+               char *cstr = new char [constr.length()+1];
+               strcpy (cstr, constr.c_str());
+               facts.push(cstr);
+       }
+       dumpAllConstraints(facts);
+       for(uint i=0; i< facts.getSize(); i++){
+               char *cstr = facts.get(i);
+               delete[] cstr;
+       }
+       delete iterator;
+}
+
+uint Interpreter::getTimeout(){
+       uint timeout =csolver->getSatSolverTimeout(); 
+       return timeout == (uint)NOTIMEOUT? 1000: timeout;
+}
+
+int Interpreter::solve(){
+       dumpFooter();
+       int result = IS_INDETER;
+       char buffer [512];
+       if( output.is_open()){
+               output.close();
+       }
+       compileRunCommand(buffer, sizeof(buffer));
+       int status = system(buffer);
+       if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
+               //Read data in from results file
+               result = getResult();
+       } else {
+               model_print("Error in running command<returned %d>: %s\n", status, buffer);
+               exit(-1);
+       }
+       return result;
+}
+
+string Interpreter::encodeConstraint(BooleanEdge c){
+       Boolean *constraint = c.getBoolean();
+       string res;
+       switch(constraint->type){
+               case LOGICOP:{
+                       res = encodeBooleanLogic((BooleanLogic *) constraint);
+                       break;
+               }
+               case PREDICATEOP:{
+                       res = encodePredicate((BooleanPredicate *) constraint);
+                       break;
+               }
+               case BOOLEANVAR:{
+                       res = encodeBooleanVar( (BooleanVar *) constraint);
+                       break;
+               }
+               default:
+                       ASSERT(0);
+       }
+       if(c.isNegated()){
+               return negateConstraint(res);
+       }
+       return res;
+}
+
+string Interpreter::encodePredicate( BooleanPredicate *bp){
+       switch (bp->predicate->type) {
+               case TABLEPRED:
+                       ASSERT(0);
+               case OPERATORPRED:
+                       return encodeOperatorPredicate(bp);
+               default:
+                       ASSERT(0);
+       }
+}
+
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+       PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
+       ASSERT(constraint->inputs.getSize() == 2);
+       string str;
+       Element *elem0 = constraint->inputs.get(0);
+       ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
+       ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
+       if(elem0->type == ELEMFUNCRETURN){
+               str += processElementFunction((ElementFunction *) elem0, elemSig1);
+       }
+       Element *elem1 = constraint->inputs.get(1);
+       ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
+       ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
+       if(elem1->type == ELEMFUNCRETURN){
+               str += processElementFunction((ElementFunction *) elem1, elemSig2);
+       }
+       str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
+       return str;
+}
+
+void Interpreter::writeToFile(string str){
+       if(!str.empty()){
+               output << str << endl;
+       }
+}
+
+bool Interpreter::getBooleanValue(Boolean *b){
+       return (bool)sigEnc.getValue(b);
+}
+
+uint64_t Interpreter::getValue(Element * element){
+       return (uint64_t)sigEnc.getValue(element);
+}
+
diff --git a/src/Interpreter/interpreter.h b/src/Interpreter/interpreter.h
new file mode 100644 (file)
index 0000000..32eed4a
--- /dev/null
@@ -0,0 +1,43 @@
+#ifndef INTERPRETER_H
+#define INTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "signature.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+class Interpreter{
+public:
+       Interpreter(CSolver *solver);
+       void encode();
+       int solve();
+       void writeToFile(string str);
+       uint64_t getValue(Element *element);
+       bool getBooleanValue(Boolean *element);
+       virtual ValuedSignature *getBooleanSignature(uint id) = 0;
+       virtual ValuedSignature *getElementSignature(uint id, Signature *ssig) = 0;
+       virtual Signature *getSetSignature(uint id, Set *set) = 0;
+       virtual ~Interpreter();
+protected:
+       virtual void dumpFooter() = 0;
+       virtual void dumpHeader() = 0;
+       uint getTimeout();
+       virtual void compileRunCommand(char * command, size_t size) = 0;
+       string encodeConstraint(BooleanEdge constraint);
+       virtual int getResult() = 0;
+       virtual string negateConstraint(string constr) = 0;
+       virtual void dumpAllConstraints(Vector<char *> &facts) = 0;
+       virtual string encodeBooleanLogic( BooleanLogic *bl) = 0;
+       virtual string encodeBooleanVar( BooleanVar *bv) = 0;
+       string encodePredicate( BooleanPredicate *bp);
+       string encodeOperatorPredicate(BooleanPredicate *constraint);
+       virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature) = 0;
+       virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) = 0;
+       CSolver *csolver;
+       SignatureEnc sigEnc;
+       ofstream output;
+};
+
+#endif
diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
new file mode 100644 (file)
index 0000000..ce95153
--- /dev/null
@@ -0,0 +1,59 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   smtsolvers.cc
+ * Author: hamed
+ * 
+ * Created on February 21, 2019, 12:26 PM
+ */
+
+#include "mathsatinterpreter.h"
+#include "solver_interface.h"
+
+MathSATInterpreter::MathSATInterpreter(CSolver *solver):
+       SMTInterpreter(solver)
+{      
+}
+
+void MathSATInterpreter::compileRunCommand(char * command , size_t size){
+       snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+MathSATInterpreter::~MathSATInterpreter(){
+}
+
+int MathSATInterpreter::getResult(){
+       ifstream input(SMTSOLUTIONFILE, ios::in);
+       string line;
+       while(getline(input, line)){
+               if(line.find("unsat")!= line.npos){
+                       return IS_UNSAT;
+               }
+               if(line.find("(") != line.npos){
+                       char cline [line.size()+1];
+                       strcpy ( cline, line.c_str() );
+                       char valuestr [512];
+                       uint id;
+                       if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){
+                               uint value;
+                               if (strcmp (valuestr, "true)") == 0 ){
+                                       value =1;
+                               }else if (strcmp(valuestr, "false)") == 0){
+                                       value = 0;
+                               }else {
+                                       ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
+                               }
+
+                               model_print("Signature%u = %u\n", id, value);
+                               sigEnc.setValue(id, value);
+                       } else {
+                               ASSERT(0);
+                       }
+               }
+       }
+       return IS_SAT;
+}
\ No newline at end of file
diff --git a/src/Interpreter/mathsatinterpreter.h b/src/Interpreter/mathsatinterpreter.h
new file mode 100644 (file)
index 0000000..ef2ec9f
--- /dev/null
@@ -0,0 +1,31 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   mathsatinterpreter.h
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 12:26 PM
+ */
+
+#ifndef MATHSATINTERPRETER_H
+#define MATHSATINTERPRETER_H
+
+#include "smtinterpreter.h"
+
+
+class MathSATInterpreter: public SMTInterpreter{
+public:
+       MathSATInterpreter(CSolver *solver);
+       virtual ~MathSATInterpreter();
+protected:
+       virtual void compileRunCommand(char * command , size_t size);
+       virtual int getResult();
+};
+
+
+#endif /* SMTSOLVERS_H */
+
diff --git a/src/Interpreter/signature.cc b/src/Interpreter/signature.cc
new file mode 100644 (file)
index 0000000..94efbb2
--- /dev/null
@@ -0,0 +1,21 @@
+#include "signature.h"
+#include "set.h"
+
+ValuedSignature::ValuedSignature(uint id): 
+       Signature(id), 
+       value(-1) 
+{
+}
+
+int ValuedSignature::getValue(){
+       ASSERT(value != -1);
+       return value;
+}
+
+string Signature::operator+(const string& str){
+       return toString() + str;
+}
+
+string operator+(const string& str, const Signature& sig){
+        return str + sig.toString();
+}
diff --git a/src/Interpreter/signature.h b/src/Interpreter/signature.h
new file mode 100644 (file)
index 0000000..e8c9e1c
--- /dev/null
@@ -0,0 +1,31 @@
+#ifndef SIGNATURE_H
+#define SIGNATURE_H
+#include <string>
+#include <iostream>
+#include "classlist.h"
+using namespace std;
+
+class Signature{
+public:
+       Signature(uint _id):id(_id){}
+       string operator+(const string& s);
+       virtual string toString() const = 0;
+       virtual string getAbsSignature() const =0;
+       virtual string getSignature() const =0;
+       virtual ~Signature(){}
+protected:
+       uint id;
+};
+
+class ValuedSignature: public Signature{
+public:
+       ValuedSignature(uint id);
+       int getValue();
+       void setValue(int v){value = v;}
+protected:
+       int value;
+};
+
+string operator+(const string& str, const Signature& sig);
+
+#endif
diff --git a/src/Interpreter/signatureenc.cc b/src/Interpreter/signatureenc.cc
new file mode 100644 (file)
index 0000000..cdc8aa1
--- /dev/null
@@ -0,0 +1,70 @@
+#include "signatureenc.h"
+#include "element.h"
+#include "set.h"
+#include "signature.h"
+#include "interpreter.h"
+
+SignatureEnc::SignatureEnc(Interpreter *inter): 
+       interpreter(inter),
+       maxValue(0)
+{
+}
+
+SignatureEnc::~SignatureEnc(){
+       for(uint i=0; i<signatures.getSize(); i++){
+               Signature *s = signatures.get(i);
+               delete s;
+       }
+}
+
+void SignatureEnc::updateMaxValue(Set *set){
+       for(uint i=0; i< set->getSize(); i++){
+               if(set->getElement(i) > maxValue){
+                       maxValue = set->getElement(i);
+               }
+       }
+}
+
+ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
+       ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar);
+       if(bsig == NULL){
+               bsig = interpreter->getBooleanSignature(getUniqueSigID());
+               encoded.put(bvar, bsig);
+               signatures.push(bsig);
+               interpreter->writeToFile(bsig->getSignature());
+       }
+       return bsig;
+}
+
+ValuedSignature *SignatureEnc::getElementSignature(Element *element){
+       ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element);
+       if(esig == NULL){
+               Set *set = element->getRange();
+               Signature *ssig = (Signature *)encoded.get((void *)set);
+               if(ssig == NULL){
+                       ssig = interpreter->getSetSignature(getUniqueSigID(), set);
+                       encoded.put(set, ssig);
+                       signatures.push(ssig);
+                       interpreter->writeToFile(ssig->getSignature());
+                       updateMaxValue(set);
+               }
+               esig = interpreter->getElementSignature(getUniqueSigID(), ssig);
+               encoded.put(element, esig);
+               signatures.push(esig);
+               interpreter->writeToFile(esig->getSignature());
+
+       }
+       return esig;
+}
+
+void SignatureEnc::setValue(uint id, uint value){
+       ValuedSignature *sig = getValuedSignature(id);
+       ASSERT(sig != NULL);
+       sig->setValue(value);
+}
+
+int SignatureEnc::getValue(void *astnode){
+       ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
+       ASSERT(sig != NULL);
+       return sig->getValue();
+}
diff --git a/src/Interpreter/signatureenc.h b/src/Interpreter/signatureenc.h
new file mode 100644 (file)
index 0000000..988ac71
--- /dev/null
@@ -0,0 +1,26 @@
+#ifndef SIGNATUREENC_H
+#define SIGNATUREENC_H
+
+#include "classlist.h"
+#include "structs.h"
+#include "cppvector.h"
+
+class SignatureEnc {
+public:
+       SignatureEnc(Interpreter *_interpreter);
+       ~SignatureEnc();
+       void setValue(uint id, uint value);
+       ValuedSignature *getElementSignature(Element *element);
+       ValuedSignature *getBooleanSignature(Boolean *bvar);
+       int getValue(void *astnode);
+       uint64_t getMaxValue(){ return maxValue;}
+private:
+       ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
+       uint getUniqueSigID(){return signatures.getSize() +1;}
+       void updateMaxValue(Set *set);
+       CloneMap encoded;
+       Vector<Signature*> signatures;
+       Interpreter *interpreter;
+       uint64_t maxValue;
+};
+#endif
diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc
new file mode 100644 (file)
index 0000000..82c887b
--- /dev/null
@@ -0,0 +1,208 @@
+#include "smtinterpreter.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "set.h"
+#include "function.h"
+#include "inc_solver.h"
+#include <fstream>
+#include "cppvector.h"
+#include "smtsig.h"
+
+using namespace std;
+
+SMTInterpreter::SMTInterpreter(CSolver *_solver): 
+       Interpreter(_solver) 
+{
+       output.open(SMTFILENAME);
+       if(!output.is_open()){
+               model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
+               exit(-1);
+       }
+}
+
+SMTInterpreter::~SMTInterpreter(){
+       if(output.is_open()){
+               output.close();
+       }
+}
+
+
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+       return new SMTBoolSig(id);
+}
+
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+       return new SMTElementSig(id, (SMTSetSig *)ssig);
+}
+
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+       return new SMTSetSig(id, set);
+}
+
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
+       for(uint i=0; i< facts.getSize(); i++){
+               char *cstr = facts.get(i);
+               writeToFile("(assert " + string(cstr) + ")");
+       }
+}
+
+void SMTInterpreter::extractValue(char *idline, char *valueline){
+       uint id;
+       if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+               char valuestr [512];
+               ASSERT(1 == sscanf(valueline,"%s)", valuestr));
+               uint value;
+               if (strcmp (valuestr, "true)") == 0 ){
+                       value =1;
+               }else if (strcmp(valuestr, "false)") == 0){
+                       value = 0;
+               }else {
+                       ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
+               }
+
+               model_print("Signature%u = %u\n", id, value);
+               sigEnc.setValue(id, value);
+       } else {
+               ASSERT(0);
+       }
+}
+
+int SMTInterpreter::getResult(){
+       ifstream input(SMTSOLUTIONFILE, ios::in);
+       string line;
+       while(getline(input, line)){
+               if(line.find("unsat")!= line.npos){
+                       return IS_UNSAT;
+               }
+               if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+                       string valueline;
+                       ASSERT(getline(input, valueline));
+                       char cline [line.size()+1];
+                       strcpy ( cline, line.c_str() );
+                       char vline [valueline.size()+1];
+                       strcpy ( vline, valueline.c_str() );
+                       extractValue(cline, vline);
+               }
+       }
+       return IS_SAT;
+}
+
+void SMTInterpreter::dumpFooter(){
+       output << "(check-sat)" << endl;
+       output << "(get-model)" << endl;
+}
+
+void SMTInterpreter::dumpHeader(){
+}
+
+void SMTInterpreter::compileRunCommand(char * command, size_t size){
+       snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+string SMTInterpreter::negateConstraint(string constr){
+       return "( not " + constr + " )";
+}
+
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+       uint size = bl->inputs.getSize();
+       string array[size];
+       for (uint i = 0; i < size; i++)
+               array[i] = encodeConstraint(bl->inputs.get(i));
+       string op;
+       switch (bl->op){
+               case SATC_OR:
+                       op = "or";
+                       break;
+               case SATC_AND:
+                       op = "and";
+                       break;
+               case SATC_NOT:
+                       op = "not";
+                       break;
+               case SATC_IMPLIES:
+                       op = "=>";
+                       break;
+               case SATC_XOR:
+               default:
+                       ASSERT(0);
+       }
+       switch (bl->op) {
+               case SATC_XOR:
+               case SATC_OR:
+               case SATC_AND:{
+                       ASSERT(size >= 2);
+                       string res = array[0];
+                       for( uint i=1; i< size; i++){
+                               res = "( " + op + " " + res + " " +  array[i] + " )";
+                       }
+                       return res;
+               }
+               case SATC_NOT:{
+                       return "( not " + array[0] + " )";
+               }
+               case SATC_IMPLIES:
+                       return "( " + op + " " + array[0] + " " + array[1] + " )";
+               case SATC_IFF:
+               default:
+                       ASSERT(0);
+
+       }
+}
+
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
+       ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+       return *boolSig + "";
+}
+
+string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+       FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
+       uint numDomains = elemFunc->inputs.getSize();
+       ASSERT(numDomains > 1);
+       ValuedSignature *inputs[numDomains];
+       string result;
+       for (uint i = 0; i < numDomains; i++) {
+               Element *elem = elemFunc->inputs.get(i);
+               inputs[i] = sigEnc.getElementSignature(elem);
+               if(elem->type == ELEMFUNCRETURN){
+                       result += processElementFunction((ElementFunction *) elem, inputs[i]);
+               }
+       }
+       string op;
+       switch(function->op){
+               case SATC_ADD:
+                       op = "+";
+                       break;
+               case SATC_SUB:
+                       op = "-";
+                       break;
+               default:
+                       ASSERT(0);
+       }
+       result += "( = " + *signature; 
+       string tmp = "" + *inputs[0];
+       for (uint i = 1; i < numDomains; i++) {
+               tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
+       }
+       result += tmp + " )";
+       return result;
+}
+
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+       switch (op) {
+               case SATC_EQUALS:
+                       return "( = " + *elemSig1 + " " + *elemSig2 +" )";
+               case SATC_LT:
+                       return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+               case SATC_GT:
+                       return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+               default:
+                       ASSERT(0);
+       }
+}
+
+
diff --git a/src/Interpreter/smtinterpreter.h b/src/Interpreter/smtinterpreter.h
new file mode 100644 (file)
index 0000000..035e76b
--- /dev/null
@@ -0,0 +1,34 @@
+#ifndef SMTINTERPRETER_H
+#define SMTINTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+#define SMTFILENAME "satune.smt"
+#define SMTSOLUTIONFILE "solution.sol"
+
+class SMTInterpreter: public Interpreter{
+public:
+       SMTInterpreter(CSolver *solver);
+       virtual ValuedSignature *getBooleanSignature(uint id);
+       virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
+       virtual Signature *getSetSignature(uint id, Set *set);
+       virtual ~SMTInterpreter();
+protected:
+       virtual void dumpFooter();
+       virtual void dumpHeader();
+       virtual void compileRunCommand(char * command , size_t size);
+       virtual int getResult();
+       virtual void dumpAllConstraints(Vector<char *> &facts);
+       virtual string negateConstraint(string constr);
+       virtual string encodeBooleanLogic( BooleanLogic *bl);
+       virtual string encodeBooleanVar( BooleanVar *bv);
+       virtual void extractValue(char *idline, char *valueline);
+       virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
+       virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
+};
+
+#endif
diff --git a/src/Interpreter/smtratinterpreter.cc b/src/Interpreter/smtratinterpreter.cc
new file mode 100644 (file)
index 0000000..ebe5113
--- /dev/null
@@ -0,0 +1,26 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   smtratinterpreter.cc
+ * Author: hamed
+ * 
+ * Created on February 21, 2019, 2:33 PM
+ */
+
+#include "smtratinterpreter.h"
+
+SMTRatInterpreter::SMTRatInterpreter(CSolver *solver): 
+       SMTInterpreter(solver)
+{      
+}
+
+void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
+       snprintf(command, size, "timeout %u ./smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+}
+
+SMTRatInterpreter::~SMTRatInterpreter(){
+}
diff --git a/src/Interpreter/smtratinterpreter.h b/src/Interpreter/smtratinterpreter.h
new file mode 100644 (file)
index 0000000..f2afb49
--- /dev/null
@@ -0,0 +1,27 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   smtratinterpreter.h
+ * Author: hamed
+ *
+ * Created on February 21, 2019, 2:33 PM
+ */
+
+#ifndef SMTRATINTERPRETER_H
+#define SMTRATINTERPRETER_H
+#include "smtinterpreter.h"
+
+class SMTRatInterpreter: public SMTInterpreter{
+public:
+       SMTRatInterpreter(CSolver *solver);
+       virtual ~SMTRatInterpreter();
+protected:
+       void compileRunCommand(char * command , size_t size);
+};
+
+#endif /* SMTRATINTERPRETER_H */
+
diff --git a/src/Interpreter/smtsig.cc b/src/Interpreter/smtsig.cc
new file mode 100644 (file)
index 0000000..4c77493
--- /dev/null
@@ -0,0 +1,81 @@
+#include "smtsig.h"
+#include "set.h"
+
+SMTBoolSig::SMTBoolSig(uint id):
+       ValuedSignature(id)
+{
+}
+
+string SMTBoolSig::toString() const{
+       return "b" + to_string(id);
+}
+
+string SMTBoolSig::getSignature() const{
+       return "(declare-const b" + to_string(id) + " Bool)";
+}
+
+string SMTBoolSig::getAbsSignature() const{
+       return "";
+}
+
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig): 
+       ValuedSignature(id),
+       ssig(_ssig)
+{
+}
+
+string SMTElementSig::toString() const{
+       return "e" + to_string(id);
+}
+
+string SMTElementSig::getSignature() const{
+       string str = "(declare-const e" + to_string(id) + " Int)\n";
+       string constraint = ssig->getAbsSignature();
+       size_t start_pos;
+       string placeholder = "$";
+       while((start_pos = constraint.find(placeholder)) != string::npos){
+               constraint.replace(start_pos, placeholder.size(), to_string(id));
+       }
+       //constraint.replace(constraint.begin(), constraint.end(), "$", );
+       str += constraint;
+       return str;
+}
+
+string SMTElementSig::getAbsSignature() const{
+       return "";
+       
+}
+
+SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+       ASSERT(set->getSize() > 0);
+       int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+       Vector<int> holes;
+       int prev = set->getElement(0);
+       for(uint i=1; i< set->getSize(); i++){
+               int curr = set->getElement(i);
+               if(prev != curr -1){
+                       for(int j=prev+1; j< curr; j++){
+                               holes.push(j);
+                       }
+               }
+               prev = curr;
+       }
+       constraint = "(assert (<= e$ " + to_string(max) +"))\n";
+       constraint += "(assert (>= e$ " + to_string(min) +"))\n";
+       for(uint i=0; i< holes.getSize(); i++){
+               constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+       }
+}
+
+string SMTSetSig::toString() const{
+       return "";
+}
+
+string SMTSetSig::getSignature() const{
+       return "";
+}
+
+string SMTSetSig::getAbsSignature() const{
+       return constraint;
+       
+}
diff --git a/src/Interpreter/smtsig.h b/src/Interpreter/smtsig.h
new file mode 100644 (file)
index 0000000..7804176
--- /dev/null
@@ -0,0 +1,40 @@
+#ifndef SMTSIG_H
+#define SMTSIG_H
+#include <string>
+#include <iostream>
+#include "signature.h"
+#include "classlist.h"
+using namespace std;
+
+class SMTBoolSig: public ValuedSignature{
+public:
+       SMTBoolSig(uint id);
+       virtual ~SMTBoolSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+};
+
+class SMTSetSig: public Signature{
+public:
+       SMTSetSig(uint id, Set *set);
+       virtual ~SMTSetSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+private:
+       string constraint;
+};
+
+class SMTElementSig: public ValuedSignature{
+public:
+       SMTElementSig(uint id, SMTSetSig *ssig);
+       virtual ~SMTElementSig(){}
+       virtual string toString() const;
+       virtual string getAbsSignature() const;
+       virtual string getSignature() const;
+private:
+       SMTSetSig *ssig;
+};
+
+#endif
index 838a478..29627f4 100644 (file)
@@ -4,17 +4,17 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard Interpreter/*.cc)
 
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard Interpreter/*.c)
 
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard Interpreter/*.h)
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -O0 -g
 CXXFLAGS := -std=c++1y -pthread
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter
 LDFLAGS := -ldl -lrt -rdynamic -g
 SHARED := -shared
 
@@ -44,6 +44,7 @@ ${OBJ_DIR}:
        ${MKDIR_P} ${OBJ_DIR}/Backend
        ${MKDIR_P} ${OBJ_DIR}/Encoders
        ${MKDIR_P} ${OBJ_DIR}/Serialize
+       ${MKDIR_P} ${OBJ_DIR}/Interpreter
 
 debug: CFLAGS += -DCONFIG_DEBUG
 debug: all
index 548619f..eac11e9 100644 (file)
@@ -17,7 +17,7 @@
 
 #define READBUFFERSIZE 16384
 
-Deserializer::Deserializer(const char *file) :
+Deserializer::Deserializer(const char *file, InterpreterType itype) :
        buffer((char *) ourmalloc(READBUFFERSIZE)),
        bufferindex(0),
        bufferbytes(0),
@@ -29,6 +29,9 @@ Deserializer::Deserializer(const char *file) :
        if (filedesc < 0) {
                exit(-1);
        }
+       if(itype != SATUNE){
+               solver->setInterpreter(itype);
+       }
 }
 
 Deserializer::~Deserializer() {
@@ -153,8 +156,8 @@ void Deserializer::deserializeBooleanConst() {
        myread(&b, sizeof(BooleanVar *));
        bool istrue;
        myread(&istrue, sizeof(bool));
-       map.put(b, istrue?solver->getBooleanTrue().getBoolean():
-                       solver->getBooleanFalse().getBoolean());
+       map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
+                                       solver->getBooleanFalse().getBoolean());
 }
 
 void Deserializer::deserializeBooleanOrder() {
index 81baeef..1a93674 100644 (file)
@@ -19,7 +19,7 @@
  */
 class Deserializer {
 public:
-       Deserializer(const char *file);
+       Deserializer(const char *file, InterpreterType itype = SATUNE);
        CSolver *deserialize();
        virtual ~Deserializer();
 private:
diff --git a/src/Test/analyzemultituner.cc b/src/Test/analyzemultituner.cc
new file mode 100644 (file)
index 0000000..effe965
--- /dev/null
@@ -0,0 +1,18 @@
+#include "csolver.h"
+#include "comptuner.h"
+#include "searchtuner.h"
+
+int main(int argc, char **argv) {
+       if (argc < 2) {
+               printf("You should specify number of runs\n");
+               exit(-1);
+       }
+       uint numruns;
+       sscanf(argv[1], "%u", &numruns);
+
+       CompTuner *multituner = new CompTuner(0, 0);
+       multituner->readData(numruns);
+       multituner->findBestThreeTuners();
+       delete multituner;
+       return 0;
+}
diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
new file mode 100644 (file)
index 0000000..cef60f4
--- /dev/null
@@ -0,0 +1,42 @@
+#include "csolver.h"
+
+
+InterpreterType getInterpreterType(char * itype){
+       if(strcmp (itype,"--alloy") == 0){
+               return ALLOY;
+       } else if(strcmp (itype,"--z3") == 0){
+               return Z3;
+       } else if(strcmp (itype,"--smtrat") == 0){
+               return SMTRAT;
+       } else if(strcmp (itype,"--mathsat") == 0){
+               return MATHSAT;
+       } else {
+               printf("Unknown interpreter type: %s\n", itype);
+               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+               exit(-1);
+       }
+}
+
+int main(int argc, char **argv) {
+       printf("%d\n", argc);
+       if (argc != 2 && argc != 3) {
+               printf("You only specify the name of the file ...\n");
+               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+               exit(-1);
+       }
+       CSolver *solver; 
+       if(argc == 3){
+               solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
+       } else {
+               solver = CSolver::deserialize(argv[1]);
+       }
+       int value = solver->solve();
+       if (value == 1) {
+               printf("%s is SAT\n", argv[1]);
+       } else {
+               printf("%s is UNSAT\n", argv[1]);
+       }
+       delete solver;
+       return 1;
+
+}
diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc
deleted file mode 100644 (file)
index c8d35c9..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "csolver.h"
-
-
-int main(int argc, char **argv) {
-       if (argc != 2) {
-               printf("You only specify the name of the file ...");
-               exit(-1);
-       }
-       CSolver *solver = CSolver::deserialize(argv[1]);
-       solver->printConstraints();
-       delete solver;
-       return 1;
-
-}
diff --git a/src/Test/deserializerun.cc b/src/Test/deserializerun.cc
new file mode 100644 (file)
index 0000000..bbfaab5
--- /dev/null
@@ -0,0 +1,33 @@
+#include "csolver.h"
+#include "searchtuner.h"
+#include <stdlib.h>
+#include <iostream>
+#include <fstream>
+
+int main(int argc, char **argv) {
+       if (argc != 5) {
+               printf("You only specify the name of the file ...");
+               exit(-1);
+       }
+       char buffer[512];
+       CSolver *solver = CSolver::deserialize(argv[1]);
+       uint timeout;
+       sscanf(argv[2], "%u", &timeout);
+       SearchTuner *tuner = new SearchTuner(argv[3]);
+       solver->setTuner(tuner);
+       solver->setSatSolverTimeout(timeout);
+       int sat = solver->solve();
+       long long metric = solver->getElapsedTime();
+       ofstream myfile;
+       myfile.open (argv[4], ios::out | ios::trunc);
+       myfile << metric << endl;
+       myfile << sat << endl;
+       myfile.close();
+       //serialize out the tuner we used
+       snprintf(buffer, sizeof(buffer), "%sused", argv[3]);
+       tuner->serializeUsed(buffer);
+
+       delete solver;
+       delete tuner;
+       return 0;
+}
diff --git a/src/Test/printtuner.cc b/src/Test/printtuner.cc
new file mode 100644 (file)
index 0000000..8a3ccbd
--- /dev/null
@@ -0,0 +1,15 @@
+#include "csolver.h"
+#include "comptuner.h"
+#include "searchtuner.h"
+
+int main(int argc, char **argv) {
+       if (argc < 2) {
+               printf("You should specify a tuner: %s <best.tuner>\n", argv[0]);
+               exit(-1);
+       }
+       
+       SearchTuner *tuner = new SearchTuner(argv[1]);
+       tuner->print();
+       delete tuner;
+       return 0;
+}
index e74b557..870ba15 100755 (executable)
@@ -1,9 +1,10 @@
 #!/bin/bash
 
+export CLASSPATH=../bin/original.jar:.:$CLASSPATH
 export LD_LIBRARY_PATH=../bin
 # For Mac OSX
 export DYLD_LIBRARY_PATH=../bin
 # For sat_solver
 export PATH=.:$PATH
-
+echo $@
 $@
diff --git a/src/Test/runmultituner.cc b/src/Test/runmultituner.cc
new file mode 100644 (file)
index 0000000..e2ecbd8
--- /dev/null
@@ -0,0 +1,61 @@
+#include "csolver.h"
+#include "searchtuner.h"
+#include "kmeanstuner.h"
+#include "satuner.h"
+#include "comptuner.h"
+#include "randomtuner.h"
+
+void printKnownTunerTypes(){
+       printf("Known Tuner Types:\nRandom Tuner=1\nComp Tuner=2\nKmeans Tuner=3\nSimulated Annealing Tuner=4\n");
+}
+
+BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout){
+       switch(tunertype){
+               case 1: return new RandomTuner(budget, timeout);
+               case 2: return new CompTuner(budget, timeout);
+               case 3: return new KMeansTuner(budget, rounds, timeout);
+               case 4: return new SATuner(budget, timeout);
+               default:
+                       printf("Tuner type %u is unknown\n", tunertype);
+                       printKnownTunerTypes();
+                       exit(-1);
+       }
+
+}
+
+int main(int argc, char **argv) {
+       if (argc < 8) {
+               printf("You should specify: %s TunerType budget rounds timeout problemfilenames - tunerfilenames\n", argv[0]);
+               printKnownTunerTypes();
+               exit(-1);
+       }
+       uint tunertype;
+       uint budget;
+       uint rounds;
+       uint timeout;
+       sscanf(argv[1], "%u", &tunertype);
+       sscanf(argv[2], "%u", &budget);
+       sscanf(argv[3], "%u", &rounds);
+       sscanf(argv[4], "%u", &timeout);
+
+       BasicTuner *multituner = createTuner(tunertype, budget, rounds, timeout);
+       bool tunerfiles = false;
+       for (int i = 5; i < argc; i++) {
+               if (!tunerfiles) {
+                       if (argv[i][0] == '-' && argv[i][1] == 0)
+                               tunerfiles = true;
+                       else
+                               multituner->addProblem(argv[i]);
+               } else
+                       multituner->addTuner(new SearchTuner(argv[i], true )); //add settings to usedsettigs
+       }
+
+       if (!tunerfiles) {
+               printf("You should specify %s budget rounds timeout problemfilenames - tunerfilenames", argv[0]);
+               exit(-1);
+       }
+
+       multituner->tune();
+       delete multituner;
+       return 0;
+}
diff --git a/src/Test/serializestatictuner.cc b/src/Test/serializestatictuner.cc
new file mode 100644 (file)
index 0000000..6c45511
--- /dev/null
@@ -0,0 +1,26 @@
+#include "csolver.h"
+#include "searchtuner.h"
+#include "tunable.h"
+#include <stdlib.h>
+
+int main(int argc, char **argv) {
+       SearchTuner *elem_bin = new SearchTuner();
+       SearchTuner *elem_onehot = new SearchTuner();
+       SearchTuner *elem_unary = new SearchTuner();
+       elem_bin->setTunable(NAIVEENCODER, &NaiveEncodingDesc, BINARYINDEX);
+       elem_onehot->setTunable(NAIVEENCODER, &NaiveEncodingDesc, ONEHOT);
+       elem_unary->setTunable(NAIVEENCODER, &NaiveEncodingDesc, UNARY);
+
+       elem_bin->serialize("binarytuner.conf");
+       elem_onehot->serialize("onehottuner.conf");
+       elem_unary->serialize("unarytuner.conf");
+       elem_bin->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+       elem_onehot->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+       elem_unary->setTunable(ENCODINGGRAPHOPT, &onoff, 1);
+       elem_bin->serialize("circuitbinarytuner.conf");
+       elem_onehot->serialize("circuitonehottuner.conf");
+       elem_unary->serialize("circuitunarytuner.conf");
+       delete elem_bin;
+       delete elem_onehot;
+       delete elem_unary;
+}
diff --git a/src/Test/tunerrun.cc b/src/Test/tunerrun.cc
new file mode 100644 (file)
index 0000000..40a0960
--- /dev/null
@@ -0,0 +1,33 @@
+#include "csolver.h"
+#include "serializetuner.h"
+#include <stdlib.h>
+#include <iostream>
+#include <fstream>
+
+int main(int argc, char **argv) {
+       if (argc != 5) {
+               printf("You only specify the name of the file ...");
+               exit(-1);
+       }
+       char buffer[512];
+       CSolver *solver = CSolver::deserialize(argv[1]);
+       uint timeout;
+       sscanf(argv[2], "%u", &timeout);
+       SerializeTuner *tuner = new SerializeTuner(argv[3]);
+       solver->setTuner(tuner);
+       solver->setSatSolverTimeout(timeout);
+       int sat = solver->solve();
+       long long metric = solver->getElapsedTime();
+       ofstream myfile;
+       myfile.open (argv[4], ios::out | ios::trunc);
+       myfile << metric << endl;
+       myfile << sat << endl;
+       myfile.close();
+       //serialize out the tuner we used
+       snprintf(buffer, sizeof(buffer), "%sused", argv[3]);
+       tuner->serializeUsed(buffer);
+
+       delete solver;
+       delete tuner;
+       return 0;
+}
index 857b21c..1bf29d8 100644 (file)
@@ -11,6 +11,8 @@ AutoTuner::AutoTuner(uint _budget) :
        budget(_budget), result(UNSETVALUE) {
 }
 
+AutoTuner::~AutoTuner() {}
+
 void AutoTuner::addProblem(CSolver *solver) {
        solvers.push(solver);
 }
@@ -55,14 +57,6 @@ SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
        return newTuner;
 }
 
-#ifdef STATICENCGEN
-SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner) {
-       SearchTuner *newTuner = oldTuner->copyUsed();
-       result = newTuner->nextStaticTuner();
-       return result==EXIT_FAILURE? newTuner: NULL;
-}
-#endif
-
 void AutoTuner::tune() {
        SearchTuner *bestTuner = NULL;
        double bestScore = DBL_MAX;
@@ -71,20 +65,6 @@ void AutoTuner::tune() {
        double base_temperature = evaluateAll(oldTuner);
        double oldScore = base_temperature;
 
-#ifdef STATICENCGEN
-       while(true){
-               SearchTuner *newTuner = mutateTuner(oldTuner);
-               if(newTuner == NULL)
-                       return;
-               double newScore = evaluateAll(newTuner);
-               newTuner->printUsed();
-               model_print("Received score %f\n", newScore);
-               delete oldTuner;
-               oldScore = newScore;
-               oldTuner = newTuner;
-       }
-#endif
-       
        for (uint i = 0; i < budget; i++) {
                SearchTuner *newTuner = mutateTuner(oldTuner, i);
                double newScore = evaluateAll(newTuner);
@@ -116,7 +96,7 @@ void AutoTuner::tune() {
        }
        model_print("Best tuner:\n");
        bestTuner->print();
-       bestTuner->serialize();
+       bestTuner->serialize("TUNER.conf");
        model_print("Received score %f\n", bestScore);
        if (bestTuner != NULL)
                delete bestTuner;
index ed276ee..e9c7b40 100644 (file)
@@ -9,16 +9,14 @@
 class AutoTuner {
 public:
        AutoTuner(uint budget);
+       virtual ~AutoTuner();
        void addProblem(CSolver *solver);
-       void tune();
+       virtual void tune();
        CMEMALLOC;
-private:
+protected:
        long long evaluate(CSolver *problem, SearchTuner *tuner);
        double evaluateAll(SearchTuner *tuner);
        SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
-#ifdef STATICENCGEN
-       SearchTuner *mutateTuner(SearchTuner *oldTuner);
-#endif
        Vector<CSolver *> solvers;
        uint budget;
        int result;
diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc
new file mode 100644 (file)
index 0000000..889b543
--- /dev/null
@@ -0,0 +1,227 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   basictuner.cc
+ * Author: hamed
+ * 
+ * Created on December 17, 2018, 2:02 PM
+ */
+
+#include "basictuner.h"
+#include "common.h"
+#include "csolver.h"
+#include "searchtuner.h"
+#include <stdlib.h>
+#include <string.h>
+#include <iostream>
+#include <fstream>
+
+Problem::Problem(const char *_problem) :
+       problemnumber(-1),
+       result(TUNERUNSETVALUE),
+       besttime(LLONG_MAX)
+{
+       uint len = strlen(_problem);
+       problem = (char *) ourmalloc(len + 1);
+       memcpy(problem, _problem, len + 1);
+}
+
+Problem::~Problem() {
+       ourfree(problem);
+}
+
+void TunerRecord::setTime(Problem *problem, long long time) {
+       timetaken.put(problem, time);
+}
+
+void TunerRecord::print(){
+       model_print("*************TUNER NUMBER=%d***********\n", tunernumber);
+       tuner->print();
+       model_print("&&&&&&&&&&&&&USED SETTINGS &&&&&&&&&&&&\n");
+       tuner->printUsed();
+       model_print("\n");
+}
+
+void TunerRecord::printProblemsInfo(){
+       for (uint j = 0; j < problems.getSize(); j++) {
+               Problem *problem = problems.get(j);
+               model_print("Problem %s\n", problem->getProblem());
+               model_print("Time = %lld\n", getTime(problem));
+       }
+}
+
+long long TunerRecord::getTime(Problem *problem) {
+       if (timetaken.contains(problem))
+               return timetaken.get(problem);
+       else return -1;
+}
+
+TunerRecord *TunerRecord::changeTuner(SearchTuner *_newtuner) {
+       TunerRecord *tr = new TunerRecord(_newtuner);
+       for (uint i = 0; i < problems.getSize(); i++) {
+               tr->problems.push(problems.get(i));
+       }
+       return tr;
+}
+
+
+BasicTuner::BasicTuner(uint _budget, uint _timeout) :
+       budget(_budget), timeout(_timeout), execnum(0){
+}
+
+BasicTuner::~BasicTuner() {
+       for (uint i = 0; i < problems.getSize(); i++)
+               ourfree(problems.get(i));
+       for (uint i = 0; i < allTuners.getSize(); i++)
+               delete allTuners.get(i);
+}
+
+void BasicTuner::addProblem(const char *filename) {
+       Problem *p = new Problem(filename);
+       p->setProblemNumber(problems.getSize());
+       problems.push(p);
+}
+
+void BasicTuner::printData() {
+       model_print("*********** DATA DUMP ***********\n");
+       for (uint i = 0; i < allTuners.getSize(); i++) {
+               TunerRecord *tuner = allTuners.get(i);
+               SearchTuner *stun = tuner->getTuner();
+               model_print("Tuner %u\n", i);
+               stun->print();
+               model_print("----------------------------------\n\n\n");
+               for (uint j = 0; j < tuner->problemsSize(); j++) {
+                       Problem *problem = tuner->getProblem(j);
+                       model_print("Problem %s\n", problem->getProblem());
+                       model_print("Time = %lld\n", tuner->getTime(problem));
+               }
+       }
+}
+
+bool BasicTuner::tunerExists(TunerRecord *tunerec){
+       SearchTuner *tuner = tunerec->getTuner();
+       for(uint i=0; i< explored.getSize(); i++){
+               if(explored.get(i)->getTuner()->equalUsed(tuner)){
+                       model_print("************Tuner <%d> is replicate of Tuner <%d>\n", tunerec->getTunerNumber(), explored.get(i)->getTunerNumber());
+                       return true;
+               }
+       }
+       return false;
+}
+
+void BasicTuner::addTuner(SearchTuner *tuner) {
+       TunerRecord *t = new TunerRecord(tuner);
+       tuners.push(t);
+       t->setTunerNumber( allTuners.getSize() );
+       allTuners.push(t);
+}
+
+long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
+       char buffer[512];
+       {
+               snprintf(buffer, sizeof(buffer), "problem%u", execnum);
+
+               ofstream myfile;
+               myfile.open (buffer, ios::out);
+
+
+               if (myfile.is_open()) {
+                       myfile << problem->getProblem() << endl;
+                       myfile << problem->getProblemNumber() << endl;
+                       myfile.close();
+               }
+       }
+
+       {
+               snprintf(buffer, sizeof(buffer), "tunernum%u", execnum);
+
+               ofstream myfile;
+               myfile.open (buffer, ios::out);
+
+
+               if (myfile.is_open()) {
+                       myfile << tuner->getTunerNumber() << endl;
+                       myfile.close();
+               }
+       }
+
+       //Write out the tuner
+       snprintf(buffer, sizeof(buffer), "tuner%u", execnum);
+       tuner->getTuner()->serialize(buffer);
+
+       //compute timeout
+       uint timeinsecs = problem->getBestTime() / NANOSEC;
+       uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
+       uint maxtime = (adaptive < timeout) ? adaptive : timeout;
+
+       //Do run
+       snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), maxtime, execnum, execnum, execnum);
+       int status = system(buffer);
+
+       long long metric = -1;
+       int sat = IS_INDETER;
+
+       if (status == 0) {
+               //Read data in from results file
+               snprintf(buffer, sizeof(buffer), "result%u", execnum);
+
+               ifstream myfile;
+               myfile.open (buffer, ios::in);
+
+
+               if (myfile.is_open()) {
+                       myfile >> metric;
+                       myfile >> sat;
+                       myfile.close();
+               }
+               updateTimeout(problem, metric);
+               snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
+               tuner->getTuner()->addUsed(buffer);
+       }
+       //Increment execution count
+       execnum++;
+
+       if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
+               problem->setResult( sat );
+       } else if (problem->getResult() != sat && sat != IS_INDETER) {
+               model_print("******** Result has changed ********\n");
+       }
+       if (sat == IS_INDETER && metric != -1) {//The case when we have a timeout
+               metric = -1;
+       }
+       return metric;
+}
+
+SearchTuner *BasicTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
+       SearchTuner *newTuner = oldTuner->copyUsed();
+       uint numSettings = oldTuner->getSize();
+       uint settingsToMutate = (uint)(AUTOTUNERFACTOR * (((double)numSettings) * (budget - k)) / (budget));
+       if (settingsToMutate < 1)
+               settingsToMutate = 1;
+       model_print("Mutating %u settings\n", settingsToMutate);
+       while (settingsToMutate-- != 0) {
+               newTuner->randomMutate();
+       }
+       return newTuner;
+}
+
+int BasicTuner::subTunerIndex(SearchTuner *newTuner){
+       for (uint i=0; i< explored.getSize(); i++){
+               SearchTuner *tuner = explored.get(i)->getTuner();
+               if(tuner->isSubTunerof(newTuner)){
+                       return i;
+               }
+       }
+       return -1;
+}
+
+
+void BasicTuner::updateTimeout(Problem *problem, long long metric) {
+       if (metric < problem->getBestTime()) {
+               problem->setBestTime( metric );
+       }
+}
diff --git a/src/Tuner/basictuner.h b/src/Tuner/basictuner.h
new file mode 100644 (file)
index 0000000..14ab7d8
--- /dev/null
@@ -0,0 +1,102 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   basictuner.h
+ * Author: hamed
+ *
+ * Created on December 17, 2018, 2:02 PM
+ */
+
+#ifndef BASICTUNER_H
+#define BASICTUNER_H
+#include "mymemory.h"
+#include "classlist.h"
+#include "cppvector.h"
+#include "hashtable.h"
+
+#define TUNERUNSETVALUE -1
+#define AUTOTUNERFACTOR 0.3
+
+class Problem {
+public:
+       Problem(const char *problem);
+       char *getProblem() {return problem;}
+       inline int getResult(){return result;}
+       inline int getProblemNumber(){return problemnumber;}
+       inline void setResult(int res){result = res;}
+       inline void setProblemNumber(int probNum){problemnumber = probNum;}
+       inline long long getBestTime() {return besttime ;} 
+       inline void setBestTime(long long time) {besttime = time;}
+       ~Problem();
+       CMEMALLOC;
+private:
+       int problemnumber;
+       int result;
+       char *problem;
+       long long besttime;
+};
+
+class TunerRecord {
+public:
+       TunerRecord(SearchTuner *_tuner) : tuner(_tuner), tunernumber(-1), isduplicate(false) {}
+       TunerRecord(SearchTuner *_tuner, int _tunernumber) : tuner(_tuner), tunernumber(_tunernumber), isduplicate(false) {}
+       SearchTuner *getTuner() {return tuner;}
+       void inline addProblem(Problem * problem){problems.push(problem);}
+       TunerRecord *changeTuner(SearchTuner *_newtuner);
+       void updateTuner(SearchTuner *_newtuner) {tuner = _newtuner;}
+       long long getTime(Problem *problem);
+       void setTime(Problem *problem, long long time);
+       inline void setTunerNumber(int numb){tunernumber = numb;}
+       inline int getTunerNumber(){return tunernumber;}
+       inline uint problemsSize() {return problems.getSize();}
+       inline void setDuplicate(bool _duplicate) { isduplicate = _duplicate;}
+       inline bool isDuplicate() {return isduplicate;}
+       inline Problem *getProblem(uint index){return problems.get(index);}
+        void print();
+       void printProblemsInfo();
+       CMEMALLOC;
+private:
+       SearchTuner *tuner;
+       Vector<Problem *> problems;
+       Hashtable<Problem *, long long, uint64_t> timetaken;
+       int tunernumber;
+       friend void clearVector(Vector<TunerRecord *> *tunerV);
+       bool isduplicate;
+};
+
+class BasicTuner {
+public:
+       BasicTuner(uint _budget, uint _timeout);
+       void addProblem(const char *filename);
+       void addTuner(SearchTuner *tuner);
+       void printData();
+       virtual ~BasicTuner();
+       virtual void tune() = 0;
+       CMEMALLOC;
+protected:
+       long long evaluate(Problem *problem, TunerRecord *tuner);
+       /**
+         * returns the index of the tuner which is subtune of
+         * the newTuner 
+         * @param newTuner
+         * @return 
+         */
+        int subTunerIndex(SearchTuner *newTuner);
+       bool tunerExists(TunerRecord *tunerRec);
+       SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
+       void updateTimeout(Problem *problem, long long metric);
+       Vector<TunerRecord *> allTuners;
+       Vector<TunerRecord *> explored;
+       Vector<Problem *> problems;
+       Vector<TunerRecord *> tuners;
+       uint budget;
+       uint timeout;
+       int execnum;
+};
+
+#endif /* BASICTUNER_H */
+
diff --git a/src/Tuner/comptuner.cc b/src/Tuner/comptuner.cc
new file mode 100644 (file)
index 0000000..895e06b
--- /dev/null
@@ -0,0 +1,236 @@
+#include "comptuner.h"
+#include <float.h>
+#include <math.h>
+#include "searchtuner.h"
+#include <iostream>
+#include <fstream>
+#include "solver_interface.h"
+
+CompTuner::CompTuner(uint _budget, uint _timeout) :
+       BasicTuner(_budget, _timeout)
+{
+}
+
+CompTuner::~CompTuner(){
+       
+}
+
+void CompTuner::findBestThreeTuners() {
+       if (allTuners.getSize() < 3) {
+               printData();
+               return;
+       }
+       TunerRecord *bestTuners[3];
+       double score = DBL_MAX;
+       for (uint i = 0; i < allTuners.getSize() - 2; i++) {
+               for (uint j = i + 1; j < allTuners.getSize() - 1; j++) {
+                       for (uint k = j + 1; k < allTuners.getSize(); k++) {
+                               TunerRecord *tuner1 = allTuners.get(i);
+                               TunerRecord *tuner2 = allTuners.get(j);
+                               TunerRecord *tuner3 = allTuners.get(k);
+                               double mintimes[problems.getSize()];
+                               for (uint l = 0; l < problems.getSize(); l++) {
+                                       Problem *problem = problems.get(l);
+                                       mintimes[l] = pow(min(tuner1->getTime(problem), tuner2->getTime(problem), tuner3->getTime(problem)), (double)1 / problems.getSize());
+                               }
+                               double result = 1;
+                               for (uint l = 0; l < problems.getSize(); l++) {
+                                       result *= mintimes[l];
+                               }
+                               if (result < score) {
+                                       score = result;
+                                       bestTuners[0] = tuner1;
+                                       bestTuners[1] = tuner2;
+                                       bestTuners[2] = tuner3;
+                               }
+                       }
+               }
+       }
+       model_print("Best 3 tuners:\n");
+       for (uint i = 0; i < 3; i++) {
+               TunerRecord *tuner = bestTuners[i];
+               SearchTuner *stun = tuner->getTuner();
+               char buffer[512];
+               snprintf(buffer, sizeof(buffer), "best%u.tuner", i);
+               stun->serialize(buffer);
+               model_print("Tuner %u\n", tuner->getTunerNumber());
+               stun->print();
+               tuner->printProblemsInfo();
+               model_print("----------------------------------\n\n\n");
+       }
+}
+
+void CompTuner::readData(uint numRuns) {
+       for (uint i = 0; i < numRuns; i++) {
+               ifstream myfile;
+               char buffer[512];
+               uint tunernumber;
+               snprintf(buffer, sizeof(buffer), "tunernum%u", i);
+               myfile.open (buffer, ios::in);
+               myfile >> tunernumber;
+               myfile.close();
+               if (allTuners.getSize() <= tunernumber)
+                       allTuners.setSize(tunernumber + 1);
+               if (allTuners.get(tunernumber) == NULL) {
+                       snprintf(buffer, sizeof(buffer), "tuner%u", i);
+                       allTuners.set(tunernumber, new TunerRecord(new SearchTuner(buffer), tunernumber));
+               }
+               //Add any new used records
+               snprintf(buffer, sizeof(buffer), "tuner%uused", i);
+               TunerRecord *tuner = allTuners.get(tunernumber);
+               tuner->getTuner()->addUsed(buffer);
+
+               char problemname[512];
+               uint problemnumber;
+               snprintf(buffer, sizeof(buffer), "problem%u", i);
+               myfile.open(buffer, ios::in);
+               myfile.getline(problemname, sizeof(problemname));
+               myfile >> problemnumber;
+               myfile.close();
+               if (problems.getSize() <= problemnumber)
+                       problems.setSize(problemnumber + 1);
+               if (problems.get(problemnumber) == NULL)
+                       problems.set(problemnumber, new Problem(problemname));
+               Problem *problem = problems.get(problemnumber);
+               long long metric = -1;
+               int sat = IS_INDETER;
+               //Read data in from results file
+               snprintf(buffer, sizeof(buffer), "result%u", i);
+
+               myfile.open (buffer, ios::in);
+
+
+               if (myfile.is_open()) {
+                       myfile >> metric;
+                       myfile >> sat;
+                       myfile.close();
+               }
+               if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
+                       problem->setResult(sat);
+               } else if (problem->getResult() != sat && sat != IS_INDETER) {
+                       model_print("******** Result has changed ********\n");
+               }
+
+               if (metric != -1) {
+                       if (tuner->getTime(problem) == -1)
+                               tuner->addProblem(problem);
+                       tuner->setTime(problem, metric);
+               }
+
+       }
+
+}
+
+void CompTuner::tune() {
+       Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+       for (uint b = 0; b < budget; b++) {
+               model_print("Round %u of %u\n", b, budget);
+               Hashtable<TunerRecord *, int, uint64_t> scores;
+               Vector<Vector<TunerRecord *> *> allplaces;
+               for(uint ii=0; ii< problems.getSize(); ii++){
+                       allplaces.push(new Vector<TunerRecord *>());
+               }
+               for (uint j = 0; j < tunerV->getSize(); j++) {
+                       TunerRecord *tuner = tunerV->get(j);
+                       
+                       for (uint i = 0; i < problems.getSize(); i++) {
+                               Vector<TunerRecord *> *places = allplaces.get(i);
+                               Problem *problem = problems.get(i);
+                               long long metric = tuner->getTime(problem);
+                               if (metric == -1) {
+                                       metric = evaluate(problem, tuner);
+                                       if (tuner->getTime(problem) == -1) {
+                                               tuner->addProblem(problem);
+                                       }
+                                       model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+                                       model_print("*****************************\n");
+                                       if (metric != -1)
+                                               tuner->setTime(problem, metric);
+                                       else
+                                               tuner->setTime(problem, -2);
+                                       
+                                       if(tunerExists(tuner)){
+                                               //Solving the problem and noticing the tuner
+                                               //already exists
+                                               tuner->setDuplicate(true);
+                                               break;
+                                       }
+                               }
+                               if (metric >= 0) {
+                                       uint k = 0;
+                                       for (; k < places->getSize(); k++) {
+                                               if (metric < places->get(k)->getTime(problem))
+                                                       break;
+                                       }
+                                       model_print("place[%u]=Tuner<%p,%d>\n", k, tuner, tuner->getTunerNumber());
+                                       places->insertAt(k, tuner);
+                               }
+                       }
+               }
+               for(uint ii=0; ii < problems.getSize(); ii++){
+                       Problem *problem = problems.get(ii);
+                       Vector<TunerRecord *> *places = allplaces.get(ii);
+                       int points = 9;
+                       for (uint k = 0; k < places->getSize() && points; k++) {
+                               TunerRecord *tuner = places->get(k);
+                               if(tuner->isDuplicate()){
+                                       continue;
+                               }
+                               int currScore = 0;
+                               if (scores.contains(tuner))
+                                       currScore = scores.get(tuner);
+                               currScore += points;
+                               model_print("Problem<%s>\tTuner<%p,%d>\tmetric<%d>\n", problem->getProblem(), tuner, tuner->getTunerNumber(),  currScore);
+                               model_print("**************************\n");
+                               scores.put(tuner, currScore);
+                               points = points / 3;
+                       }
+               }
+               for(uint ii=0; ii< problems.getSize(); ii++){
+                       delete allplaces.get(ii);
+               }
+               Vector<TunerRecord *> ranking;
+               for (uint i = 0; i < tunerV->getSize(); i++) {
+                       TunerRecord *tuner = tunerV->get(i);
+                       int score = 0;
+                       if (scores.contains(tuner))
+                               score = scores.get(tuner);
+                       uint j = 0;
+                       for (; j < ranking.getSize(); j++) {
+                               TunerRecord *t = ranking.get(j);
+                               int tscore = 0;
+                               if (scores.contains(t))
+                                       tscore = scores.get(t);
+                               if (score > tscore)
+                                       break;
+                       }
+                       model_print("ranking[%u]=tuner<%p,%u>(Score=%d)\n", j, tuner, tuner->getTunerNumber(), score);
+                       model_print("************************\n");
+                       ranking.insertAt(j, tuner);
+               }
+               model_print("tunerSize=%u\trankingSize=%u\ttunerVSize=%u\n", tuners.getSize(), ranking.getSize(), tunerV->getSize());
+               for (uint i = tuners.getSize(); i < ranking.getSize(); i++) {
+                       TunerRecord *tuner = ranking.get(i);
+                       model_print("Removing tuner %u\n", tuner->getTunerNumber());
+                       for (uint j = 0; j < tunerV->getSize(); j++) {
+                               if (tunerV->get(j) == tuner)
+                                       tunerV->removeAt(j);
+                       }
+               }
+               uint tSize = tunerV->getSize();
+               for (uint i = 0; i < tSize; i++) {
+                       SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
+                       while(subTunerIndex(tmpTuner) != -1){
+                               model_print("******** New Tuner already explored...\n");
+                               delete tmpTuner;
+                               tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
+                       }
+                       TunerRecord *tmp = new TunerRecord(tmpTuner);
+                       tmp->setTunerNumber(allTuners.getSize());
+                       model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
+                       allTuners.push(tmp);
+                       tunerV->push(tmp);
+               }
+       }
+       printData();
+}
diff --git a/src/Tuner/comptuner.h b/src/Tuner/comptuner.h
new file mode 100644 (file)
index 0000000..dd28105
--- /dev/null
@@ -0,0 +1,24 @@
+#ifndef COMPTUNER_H
+#define COMPTUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "basictuner.h"
+
+
+class CompTuner : public BasicTuner {
+public:
+       CompTuner(uint budget, uint timeout);
+       virtual ~CompTuner();
+       void readData(uint numRuns);
+       void tune();
+       void findBestThreeTuners();
+protected:
+       
+};
+
+inline long long min(long long num1, long long num2, long long num3) {
+       return num1 < num2 && num1 < num3 ? num1 :
+                                num2 < num3 ? num2 : num3;
+}
+
+#endif
diff --git a/src/Tuner/kmeanstuner.cc b/src/Tuner/kmeanstuner.cc
new file mode 100644 (file)
index 0000000..333d9d9
--- /dev/null
@@ -0,0 +1,144 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   kmeanstuner.cc
+ * Author: hamed
+ * 
+ * Created on December 19, 2018, 4:16 PM
+ */
+
+#include "kmeanstuner.h"
+#include "float.h"
+#include "searchtuner.h"
+#include "math.h"
+
+KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) : 
+       BasicTuner(budget, timeout),
+       rounds(_rounds) {
+}
+
+KMeansTuner::~KMeansTuner() {
+}
+
+void clearVector(Vector<TunerRecord *> *tunerV) {
+       for (uint j = 0; j < tunerV->getSize(); j++) {
+               TunerRecord *tuner = tunerV->get(j);
+               tuner->problems.clear();
+       }
+}
+
+void KMeansTuner::tune() {
+       Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+       for (uint i = 0; i < rounds; i++) {
+               clearVector(tunerV);
+               mapProblemsToTuners(tunerV);
+               improveTuners(tunerV);
+       }
+       model_print("Best tuners\n");
+       for (uint j = 0; j < tunerV->getSize(); j++) {
+               TunerRecord *tuner = tunerV->get(j);
+               char buffer[256];
+               sprintf(buffer, "tuner%u.conf", j);
+               tuner->getTuner()->serialize(buffer);
+               tuner->getTuner()->print();
+       }
+       delete tunerV;
+}
+
+void KMeansTuner::improveTuners(Vector<TunerRecord *> *tunerV) {
+       for (uint j = 0; j < tunerV->getSize(); j++) {
+               TunerRecord *tuner = tunerV->get(j);
+               TunerRecord *newtuner = tune(tuner);
+               tunerV->set(j, newtuner);
+       }
+}
+
+double KMeansTuner::evaluateAll(TunerRecord *tuner) {
+       double product = 1;
+       for (uint i = 0; i < tuner->problemsSize(); i++) {
+               Problem *problem = tuner->getProblem(i);
+               long long metric = tuner->getTime(problem);
+               if (metric == -1) {
+                       metric = evaluate(problem, tuner);
+                       if (metric != -1)
+                               tuner->setTime(problem, metric);
+                       else
+                               tuner->setTime(problem, -2);
+               }
+
+               double score = metric;
+               if (metric < 0)
+                       score = timeout;
+               product *= score;
+       }
+       return pow(product, 1 / ((double)tuner->problemsSize()));
+}
+
+TunerRecord *KMeansTuner::tune(TunerRecord *tuner) {
+       TunerRecord *bestTuner = NULL;
+       double bestScore = DBL_MAX;
+
+       TunerRecord *oldTuner = tuner;
+       double base_temperature = evaluateAll(oldTuner);
+       double oldScore = base_temperature;
+
+       for (uint i = 0; i < budget; i++) {
+               SearchTuner *tmpTuner = mutateTuner(oldTuner->getTuner(), i);
+               TunerRecord *newTuner = oldTuner->changeTuner(tmpTuner);
+               newTuner->setTunerNumber( allTuners.getSize() );
+               allTuners.push(newTuner);
+               double newScore = evaluateAll(newTuner);
+               newTuner->getTuner()->printUsed();
+               model_print("Received score %f\n", newScore);
+               double scoreDiff = newScore - oldScore; //smaller is better
+               if (newScore < bestScore) {
+                       bestScore = newScore;
+                       bestTuner = newTuner;
+               }
+
+               double acceptanceP;
+               if (scoreDiff < 0) {
+                       acceptanceP = 1;
+               } else {
+                       double currTemp = base_temperature * (((double)budget - i) / budget);
+                       acceptanceP = exp(-scoreDiff / currTemp);
+               }
+               double ran = ((double)random()) / RAND_MAX;
+               if (ran <= acceptanceP) {
+                       oldScore = newScore;
+                       oldTuner = newTuner;
+               }
+       }
+
+       return bestTuner;
+}
+
+void KMeansTuner::mapProblemsToTuners(Vector<TunerRecord *> *tunerV) {
+       for (uint i = 0; i < problems.getSize(); i++) {
+               Problem *problem = problems.get(i);
+               TunerRecord *bestTuner = NULL;
+               long long bestscore = 0;
+               for (uint j = 0; j < tunerV->getSize(); j++) {
+                       TunerRecord *tuner = tunerV->get(j);
+                       long long metric = tuner->getTime(problem);
+                       if (metric == -1) {
+                               metric = evaluate(problem, tuner);
+                               if (metric != -1)
+                                       tuner->setTime(problem, metric);
+                               else
+                                       tuner->setTime(problem, -2);
+                       }
+                       if ((bestTuner == NULL && metric >= 0) ||
+                                       (metric < bestscore && metric >= 0)) {
+                               bestTuner = tuner;
+                               bestscore = metric;
+                       }
+               }
+               if (bestTuner != NULL)
+                       bestTuner->addProblem(problem);
+       }
+}
\ No newline at end of file
diff --git a/src/Tuner/kmeanstuner.h b/src/Tuner/kmeanstuner.h
new file mode 100644 (file)
index 0000000..a6025a3
--- /dev/null
@@ -0,0 +1,34 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   kmeanstuner.h
+ * Author: hamed
+ *
+ * Created on December 19, 2018, 4:16 PM
+ */
+
+#ifndef KMEANSTUNER_H
+#define KMEANSTUNER_H
+
+#include "basictuner.h"
+
+
+class KMeansTuner : public BasicTuner {
+public:
+       KMeansTuner(uint budget, uint rounds, uint timeout );
+       virtual ~KMeansTuner();
+       void tune();
+private:
+       double evaluateAll(TunerRecord *tuner);
+       void mapProblemsToTuners(Vector<TunerRecord *> *tunerV);
+       void improveTuners(Vector<TunerRecord *> *tunerV);
+       TunerRecord *tune(TunerRecord *tuner);
+       uint rounds;
+};
+
+#endif /* KMEANSTUNER_H */
+
diff --git a/src/Tuner/randomtuner.cc b/src/Tuner/randomtuner.cc
new file mode 100644 (file)
index 0000000..6fefc46
--- /dev/null
@@ -0,0 +1,65 @@
+#include "randomtuner.h"
+#include "csolver.h"
+#include "searchtuner.h"
+#include "comptuner.h"
+#include <math.h>
+#include <stdlib.h>
+#include <limits>
+
+#define UNSETVALUE -1
+
+RandomTuner::RandomTuner(uint _budget, uint _timeout) : 
+       BasicTuner(_budget, _timeout) {
+}
+
+RandomTuner::~RandomTuner(){
+       
+}
+
+void RandomTuner::tune() {
+       for (uint r = 0; r < budget; r++) {
+               model_print("Round %u of %u\n", r, budget);
+               for (uint i = 0; i < tuners.getSize(); i++){
+                       TunerRecord *tuner = tuners.get(i);
+                       bool isNew = true;
+                       for (uint j = 0; j < problems.getSize(); j++){
+                               Problem *problem = problems.get(j);
+                               long long metric = tuner->getTime(problem);
+                               if(metric == -1){
+                                       metric = evaluate(problem, tuner);
+                                       ASSERT(tuner->getTime(problem) == -1);
+                                       tuner->addProblem(problem);
+                                       model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+                                       if (metric != -1)
+                                               tuner->setTime(problem, metric);
+                                       else
+                                               tuner->setTime(problem, -2);
+                                       if(tunerExists(tuner)){
+                                               //Solving the problem and noticing the tuner
+                                               //already exists
+                                               isNew = false;
+                                               break;
+                                       }
+                               }
+                       }
+                       if(isNew){
+                               explored.push(tuner);
+                       }
+                       
+               }
+               uint tSize = tuners.getSize();
+               for (uint i = 0; i < tSize; i++) {
+                       SearchTuner *tmpTuner = mutateTuner(tuners.get(i)->getTuner(), budget);
+                       while(subTunerIndex(tmpTuner) != -1){
+                               tmpTuner->randomMutate();
+                       }
+                       TunerRecord *tmp = new TunerRecord(tmpTuner);
+                       tmp->setTunerNumber(allTuners.getSize());
+                       model_print("Mutated tuner %u to generate tuner %u\n", tuners.get(i)->getTunerNumber(), tmp->getTunerNumber());
+                       allTuners.push(tmp);
+                       tuners.set(i, tmp);
+               }
+       }
+       printData();
+       
+}
diff --git a/src/Tuner/randomtuner.h b/src/Tuner/randomtuner.h
new file mode 100644 (file)
index 0000000..75b8800
--- /dev/null
@@ -0,0 +1,21 @@
+#ifndef RANDOMTUNER_H
+#define RANDOMTUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "comptuner.h"
+#include "basictuner.h"
+
+/**
+ * This is a Tuner which is being used for 
+ */
+class RandomTuner : public BasicTuner {
+public:
+       RandomTuner(uint _budget, uint _timeout);
+       virtual ~RandomTuner();
+       void tune();
+protected:
+        bool randomMutation(SearchTuner *tuner);        
+       TunerRecord *tune(SearchTuner *tuner);
+};
+
+#endif
diff --git a/src/Tuner/satuner.cc b/src/Tuner/satuner.cc
new file mode 100644 (file)
index 0000000..61c9c35
--- /dev/null
@@ -0,0 +1,185 @@
+#include "satuner.h"
+#include <float.h>
+#include <math.h>
+#include "searchtuner.h"
+#include <iostream>
+#include <fstream>
+#include "solver_interface.h"
+#include <stdlib.h>
+
+SATuner::SATuner(uint _budget, uint _timeout) :
+       BasicTuner(_budget, _timeout)
+{
+}
+
+SATuner::~SATuner(){
+
+}
+
+void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric){
+       uint k = 0;
+       for (; k < places->getSize(); k++) {
+               if (metric < places->get(k)->getTime(problem))
+                       break;
+       }
+       model_print("Problem<%s>:place[%u]=Tuner<%p,%d>\n", problem->getProblem(), k, tuner, tuner->getTunerNumber());
+       places->insertAt(k, tuner);             
+}
+
+void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces){
+       TunerRecord *tuner = tunerV->get(index);
+       model_print("Removing Tuner %d\n", tuner->getTunerNumber());
+       tunerV->set(index, NULL);
+       for(uint i=0; i < allplaces.getSize(); i++){
+               Vector<TunerRecord *> *places = allplaces.get(i);
+               for(uint j=0; j < places->getSize(); j++){
+                       if(tuner == places->get(j)){
+                               places->removeAt(j);
+                               break;
+                       }
+               }
+       }
+
+}
+
+void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV){
+       for (int i= tunerV->getSize() -1; i >= 0; i--){
+               if(tunerV->get(i) == NULL){
+                       tunerV->removeAt(i);
+               }
+       }
+       model_print("TunerV size after removing nulls = %u\n", tunerV->getSize());
+}
+
+void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces){
+       for(uint ii=0; ii< problems.getSize(); ii++){
+               allplaces.push(new Vector<TunerRecord *>());
+       }
+       for (uint j = 0; j< tunerV->getSize(); j++){
+               TunerRecord *tuner = tunerV->get(j);
+               for (uint i=0; i < problems.getSize(); i++){
+                       Problem *problem = problems.get(i);
+                       long long metric = evaluate(problem, tuner);
+                       ASSERT(tuner->getTime(problem) == -1);
+                       tuner->addProblem(problem);
+                       if(metric != -1){
+                               tuner->setTime(problem , metric);
+                       }else{
+                               tuner->setTime(problem , -2);
+                       }
+                       if(metric >=0){
+                               Vector<TunerRecord *> *places = allplaces.get(i);
+                               rankTunerForProblem(places, tuner, problem, metric);
+                       }
+               }
+       }
+
+}
+
+void SATuner::tune() {
+       Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);     
+       Vector<Vector<TunerRecord *> *> allplaces;
+       uint tunerNumber = tuners.getSize();
+       //Initialization
+       initialize(tunerV, allplaces);
+       //Starting the body of algorithm
+       for (uint t = budget; t >0; t--) {
+               model_print("Current Temperature = %u\n", t);
+               Hashtable<TunerRecord *, int, uint64_t> scores;
+               for (uint i = 0; i < tunerNumber; i++) {
+                       SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget-t);
+                       int tunerIndex = subTunerIndex(tmpTuner);
+                       TunerRecord *tmp = NULL;
+                       if(tunerIndex == -1){
+                               tmp = new TunerRecord(tmpTuner);
+                               tmp->setTunerNumber(allTuners.getSize());
+                               model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
+                               allTuners.push(tmp);    
+                       }else{
+                               //Previous tuners might get explored with new combination of tuners.
+                               tmp = explored.get(tunerIndex); 
+                               model_print("Using exploread tuner <%u>\n", tmp->getTunerNumber());
+                       }
+                       tunerV->push(tmp);
+               }
+               ASSERT(tunerNumber * 2 == tunerV->getSize());
+               for (uint j = tunerNumber; j < tunerV->getSize(); j++) {
+                       TunerRecord *tuner = tunerV->get(j);
+                       for (uint i = 0; i < problems.getSize(); i++) {
+                               Problem *problem = problems.get(i);
+                               long long metric = tuner->getTime(problem);
+                               if (metric == -1) {
+                                       metric = evaluate(problem, tuner);
+                                       if (tuner->getTime(problem) == -1) {
+                                               tuner->addProblem(problem);
+                                       }
+                                       model_print("%u.Problem<%s>\tTuner<%p, %d>\tMetric<%lld>\n", i, problem->getProblem(),tuner, tuner->getTunerNumber(), metric);
+                                       model_print("*****************************\n");
+                                       if (metric != -1)
+                                               tuner->setTime(problem, metric);
+                                       else
+                                               tuner->setTime(problem, -2);
+
+                               }
+                               if (metric >= 0) {
+                                       ASSERT(i < allplaces.getSize());
+                                       Vector<TunerRecord *> *places = allplaces.get(i);
+                                       model_print("Problem<%s>:place[size=%u]=Tuner<%p,%d>\n", problem->getProblem(), places->getSize(), tuner, tuner->getTunerNumber());
+                                       rankTunerForProblem(places, tuner, problem, metric);
+                               }
+                       }
+               }
+               for(uint ii=0; ii < problems.getSize(); ii++){
+                       Problem *problem = problems.get(ii);
+                       ASSERT(ii < allplaces.getSize());
+                       Vector<TunerRecord *> *places = allplaces.get(ii);
+                       int points = pow(tunerNumber*1.0, 2*tunerNumber - 1);
+                       for (uint k = 0; k < places->getSize() && points; k++) {
+                               TunerRecord *tuner = places->get(k);
+                               int currScore = 0;
+                               if (scores.contains(tuner))
+                                       currScore = scores.get(tuner);
+                               currScore += points;
+                               model_print("Problem<%s>\tTuner<%p,%d>\tmetric<%d>\n", problem->getProblem(), tuner, tuner->getTunerNumber(),  currScore);
+                               model_print("**************************\n");
+                               scores.put(tuner, currScore);
+                               points = points / tunerNumber;
+                       }
+               }
+
+               for(uint i= 0; i < tunerNumber; i++){
+                       ASSERT(i < tunerV->getSize());
+                       TunerRecord *tuner1 = tunerV->get(i);
+                       TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
+                       ASSERT( tunerNumber + i < tunerV->getSize());
+                       model_print("Tuner1 = %d \tTuner2 = %d\n", tuner1->getTunerNumber(), tuner2->getTunerNumber());
+                       ASSERT(scores.contains(tuner1));
+                       ASSERT(scores.contains(tuner2));
+                       int score1 = scores.get(tuner1);
+                       int score2 = scores.get(tuner2);
+                       if( score2 > score1 ){
+                               removeTunerIndex(tunerV, i, allplaces);
+                       } else if( score2 < score1){
+                               model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1-score2)*1.0/t));
+                               double prob = 1/(exp((score1-score2)*1.0/t) );
+                               double random = ((double) rand() / (RAND_MAX));
+                               model_print("prob=%f\trandom=%f\n", prob, random);
+                               if(prob > random){
+                                       removeTunerIndex(tunerV, i, allplaces);
+                               }else{
+                                       removeTunerIndex(tunerV, tunerNumber + i, allplaces);
+                               }
+                       } else{
+                               double random = ((double) rand() / (RAND_MAX));
+                               int index = random > 0.5? i : tunerNumber + i;
+                               removeTunerIndex(tunerV, index, allplaces);
+                       }
+               }
+               removeNullsFromTunerVector(tunerV);
+               
+       }
+       for(uint ii=0; ii< allplaces.getSize(); ii++){
+               delete allplaces.get(ii);
+       }
+       printData();
+}
diff --git a/src/Tuner/satuner.h b/src/Tuner/satuner.h
new file mode 100644 (file)
index 0000000..fd05423
--- /dev/null
@@ -0,0 +1,25 @@
+#ifndef SATUNER_H
+#define SATUNER_H
+#include "classlist.h"
+#include "structs.h"
+#include "basictuner.h"
+
+/**
+*This tuner has the simulated annealing in its core
+*
+*/
+class SATuner : public BasicTuner {
+public:
+       SATuner(uint budget, uint timeout);
+       virtual ~SATuner();
+       void tune();
+protected:
+       void insertInPlace(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric);
+       void initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces);
+       void rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric);
+       void removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces);
+       void removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV);
+};
+
+
+#endif
index 4e96355..a600580 100644 (file)
@@ -1,26 +1,8 @@
 #include "searchtuner.h"
-#include "tunabledependent.h"
 #include <iostream>
 #include <fstream>
-#include <valarray>
 using namespace std;
 
-HashsetTunableDep initializeTunableDependencies()
-{
-  HashsetTunableDep dep;
-  dep.add(new TunableDependent(MUSTREACHGLOBAL, DECOMPOSEORDER));
-  dep.add(new TunableDependent(MUSTREACHLOCAL, DECOMPOSEORDER));
-  dep.add(new TunableDependent(MUSTREACHPRUNE, DECOMPOSEORDER));
-  dep.add(new TunableDependent(MUSTEDGEPRUNE, DECOMPOSEORDER));
-  dep.add(new TunableDependent(NODEENCODING, ENCODINGGRAPHOPT));
-  dep.add(new TunableDependent(EDGEENCODING, ENCODINGGRAPHOPT));
-  dep.add(new TunableDependent(ELEMENTOPTSETS, ELEMENTOPT));
-  return dep;
-}
-
-
-HashsetTunableDep SearchTuner::tunableDependency = initializeTunableDependencies();
-
 TunableSetting::TunableSetting(VarType _type, TunableParam _param) :
        hasVar(true),
        type1(_type),
@@ -70,16 +52,6 @@ void TunableSetting::print() {
        model_print("\n");
 }
 
-unsigned int tunableSettingHash(TunableSetting *setting) {
-       return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
-}
-
-bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
-       return setting1->hasVar == setting2->hasVar &&
-                                setting1->type1 == setting2->type1 &&
-                                setting1->type2 == setting2->type2 &&
-                                setting1->param == setting2->param;
-}
 
 ostream &operator<<(ostream &os, const TunableSetting &ts)
 {
@@ -90,12 +62,11 @@ ostream &operator<<(ostream &os, const TunableSetting &ts)
 
 
 SearchTuner::SearchTuner() {
-#ifdef STATICENCGEN
-        graphEncoding =false;
-        naiveEncoding = ELEM_UNASSIGNED;
-#endif
+}
+
+SearchTuner::SearchTuner(const char *filename, bool addused) {
        ifstream myfile;
-       myfile.open (TUNEFILE, ios::in);
+       myfile.open (filename, ios::in);
        if (myfile.is_open()) {
                bool hasVar;
                VarType type1;
@@ -114,10 +85,92 @@ SearchTuner::SearchTuner() {
                                setting = new TunableSetting(param);
                        }
                        setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
-                       usedSettings.add(setting);
+                       settings.add(setting);
+                       if(addused){
+                               usedSettings.add(setting);
+                       }
                }
                myfile.close();
+       } else {
+               model_print("Warning: Tuner %s couldn't be loaded ... Using default tuner instead ....\n", filename);
+       }
+}
+
+bool SearchTuner::equalUsed(SearchTuner* tuner){
+       if(tuner->usedSettings.getSize() != usedSettings.getSize()){
+               return false;
+       }
+       bool result = true;
+       SetIteratorTunableSetting *iterator = usedSettings.iterator();
+       while(iterator->hasNext()){
+               TunableSetting *setting = iterator->next();
+               if(!tuner->usedSettings.contains(setting)){
+                       result = false;
+                       break;
+               }else{
+                       TunableSetting *tunerSetting = tuner->usedSettings.get(setting);
+                       if(tunerSetting->selectedValue != setting->selectedValue){
+                               result = false;
+                               break;
+                       }
+               }
        }
+       delete iterator;
+       return result;
+}
+
+void SearchTuner::addUsed(const char *filename) {
+       ifstream myfile;
+       myfile.open (filename, ios::in);
+       if (myfile.is_open()) {
+               bool hasVar;
+               VarType type1;
+               VarType type2;
+               TunableParam param;
+               int lowValue;
+               int highValue;
+               int defaultValue;
+               int selectedValue;
+               while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
+                       TunableSetting *setting;
+
+                       if (hasVar) {
+                               setting = new TunableSetting(type1, type2, param);
+                       } else {
+                               setting = new TunableSetting(param);
+                       }
+                       setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
+                       if (!settings.contains(setting)) {
+                               settings.add(setting);
+                               usedSettings.add(setting);
+                       } else {
+                               TunableSetting *tmp = settings.get(setting);
+                               settings.remove(tmp);
+                               usedSettings.remove(tmp);
+                               delete tmp;
+                               settings.add(setting);
+                               usedSettings.add(setting);
+                       }
+               }
+               myfile.close();
+       }
+}
+
+bool SearchTuner::isSubTunerof(SearchTuner *newTuner){
+       SetIteratorTunableSetting *iterator = usedSettings.iterator();
+       while (iterator->hasNext()) {
+               TunableSetting *setting = iterator->next();
+               if(!newTuner->settings.contains(setting)){
+                       return false;
+               } else{
+                       TunableSetting *newSetting = newTuner->settings.get(setting);
+                       if(newSetting->selectedValue != setting->selectedValue){
+                               return false;
+                       }
+               }
+       }
+       delete iterator;
+       return true;
 }
 
 SearchTuner *SearchTuner::copyUsed() {
@@ -128,12 +181,6 @@ SearchTuner *SearchTuner::copyUsed() {
                TunableSetting *copy = new TunableSetting(setting);
                tuner->settings.add(copy);
        }
-#ifdef STATICENCGEN
-       if(naiveEncoding != ELEM_UNASSIGNED){
-               tuner->graphEncoding = graphEncoding;
-               tuner->naiveEncoding = naiveEncoding;
-       }
-#endif
        delete iterator;
        return tuner;
 }
@@ -147,6 +194,24 @@ SearchTuner::~SearchTuner() {
        delete iterator;
 }
 
+void SearchTuner::setTunable(TunableParam param, TunableDesc *descriptor, uint value) {
+       TunableSetting *result = new TunableSetting(param);
+       result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
+       settings.add(result);
+       usedSettings.add(result);
+}
+
+void SearchTuner::setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value) {
+       setVarTunable(vartype, 0, param, descriptor, value);
+}
+
+void SearchTuner::setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value) {
+       TunableSetting *result = new TunableSetting(vartype1, vartype2, param);
+       result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
+       settings.add(result);
+       usedSettings.add(result);
+}
+
 int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
        TunableSetting setting(param);
        TunableSetting *result = usedSettings.get(&setting);
@@ -184,35 +249,8 @@ int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
        return result->selectedValue;
 }
 
-bool SearchTuner::validTunableSetting(TunableSetting* setting){
-       TunableDependent tuneDep((Tunables)setting->param);
-       bool result = true;
-       while(tunableDependency.contains(&tuneDep)){
-               TunableDependent *dependent = tunableDependency.get(&tuneDep);
-               TunableSetting p(dependent->parent);
-               if(!settings.contains(&p)){
-                       SetIteratorTunableSetting *iter = settings.iterator();
-                       while(iter->hasNext()){
-                               model_print("*******************\n");
-                               iter->next()->print();
-                       }
-                       delete iter;
-               }
-               ASSERT(settings.contains(&p));
-               TunableSetting *parent = settings.get(&p);
-               if(!(bool)parent->selectedValue){ //Check parent config is already off
-                       return false;
-               }
-               tuneDep.dependent = dependent->parent;
-       }
-       return result;
-}
-
 void SearchTuner::randomMutate() {
-       TunableSetting *randomSetting;
-       do{
-               randomSetting= settings.getRandomElement();
-       }while(!validTunableSetting(randomSetting));
+       TunableSetting *randomSetting = settings.getRandomElement();
        int range = randomSetting->highValue - randomSetting->lowValue;
        int randomchoice = (random() % range) + randomSetting->lowValue;
        if (randomchoice < randomSetting->selectedValue)
@@ -224,50 +262,6 @@ void SearchTuner::randomMutate() {
        model_print("&&&&&&&&&&&&&&&&&&&&&&&\n");
 }
 
-#ifdef STATICENCGEN
-int SearchTuner::nextStaticTuner() {
-       if(naiveEncoding == ELEM_UNASSIGNED){
-               naiveEncoding = ONEHOT;
-               SetIteratorTunableSetting *iter = settings.iterator();
-               while(iter->hasNext()){
-                       TunableSetting *setting = iter->next();
-                       if (setting->param == NAIVEENCODER){
-                               setting->selectedValue = ONEHOT;
-                       } else if(setting->param == ENCODINGGRAPHOPT){
-                               setting->selectedValue = false;
-                       }
-               }
-               delete iter;
-               return EXIT_FAILURE;
-       }
-       int result=EXIT_FAILURE;
-       if(naiveEncoding == BINARYINDEX && graphEncoding){
-               model_print("Best tuner\n");
-               return EXIT_SUCCESS;
-       }else if (naiveEncoding == BINARYINDEX && !graphEncoding){
-               naiveEncoding = ONEHOT;
-               graphEncoding = true;
-       }else {
-               naiveEncoding = (ElementEncodingType)((int)naiveEncoding + 1);
-       }
-       SetIteratorTunableSetting *iter = settings.iterator();
-       uint count = 0;
-       while(iter->hasNext()){
-               TunableSetting * setting = iter->next();
-               if (setting->param == NAIVEENCODER){
-                       setting->selectedValue = naiveEncoding;
-                       count++;
-               } else if(setting->param == ENCODINGGRAPHOPT){
-                       setting->selectedValue = graphEncoding;
-                       count++;
-               }
-       }
-       model_print("Mutating %u settings\n", count);
-       delete iter;
-       return result;
-}
-#endif
-
 void SearchTuner::print() {
        SetIteratorTunableSetting *iterator = settings.iterator();
        while (iterator->hasNext()) {
@@ -278,9 +272,9 @@ void SearchTuner::print() {
 
 }
 
-void SearchTuner::serialize() {
+void SearchTuner::serialize(const char *filename) {
        ofstream myfile;
-       myfile.open (TUNEFILE, ios::out | ios::trunc);
+       myfile.open (filename, ios::out | ios::trunc);
        SetIteratorTunableSetting *iterator = settings.iterator();
        while (iterator->hasNext()) {
                TunableSetting *setting = iterator->next();
@@ -290,6 +284,18 @@ void SearchTuner::serialize() {
        delete iterator;
 }
 
+void SearchTuner::serializeUsed(const char *filename) {
+       ofstream myfile;
+       myfile.open (filename, ios::out | ios::trunc);
+       SetIteratorTunableSetting *iterator = usedSettings.iterator();
+       while (iterator->hasNext()) {
+               TunableSetting *setting = iterator->next();
+               myfile << *setting << endl;
+       }
+       myfile.close();
+       delete iterator;
+}
+
 void SearchTuner::printUsed() {
        SetIteratorTunableSetting *iterator = usedSettings.iterator();
        while (iterator->hasNext()) {
index 190bc5e..935f527 100644 (file)
@@ -5,7 +5,6 @@
 #include "structs.h"
 #include <ostream>
 using namespace std;
-#define TUNEFILE "tune.conf"
 
 class TunableSetting {
 public:
@@ -29,45 +28,38 @@ private:
        friend unsigned int tunableSettingHash(TunableSetting *setting);
        friend bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
        friend class SearchTuner;
+       friend class SerializeTuner;
 };
 
-unsigned int tunableSettingHash(TunableSetting *setting);
-bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2);
-
-typedef Hashset<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> HashsetTunableSetting;
-typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> SetIteratorTunableSetting;
-
 class SearchTuner : public Tuner {
 public:
        SearchTuner();
+       SearchTuner(const char *filename, bool addused = false);
        ~SearchTuner();
-       int getTunable(TunableParam param, TunableDesc *descriptor);
+       virtual int getTunable(TunableParam param, TunableDesc *descriptor);
        int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
-       int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+       virtual int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+       void setTunable(TunableParam param, TunableDesc *descriptor, uint value);
+       void setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value);
+       void setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value);
        SearchTuner *copyUsed();
+        bool isSubTunerof(SearchTuner *newTuner);
        void randomMutate();
        uint getSize() { return usedSettings.getSize();}
        void print();
        void printUsed();
-       void serialize();
-
+       void serialize(const char *file);
+       void serializeUsed(const char *file);
+       void addUsed(const char *file);
+        bool equalUsed(SearchTuner *tuner);
        CMEMALLOC;
-private:
-        bool validTunableSetting(TunableSetting* setting);
-        static HashsetTunableDep tunableDependency;
+protected:
        /** Used Settings keeps track of settings that were actually used by
           the example. Mutating settings may cause the Constraint Compiler
           not to query other settings.*/
        HashsetTunableSetting usedSettings;
        /** Settings contains all settings. */
        HashsetTunableSetting settings;
-#ifdef STATICENCGEN
-        bool graphEncoding;
-        ElementEncodingType naiveEncoding;
-public:
-        int nextStaticTuner();
-#endif
 };
 
-
 #endif
diff --git a/src/Tuner/serializetuner.cc b/src/Tuner/serializetuner.cc
new file mode 100644 (file)
index 0000000..db043fb
--- /dev/null
@@ -0,0 +1,70 @@
+#include "serializetuner.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+SerializeTuner::SerializeTuner(const char *filename) {
+       ifstream myfile;
+       myfile.open (filename, ios::in);
+       if (myfile.is_open()) {
+               bool hasVar;
+               VarType type1;
+               VarType type2;
+               TunableParam param;
+               int lowValue;
+               int highValue;
+               int defaultValue;
+               int selectedValue;
+               while (myfile >> hasVar >> type1 >> type2 >> param >> lowValue >> highValue >> defaultValue >> selectedValue) {
+                       TunableSetting *setting;
+
+                       if (hasVar) {
+                               setting = new TunableSetting(type1, type2, param);
+                       } else {
+                               setting = new TunableSetting(param);
+                       }
+                       setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
+                       settings.add(setting);
+                       usedSettings.add(setting);
+               }
+               myfile.close();
+       } else {
+               model_print("Warning: Tuner %s couldn't be loaded ... Using default tuner instead ....\n", filename);
+       }
+}
+
+/*SearchTuner::~SearchTuner() {
+   SetIteratorTunableSetting *iterator = settings.iterator();
+   while (iterator->hasNext()) {
+    TunableSetting *setting = iterator->next();
+    delete setting;
+   }
+   delete iterator;
+   }*/
+
+
+int SerializeTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
+       TunableSetting setting(param);
+       TunableSetting *result = usedSettings.get(&setting);
+       if (result == NULL) {
+               result = settings.get(&setting);
+               if ( result == NULL) {
+                       return descriptor->defaultValue;
+               }
+               usedSettings.add(result);
+       }
+       return result->selectedValue;
+}
+
+int SerializeTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+       TunableSetting setting(vartype1, vartype2, param);
+       TunableSetting *result = usedSettings.get(&setting);
+       if (result == NULL) {
+               result = settings.get(&setting);
+               if ( result == NULL) {
+                       return descriptor->defaultValue;
+               }
+               usedSettings.add(result);
+       }
+       return result->selectedValue;
+}
diff --git a/src/Tuner/serializetuner.h b/src/Tuner/serializetuner.h
new file mode 100644 (file)
index 0000000..a4039a6
--- /dev/null
@@ -0,0 +1,13 @@
+#ifndef SERIALIZETUNER_H
+#define SERIALIZETUNER_H
+#include "searchtuner.h"
+
+class SerializeTuner : public SearchTuner {
+public:
+       SerializeTuner(const char *filename);
+       int getTunable(TunableParam param, TunableDesc *descriptor);
+       int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
+       CMEMALLOC;
+};
+
+#endif
index 115e04e..9d45407 100644 (file)
@@ -15,41 +15,43 @@ int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
        return descriptor->defaultValue;
 }
 
-const char* tunableParameterToString(Tunables tunable){
-       switch(tunable){
-                case DECOMPOSEORDER:
-                        return "DECOMPOSEORDER";
-                case MUSTREACHGLOBAL:
-                        return "MUSTREACHGLOBAL";
-                case MUSTREACHLOCAL:
-                        return "MUSTREACHLOCAL";
-                case MUSTREACHPRUNE:
-                        return "MUSTREACHPRUNE";
-                case OPTIMIZEORDERSTRUCTURE:
-                        return "OPTIMIZEORDERSTRUCTURE";
-                case ORDERINTEGERENCODING:
-                        return "ORDERINTEGERENCODING";
-                case PREPROCESS:
-                        return "PREPROCESS";
-                case NODEENCODING:
-                        return "NODEENCODING";
-                case EDGEENCODING:
-                        return "EDGEENCODING";
-                case MUSTEDGEPRUNE:
-                        return "MUSTEDGEPRUNE";
-               case ELEMENTOPT: 
-                       return "ELEMENTOPT";
-               case ELEMENTOPTSETS:
-                       return "ELEMENTOPTSETS";
-               case PROXYVARIABLE:
-                       return "PROXYVARIABLE";
-               case ENCODINGGRAPHOPT:
-                       return "ENCODINGGRAPHOPT";
-               case NAIVEENCODER:
-                       return "NAIVEENCODER";
-               case MUSTVALUE:
-                       return "MUSTVALUE";
-                default:
-                        ASSERT(0);
-        }
+const char *tunableParameterToString(Tunables tunable) {
+       switch (tunable) {
+       case DECOMPOSEORDER:
+               return "DECOMPOSEORDER";
+       case MUSTREACHGLOBAL:
+               return "MUSTREACHGLOBAL";
+       case MUSTREACHLOCAL:
+               return "MUSTREACHLOCAL";
+       case MUSTREACHPRUNE:
+               return "MUSTREACHPRUNE";
+       case OPTIMIZEORDERSTRUCTURE:
+               return "OPTIMIZEORDERSTRUCTURE";
+       case ORDERINTEGERENCODING:
+               return "ORDERINTEGERENCODING";
+       case PREPROCESS:
+               return "PREPROCESS";
+       case NODEENCODING:
+               return "NODEENCODING";
+       case EDGEENCODING:
+               return "EDGEENCODING";
+       case MUSTEDGEPRUNE:
+               return "MUSTEDGEPRUNE";
+       case ELEMENTOPT:
+               return "ELEMENTOPT";
+       case ELEMENTOPTSETS:
+               return "ELEMENTOPTSETS";
+       case PROXYVARIABLE:
+               return "PROXYVARIABLE";
+       case ENCODINGGRAPHOPT:
+               return "ENCODINGGRAPHOPT";
+       case NAIVEENCODER:
+               return "NAIVEENCODER";
+       case MUSTVALUE:
+               return "MUSTVALUE";
+       case VARIABLEORDER:
+               return "VARIABLEORDER";
+       default:
+               ASSERT(0);
+       }
 }
index d838547..22660fb 100644 (file)
@@ -39,13 +39,13 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);
-static TunableDesc mustValueBinaryIndex(5, 9, 8);
+static TunableDesc mustValueBinaryIndex(0, 6, 3);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
-static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, BINARYINDEX);
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, 
-        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
+                                                        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);
diff --git a/src/analyzer/analyze.sh b/src/analyzer/analyze.sh
new file mode 100755 (executable)
index 0000000..efd8cd5
--- /dev/null
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+REPORTDIR=./report
+PICSDIR=$REPORTDIR/pics
+
+
+set -e
+if [ "$#" -lt 1 ]; then
+        echo "Illegal number of argument"
+        echo "./analyze.sh [path/to/log/folder]"
+        exit 1
+fi
+
+mkdir -p $PICSDIR
+python tunerloganalyzer.py -f $1
+cd $REPORTDIR
+make
diff --git a/src/analyzer/plot.py b/src/analyzer/plot.py
new file mode 100644 (file)
index 0000000..d3ec57d
--- /dev/null
@@ -0,0 +1,42 @@
+import numpy as np
+import matplotlib.pyplot as plt
+IMAGEDIR = "report/pics/"
+
+def generateHistograms(X, header):
+       global IMAGEDIR
+       for i, c in enumerate(X.T):
+               plt.hist(c)
+               plt.savefig(IMAGEDIR + header[i] + "-hist.pdf")
+               plt.clf()
+
+def generateScatterPlot(X, Y, header):
+       global IMAGEDIR
+       for i, feature in enumerate(X.T):
+               values = np.unique(feature)
+               values = np.sort(values)
+               geomean = []
+               for value in values:
+                       a =Y[np.where(feature == value)]
+                       a = np.array(list(map(lambda x :  x**(1.0/len(a)), a)))
+                       geomean.append(a.prod())
+               plt.plot(feature, Y, 'r.')
+               for ii in range(0, len(geomean)-1):
+                       plt.plot(values[ii:ii + 2], geomean[ii:ii + 2], 'bo-')
+               plt.savefig(IMAGEDIR + header[i] + "-scat.pdf")
+               plt.clf()
+
+def plot(data, header):
+       global IMAGEDIR
+       header=header[6:-1]
+       data = np.array(data)
+       X = data[:, 6:-4]
+       X[X==''] = '-1'
+       X = X.astype(np.float)
+       Y = data[:, -2]
+       Y = Y.astype(np.float)
+       generateHistograms(X, header)
+       generateScatterPlot(X, Y, header)
+
+       
+
+
diff --git a/src/analyzer/report/makefile b/src/analyzer/report/makefile
new file mode 100644 (file)
index 0000000..9dd7774
--- /dev/null
@@ -0,0 +1,92 @@
+LATEX := pdflatex -halt-on-error
+FIGURES :=
+.SUFFIXES : .tex .bbl .aux .eps .ps .dot .pdf
+
+.tex.bbl:
+       bibtex $*
+
+.tex.aux:
+       latex $*
+
+%.eps: %.ps
+       ps2epsi $< $@
+
+%.ps: %.dot
+       dot -Tps $< -o $@
+
+%.pdf: %.dot
+       dot -Tpdf $< -o $@
+
+%.png: %.dot
+       dot -Tpng $< -o $@
+
+%.aux: %.tex
+       $(LATEX) $<
+
+#%.dot: %.dotpiece $(FIGHEAD) $(FIGFOOT)
+#      cat $(FIGHEAD) $< $(FIGFOOT) > $@
+
+# latex the paper (default)
+new:   biblinks newpaper
+
+# latex + bibtex the paper
+bib:   bibpaper newpaper
+
+# save a backup of tex files in BACKUPS
+bak:   backuppaper
+
+biblinks: figures
+       $(LATEX) paper.tex
+       $(LATEX) paper.tex
+
+bibsuppl: figures
+       $(LATEX) suppl.tex
+       $(LATEX) suppl.tex
+
+cl: cover-letter.tex
+       $(LATEX) cover-letter.tex
+
+newpaper: figures biblinks
+       $(LATEX) paper.tex
+
+suppl: figures bibsuppl
+       $(LATEX) suppl.tex
+
+
+bibpaper: paper.aux paper.bbl
+       latex paper.tex
+
+
+backuppaper: 
+       @if [ ! -d BACKUPS ]; then mkdir BACKUPS; fi;   \
+       crtdate=`date '+%m-%d-%y--%H:%M:%S'`;           \
+       bakdir=BACKUPS/$$crtdate;                       \
+       mkdir $$bakdir;                                 \
+       cp *.tex $$bakdir
+
+spell:
+       @for i in *.tex; \
+       do if [ $$i != "paper.tex" ]; then aspell -c $$i -p ./spell.lst; fi;\
+       done
+
+total:
+       pdflatex paper.tex
+       pdflatex paper.tex
+       pdflatex paper.tex
+       @echo ================================================================
+       pdflatex paper.tex | grep -E 'arning|erfull'
+       @echo ================================================================
+
+figures: $(FIGURES)
+
+errinjfig:
+       gnuplot err-inj-fig/nve2latex.cmds
+       epstopdf injectErrorFig.eps
+       mv injectErrorFig.* figures
+
+
+clean:
+       rm -f *.dvi *.log *.aux *.blg *.bbl *~ err-inj-fig/*~
+       rm -f paper.ps paper.pdf 
+       rm -f injectErrorFig*
+       rm -rf $(PDF_DIR)
diff --git a/src/analyzer/report/paper.bib b/src/analyzer/report/paper.bib
new file mode 100644 (file)
index 0000000..1443ef4
--- /dev/null
@@ -0,0 +1,19 @@
+@BOOK{Smith:2012qr,
+       title = {{B}ook {T}itle},
+       publisher = {Publisher},
+       author = {Smith, J.~M. and Jones, A.~B.},
+       year = {2012},
+       edition = {7th},
+}
+
+@ARTICLE{Smith:2013jd,
+       author = {Jones, A.~B. and Smith, J.~M.},
+       title = {{A}rticle {T}itle},
+       journal = {Journal title},
+       year = {2013},
+       volume = {13},
+       pages = {123-456},
+       number = {52},
+       month = {March},
+       publisher = {Publisher}
+}
\ No newline at end of file
diff --git a/src/analyzer/report/paper.tex b/src/analyzer/report/paper.tex
new file mode 100644 (file)
index 0000000..146460e
--- /dev/null
@@ -0,0 +1,35 @@
+\documentclass[a4paper, 11pt]{article} % Font size (can be 10pt, 11pt or 12pt) and paper size (remove a4paper for US letter paper)\r
+\r
+\usepackage[protrusion=true,expansion=true]{microtype} % Better typography\r
+\usepackage{graphicx} % Required for including pictures\r
+\usepackage{wrapfig} % Allows in-line images\r
+\r
+\usepackage{mathpazo} % Use the Palatino font\r
+\usepackage[T1]{fontenc} % Required for accented characters\r
+\usepackage{float}\r
+\linespread{1.05} % Change line spacing here, Palatino benefits from a slight increase by default\r
+\r
+%---------------------------------------------------------------------------------------tyle{acmnumeric}\r
+%      TITLE\r
+%----------------------------------------------------------------------------------------\r
+\r
+\title{\textbf{SATTune Tuning Report}}\r
+\r
+%\author{\textsc{Ford Prefect} % Author\r
+%\\{\textit{Interstellar University}}} % Institution\r
+\r
+%\date{\today} % Date\r
+\r
+%----------------------------------------------------------------------------------------\r
+\r
+\begin{document}\r
+\r
+\maketitle % Print the title section\r
+\r
+\r
+\input{tech}\r
+\r
+%\bibliographystyle{unsrt}\r
+%\bibliography{paper}\r
+\r
+\end{document}\r
diff --git a/src/analyzer/report/tech.tex b/src/analyzer/report/tech.tex
new file mode 100644 (file)
index 0000000..21c84ad
--- /dev/null
@@ -0,0 +1,166 @@
+\section{Evaluation}\label{sec:eval}\r
+\r
+\subsection{Histogram Plots}\label{subsec:hist}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/EDGEENCODING-hist.pdf}\r
+       \caption{Encoding Edge Histogram: 0=Edge Unassiged, 1= Edge Break, 2= Edge Match}\r
+       \label{fig:edgeencoding}\r
+\end{figure}\r
+\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ELEMENTOPTSETS-hist.pdf}\r
+       \caption{Element Opt Set Histogram: Whether tuner should update sets or not. 0= OFF, 1= ON}\r
+       \label{fig:elementoptset}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ELEMENTOPT-hist.pdf}\r
+       \caption{Element Opt Histogram: 0 = OFF, 1= ON}\r
+       \label{fig:elementopt}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ENCODINGGRAPHOPT-hist.pdf}\r
+       \caption{Encoding Graph Optimization Histogram: 0= OFF, 1=ON}\r
+       \label{fig:encodinggraph}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/MUSTEDGEPRUNE-hist.pdf}\r
+       \caption{Must Prune Histogram: 0= OFF, 1= ON}\r
+       \label{fig:mustedgeprune}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/MUSTVALUE-hist.pdf}\r
+       \caption{Must Value Histogram: Binary Index must have value heuristic. The value varies from 0-6}\r
+       \label{fig:mustvalue}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/NODEENCODING-hist.pdf}\r
+       \caption{Node Encoding Histogram: 0= Unassigned, 1= OneHot, 2= Unary, 3= BinaryIndex}\r
+       \label{fig:nodeencoding}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/NAIVEENCODER-hist.pdf}\r
+       \caption{Naive Encoder Histogram: 1= OneHot, 2=Unary, 3=BinaryIndex}\r
+       \label{fig:naiveencoder}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/PREPROCESS-hist.pdf}\r
+       \caption{Preprocess Histogram: Replace Boolean Variables with T or F based on their polarity. 0= OFF, 1= ON}\r
+       \label{fig:preprocess}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/PROXYVARIABLE-hist.pdf}\r
+       \caption{Proxy Variable Histogram: Threshold for using proxy variables. Value varies from 1 to 5}\r
+       \label{fig:proxyvariable}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/VARIABLEORDER-hist.pdf}\r
+       \caption{Variable Order Histogram: 0= ConstraintOrdering, 1= ElementOrdering, 2=ReverseOrdering}\r
+       \label{fig:variableorder}\r
+\end{figure}\r
+\r
+\clearpage\r
+\subsection{Scatter Plots}\label{subsec:scatter}\r
+\r
+Y axis represents execution time and X axis shows the possible value of for each knob.\r
+Geometric mean of each value has been calculated and they are connected with solid lines.\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/EDGEENCODING-scat.pdf}\r
+       \caption{Encoding Edge plot}\r
+       \label{fig:edgeencodings}\r
+\end{figure}\r
+\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ELEMENTOPTSETS-scat.pdf}\r
+       \caption{Element Opt Set plot}\r
+       \label{fig:elementoptsets}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ELEMENTOPT-scat.pdf}\r
+       \caption{Element Opt plot}\r
+       \label{fig:elementopts}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/ENCODINGGRAPHOPT-scat.pdf}\r
+       \caption{Encoding Graph Optimization plot}\r
+       \label{fig:encodinggraphs}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/MUSTEDGEPRUNE-scat.pdf}\r
+       \caption{Must Prune plot}\r
+       \label{fig:mustedgeprunes}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/MUSTVALUE-scat.pdf}\r
+       \caption{Must Value plot}\r
+       \label{fig:mustvalues}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/NODEENCODING-scat.pdf}\r
+       \caption{Node Encoding plot}\r
+       \label{fig:nodeencodings}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/NAIVEENCODER-scat.pdf}\r
+       \caption{Naive Encoder plot}\r
+       \label{fig:naiveencoders}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/PREPROCESS-scat.pdf}\r
+       \caption{Preprocess Plot}\r
+       \label{fig:preprocesss}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/PROXYVARIABLE-scat.pdf}\r
+       \caption{Proxy Variable plot}\r
+       \label{fig:proxyvariables}\r
+\end{figure}\r
+\r
+\begin{figure}[htb]\r
+       \centering\r
+       \includegraphics[scale=0.6]{pics/VARIABLEORDER-scat.pdf}\r
+       \caption{Variable Order Plot}\r
+       \label{fig:variableorders}\r
+\end{figure}\r
+\r
diff --git a/src/analyzer/tunerloganalyzer.py b/src/analyzer/tunerloganalyzer.py
new file mode 100644 (file)
index 0000000..993e445
--- /dev/null
@@ -0,0 +1,204 @@
+import re
+import argparse
+import sys
+import os
+import plot as pl
+
+class AutoTunerArgParser:
+       def __init__(self):
+               self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...')
+               self.parser.add_argument('--folder', '-f', metavar='bin', type=str, nargs=1,help='output log of running the autotuner ...')
+               self.args = self.parser.parse_args()
+
+       def getFolder(self):
+               return self.args.folder[0]
+
+PROBLEMS = []
+
+TUNABLEHEADER = ["DECOMPOSEORDER", "MUSTREACHGLOBAL", "MUSTREACHLOCAL", "MUSTREACHPRUNE", "OPTIMIZEORDERSTRUCTURE",
+                "ORDERINTEGERENCODING", "PREPROCESS", "NODEENCODING", "EDGEENCODING", "MUSTEDGEPRUNE", "ELEMENTOPT",
+                "ENCODINGGRAPHOPT", "ELEMENTOPTSETS", "PROXYVARIABLE", "MUSTVALUE", "NAIVEENCODER", "VARIABLEORDER",
+                "PROBLEM","SATTIME", "EXECTIME","TUNERNUMBER"]
+
+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 TUNABLEHEADER
+       mystr=""
+       for header in TUNABLEHEADER:
+                mystr+=str(header)+","
+       file.write(mystr)
+       file.write("\n")
+
+def dump(file, row):
+       global TUNABLEHEADER
+       mystr=""
+       data = []
+       for i in range(len(TUNABLEHEADER)):
+               mystr += row[TUNABLEHEADER[i]]+ ","
+               data.append(row[TUNABLEHEADER[i]])
+       print ("mystr is:"+ mystr)
+       file.write(mystr)
+       file.write("\n")
+       return data
+
+def loadTunerInfo(row, filename):
+       with open(filename) as f:
+               for line in f:
+                       numbers = re.findall('\d+',line)
+                       numbers = list(map(int,numbers))
+                       row[TUNABLEHEADER[numbers[3]]] = row[TUNABLEHEADER[numbers[3]]] + str(numbers[7])
+
+def loadSolverTime(row, filename):
+       global REGEXES
+       global configs
+       with open(filename) as f:
+               for line in f:
+                       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]
+       row["SATTIME"] = configs["SATTIME"]
+       row["EXECTIME"] = configs["EXECTIME"]
+
+def loadProblemName(row,filename):
+       global PROBLEMS
+       with open(filename) as f:
+               problem = f.readline().replace("\n","")
+               probNumber = int(f.readline())
+               if probNumber >= len(PROBLEMS):
+                       PROBLEMS.insert(probNumber,problem)
+               elif PROBLEMS[probNumber] != problem:
+                       PROBLEMS[probNumber] = problem
+               row["PROBLEM"] = problem
+
+def loadTunerNumber(row, filename):
+       with open(filename) as f:
+               row["TUNERNUMBER"] = f.readline().replace("\n","")
+def analyzeLogs(file):
+       global configs
+       argprocess = AutoTunerArgParser()
+       printHeader(file)
+       rows = []
+       data = []
+       i = 0
+       while True :
+               row = {"DECOMPOSEORDER" : "",
+                       "MUSTREACHGLOBAL" : "",
+                       "MUSTREACHLOCAL" : "",
+                       "MUSTREACHPRUNE" : "", 
+                       "OPTIMIZEORDERSTRUCTURE" : "",
+                       "ORDERINTEGERENCODING" : "",
+                       "PREPROCESS" : "",
+                       "NODEENCODING" : "",
+                       "EDGEENCODING" : "",
+                       "MUSTEDGEPRUNE" : "",
+                       "ELEMENTOPT" : "",
+                       "ENCODINGGRAPHOPT" : "", 
+                       "ELEMENTOPTSETS" : "", 
+                       "PROXYVARIABLE" : "", 
+                       "MUSTVALUE" : "", 
+                       "NAIVEENCODER" : "", 
+                       "VARIABLEORDER" : "",
+                       "PROBLEM":"",
+                       "SATTIME":"",
+                       "EXECTIME": "",
+                       "TUNERNUMBER":""
+               }
+               try:
+                       loadTunerNumber(row, argprocess.getFolder() + "/tunernum" + str(i))
+                       loadTunerInfo(row, argprocess.getFolder()+"/tuner"+str(i)+"used")
+                       loadSolverTime(row, argprocess.getFolder()+"/log"+str(i))
+                       loadProblemName(row, argprocess.getFolder()+"/problem"+str(i))
+                       data.append(dump(file, row))
+                       rows.append(row)
+               except IOError:
+                       break
+               i += 1
+       return rows, data
+
+def tunerCountAnalysis(file, rows):
+       global TUNABLEHEADER
+       global PROBLEMS
+       tunercount = {}
+       tunernumber = {}
+       for row in rows:
+               mystr=""
+               for i in range(18):
+                       if not row[TUNABLEHEADER[i]]:
+                               mystr += "."
+                       else:
+                               mystr+=row[TUNABLEHEADER[i]]
+               if mystr not in tunercount:
+                       tunercount.update({mystr : 1})
+                       tunernumber.update({mystr : str(row["TUNERNUMBER"])})
+               else :
+                       tunercount[mystr] += 1
+                       tunernumber[mystr] += "-" + str(row["TUNERNUMBER"])
+
+       problems = set(map(lambda x: x["PROBLEM"], rows))
+       print ("Number of repititive tuners")
+       for key in tunercount:
+               if tunercount[key] > 1:
+                       print( key + "(ids:" + tunernumber[key]  + ") = #" + str(tunercount[key]) )
+
+def combineRowForEachTuner(rows):
+       global PROBLEMS
+       newRows = []
+       combined = None
+       for row in rows:
+               if row["PROBLEM"] == PROBLEMS[0]:
+                       combined = row
+               for key in row:
+                       if row[key]:
+                               combined[key] = row[key]
+               if row["PROBLEM"] == PROBLEMS[len(PROBLEMS)-1]:
+                       newRows.append(combined)
+       return newRows
+
+def transformDataset(rows):
+       print(rows)
+
+
+def main():
+       global TUNABLEHEADER
+       file = open("tuner.csv", "w")
+       rows, data = analyzeLogs(file)
+       tunerCountAnalysis(file, combineRowForEachTuner(rows) )
+       file.close()
+       #transformDataset(data)
+       pl.plot(data, TUNABLEHEADER)
+
+
+if __name__ == "__main__":
+       main()
index f9ebdbb..7acd00f 100644 (file)
@@ -145,6 +145,10 @@ void mustHaveValue(void *solver, void *element) {
        CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
+void setInterpreter(void *solver, unsigned int type){
+       CCSOLVER(solver)->setInterpreter((InterpreterType)type);
+}
+
 void *clone(void *solver) {
        return CCSOLVER(solver)->clone();
 }
\ No newline at end of file
index c88214e..2051cc9 100644 (file)
@@ -41,6 +41,7 @@ int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
+void setAlloyEncoder(void *solver);
 void *clone(void *solver);
 #ifdef __cplusplus
 }
index 58f5a02..5369a05 100644 (file)
@@ -28,6 +28,7 @@ class Set;
 class BooleanLogic;
 class Serializer;
 class ElementFunction;
+class Interpreter;
 
 typedef uint64_t VarType;
 typedef unsigned int uint;
index e17ba84..9616bc2 100644 (file)
@@ -57,11 +57,13 @@ class OrderEdge;
 class DOREdge;
 
 class AutoTuner;
+class CompTuner;
 class SearchTuner;
 class TunableSetting;
 
+class SerializeTuner;
+
 class TunableDesc;
-class TunableDependent;
 
 class OrderResolver;
 class DecomposeOrderResolver;
@@ -70,7 +72,12 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 class EncodingSubGraph;
-
+class SignatureEnc;
+class Signature;
+class ValuedSignature;
+class AlloyElementSig;
+class AlloySetSig;
+class AlloyBoolSig;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
index 48b2a7e..401a5e8 100644 (file)
@@ -18,6 +18,7 @@
 #include "config.h"
 #include "time.h"
 
+#define NANOSEC 1000000000.0
 
 #if 0
 extern int model_out;
index ef0b9b1..ce13d3c 100644 (file)
@@ -19,8 +19,6 @@
 //#define CONFIG_DEBUG
 #endif
 
-//#define STATICENCGEN
-
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
 #endif
index 983333b..1eba56d 100644 (file)
 #include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
+#include "alloyinterpreter.h"
+#include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
        boolFalse(boolTrue.negate()),
        unsat(false),
+       booleanVarUsed(false),
        tuner(NULL),
        elapsedTime(0),
-       satsolverTimeout(NOTIMEOUT)
+       satsolverTimeout(NOTIMEOUT),
+       interpreter(NULL)
 {
        satEncoder = new SATEncoder(this);
 }
@@ -79,6 +85,10 @@ CSolver::~CSolver() {
        for (uint i = 0; i < size; i++) {
                delete allFunctions.get(i);
        }
+       
+       if(interpreter != NULL){
+               delete interpreter;
+       }
 
        delete boolTrue.getBoolean();
        delete satEncoder;
@@ -136,6 +146,7 @@ void CSolver::resetSolver() {
        boolTrue = BooleanEdge(new BooleanConst(true));
        boolFalse = boolTrue.negate();
        unsat = false;
+       booleanVarUsed = false;
        elapsedTime = 0;
        tuner = NULL;
        satEncoder->resetSATEncoder();
@@ -154,9 +165,9 @@ CSolver *CSolver::clone() {
        return copy;
 }
 
-CSolver *CSolver::deserialize(const char *file) {
+CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
        model_print("deserializing %s ...\n", file);
-       Deserializer deserializer(file);
+       Deserializer deserializer(file, itype);
        return deserializer.deserialize();
 }
 
@@ -308,6 +319,8 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
        allBooleans.push(boolean);
+       if(!booleanVarUsed)
+               booleanVarUsed = true;
        return BooleanEdge(boolean);
 }
 
@@ -384,80 +397,88 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-       BooleanEdge newarray[asize];
-       switch (op) {
-       case SATC_NOT: {
-               return array[0].negate();
-       }
-       case SATC_IFF: {
-               for (uint i = 0; i < 2; i++) {
-                       if (isTrue(array[i])) { // It can be undefined
-                               return array[1 - i];
-                       } else if (isFalse(array[i])) {
-                               newarray[0] = array[1 - i];
-                               return applyLogicalOperation(SATC_NOT, newarray, 1);
-                       } else if (array[i]->type == LOGICOP) {
-                               BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
-                               if (b->replaced) {
-                                       return rewriteLogicalOperation(op, array, asize);
+       if(!useInterpreter()){
+               BooleanEdge newarray[asize];
+               switch (op) {
+               case SATC_NOT: {
+                       return array[0].negate();
+               }
+               case SATC_IFF: {
+                       for (uint i = 0; i < 2; i++) {
+                               if (isTrue(array[i])) { // It can be undefined
+                                       return array[1 - i];
+                               } else if (isFalse(array[i])) {
+                                       newarray[0] = array[1 - i];
+                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
+                               } else if (array[i]->type == LOGICOP) {
+                                       BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
+                                       if (b->replaced) {
+                                               return rewriteLogicalOperation(op, array, asize);
+                                       }
                                }
                        }
+                       break;
                }
-               break;
-       }
-       case SATC_OR: {
-               for (uint i = 0; i < asize; i++) {
-                       newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+               case SATC_OR: {
+                       for (uint i = 0; i < asize; i++) {
+                               newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+                       }
+                       return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
                }
-               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
-       }
-       case SATC_AND: {
-               uint newindex = 0;
-               for (uint i = 0; i < asize; i++) {
-                       BooleanEdge b = array[i];
-                       if (b->type == LOGICOP) {
-                               if (((BooleanLogic *)b.getBoolean())->replaced)
-                                       return rewriteLogicalOperation(op, array, asize);
+               case SATC_AND: {
+                       uint newindex = 0;
+                       for (uint i = 0; i < asize; i++) {
+                               BooleanEdge b = array[i];
+                               if (b->type == LOGICOP) {
+                                       if (((BooleanLogic *)b.getBoolean())->replaced)
+                                               return rewriteLogicalOperation(op, array, asize);
+                               }
+                               if (isTrue(b))
+                                       continue;
+                               else if (isFalse(b)) {
+                                       return boolFalse;
+                               } else
+                                       newarray[newindex++] = b;
+                       }
+                       if (newindex == 0) {
+                               return boolTrue;
+                       } else if (newindex == 1) {
+                               return newarray[0];
+                       } else {
+                               bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
+                               array = newarray;
+                               asize = newindex;
                        }
-                       if (isTrue(b))
-                               continue;
-                       else if (isFalse(b)) {
-                               return boolFalse;
-                       } else
-                               newarray[newindex++] = b;
+                       break;
+               }
+               case SATC_XOR: {
+                       //handle by translation
+                       return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
+               }
+               case SATC_IMPLIES: {
+                       //handle by translation
+                       return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
                }
-               if (newindex == 0) {
-                       return boolTrue;
-               } else if (newindex == 1) {
-                       return newarray[0];
+               }
+       
+               ASSERT(asize != 0);
+               Boolean *boolean = new BooleanLogic(this, op, array, asize);
+               Boolean *b = boolMap.get(boolean);
+               if (b == NULL) {
+                       boolean->updateParents();
+                       boolMap.put(boolean, boolean);
+                       allBooleans.push(boolean);
+                       return BooleanEdge(boolean);
                } else {
-                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
-                       array = newarray;
-                       asize = newindex;
+                       delete boolean;
+                       return BooleanEdge(b);
                }
-               break;
-       }
-       case SATC_XOR: {
-               //handle by translation
-               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
-       }
-       case SATC_IMPLIES: {
-               //handle by translation
-               return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
-       }
-       }
-
-       ASSERT(asize != 0);
-       Boolean *boolean = new BooleanLogic(this, op, array, asize);
-       Boolean *b = boolMap.get(boolean);
-       if (b == NULL) {
-               boolean->updateParents();
-               boolMap.put(boolean, boolean);
+       } else {
+               ASSERT(asize != 0);
+               Boolean *boolean = new BooleanLogic(this, op, array, asize);
                allBooleans.push(boolean);
                return BooleanEdge(boolean);
-       } else {
-               delete boolean;
-               return BooleanEdge(b);
+       
        }
 }
 
@@ -476,77 +497,83 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                }
        }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       Boolean *b = boolMap.get(constraint);
-
-       if (b == NULL) {
-               allBooleans.push(constraint);
-               boolMap.put(constraint, constraint);
-               constraint->updateParents();
-               if (order->graph != NULL) {
-                       OrderGraph *graph = order->graph;
-                       OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
-                       if (from != NULL) {
-                               OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
-                               if (to != NULL) {
-                                       OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-                                       OrderEdge *invedge;
-
-                                       if (edge != NULL && edge->mustPos) {
-                                               replaceBooleanWithTrueNoRemove(constraint);
-                                       } else if (edge != NULL && edge->mustNeg) {
-                                               replaceBooleanWithFalseNoRemove(constraint);
-                                       } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
-                                                                                && invedge->mustPos) {
-                                               replaceBooleanWithFalseNoRemove(constraint);
+       if (!useInterpreter() ){ 
+               Boolean *b = boolMap.get(constraint);
+
+               if (b == NULL) {
+                       allBooleans.push(constraint);
+                       boolMap.put(constraint, constraint);
+                       constraint->updateParents();
+                       if ( order->graph != NULL) {
+                               OrderGraph *graph = order->graph;
+                               OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
+                               if (from != NULL) {
+                                       OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
+                                       if (to != NULL) {
+                                               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
+                                               OrderEdge *invedge;
+
+                                               if (edge != NULL && edge->mustPos) {
+                                                       replaceBooleanWithTrueNoRemove(constraint);
+                                               } else if (edge != NULL && edge->mustNeg) {
+                                                       replaceBooleanWithFalseNoRemove(constraint);
+                                               } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+                                                                                        && invedge->mustPos) {
+                                                       replaceBooleanWithFalseNoRemove(constraint);
+                                               }
                                        }
                                }
                        }
+               } else {
+                       delete constraint;
+                       constraint = b;
                }
-       } else {
-               delete constraint;
-               constraint = b;
        }
-
        BooleanEdge be = BooleanEdge(constraint);
        return negate ? be.negate() : be;
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if (isTrue(constraint))
-               return;
-       else if (isFalse(constraint)) {
-               setUnSAT();
-       }
-       else {
-               if (constraint->type == LOGICOP) {
-                       BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
-                       if (!constraint.isNegated()) {
-                               if (b->op == SATC_AND) {
-                                       uint size = b->inputs.getSize();
-                                       //Handle potential concurrent modification
-                                       BooleanEdge array[size];
-                                       for (uint i = 0; i < size; i++) {
-                                               array[i] = b->inputs.get(i);
-                                       }
-                                       for (uint i = 0; i < size; i++) {
-                                               addConstraint(array[i]);
+       if(!useInterpreter()){
+               if (isTrue(constraint))
+                       return;
+               else if (isFalse(constraint)) {
+                       setUnSAT();
+               }
+               else {
+                       if (constraint->type == LOGICOP) {
+                               BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
+                               if (!constraint.isNegated()) {
+                                       if (b->op == SATC_AND) {
+                                               uint size = b->inputs.getSize();
+                                               //Handle potential concurrent modification
+                                               BooleanEdge array[size];
+                                               for (uint i = 0; i < size; i++) {
+                                                       array[i] = b->inputs.get(i);
+                                               }
+                                               for (uint i = 0; i < size; i++) {
+                                                       addConstraint(array[i]);
+                                               }
+                                               return;
                                        }
+                               }
+                               if (b->replaced) {
+                                       addConstraint(doRewrite(constraint));
                                        return;
                                }
                        }
-                       if (b->replaced) {
-                               addConstraint(doRewrite(constraint));
-                               return;
+                       constraints.add(constraint);
+                       Boolean *ptr = constraint.getBoolean();
+
+                       if (ptr->boolVal == BV_UNSAT) {
+                               setUnSAT();
                        }
-               }
-               constraints.add(constraint);
-               Boolean *ptr = constraint.getBoolean();
 
-               if (ptr->boolVal == BV_UNSAT) {
-                       setUnSAT();
+                       replaceBooleanWithTrueNoRemove(constraint);
+                       constraint->parents.clear();
                }
-
-               replaceBooleanWithTrueNoRemove(constraint);
+       } else{
+               constraints.add(constraint);
                constraint->parents.clear();
        }
 }
@@ -577,7 +604,6 @@ void CSolver::inferFixedOrders() {
        }
 }
 
-#define NANOSEC 1000000000.0
 int CSolver::solve() {
        long long startTime = getTimeNano();
        bool deleteTuner = false;
@@ -585,61 +611,70 @@ int CSolver::solve() {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
-
-
-       {
-               SetIteratorOrder *orderit = activeOrders.iterator();
-               while (orderit->hasNext()) {
-                       Order *order = orderit->next();
-                       if (order->graph != NULL) {
-                               delete order->graph;
-                               order->graph = NULL;
+       int result = IS_INDETER;
+       if(useInterpreter()){
+               interpreter->encode();
+               model_print("Problem encoded in Interpreter\n");
+               result = interpreter->solve();
+               model_print("Problem solved by Interpreter\n");
+       } else{
+
+               {
+                       SetIteratorOrder *orderit = activeOrders.iterator();
+                       while (orderit->hasNext()) {
+                               Order *order = orderit->next();
+                               if (order->graph != NULL) {
+                                       delete order->graph;
+                                       order->graph = NULL;
+                               }
                        }
+                       delete orderit;
                }
-               delete orderit;
-       }
-       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);
+               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);
+               DecomposeOrderTransform dot(this);
+               dot.doTransform();
+               time1 = getTimeNano();
+               model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
-       IntegerEncodingTransform iet(this);
-       iet.doTransform();
+               IntegerEncodingTransform iet(this);
+               iet.doTransform();
 
-       ElementOpt eop(this);
-       eop.doTransform();
+               ElementOpt eop(this);
+               eop.doTransform();
 
-       EncodingGraph eg(this);
-       eg.encode();
+               EncodingGraph eg(this);
+               eg.encode();
 
-       naiveEncodingDecision(this);
-//     eg.validate();
+               naiveEncodingDecision(this);
+       //      eg.validate();
 
-       VarOrderingOpt bor(this, satEncoder);
-       bor.doTransform();
-       
-       time2 = getTimeNano();
-       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-       
-       satEncoder->encodeAllSATEncoder(this);
-       time1 = getTimeNano();
+               VarOrderingOpt bor(this, satEncoder);
+               bor.doTransform();
 
-       model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+               time2 = getTimeNano();
+               model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 
-       model_print("Is problem UNSAT after encoding: %d\n", unsat);
-       int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
-       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : result == IS_INDETER? "INDETERMINATE" : " UNSAT");
-       time2 = getTimeNano();
-       elapsedTime = time2 - startTime;
-       model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+               satEncoder->encodeAllSATEncoder(this);
+               time1 = getTimeNano();
+
+               model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
+               model_print("Is problem UNSAT after encoding: %d\n", unsat);
+               
+
+               result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
+               model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
+               time2 = getTimeNano();
+               elapsedTime = time2 - startTime;
+               model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+       }
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
@@ -647,6 +682,32 @@ int CSolver::solve() {
        return result;
 }
 
+void CSolver::setInterpreter(InterpreterType type){
+       if(interpreter == NULL){
+               switch(type){
+                       case SATUNE:
+                               break;
+                       case ALLOY:{
+                               interpreter = new AlloyInterpreter(this);
+                               break;
+                       }case Z3:{
+                               interpreter = new SMTInterpreter(this);
+                               break;
+                       }
+                       case MATHSAT:{
+                               interpreter = new MathSATInterpreter(this);
+                               break;
+                       }
+                       case SMTRAT:{
+                               interpreter = new SMTRatInterpreter(this);
+                               break;
+                       }
+                       default:
+                               ASSERT(0);
+               }
+       }
+}
+
 void CSolver::printConstraints() {
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -665,7 +726,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return getElementValueSATTranslator(this, element);
+               return useInterpreter()? interpreter->getValue(element):
+                       getElementValueSATTranslator(this, element);
        default:
                ASSERT(0);
        }
@@ -676,7 +738,8 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) {
        Boolean *boolean = bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
-               return getBooleanVariableValueSATTranslator(this, boolean);
+               return useInterpreter()? interpreter->getBooleanValue(boolean):
+                       getBooleanVariableValueSATTranslator(this, boolean);
        default:
                ASSERT(0);
        }
index 58484bd..d7ccdb5 100644 (file)
@@ -139,9 +139,9 @@ public:
        bool isFalse(BooleanEdge b);
 
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
-        void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
+       void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
        bool isUnSAT() { return unsat; }
-
+        bool isBooleanVarUsed(){return booleanVarUsed;}
        void printConstraint(BooleanEdge boolean);
        void printConstraints();
 
@@ -161,16 +161,17 @@ public:
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
        void serialize();
-       static CSolver *deserialize(const char *file);
+       static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE);
        void autoTune(uint budget);
        void inferFixedOrders();
        void inferFixedOrder(Order *order);
-
-
+       void setInterpreter(InterpreterType type);
+       bool useInterpreter() {return interpreter != NULL;}
        void setTuner(Tuner *_tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
        long long getSolveTime();
+       long getSatSolverTimeout() { return satsolverTimeout;}
 
        CMEMALLOC;
 
@@ -218,11 +219,13 @@ private:
 
        SATEncoder *satEncoder;
        bool unsat;
-       Tuner *tuner;
+        bool booleanVarUsed;
+        Tuner *tuner;
        long long elapsedTime;
-        long satsolverTimeout;
+       long satsolverTimeout;
+       Interpreter *interpreter;
        friend class ElementOpt;
-        friend class VarOrderingOpt;
+       friend class VarOrderingOpt;
 };
 
 inline CompOp flipOp(CompOp op) {
diff --git a/src/learn.sh b/src/learn.sh
deleted file mode 100755 (executable)
index 221fea5..0000000
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/bin/bash
-# run as the following:
-# ./learn.sh [hexiom]
-# ./learn.sh [nqueens]
-# ./learn.sh [sudoku-csolver]
-# ./learn.sh [killerSudoku]
-
-
-
-BIN=./bin
-DUMP=$(find . -name "*.dump")
-cd $BIN
-for d in $DUMP; do
-       if [[ $d = *$@* ]]; then
-               echo $d
-               ./run.sh deserializerautotune "."$d
-       fi
-done
index b0e43a9..000ff18 100644 (file)
@@ -113,5 +113,7 @@ def loadCSolver():
        csolverlb.clone.restype = c_void_p
        csolverlb.serialize.argtypes = [c_void_p]
        csolverlb.serialize.restype = None
+        csolverlb.setInterpreter.argtypes = [c_void_p, c_uint]
+       csolverlb.setInterpreter.restype = None
        return csolverlb
 
diff --git a/src/runbench.sh b/src/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/tunermonitor.sh b/tunermonitor.sh
new file mode 100755 (executable)
index 0000000..d294333
--- /dev/null
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+#Terminate the script if even one command fails
+#set -e
+
+SATSOLVER=sat_solver
+CSOLVER=runcomptuner
+DESERALIZE=deserializerun
+MONITOR=tunermonitor
+SLEEPTIME=10
+FILE=monitor.log
+
+
+kill -9 `jobs -ps` &>$FILE
+
+while true; do
+       date >> $FILE
+       free >> $FILE
+       ps aux | grep $SATSOLVER | grep -v "grep" >> $FILE
+       ps aux | grep $CSOLVER | grep -v "run.sh" | grep -v "grep" >> $FILE
+       ps aux | grep $DESERALIZE | grep -v "run.sh" | grep -v "grep" >> $FILE
+       ps aux | grep $MONITOR | grep -v "grep" >> $FILE
+       echo "*************************" >> $FILE
+       sleep $SLEEPTIME
+done