Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.

src/base/abci/abcRec2.c

@@ -1619,8 +1619,8 @@ s_pMan->timeBuild += clock() - timeBuild;
     timeInsert = clock();
     Abc_NtkRecInsertToLookUpTable2(s_pMan, ppSpot, pPO, nLeaves, pTruth, s_pMan->fTrim);
     s_pMan->timeInsert += clock() - timeInsert;
-//     if (pIfMan->pPars->fDelayOpt)
-//         Abc_NtkRecAddSOPB(pIfMan, pCut, pTruth, pCanonPerm, uCanonPhase );
+//  if (pIfMan->pPars->fDelayOpt)
+//      Abc_NtkRecAddSOPB(pIfMan, pCut, pTruth, pCanonPerm, uCanonPhase );
     return 1;
 }
 

src/bool/lucky/lucky.c

@@ -49,7 +49,7 @@ inline int memCompare(word* x, word*  y, int nVars)
      word tempWord;
      qsort(a,WordsN,sizeof(word),compareWords1);
      tempWord = a[0];
-     for(i=1;i<WordsN;i++)    
+     for(i=1;i<WordsN;i++)  
          if(tempWord != a[i])
          {
              a[count] = a[i];
@@ -67,7 +67,7 @@ int compareWords2 (const void ** x, const void ** y)
     else if(**(word**)x < **(word**)y)
         return -1;
     else
-        return 0;    
+        return 0;   
     
 }
 int compareWords (const void ** a, const void ** b)
@@ -75,11 +75,11 @@ int compareWords (const void ** a, const void ** b)
      if( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) > 0 )
          return 1;
      else
