merge

[satune.git] / src / Backend / satelemencoder.cc

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 60625917a9f8ffde48e169319103e52b262c4077..3391e1d44d8289f063c82c063a910e92269fe90b 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -5,7 +5,9 @@
 #include "element.h"
 #include "set.h"
 #include "predicate.h"
-
+#include "csolver.h"
+#include "tunable.h"
+#include <cmath>
 
 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
@@ -214,7 +216,7 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYVAL);
        allocElementConstraintVariables(encoding, encoding->numBits);
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->anyValue)
+       if (encoding->element->anyValue)
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
@@ -222,8 +224,16 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->anyValue)
-               generateAnyValueBinaryIndexEncoding(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)) {
+                       generateAnyValueBinaryIndexEncodingPositive(encoding);
+               } else {
+                       generateAnyValueBinaryIndexEncoding(encoding);
+               }
+       }
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -234,7 +244,7 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
-       if (encoding->anyValue)
+       if (encoding->element->anyValue)
                addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 
@@ -270,9 +280,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)) {
@@ -282,6 +290,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));
        }
@@ -293,6 +308,20 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
        }
 }
 
+void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
+       if (encoding->numVars == 0)
+               return;
+       Edge carray[encoding->encArraySize];
+       uint size = 0;
+       for (uint i = 0; i < encoding->encArraySize; i++) {
+               if (encoding->isinUseElement(i)) {
+                       carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
+                       size++;
+               }
+       }
+       addConstraintCNF(cnf, constraintOR(cnf, size, carray));
+}
+
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
        uint64_t minvalueminusoffset = encoding->low - encoding->offset;
        uint64_t maxvalueminusoffset = encoding->high - encoding->offset;