Merging + fixing memory bugs

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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index d2c04f62ac2a1aeeb7c9cddb4207c7fa07d61459..7687f3532e6b5f84840588aa56ae4dd3df87e032 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -7,6 +7,7 @@
 #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();
@@ -219,15 +220,37 @@ 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){
+       if (encoding->element->anyValue) {
                uint setSize = encoding->element->getRange()->getSize();
-               uint encArraySize = encoding->encArraySize;
-               model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
-               if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
+               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);
@@ -279,23 +302,26 @@ 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)));
                }