bug fix

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index b7d4c8df1c0285521fc5308a63d516f7bbdf59e6..66d86062aa2d5a7c08513a80001b25a582b73f66 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, &onoff) == 0)
+       if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
                return;
        buildGraph();
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 61db2fd35e5045f407a5bdf91d98c7708951aa53..3aa0927c3d04b32a6d19be61af1b526c5a87aa8a 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -226,12 +226,11 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
        if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
-               int maxIndex = getMaximumUsedIndex(encoding);
-               maxIndex = maxIndex == -1? (int)encoding->encArraySize : maxIndex;
-               if(setSize == encoding->encArraySize && maxIndex == (int)setSize){
+               int maxIndex = getMaximumUsedSize(encoding);
+               if (setSize == encoding->encArraySize && maxIndex == (int)setSize) {
                        return;
                }
-               double ratio = (setSize*(1+2*encoding->numVars))/ (encoding->numVars*(encoding->numVars + maxIndex*1.0 - setSize));
+               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);
@@ -285,28 +284,23 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
-int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding) {
-       int index = -1;
-       for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
-               if (encoding->isinUseElement(i)) {
-                       if (i + 1 < encoding->encArraySize) {
-                               index = i + 1;
-                       }
-                       break;
-               }
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+       for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+               if (encoding->isinUseElement(i))
+                       return i + 1;
        }
-       return index;
+       ASSERT(false);
+       return -1;
 }
 
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
        if (encoding->numVars == 0)
                return;
-       int index = getMaximumUsedIndex(encoding);
-       if ( index != -1 ) {
+       int index = getMaximumUsedSize(encoding);
+       if ( index != encoding->encArraySize ) {
                addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
        }
-       index = index == -1 ? encoding->encArraySize - 1 : index - 1;
-       for (int i = index; i >= 0; i--) {
+       for (int i = index - 1; i >= 0; i--) {
                if (!encoding->isinUseElement(i)) {
                        addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
                }

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index a89ab1b9b9ffe99f36392c50ebc0e42bcd026b6a..63b5a619babcdd4f9b7152457436f55c05fe7e1a 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -63,7 +63,7 @@ private:
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
-       int getMaximumUsedIndex(ElementEncoding *encoding);
+       int getMaximumUsedSize(ElementEncoding *encoding);
        void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;