Merging + fixing memory bugs

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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3aa0927c3d04b32a6d19be61af1b526c5a87aa8a..7687f3532e6b5f84840588aa56ae4dd3df87e032 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -220,6 +220,24 @@ 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));
@@ -285,6 +303,9 @@ 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;
@@ -297,7 +318,7 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
        if (encoding->numVars == 0)
                return;
        int index = getMaximumUsedSize(encoding);
-       if ( index != encoding->encArraySize ) {
+       if ( index != (int)encoding->encArraySize ) {
                addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
        }
        for (int i = index - 1; i >= 0; i--) {