From 31d8e919360f167a7a3317d7e9482e3bd9f70b8e Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Sat, 29 Sep 2018 16:13:17 -0700 Subject: [PATCH] 1)Making naiveencoder and encoding graph use tuner 2)Adding timeout to the sat solver 3)Adding similarity based heuristic for merging the subgraph on top of bit number heuristic --- src/ASTAnalyses/Encoding/encodinggraph.cc | 53 ++++++++++++------ src/ASTAnalyses/Encoding/encodinggraph.h | 3 + src/ASTAnalyses/Encoding/subgraph.cc | 52 +++++++++++++++++ src/ASTAnalyses/Encoding/subgraph.h | 3 +- src/Backend/inc_solver.cc | 33 ++++++++++- src/Backend/inc_solver.h | 4 ++ src/Backend/satelemencoder.cc | 27 ++++++++- src/Backend/satencoder.cc | 3 +- src/Backend/satencoder.h | 3 +- src/Encoders/naiveencoder.cc | 23 ++++---- src/Encoders/naiveencoder.h | 8 +-- src/Tuner/autotuner.cc | 68 +++-------------------- src/Tuner/searchtuner.cc | 5 +- src/Tuner/tunable.cc | 4 ++ src/Tuner/tunable.h | 6 +- src/common.mk | 2 +- src/csolver.cc | 12 ++-- src/csolver.h | 2 + 18 files changed, 201 insertions(+), 110 deletions(-) diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index 472fd27..8ec4ac8 100644 --- 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 f3d58a2..a5b91b4 100644 --- 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 f99783e..de76e4d 100644 --- 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 9327b97..1392dba 100644 --- 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 80c4e4c..c1bebb8 100644 --- a/src/Backend/inc_solver.cc +++ b/src/Backend/inc_solver.cc @@ -12,7 +12,6 @@ #include #include "common.h" #include -#include 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 78506b4..4692cfe 100644 --- 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 ad0722b..84880ff 100644 --- 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 659c0d9..62adb2f 100644 --- 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 0ccf31c..2b2b42a 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -10,7 +10,7 @@ typedef Hashtable 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 7e33c1b..17b9914 100644 --- 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 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 dbc9148..fe84a2b 100644 --- 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 29c3289..6a17807 100644 --- a/src/Tuner/autotuner.cc +++ b/src/Tuner/autotuner.cc @@ -4,52 +4,9 @@ #include #include #include -#include -#include -#include -#include -#include -#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 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 3486a9c..c7b3aab 100644 --- 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 a06d0f1..dd2cb7f 100644 --- 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 9fd614a..0213f03 100644 --- 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 fbd6f88..8ffb364 100644 --- 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 b7c9aa4..2c15b62 100644 --- 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 19ba3e1..60e7c68 100644 --- 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; }; -- 2.34.1