1)Making naiveencoder and encoding graph use tuner 2)Adding timeout to the sat solver...

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 472fd279b255f5e84d003272c3314e0622188af7..8ec4ac84eafe0b1d3cea3139964f94358768e0b4 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -113,8 +113,11 @@ void EncodingGraph::validate() {
 
 
 void EncodingGraph::encode() {
+       if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+               return;
+       buildGraph();
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
-       DEBUG("#SubGraph = %u", subgraphs.getSize());
+       model_print("#SubGraph = %u\n", subgraphs.getSize());
        while (itesg->hasNext()) {
                EncodingSubGraph *sg = itesg->next();
                sg->encode();
@@ -332,7 +335,6 @@ void EncodingGraph::decideEdges() {
                }
                
                uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
-               uint64_t totalCost = 0;
                bool merge = false;
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
@@ -340,36 +342,29 @@ void EncodingGraph::decideEdges() {
                        newSize = convertSize(left->s->getUnionSize(right->s));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * left->elements.getSize() +
-                                                                       (newSize - rightSize) * right->elements.getSize();
                        max = rightSize > leftSize? rightSize : leftSize;
-                       if(newSize == max){
-                               merge = true;
-                       }
+//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
+                       merge = left->measureSimilarity(right) > 1.5 || max == newSize;
                } else if (leftGraph != NULL && rightGraph == NULL) {
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * right->elements.getSize();
                        max = rightSize > leftSize? rightSize : leftSize;
-                       if(newSize == max){
-                               merge = true;
-                       }
+//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
+                       merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
                } else {
                        //Neither are null
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(rightGraph->encodingSize);
                        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;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * rightGraph->numElements;
-                       if(rightSize < 64 && leftSize < 64){
-                               merge = true;
-                       }
+//                     model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
+                       max = rightSize > leftSize? rightSize : leftSize;
+                       merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
                }
                if (merge) {
                        //add the edge
@@ -427,11 +422,33 @@ uint EncodingNode::getSize() const {
        return s->getSize();
 }
 
+uint64_t EncodingNode::getIndex(uint index){
+       return s->getElement(index);
+}
+
 VarType EncodingNode::getType() const {
        return s->getType();
 }
 
-static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+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){
+       uint common = 0;
+       for(uint i=0; i < s->getSize(); i++){
+               uint64_t item = s->getElement(i);
+               if(node->itemExists(item)){
+                       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();
+}
 
 EncodingNode *EncodingGraph::createNode(Element *e) {
        if (e->type == ELEMCONST)

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index f3d58a220155d2153ea01b0d927e6d7eea7c31ba..a5b91b4360790874e1961b4fd409a545eb0ebae4 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -42,9 +42,12 @@ public:
        EncodingNode(Set *_s);
        void addElement(Element *e);
        uint getSize() const;
+       uint64_t getIndex(uint index);
        VarType getType() const;
+        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:

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index f99783e42410e63fda746d12cfb3e74dc4694c2a..de76e4d0e6890d149fd703795f3713dc455ad3be 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -121,6 +121,58 @@ uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
        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) )){
+                       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();
+}
+
+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()){
+               uint64_t item1 = setIter1->next();
+               if( set2.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();
+}
+
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
        SetIteratorEncodingEdge *eeit = n->edges.iterator();
        uint newsize = n->getSize();

diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index 9327b977ea0581917f2aef8eae919c37c32debb5..1392dba72b70ee98df814d55102c73eecce9eab2 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -45,7 +45,8 @@ public:
        void encode();
        uint getEncoding(EncodingNode *n, uint64_t val);
        uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;}
-
+        double measureSimilarity(EncodingNode *n);
+        double measureSimilarity(EncodingSubGraph *sg);
        CMEMALLOC;
 private:
        uint estimateNewSize(EncodingNode *n);

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 80c4e4c9f6b4b4857e4add875aff110f1990932d..c1bebb806ad0e453ebd1e5a7e087ca34ac697551 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -12,7 +12,6 @@
 #include <fcntl.h>
 #include "common.h"
 #include <string.h>
-#include <stdexcept>
 
 IncrementalSolver *allocIncrementalSolver() {
        IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -20,6 +19,7 @@ IncrementalSolver *allocIncrementalSolver() {
        This->solution = NULL;
        This->solutionsize = 0;
        This->offset = 0;
+       This->timeout = NOTIMEOUT;
        createSolver(This);
        return This;
 }
@@ -91,7 +91,7 @@ void startSolve(IncrementalSolver *This) {
 }
 
 int getSolution(IncrementalSolver *This) {
-       int result = readIntSolver(This);
+       int result = readStatus(This);
        if (result == IS_SAT) {
                int numVars = readIntSolver(This);
                if (numVars > This->solutionsize) {
@@ -112,6 +112,33 @@ int readIntSolver(IncrementalSolver *This) {
        return value;
 }
 
+int readStatus(IncrementalSolver *This) {
+       int retval;
+       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 {
+               struct timeval tv;
+               tv.tv_sec = This->timeout;
+               tv.tv_usec = 0;
+               retval = select(This->from_solver_fd+1, &rfds, NULL, NULL, &tv);
+       }
+       if(retval == -1){
+               perror("Error in select()");
+               exit(EXIT_FAILURE);
+       }
+       else if (retval){
+               printf("Data is available now.\n");
+               return readIntSolver(This);
+       }else{
+               printf("Timeout for the solver\n");
+               return IS_INDETER;
+       }
+}
+
 void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
        char *result = (char *) tmp;
        ssize_t bytestoread = size;
@@ -120,7 +147,7 @@ void readSolver(IncrementalSolver *This, void *tmp, ssize_t size) {
                ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
                if (n == -1) {
                        model_print("Read failure\n");
-                       throw std::runtime_error("Read failure\n");
+                       exit(-1);
                }
                bytestoread -= n;
                bytesread += n;

diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h
index 78506b45dbc7ddc6526b69cb3ab5b6396017cc8c..4692cfe626f0e6fd3add84adaf4a615bcfe4ddd1 100644 (file)
--- a/src/Backend/inc_solver.h
+++ b/src/Backend/inc_solver.h
@@ -18,6 +18,8 @@
 #include "solver_interface.h"
 #include "classlist.h"
 
+#define NOTIMEOUT -1
+
 struct IncrementalSolver {
        int *buffer;
        int *solution;
@@ -26,6 +28,7 @@ struct IncrementalSolver {
        pid_t solver_pid;
        int to_solver_fd;
        int from_solver_fd;
+        long timeout;
 };
 
 IncrementalSolver *allocIncrementalSolver();
@@ -43,5 +46,6 @@ void createSolver(IncrementalSolver *This);
 void killSolver(IncrementalSolver *This);
 void flushBufferSolver(IncrementalSolver *This);
 int readIntSolver(IncrementalSolver *This);
+int readStatus(IncrementalSolver *This);
 void readSolver(IncrementalSolver *This, void *buffer, ssize_t size);
 #endif

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ad0722b2d262bf4a89a792fa220c2d1b8a554013..84880fff21574f387accacf7afcf2138defcb1f1 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -5,7 +5,8 @@
 #include "element.h"
 #include "set.h"
 #include "predicate.h"
-
+#include "csolver.h"
+#include "tunable.h"
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
@@ -222,8 +223,16 @@ 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;
+               model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
+               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+                       generateAnyValueBinaryIndexEncodingPositive(encoding);
+               } else {
                generateAnyValueBinaryIndexEncoding(encoding);
+               }
+       }
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -293,6 +302,20 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
        }
 }
 
+void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
+       if (encoding->numVars == 0)
+               return;
+       Edge carray[encoding->encArraySize];
+       uint size = 0;
+       for (uint i = 0; i < encoding->encArraySize; i++) {
+               if (encoding->isinUseElement(i)) {
+                       carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
+                       size++;
+               }
+       }
+       addConstraintCNF(cnf, constraintOR(cnf, size, carray));
+}
+
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
        uint64_t minvalueminusoffset = encoding->low - encoding->offset;
        uint64_t maxvalueminusoffset = encoding->high - encoding->offset;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 659c0d980776e4689c4271873768580e1af4be48..62adb2fa9a635fbdde70862b5d2f75c3c4eac304 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,7 +29,8 @@ void SATEncoder::resetSATEncoder() {
        booledgeMap.reset();
 }
 
-int SATEncoder::solve() {
+int SATEncoder::solve(long timeout) {
+       cnf->solver->timeout = timeout;
        return solveCNF(cnf);
 }
 

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31cfcdcb012ee00a533e81e1ed788dfea2c3..2b2b42a333a10e410c5dff983bfad437433e87e7 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -10,7 +10,7 @@ typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
 
 class SATEncoder {
 public:
-       int solve();
+       int solve(long timeout);
        SATEncoder(CSolver *solver);
        ~SATEncoder();
        void resetSATEncoder();
@@ -62,6 +62,7 @@ private:
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+       void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;
        CSolver *solver;

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 7e33c1b26ca8fd307a4235c37891f3dd2fedde00..17b9914c80bfe9ccbfe1e004d9089689300dd331 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -11,18 +11,19 @@
 #include "table.h"
 #include "tableentry.h"
 #include "order.h"
+#include "tunable.h"
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge b = iterator->next();
-               naiveEncodingConstraint(b.getBoolean());
+               naiveEncodingConstraint(This, b.getBoolean());
        }
        delete iterator;
 }
 
-void naiveEncodingConstraint(Boolean *This) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
        switch (This->type) {
        case BOOLEANVAR: {
                return;
@@ -33,11 +34,11 @@ void naiveEncodingConstraint(Boolean *This) {
                return;
        }
        case LOGICOP: {
-               naiveEncodingLogicOp((BooleanLogic *) This);
+               naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
                return;
        }
        case PREDICATEOP: {
-               naiveEncodingPredicate((BooleanPredicate *) This);
+               naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
                return;
        }
        default:
@@ -45,30 +46,30 @@ void naiveEncodingConstraint(Boolean *This) {
        }
 }
 
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
        for (uint i = 0; i < This->inputs.getSize(); i++) {
-               naiveEncodingConstraint(This->inputs.get(i).getBoolean());
+               naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
        }
 }
 
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
        FunctionEncoding *encoding = This->getFunctionEncoding();
        if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
                This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 
        for (uint i = 0; i < This->inputs.getSize(); i++) {
                Element *element = This->inputs.get(i);
-               naiveEncodingElement(element);
+               naiveEncodingElement(csolver, element);
        }
 }
 
-void naiveEncodingElement(Element *This) {
+void naiveEncodingElement(CSolver *csolver, Element *This) {
        ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
                if(This->type != ELEMCONST){
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
-               encoding->setElementEncodingType(BINARYINDEX);
+               encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
                encoding->encodingArrayInitialization();
        }
 
@@ -76,7 +77,7 @@ void naiveEncodingElement(Element *This) {
                ElementFunction *function = (ElementFunction *) This;
                for (uint i = 0; i < function->inputs.getSize(); i++) {
                        Element *element = function->inputs.get(i);
-                       naiveEncodingElement(element);
+                       naiveEncodingElement(csolver, element);
                }
                FunctionEncoding *encoding = function->getElementFunctionEncoding();
                if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index dbc9148d6199d72257498de94791381f3f5417d6..fe84a2b64eb874b13fc6ba284e1dba3080feb5b6 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -10,8 +10,8 @@
  */
 
 void naiveEncodingDecision(CSolver *csolver);
-void naiveEncodingConstraint(Boolean *This);
-void naiveEncodingLogicOp(BooleanLogic *This);
-void naiveEncodingPredicate(BooleanPredicate *This);
-void naiveEncodingElement(Element *This);
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This);
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This);
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This);
+void naiveEncodingElement(CSolver *csolver, Element *This);
 #endif

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 29c3289ec2d371f71f9e47f0ea2745e8ee71e023..6a178078d453c04950f5305113a8d4aecf49b726 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -4,52 +4,9 @@
 #include <math.h>
 #include <stdlib.h>
 #include <float.h>
-#include <iostream>
-#include <chrono>
-#include <thread>
-#include <mutex>
-#include <condition_variable>
 
-#define TIMEOUT 1000s
 #define UNSETVALUE -1
-#define POSINFINITY 9999999999L
-
-using namespace std::chrono_literals;
-
-int solve(CSolver *solver)
-{
-       try{
-               return solver->solve();
-       }
-       catch(std::runtime_error& e) {
-               return UNSETVALUE;
-       }
-}
-
-int solveWrapper(CSolver *solver)
-{
-       std::mutex m;
-       std::condition_variable cv;
-       int retValue;
-
-       std::thread t([&cv, &retValue, solver]()
-       {
-               retValue = solve(solver);
-               cv.notify_one();
-       });
-
-       t.detach();
-
-       {
-               std::unique_lock<std::mutex> l(m);
-               if(cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
-                       throw std::runtime_error("Timeout");
-       }
-
-       return retValue;
-}
-
-
+#define TIMEOUTSEC 60
 AutoTuner::AutoTuner(uint _budget) :
        budget(_budget), result(UNSETVALUE) {
 }
@@ -61,23 +18,16 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
+       copy->setSatSolverTimeout(TIMEOUTSEC);
        model_print("**********************\n");
-       long long metric = 0L;
-       try {
-               int sat = solveWrapper(copy);
-               if (result == UNSETVALUE)
-                       result = sat;
-               else if (result != sat) {
-                       model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
-                       copy->printConstraints();
-               }
-               metric = copy->getElapsedTime();
-       }
-       catch(std::runtime_error& e) {
-               metric = POSINFINITY;
-               model_print("TimeOut has hit\n");
+       int sat = copy->solve();
+       if (result == UNSETVALUE && sat != IS_INDETER)
+               result = sat;
+       else if (result != sat && sat != IS_INDETER) {
+               model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+               copy->printConstraints();
        }
-       
+       long long metric = copy->getElapsedTime();
        delete copy;
        return metric;
 }

diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index 3486a9c737eab26ca7b120df730d389857fa8b64..c7b3aab2b690036f07fc26e791a63a1765e4aafc 100644 (file)
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -44,11 +44,12 @@ void TunableSetting::setDecision(int _low, int _high, int _default, int _selecti
 }
 
 void TunableSetting::print() {
+       model_print("Param %s = %u \t range=[%u,%u]", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
        if (hasVar) {
-               model_print("VarType1 %" PRIu64 ", ", type1);
+               model_print("\tVarType1 %" PRIu64 ", ", type1);
                model_print("VarType2 %" PRIu64 ", ", type2);
        }
-       model_print("Param %s = %u \t range=[%u,%u]\n", tunableParameterToString( (Tunables)param), selectedValue, lowValue, highValue);
+       model_print("\n");
 }
 
 unsigned int tunableSettingHash(TunableSetting *setting) {

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index a06d0f1290b888bcb0a167b86a2961a2c7ec1f21..dd2cb7f5065b558b3f4818378f1a8da94fbe9a23 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -43,6 +43,10 @@ const char* tunableParameterToString(Tunables tunable){
                        return "ELEMENTOPTSETS";
                case PROXYVARIABLE:
                        return "PROXYVARIABLE";
+               case ENCODINGGRAPHOPT:
+                       return "ENCODINGGRAPHOPT";
+               case NAIVEENCODER:
+                       return "NAIVEENCODER";
                 default:
                         ASSERT(0);
         }

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 9fd614a5eefc447412c6f962497fdf2b47f160a3..0213f0330193c26d872d2b9938e0718ec8f6c82d 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,8 +39,12 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 static TunableDesc proxyparameter(1, 5, 2);
+static TunableDesc mustValueBinaryIndex(1, 9, 5);
+static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, 
+        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);

diff --git a/src/common.mk b/src/common.mk
index fbd6f8872dda4dde337b90d42c0dad8f722ae7d6..8ffb36415bedd1a82654855695bdbf3b0be88dcd 100644 (file)
--- a/src/common.mk
+++ b/src/common.mk
@@ -1,7 +1,7 @@
 # A few common Makefile items
 
 CC := gcc
-CXX := g++-5
+CXX := g++
 
 UNAME := $(shell uname)
 

diff --git a/src/csolver.cc b/src/csolver.cc
index b7c9aa4fcb9f9ac6d4bab090dc1b41b2a9e0c2bd..2c15b62fd87e6322fb92d60f0fad6ca7d5e19047 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -34,7 +34,8 @@ CSolver::CSolver() :
        boolFalse(boolTrue.negate()),
        unsat(false),
        tuner(NULL),
-       elapsedTime(0)
+       elapsedTime(0),
+       satsolverTimeout(NOTIMEOUT)
 {
        satEncoder = new SATEncoder(this);
 }
@@ -615,9 +616,8 @@ int CSolver::solve() {
        ElementOpt eop(this);
        eop.doTransform();
 
-//     EncodingGraph eg(this);
-//     eg.buildGraph();
-//     eg.encode();
+       EncodingGraph eg(this);
+       eg.encode();
 
        naiveEncodingDecision(this);
 //     eg.validate();
@@ -631,8 +631,8 @@ int CSolver::solve() {
        model_print("Elapse Encode time: %f\n", (time1- startTime) / NANOSEC);
        
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
-       int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : " 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);

diff --git a/src/csolver.h b/src/csolver.h
index 19ba3e12db5eac9f06affa74540cf66bf774f997..60e7c6861033e70216aa782238d80c7b8f6c0c43 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -139,6 +139,7 @@ public:
        bool isFalse(BooleanEdge b);
 
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
+        void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
        bool isUnSAT() { return unsat; }
 
        void printConstraint(BooleanEdge boolean);
@@ -219,6 +220,7 @@ private:
        bool unsat;
        Tuner *tuner;
        long long elapsedTime;
+        long satsolverTimeout;
        friend class ElementOpt;
 };