-         return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;        
+         return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;       
 }
 int compareWords3 (const void ** x, const void ** y)
 {
-    return memCompare(*(word**)x, *(word**)y, 16);     
+    return memCompare(*(word**)x, *(word**)y, 16);   
 } 
 void sortAndUnique(word** a, Abc_TtStore_t* p)
 {
@@ -87,7 +87,7 @@ void sortAndUnique(word** a, Abc_TtStore_t* p)
      word* tempWordPtr;
      qsort(a,WordsPtrN,sizeof(word*),(int(*)(const void *,const void *))compareWords3);
      tempWordPtr = a[0];
-     for(i=1;i<WordsPtrN;i++)    
+     for(i=1;i<WordsPtrN;i++)   
          if(memcmp(a[i],tempWordPtr,sizeof(word)*(p->nWords)) != 0)
          {
              a[count] = a[i];
@@ -159,117 +159,117 @@ void freeArrayB(word* b)
 // if pInOnt changed(minimized) by function return 1 if not 0
 // inline int minimalInitialFlip_propper(word* pInOut, word* pDuplicat, int  nVars)
 // {
-//     word oneWord=1;
-//     Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
-//     Kit_TruthNot_64bit( pDuplicat, nVars );
-//     if( memCompare(pDuplicat,pInOut,nVars) == -1)
-//     {
-//         Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
-//         return 1;
-//     }
-//     return 0;
+//  word oneWord=1;
+//  Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
+//  Kit_TruthNot_64bit( pDuplicat, nVars );
+//  if( memCompare(pDuplicat,pInOut,nVars) == -1)
+//  {
+//      Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
+//      return 1;
+//  }
+//  return 0;
 // }
 // inline int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
 // {
-//     int i;
-//     int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
-//     memcpy(pMinimal, pInOut, blockSize);
-//     memcpy(PDuplicat, pInOut, blockSize);
-//     for(i=0;i<nVars;i++)
-//     {
-//         Kit_TruthChangePhase_64bit( pInOut, nVars, i );
-//         if( memCompare(pMinimal,pInOut,nVars) == 1)
-//             memcpy(pMinimal, pInOut, blockSize);
-//         memcpy(pInOut,PDuplicat,blockSize);
-//     }
-//     memcpy(pInOut,pMinimal,blockSize);
-//     if(memCompare(pMinimal,PDuplicat,nVars) == 0)
-//         return 0;
-//     else
-//         return 1;
+//  int i;
+//  int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
+//  memcpy(pMinimal, pInOut, blockSize);
+//  memcpy(PDuplicat, pInOut, blockSize);
+//  for(i=0;i<nVars;i++)
+//  {
+//      Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+//      if( memCompare(pMinimal,pInOut,nVars) == 1)
+//          memcpy(pMinimal, pInOut, blockSize);
+//      memcpy(pInOut,PDuplicat,blockSize);
+//  }
+//  memcpy(pInOut,pMinimal,blockSize);
+//  if(memCompare(pMinimal,PDuplicat,nVars) == 0)
+//      return 0;
+//  else
+//      return 1;
 // }
 // inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars) 
 // {
-//     int i;    
-//     int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
-//     memcpy(pMinimal, pInOut, blockSize);
-//     memcpy(PDuplicat, pInOut, blockSize);
-//     for(i=0;i<nVars-1;i++)
-//     {
-//         Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
-//         if(memCompare(pMinimal,pInOut,nVars) == 1)
-//             memcpy(pMinimal, pInOut, blockSize);
-//         memcpy(pInOut,PDuplicat,blockSize);
-//     }
-//     memcpy(pInOut,pMinimal,blockSize);
-//     if(memCompare(pMinimal,PDuplicat,nVars) == 0)
-//         return 0;
-//     else
-//         return 1;
+//  int i;  
+//  int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
+//  memcpy(pMinimal, pInOut, blockSize);
+//  memcpy(PDuplicat, pInOut, blockSize);
+//  for(i=0;i<nVars-1;i++)
+//  {
+//      Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+//      if(memCompare(pMinimal,pInOut,nVars) == 1)
+//          memcpy(pMinimal, pInOut, blockSize);
+//      memcpy(pInOut,PDuplicat,blockSize);
+//  }
+//  memcpy(pInOut,pMinimal,blockSize);
+//  if(memCompare(pMinimal,PDuplicat,nVars) == 0)
+//      return 0;
+//  else
+//      return 1;
 // }
 // 
 // void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int  nVars, cycleCtr* cCtr)
 // {
-//     int counter=1, cycles=0;   
-//     assert( nVars <= 16 );
-//     while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
-//     {
-//         counter=0;
-//         counter += minimalInitialFlip(pInOut, nVars);
-//         counter += minimalFlip(pInOut, pAux, pAux1, nVars);
-//         counter += minimalSwap(pInOut, pAux, pAux1, nVars);
-//         cCtr->totalCycles++;
-//         cycles++;
-//     }
-//     if(cycles < cCtr->minNCycles)
-//         cCtr->minNCycles = cycles;
-//     else if(cycles > cCtr->maxNCycles)
-//         cCtr->maxNCycles = cycles;
+//  int counter=1, cycles=0;   
+//  assert( nVars <= 16 );
+//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
+//  {
+//      counter=0;
+//      counter += minimalInitialFlip(pInOut, nVars);
+//      counter += minimalFlip(pInOut, pAux, pAux1, nVars);
+//      counter += minimalSwap(pInOut, pAux, pAux1, nVars);
+//      cCtr->totalCycles++;
+//      cycles++;
+//  }
+//  if(cycles < cCtr->minNCycles)
+//      cCtr->minNCycles = cycles;
+//  else if(cycles > cCtr->maxNCycles)
+//      cCtr->maxNCycles = cycles;
 // }
 //  runs paralel F and ~F in luckyCanonicizer
 // void luckyCanonicizer2(word* pInOut, word* pAux, word* pAux1, word* temp, int  nVars)
 // {
-//     int nWords = Kit_TruthWordNum_64bit( nVars );
-//     int counter=1, nOnes;   
-//     assert( nVars <= 16 );
-//     nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-//     
+//  int nWords = Kit_TruthWordNum_64bit( nVars );
+//  int counter=1, nOnes;   
+//  assert( nVars <= 16 );
+//  nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+//  
 //     if ( (nOnes*2 == nWords * 32) )
 //     { 
-//         Kit_TruthCopy_64bit( temp, pInOut, nVars );
-//         Kit_TruthNot_64bit( temp, nVars );
+//      Kit_TruthCopy_64bit( temp, pInOut, nVars );
+//      Kit_TruthNot_64bit( temp, nVars );
 //         luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars);
-//         luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
-//         if( memCompare(temp,pInOut,nVars) == -1)        
-//             Kit_TruthCopy_64bit(pInOut, temp, nVars );    
-//         return;        
-//     }
-//     while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
-//     {
-//         counter=0;
-//         counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
-//         counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
-//         counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+//      luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
+//      if( memCompare(temp,pInOut,nVars) == -1)        
+//          Kit_TruthCopy_64bit(pInOut, temp, nVars );  
+//      return;     
 //     }
+//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
+//  {
+//      counter=0;
+//      counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
+//      counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
+//      counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+//  }
 // }
 // same as luckyCanonicizer + cycleCtr stutistics 
 // void luckyCanonicizer1(word* pInOut, word* pAux, word* pAux1, int  nVars, cycleCtr* cCtr)
 // {
-//     int counter=1, cycles=0;   
-//     assert( nVars <= 16 );
-//     while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
-//     {
-//         counter=0;
-//         counter += minimalInitialFlip1(pInOut, nVars);
-//         counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
-//         counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
-//         cCtr->totalCycles++;
-//         cycles++;
-//     }
-//     if(cycles < cCtr->minNCycles)
-//         cCtr->minNCycles = cycles;
-//     else if(cycles > cCtr->maxNCycles)
-//         cCtr->maxNCycles = cycles;
+//  int counter=1, cycles=0;   
+//  assert( nVars <= 16 );
+//  while(counter>0 )   //  && cycles < 10 if we wanna limit cycles
+//  {
+//      counter=0;
+//      counter += minimalInitialFlip1(pInOut, nVars);
+//      counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
+//      counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+//      cCtr->totalCycles++;
+//      cycles++;
+//  }
+//  if(cycles < cCtr->minNCycles)
+//      cCtr->minNCycles = cycles;
+//  else if(cycles > cCtr->maxNCycles)
+//      cCtr->maxNCycles = cycles;
 // }
 // luckyCanonicizer 
 
@@ -404,7 +404,7 @@ inline int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars
         memcpy(pInOut, pMinimal, blockSize);
         *p_uCanonPhase = minTemp;
     }
-    if(memcmp(pInOut,PDuplicat,blockSize) == 0)    
+    if(memcmp(pInOut,PDuplicat,blockSize) == 0) 
         return 0;
     else
         return 1;
@@ -437,7 +437,7 @@ inline void swapInfoAdjacentVars(int iVar, char * pCanonPerm, unsigned* p_uCanon
 // this version is buggy and is fixed below
 inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase) 
 {
-    int i;    
+    int i;  
     int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
     int blockSizeChar = nVars *sizeof(char);
     memcpy(pMinimal, pInOut, blockSizeWord);
@@ -455,7 +455,7 @@ inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars
         else
         {
             memcpy(pInOut, pMinimal, blockSizeWord);
-            memcpy(pCanonPerm, tempArray, blockSizeChar);    
+            memcpy(pCanonPerm, tempArray, blockSizeChar);   
         }
         Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
         swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
@@ -474,7 +474,7 @@ inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars
 
 inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int  nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase) 
 {
-    int i;    
+    int i;  
     int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
     int blockSizeChar = nVars *sizeof(char);
     unsigned TempuCanonPhase = *p_uCanonPhase;
@@ -570,7 +570,7 @@ inline void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int  nVars,
         counter=0;
         counter += minimalInitialFlip(pInOut, nVars, p_uCanonPhase);
         counter += minimalFlip(pInOut, pAux, pAux1, nVars, p_uCanonPhase);
-        counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);    
+        counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);   
     }
 }
 // tries to find minimal F till F at the beginning of the loop is the same as at the end - irreducible 
