Freezing bug fix - Incremental SATTune works for Sypet
authorHamed Gorjiara <hgorjiar@uci.edu>
Mon, 1 Jul 2019 19:36:24 +0000 (12:36 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Mon, 1 Jul 2019 19:36:24 +0000 (12:36 -0700)
src/Backend/satelemencoder.cc

index aa73924..d924e6a 100644 (file)
@@ -227,6 +227,15 @@ void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
                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) {
@@ -294,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;