From: bdemsky Date: Tue, 23 Oct 2018 02:43:16 +0000 (-0700) Subject: Clean up merge heuristic to do what we said it did X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67ab65d6d34fc2d8e66df7c024c7d4b1c8a5e95d;p=satune.git Clean up merge heuristic to do what we said it did --- diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index 6ebea56..a4efe1f 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.cc +++ b/src/ASTAnalyses/Encoding/encodinggraph.cc @@ -305,7 +305,6 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) { } uint convertSize(uint cost) { - cost = FUDGEFACTOR * cost;// fudge factor return NEXTPOW2(cost); } @@ -334,7 +333,7 @@ void EncodingGraph::decideEdges() { 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,28 +341,28 @@ void EncodingGraph::decideEdges() { newSize = convertSize(left->s->getUnionSize(right->s)); newSize = (leftSize > newSize) ? leftSize : newSize; newSize = (rightSize > newSize) ? rightSize : newSize; - max = rightSize > leftSize ? rightSize : leftSize; - merge = left->measureSimilarity(right) > 1.5 || max == 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; + min = rightSize > leftSize ? leftSize : rightSize; // model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right)); - merge = left->measureSimilarity(right) > 1.5 || max == newSize; + merge = leftGraph->measureSimilarity(right) > 1.5 || min == newSize; } 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; + min = rightSize > leftSize ? leftSize : rightSize; // model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right)); - merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize; + merge = leftGraph->measureSimilarity(rightGraph) > 1.5 || min == newSize; } if (merge) { //add the edge @@ -429,23 +428,22 @@ 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) { 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(); } diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h index 96c163e..b53568e 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.h +++ b/src/ASTAnalyses/Encoding/encodinggraph.h @@ -4,8 +4,6 @@ #include "structs.h" #include "graphstructs.h" -#define FUDGEFACTOR 1.2 -#define CONVERSIONFACTOR 0.5 class EncodingGraph { public: @@ -47,7 +45,6 @@ public: 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 577ed5f..b36b8c0 100644 --- a/src/ASTAnalyses/Encoding/subgraph.cc +++ b/src/ASTAnalyses/Encoding/subgraph.cc @@ -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(); + 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() { diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h index 0ceb306..00264a6 100644 --- a/src/ASTAnalyses/Encoding/subgraph.h +++ b/src/ASTAnalyses/Encoding/subgraph.h @@ -47,6 +47,7 @@ public: uint getEncodingMaxVal(EncodingNode *n) { return maxEncodingVal;} 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; }; diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 6f421ee..00eadc8 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -227,7 +227,7 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) { if (encoding->element->anyValue) { uint setSize = encoding->element->getRange()->getSize(); int maxIndex = getMaximumUsedIndex(encoding); - if (maxIndex !=-1 && (maxIndex - setSize) != 0 && (setSize/(maxIndex-setSize)) < pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) { + if (maxIndex != -1 && (maxIndex - setSize) != 0 && (setSize / (maxIndex - setSize)) < pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) { generateAnyValueBinaryIndexEncodingPositive(encoding); } else { generateAnyValueBinaryIndexEncoding(encoding); @@ -279,7 +279,7 @@ void SATEncoder::generateElementEncoding(Element *element) { } } -int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding){ +int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding) { int index = -1; for (uint i = encoding->encArraySize - 1; i >= 0; i--) { if (encoding->isinUseElement(i)) { diff --git a/src/Tuner/multituner.cc b/src/Tuner/multituner.cc index 0850f66..206a62e 100644 --- a/src/Tuner/multituner.cc +++ b/src/Tuner/multituner.cc @@ -77,28 +77,28 @@ void MultiTuner::printData() { } void MultiTuner::findBestThreeTuners() { - if(allTuners.getSize() < 3){ + if (allTuners.getSize() < 3) { printData(); return; } - TunerRecord * bestTuners[3]; + 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; kgetTime(problem), tuner2->getTime(problem), tuner3->getTime(problem)), (double)1 / problems.getSize()); } - double result=1; - for(uint l=0; l< problems.getSize(); l++){ + double result = 1; + for (uint l = 0; l < problems.getSize(); l++) { result *= mintimes[l]; } - if(result < score){ + if (result < score) { score = result; bestTuners[0] = tuner1; bestTuners[1] = tuner2; @@ -108,8 +108,8 @@ void MultiTuner::findBestThreeTuners() { } } model_print("Best 3 tuners:\n"); - for(uint i=0; i<3; i++){ - TunerRecord * tuner = bestTuners[i]; + for (uint i = 0; i < 3; i++) { + TunerRecord *tuner = bestTuners[i]; SearchTuner *stun = tuner->getTuner(); model_print("Tuner %u\n", tuner->tunernumber); stun->print(); diff --git a/src/Tuner/multituner.h b/src/Tuner/multituner.h index 398eb84..deb980b 100644 --- a/src/Tuner/multituner.h +++ b/src/Tuner/multituner.h @@ -56,11 +56,6 @@ protected: void mapProblemsToTuners(Vector *tunerV); void improveTuners(Vector *tunerV); TunerRecord *tune(TunerRecord *tuner); - inline long long min(long long num1, long long num2, long long num3){ - return num1 < num2 && num1 < num3? num1: - num2 < num3? num2 : num3; - } - Vector allTuners; Vector problems; Vector tuners; @@ -69,4 +64,10 @@ protected: uint timeout; int execnum; }; + +inline long long min(long long num1, long long num2, long long num3) { + return num1 < num2 && num1 < num3 ? num1 : + num2 < num3 ? num2 : num3; +} + #endif