@@ -629,22 +629,22 @@ unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nV
 
 int main () 
 {
-//     char * pFileInput  = "nonDSDfunc06var1M.txt";
-//     char * pFileInput1 = "partDSDfunc06var1M.txt";
-//     char * pFileInput2 = "fullDSDfunc06var1M.txt";
+//  char * pFileInput  = "nonDSDfunc06var1M.txt";
+//  char * pFileInput1 = "partDSDfunc06var1M.txt";
+//  char * pFileInput2 = "fullDSDfunc06var1M.txt";
 
-//     char * pFileInput  = "nonDSDfunc10var100K.txt";
-//     char * pFileInput1 = "partDSDfunc10var100K.txt";
-//     char * pFileInput2 = "fullDSDfunc10var100K.txt";
+//  char * pFileInput  = "nonDSDfunc10var100K.txt";
+//  char * pFileInput1 = "partDSDfunc10var100K.txt";
+//  char * pFileInput2 = "fullDSDfunc10var100K.txt";
 
-//    char * pFileInput = "partDSDfunc12var100K.txt";
-//    char * pFileInput  = "nonDSDfunc12var100K.txt";
-//     char * pFileInput1 = "partDSDfunc12var100K.txt";
-//     char * pFileInput2 = "fullDSDfunc12var100K.txt";
+//  char * pFileInput = "partDSDfunc12var100K.txt";
+//  char * pFileInput  = "nonDSDfunc12var100K.txt";
+//  char * pFileInput1 = "partDSDfunc12var100K.txt";
+//  char * pFileInput2 = "fullDSDfunc12var100K.txt";
 
-//     char * pFileInput  = "nonDSDfunc14var10K.txt";
-//     char * pFileInput1 = "partDSDfunc14var10K.txt";
-//     char * pFileInput2 = "fullDSDfunc14var10K.txt";
+//  char * pFileInput  = "nonDSDfunc14var10K.txt";
+//  char * pFileInput1 = "partDSDfunc14var10K.txt";
+//  char * pFileInput2 = "fullDSDfunc14var10K.txt";
 
     char * pFileInput  = "nonDSDfunc16var10K.txt";
     char * pFileInput1 = "partDSDfunc16var10K.txt";
@@ -656,7 +656,7 @@ int main ()
     Abc_TtStore_t* p;
     word * pAux, * pAux1;
     int * pStore;
-//    cycleCtr* cCtr;
+//  cycleCtr* cCtr;
     charArray = (char**)malloc(sizeof(char*)*3);
 
     charArray[0] = pFileInput;
@@ -664,35 +664,35 @@ int main ()
     charArray[2] = pFileInput2;
     for(j=0;j<3;j++)
     {
-        p = setTtStore(charArray[j]);    
-//        p = setTtStore(pFileInput);    
+        p = setTtStore(charArray[j]);   
+//      p = setTtStore(pFileInput); 
         a = makeArray(p);
-        b = makeArray(p);    
-//        cCtr = setCycleCtrPtr();
+        b = makeArray(p);   
+//      cCtr = setCycleCtrPtr();
 
-         pAux = (word*)malloc(sizeof(word)*(p->nWords));
-         pAux1 = (word*)malloc(sizeof(word)*(p->nWords));    
+        pAux = (word*)malloc(sizeof(word)*(p->nWords));
+        pAux1 = (word*)malloc(sizeof(word)*(p->nWords));    
         pStore = (int*)malloc(sizeof(int)*(p->nVars));
         printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
         
-         tempNF = p->nFuncs;
+        tempNF = p->nFuncs;
 
-        TimePrint("start");        
+        TimePrint("start");     
         for(i=0;i<p->nFuncs;i++)        
             luckyCanonicizer_final(a[i], pAux, pAux1, p->nVars, pStore);        
-         TimePrint("done with A");
+        TimePrint("done with A");
 
         sortAndUnique(a, p);
         printf("F left in A final = %d\n",p->nFuncs);
         freeArray(a,p);
-         TimePrint("Done with sort");
+        TimePrint("Done with sort");
         
 
-// delete data-structures    
+// delete data-structures   
         free(pAux);
         free(pAux1);    
         free(pStore);
-//        freeCycleCtr(cCtr);
+//      freeCycleCtr(cCtr);
         Abc_TruthStoreFree( p );
     }
     return 0;

src/bool/lucky/luckyFast16.c

@@ -24,7 +24,7 @@ static word SFmask[5][4] = {
     {0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
     {0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
     {0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
-    {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}    
+    {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}   
 };
 
 
@@ -44,7 +44,7 @@ inline void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ,
     int i;
     int  blockSize = 1<<iVar;
     for(i=start;i>=0;i--)
-    {    
+    {   
         pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) |
             (((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) |
             (((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) |
@@ -174,15 +174,15 @@ inline int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ,
 inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
 {
     int min1, min2, DifStart0, DifStart1, DifStartMin;
-    int M[2];    
+    int M[2];   
     int  blockSize = 1<<iVar;
-    int  shiftSize = blockSize*4;
+//  int  shiftSize = blockSize*4;
 
     M[0] = minTemp0_fast(pInOut, iVar, nWords, &DifStart0); // 0, 3
     M[1] = minTemp1_fast(pInOut, iVar, nWords, &DifStart1); // 1, 2
     min1 = minTemp2_fast(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
     if(DifStart0 != DifStart1)
-    {    
+    {   
         if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
             arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
         else if( DifStart0 > DifStart1)
@@ -213,12 +213,12 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
     int i,blockSize,shiftSize;
     unsigned* tempPtr = temp+start;
     if(iQ == 0 && jQ == 1)
-        return;    
+        return; 
     blockSize = sizeof(unsigned);
     shiftSize = 4;
     for(i=start-1;i>0;i-=shiftSize)
-    {        
-        tempPtr -= 1;        
+    {       
+        tempPtr -= 1;       
         memcpy(tempPtr, pInOut+i-iQ, blockSize);
         tempPtr -= 1;
         memcpy(tempPtr, pInOut+i-jQ, blockSize);
@@ -227,7 +227,7 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
         tempPtr -= 1;
         memcpy(tempPtr, pInOut+i-lQ, blockSize);        
         
-    }    
+    }   
     memcpy(pInOut, temp, start*sizeof(unsigned));
     updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
 }
@@ -237,7 +237,7 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
 inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
 {
     int i, temp;
-    for(i=(nWords)*2 - 1; i>=0; i-=4)    
+    for(i=(nWords)*2 - 1; i>=0; i-=4)   
     {
         temp = CompareWords(pInOut[i],pInOut[i-3]);
         if(temp == 0)
@@ -262,7 +262,7 @@ inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
 inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
 {
     int i, temp;
-    for(i=(nWords)*2 - 2; i>=0; i-=4)    
+    for(i=(nWords)*2 - 2; i>=0; i-=4)   
     {
         temp = CompareWords(pInOut[i],pInOut[i-1]);
         if(temp == 0)
@@ -287,7 +287,7 @@ inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
 inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart)
 {
     int i, temp;
-    for(i=(nWords)*2 - 1; i>=0; i-=4)    
+    for(i=(nWords)*2 - 1; i>=0; i-=4)   
     {
         temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
         if(temp == 0)
@@ -311,7 +311,7 @@ inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int
 inline int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart)
 {
     int i, temp;
-    for(i=start-1; i>=finish; i-=4)    
+    for(i=start-1; i>=finish; i-=4) 
     {
         temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
         if(temp == 0)
@@ -342,7 +342,7 @@ inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords,
     M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2
     min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin);
     if(DifStart0 != DifStart1)
-    {    
+    {   
         if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
             arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
         else if( DifStart0 > DifStart1)
@@ -379,17 +379,17 @@ inline void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int sta
     blockSize = wordBlock*sizeof(word);
     shiftSize = wordBlock*4;
     for(i=start-wordBlock;i>0;i-=shiftSize)
-    {        
-        tempPtr -= wordBlock;        
+    {       
+        tempPtr -= wordBlock;       
         memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize);
         tempPtr -= wordBlock;
         memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize);
         tempPtr -= wordBlock;
         memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize);
         tempPtr -= wordBlock;
-        memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);        
+        memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);      
         
-    }    
+    }   
     memcpy(pInOut, temp, start*sizeof(word));
     updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
 }
@@ -513,13 +513,13 @@ inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, i
     int M[2];
     word temp[1024];
     int  blockSize = 1<<(iVar-6);
-    int  shiftSize = blockSize*4;
+//  int  shiftSize = blockSize*4;
 
     M[0] = minTemp0_fast_moreThen5(pInOut, iVar, nWords, &DifStart0); // 0, 3
     M[1] = minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1); // 1, 2
     min1 = minTemp2_fast_moreThen5(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
     if(DifStart0 != DifStart1)
-    {    
+    {   
         if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
             arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
         else if( DifStart0 > DifStart1)
@@ -549,7 +549,7 @@ inline void minimalInitialFlip_fast_16Vars(word* pInOut, int  nVars, unsigned* p
     if(  (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
     {
         Kit_TruthNot_64bit( pInOut, nVars );
-        (* pCanonPhase) ^=(1<<nVars);        
+        (* pCanonPhase) ^=(1<<nVars);       
     }
 
 }
@@ -559,7 +559,7 @@ inline void minimalInitialFlip_fast_16Vars(word* pInOut, int  nVars, unsigned* p
 inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
 {
     int i;
-    word pDuplicate[1024];    
+    word pDuplicate[1024];  
     int bitInfoTemp = pStore[0];
     memcpy(pDuplicate,pInOut,nWords*sizeof(word));
     for(i=0;i<5;i++)
@@ -602,21 +602,21 @@ inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int  nVars, int nWord
 
 inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
 {
-//     word pDuplicateLocal[1024]={0};
-//     memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
+//  word pDuplicateLocal[1024]={0};
+//  memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
     assert( nVars <= 16 );
     assert( nVars > 6 );
     (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
     luckyCanonicizerS_F_first_16Vars(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
-//     memcpy(pDuplicate,pInOut,nWords*sizeof(word));
-//     assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
+//  memcpy(pDuplicate,pInOut,nWords*sizeof(word));
+//  assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
 }
 
 // top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
 int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
 {
     int pStore[16];
-    int uCanonPhase = 0;
+    unsigned uCanonPhase = 0;
     int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
     if ( nVars <= 6 )
         pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );

src/bool/lucky/luckyFast6.c

@@ -89,7 +89,7 @@ inline word Abc_allFlip(word x, unsigned* pCanonPhase)
 }
 
 inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
-{    
+{   
     if(info<4)
         return (uCanonPhase ^= (info << iVar));
     else
@@ -104,7 +104,7 @@ inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int
             uCanonPhase ^= (1 << iVar);
             uCanonPhase ^= (1 << (iVar+1));
         }
-        return uCanonPhase;    
+        return uCanonPhase; 
     }
 
 
@@ -207,8 +207,8 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
         tMin0 = tMin;
         for ( i = 0; i < 5; i++ )
         {
-            if(bitInfoTemp == pStore[i+1])            
-                tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );            
+            if(bitInfoTemp == pStore[i+1])          
+                tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );         
             else
                 bitInfoTemp = pStore[i+1];
         } 
@@ -220,9 +220,9 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
 
 inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
 {
-//    word temp, duplicat = InOut;
+//  word temp, duplicat = InOut;
     (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
-//     InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
+//  InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
 //      temp = InOut;
 //      assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
 //      return(InOut); 

src/bool/lucky/luckyInt.h

@@ -78,7 +78,7 @@ typedef struct
     int totalSwaps;
     int* flipArray;
     int flipCtr;
-    int totalFlips;    
+    int totalFlips; 
 }permInfo;
 
 

src/bool/lucky/luckySwap.c

@@ -20,7 +20,7 @@
 ABC_NAMESPACE_IMPL_START
 
 
-static word mask0[6] = { 0x5555555555555555,0x3333333333333333, 0x0F0F0F0F0F0F0F0F,0x00FF00FF00FF00FF,0x0000FFFF0000FFFF, 0x00000000FFFFFFFF};    
+static word mask0[6] = { 0x5555555555555555,0x3333333333333333, 0x0F0F0F0F0F0F0F0F,0x00FF00FF00FF00FF,0x0000FFFF0000FFFF, 0x00000000FFFFFFFF};  
 /*
 static word mask1[6] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
 static word mask[6][2] =   {
@@ -55,7 +55,7 @@ inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars )
 }
 
 inline void Kit_TruthCountOnesInCofs_64bit( word * pTruth, int nVars, int * pStore )
-{     
+{    
     int nWords = Kit_TruthWordNum_64bit( nVars );
     int i, k, Counter;
     memset( pStore, 0, sizeof(int) * nVars );
@@ -72,7 +72,7 @@ inline void Kit_TruthCountOnesInCofs_64bit( word * pTruth, int nVars, int * pSto
         if ( nVars > 4 )       
             pStore[4] = Kit_WordCountOnes_64bit( pTruth[0] & 0x0000FFFF0000FFFF ); 
         if ( nVars > 5 )       
-            pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00000000FFFFFFFF );         
+            pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00000000FFFFFFFF );      
         return;
     }
     // nVars > 6
@@ -114,13 +114,13 @@ inline void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar )
         Step = (1 << (iVar - 6));
         SizeOfBlock = sizeof(word)*Step;
         for ( i = 0; i < nWords; i += 2*Step )
-        {    
+        {   
             memcpy(Temp,pInOut,SizeOfBlock);
             memcpy(pInOut,pInOut+Step,SizeOfBlock);
             memcpy(pInOut+Step,Temp,SizeOfBlock);
-            //             Temp = pInOut[i];
-            //             pInOut[i] = pInOut[Step+i];
-            //             pInOut[Step+i] = Temp;            
+            //          Temp = pInOut[i];
+            //          pInOut[i] = pInOut[Step+i];
+            //          pInOut[Step+i] = Temp;          
             pInOut += 2*Step;
         }
     }
@@ -164,7 +164,7 @@ inline void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar
         SizeOfBlock = sizeof(word)*Step;
         pInOut += 2*Step;
         for(i=2*Step; i<nWords; i+=4*Step)
-        {            
+        {           
             memcpy(temp,pInOut-Step,SizeOfBlock);
             memcpy(pInOut-Step,pInOut,SizeOfBlock);
             memcpy(pInOut,temp,SizeOfBlock);
@@ -236,7 +236,7 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
                 uCanonPhase ^= (1 << (i+1));
             }
             
-            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );            
         }
     } while ( fChange );
     return uCanonPhase;
@@ -250,8 +250,8 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
     assert( nVars <= 16 );
     
     nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-    //     if ( (nOnes == nWords * 32) )
-    //         return 999999;
+    //  if ( (nOnes == nWords * 32) )
+    //      return 999999;
     
     if ( (nOnes > nWords * 32) )
     {
@@ -266,8 +266,8 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
-        //         if (  pStore[i]  == nOnes-pStore[i])
-        //             return 999999;
+        //      if (  pStore[i]  == nOnes-pStore[i])
+        //          return 999999;
         if ( pStore[i] >= nOnes-pStore[i])
             continue;
         uCanonPhase |= (1 << i);
@@ -298,7 +298,7 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
                 uCanonPhase ^= (1 << (i+1));
             }
             
-            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );            
         }
     } while ( fChange );
     return uCanonPhase;
@@ -311,19 +311,19 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
 //     int pStore[16];
 //     int nWords = Kit_TruthWordNum_64bit( nVars );
 //     int i, Temp, fChange, nOnes; 
-//     assert( nVars <= 16 );
-//     
+//  assert( nVars <= 16 );
+//  
 //     nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-//     
+//  
 //     if ( (nOnes > nWords * 32) )
 //     { 
 //         Kit_TruthNot_64bit( pInOut, nVars );
-//         nOnes = nWords*64 - nOnes;
+//      nOnes = nWords*64 - nOnes;
 //     }
-//     
+//  
 //     // collect the minterm counts
 //     Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
-//     
+//  
 //     // canonicize phase
 //     for ( i = 0; i < nVars; i++ )
 //     {
@@ -332,19 +332,19 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
 //         pStore[i] = nOnes-pStore[i]; 
 //         Kit_TruthChangePhase_64bit( pInOut, nVars, i );
 //     }  
-//     
+//  
 //     do {
 //         fChange = 0;
 //         for ( i = 0; i < nVars-1; i++ )
 //         {
 //             if ( pStore[i] <= pStore[i+1] )
 //                 continue;            
-//             fChange = 1;            
-//             
+//             fChange = 1;         
+//          
 //             Temp = pStore[i];
 //             pStore[i] = pStore[i+1];
 //             pStore[i+1] = Temp;
-//             
+//          
 //             Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
 //         }
 //     } while ( fChange ); 
@@ -389,7 +389,7 @@ inline void  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int
             pStore[i] = pStore[i+1];
             pStore[i+1] = Temp;
             
-            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );            
         }
     } while ( fChange ); 
 }

src/bool/lucky/luckySwapIJ.c

@@ -24,7 +24,7 @@ void swap_ij_case1( word* f,int totalVars, int i, int j)
 {
     int e,wordsNumber,n,shift;
     word maskArray[45]=
-    {    0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
+    {   0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
     0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 ,0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 ,
     0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 ,0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 ,
     0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 ,0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 ,
@@ -51,7 +51,7 @@ void swap_ij_case2( word* f,int totalVars, int i, int j)
     word temp;
     int x,y,wj;
     int WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
-    //    int forShift = ((Word)1)<<i;
+    //  int forShift = ((Word)1)<<i;
     int forShift = (1<<i);
     wj = 1 << (j - 6);
     x = 0;