Merging + fixing memory bugs

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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ad0722b2d262bf4a89a792fa220c2d1b8a554013..7687f3532e6b5f84840588aa56ae4dd3df87e032 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();
@@ -218,12 +220,42 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
+void SATEncoder::freezeElementVariables(ElementEncoding *encoding) {
+       ASSERT(encoding->element->frozen);
+       for (uint i = 0; i < encoding->numVars; i++) {
+               Edge e = encoding->variables[i];
+               ASSERT(edgeIsVarConst(e));
+               freezeVariable(cnf, e);
+       }
+       for(uint i=0; i< encoding->encArraySize; i++){
+               if(encoding->isinUseElement(i) && encoding->encoding != EENC_NONE && encoding->numVars > 1){
+                       Edge e = encoding->edgeArray[i];
+                       if(!edgeIsNull(e)){
+                               ASSERT(edgeIsVarConst(e));
+                               freezeVariable(cnf, e);
+                       }
+               }
+       }
+}
+
 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if (encoding->element->anyValue)
-               generateAnyValueBinaryIndexEncoding(encoding);
+       if (encoding->element->anyValue) {
+               uint setSize = encoding->element->getRange()->getSize();
+               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));
+//             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);
+               }
+       }
 }
 
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
@@ -270,29 +302,46 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+       if(encoding->encArraySize == 1){
+               return 1;
+       }
+       for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+               if (encoding->isinUseElement(i))
+                       return i + 1;
+       }
+       ASSERT(false);
+       return -1;
+}
+
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
        if (encoding->numVars == 0)
                return;
-       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;
-               }
-       }
-       if ( index != -1 ) {
+       int index = getMaximumUsedSize(encoding);
+       if ( index != (int)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)));
                }
        }
 }
 
+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;