fixing the heuristic for the BinaryIndex anyvalue constraints

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index a4efe1fa773bdb0888f77f481d41ef327593440e..b7d4c8df1c0285521fc5308a63d516f7bbdf59e6 100644 (file)
--- 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 3391e1d44d8289f063c82c063a910e92269fe90b..61db2fd35e5045f407a5bdf91d98c7708951aa53 100644 (file)
--- 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);