Bug fix: Droping the log from the anyvalue heuristic...

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3cd2c1c70b9385e032d7cf4ba99e446f2829f212..6f421ee627d97dc7509dbb4bd1bf85879978a1d9 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -226,9 +226,8 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
        if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
-               uint encArraySize = encoding->encArraySize;
-               double metric = encArraySize == setSize?setSize:setSize/(encArraySize-setSize);
-               if ( log(metric) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
+               int maxIndex = getMaximumUsedIndex(encoding);
+               if (maxIndex !=-1 && (maxIndex - setSize) != 0 && (setSize/(maxIndex-setSize)) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
                        generateAnyValueBinaryIndexEncodingPositive(encoding);
                } else {
                        generateAnyValueBinaryIndexEncoding(encoding);
@@ -280,9 +279,7 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
-       if (encoding->numVars == 0)
-               return;
+int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding){
        int index = -1;
        for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
                if (encoding->isinUseElement(i)) {
@@ -292,6 +289,13 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
                        break;
                }
        }
+       return index;
+}
+
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+       if (encoding->numVars == 0)
+               return;
+       int index = getMaximumUsedIndex(encoding);
        if ( index != -1 ) {
                addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
        }

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