From 0f946bac3c7689fecfa343396351e6850c0c3723 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Tue, 23 Oct 2018 15:48:43 -0700 Subject: [PATCH] fixing the heuristic for the BinaryIndex anyvalue constraints --- src/ASTAnalyses/Encoding/encodinggraph.cc | 6 +++--- src/Backend/satelemencoder.cc | 9 +++++++-- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index a4efe1f..b7d4c8d 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.cc +++ b/src/ASTAnalyses/Encoding/encodinggraph.cc @@ -113,7 +113,7 @@ void EncodingGraph::validate() { void EncodingGraph::encode() { - if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0) + if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &onoff) == 0) return; buildGraph(); SetIteratorEncodingSubGraph *itesg = subgraphs.iterator(); @@ -350,8 +350,8 @@ void EncodingGraph::decideEdges() { newSize = (leftSize > newSize) ? leftSize : newSize; newSize = (rightSize > newSize) ? rightSize : newSize; min = rightSize > leftSize ? leftSize : rightSize; -// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right)); 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->numValues()); @@ -361,8 +361,8 @@ void EncodingGraph::decideEdges() { newSize = (leftSize > newSize) ? leftSize : newSize; newSize = (rightSize > newSize) ? rightSize : newSize; min = rightSize > leftSize ? leftSize : rightSize; -// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right)); 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 diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 3391e1d..61db2fd 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -227,8 +227,13 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) { if (encoding->element->anyValue) { uint setSize = encoding->element->getRange()->getSize(); int maxIndex = getMaximumUsedIndex(encoding); -// model_print("maxIndex=%d\tsetSize=%u\tmetric=%f\n", maxIndex, setSize, (maxIndex - setSize) == 0? -1.0 : (setSize*1.0/(maxIndex-setSize)) ); - if (maxIndex != -1 && (maxIndex - setSize) != 0 && (setSize * 1.0 / (maxIndex - setSize)) < pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) { + maxIndex = maxIndex == -1? (int)encoding->encArraySize : maxIndex; + 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); -- 2.34.1