Freezing bug fix - Incremental SATTune works for Sypet

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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index aa739242d002acb28330e6112a6f702ec7548b41..d924e6a9062e0b900f0e65bdbc5988bb6c2f4b83 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -227,6 +227,15 @@ void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
                ASSERT(edgeIsVarConst(e));
                freezeVariable(cnf, e);
        }
                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) {
 }
 
 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {


@@ -294,6 +303,9 @@ void SATEncoder::generateElementEncoding(Element *element) {
 }
 
 int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
 }
 
 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;
        for (int i = encoding->encArraySize - 1; i >= 0; i--) {
                if (encoding->isinUseElement(i))
                        return i + 1;