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

8 files changed, 1112 insertions, 10 deletions

diff --git a/src/bool/lucky/lucky.c b/src/bool/lucky/lucky.c
index 8fc413be..159c54bc 100644
--- a/src/bool/lucky/lucky.c
+++ b/src/bool/lucky/lucky.c
@@ -655,7 +655,7 @@ int main ()
     word** a, ** b;
     Abc_TtStore_t* p;
     word * pAux, * pAux1;
-    short * pStore;
+    int * pStore;
 //    cycleCtr* cCtr;
     charArray = (char**)malloc(sizeof(char*)*3);
 
@@ -672,7 +672,7 @@ int main ()
 
          pAux = (word*)malloc(sizeof(word)*(p->nWords));
          pAux1 = (word*)malloc(sizeof(word)*(p->nWords));    
-        pStore = (short*)malloc(sizeof(short)*(p->nVars));
+        pStore = (int*)malloc(sizeof(int)*(p->nVars));
         printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
         
          tempNF = p->nFuncs;
diff --git a/src/bool/lucky/lucky.h b/src/bool/lucky/lucky.h
index 7b866bc7..0a055b40 100644
--- a/src/bool/lucky/lucky.h
+++ b/src/bool/lucky/lucky.h
@@ -6,7 +6,7 @@
 
   PackageName [Semi-canonical form computation package.]
 
-  Synopsis    [Internal declarations.]
+  Synopsis    [External declarations.]
 
   Author      [Jake]
 
@@ -21,6 +21,8 @@
 ABC_NAMESPACE_HEADER_START
 
 extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
+extern int      luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
+extern void     resetPCanonPermArray(char* x, int nVars); 
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/bool/lucky/luckyFast16.c b/src/bool/lucky/luckyFast16.c
new file mode 100644
index 00000000..518f236b
--- /dev/null
+++ b/src/bool/lucky/luckyFast16.c
@@ -0,0 +1,625 @@
+/**CFile****************************************************************
+
+  FileName    [luckyFast16.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Truth table minimization procedures for up to  16 vars.]
+
+  Author      [Jake]
+
+  Date        [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
+//updataInfo updates CanonPerm and CanonPhase based on what quoter in position iQ and jQ
+inline void updataInfo(int iQ, int jQ, int iVar,  char * pCanonPerm, unsigned* pCanonPhase)
+{
+    *pCanonPhase = adjustInfoAfterSwap(pCanonPerm, *pCanonPhase, iVar, ((abs(iQ-jQ)-1)<<2) + iQ );
+
+}
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    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) |
+            (((pInOut[i] & SFmask[iVar][lQ])<<(lQ*blockSize))>>3*blockSize);
+    }
+    updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+    int i, j=1;
+    int  blockSize = 1<<iVar;
+    int  shiftSize = blockSize*4;
+    word temp;
+    for(i=nWords - 1; i>=0; i--)
+    {
+        temp = ((pInOut[i] & SFmask[iVar][0])) ^ ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize));
+        if( temp == 0)
+            continue;
+        else
+        {
+            *pDifStart = i*100;
+            while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+                j++;
+            *pDifStart += 21 - j;
+
+            if( ((pInOut[i] & SFmask[iVar][0])) < ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)) )
+                return 0;
+            else
+                return 3;
+        }
+    }
+    *pDifStart=0;
+    return 0;
+
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+    int i, j=1;
+    int  blockSize = 1<<iVar;
+    int  shiftSize = blockSize*4;
+    word temp;
+    for(i=nWords - 1; i>=0; i--)
+    {
+        temp = ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) ^ ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize));
+        if( temp == 0)
+            continue;
+        else
+        {
+            *pDifStart = i*100;
+            while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+                j++;
+            *pDifStart += 21 - j;
+            if( ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) < ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)) )
+                return 1;
+            else
+                return 2;
+        }
+    }
+    *pDifStart=0;
+    return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+inline int minTemp2_fast(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
+{
+    int i, j=1;
+    int  blockSize = 1<<iVar;
+    int  shiftSize = blockSize*4;
+    word temp;
+    for(i=nWords - 1; i>=0; i--)
+    {
+        temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
+        if( temp == 0)
+            continue;
+        else
+        {
+            *pDifStart = i*100;
+            while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+                j++;
+            *pDifStart += 21 - j;
+            if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
+                return 0;
+            else
+                return 1;
+        }
+    }
+    *pDifStart=0;
+    return iQ;
+}
+// same as minTemp2_fast but this one has a start position
+inline int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
+{
+    int i, j=1;
+    int  blockSize = 1<<iVar;
+    int  shiftSize = blockSize*4;
+    word temp;
+    for(i=start; i>=finish; i--)
+    {
+        temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
+        if( temp == 0)
+            continue;
+        else
+        {
+            *pDifStart = i*100;
+            while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+                j++;
+            *pDifStart += 21 - j;
+
+            if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
+                return 0;
+            else
+                return 1;
+        }
+    }
+    *pDifStart=0;
+    return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them  
+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  blockSize = 1<<iVar;
+    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)
+            arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart0/100), M[0], M[1], 3 - M[1], 3 - M[0], iVar, nWords, pCanonPerm, pCanonPhase);
+        else
+            arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart1/100), M[1], M[0], 3 - M[0], 3 - M[1], iVar, nWords, pCanonPerm, pCanonPhase);
+    }
+    else
+    {
+        if(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
+        {
+            min2 = minTemp3_fast(pInOut, iVar, DifStart0/100, DifStartMin/100, 3-M[0], 3-M[1], &DifStart1);  // reuse DifStart1 because DifStart1 = DifStart1=0
+            if(DifStart1>DifStartMin)
+                arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, nWords, pCanonPerm, pCanonPhase);
+            else
+                arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
+        }
+    }
+}
+////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int start,  int iQ, int jQ, int kQ, int lQ, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int i,blockSize,shiftSize;
+    unsigned* tempPtr = temp+start;
+    if(iQ == 0 && jQ == 1)
+        return;    
+    blockSize = sizeof(unsigned);
+    shiftSize = 4;
+    for(i=start-1;i>0;i-=shiftSize)
+    {        
+        tempPtr -= 1;        
+        memcpy(tempPtr, pInOut+i-iQ, blockSize);
+        tempPtr -= 1;
+        memcpy(tempPtr, pInOut+i-jQ, blockSize);
+        tempPtr -= 1;
+        memcpy(tempPtr, pInOut+i-kQ, blockSize);
+        tempPtr -= 1;
+        memcpy(tempPtr, pInOut+i-lQ, blockSize);        
+        
+    }    
+    memcpy(pInOut, temp, start*sizeof(unsigned));
+    updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
+{
+    int i, temp;
+    for(i=(nWords)*2 - 1; i>=0; i-=4)    
+    {
+        temp = CompareWords(pInOut[i],pInOut[i-3]);
+        if(temp == 0)
+            continue;
+        else if(temp == -1)
+        {
+            *pDifStart = i+1;
+            return 0;
+        }
+        else
+        {
+            *pDifStart = i+1;
+            return 3;
+        }
+    }
+    *pDifStart=0;
+    return 0;
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
+{
+    int i, temp;
+    for(i=(nWords)*2 - 2; i>=0; i-=4)    
+    {
+        temp = CompareWords(pInOut[i],pInOut[i-1]);
+        if(temp == 0)
+            continue;
+        else if(temp == -1)
+        {
+            *pDifStart = i+2;
+            return 1;
+        }
+        else
+        {
+            *pDifStart = i+2;
+            return 2;
+        }
+    }
+    *pDifStart=0;
+    return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+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)    
+    {
+        temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
+        if(temp == 0)
+            continue;
+        else if(temp == -1)
+        {
+            *pDifStart = i+1;
+            return 0;
+        }
+        else
+        {
+            *pDifStart = i+1;
+            return 1;
+        }
+    }
+    *pDifStart=0;
+    return iQ;
+}
+
+// same as minTemp2_fast but this one has a start position
+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)    
+    {
+        temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
+        if(temp == 0)
+            continue;
+        else if(temp == -1)
+        {
+            *pDifStart = i+1;
+            return 0;
+        }
+        else
+        {
+            *pDifStart = i+1;
+            return 1;
+        }
+    }
+    *pDifStart=0;
+    return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them 
+inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int min1, min2, DifStart0, DifStart1, DifStartMin;
+    int M[2];
+    unsigned temp[2048];
+
+    M[0] = minTemp0_fast_iVar5(pInOut, nWords, &DifStart0); // 0, 3
+    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)
+            arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], pCanonPerm, pCanonPhase);
+        else
+            arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], pCanonPerm, pCanonPhase);
+    }
+    else
+    {
+        if(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
+        {
+            min2 = minTemp3_fast_iVar5(pInOut, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1);  // reuse DifStart1 because DifStart1 = DifStart1=0
+            if(DifStart1>DifStartMin)
+                arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], pCanonPerm, pCanonPhase);
+            else
+                arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
+        }
+    }
+}
+
+////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int start,  int iQ, int jQ, int kQ, int lQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int i,wordBlock,blockSize,shiftSize;
+    word* tempPtr = temp+start;
+    if(iQ == 0 && jQ == 1)
+        return;
+    wordBlock = (1<<(iVar-6));
+    blockSize = wordBlock*sizeof(word);
+    shiftSize = wordBlock*4;
+    for(i=start-wordBlock;i>0;i-=shiftSize)
+    {        
+        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(pInOut, temp, start*sizeof(word));
+    updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+    int i, j, temp;
+    int  wordBlock = 1<<(iVar-6);
+    int wordDif = 3*wordBlock;
+    int  shiftBlock = wordBlock*4;
+    for(i=nWords - 1; i>=0; i-=shiftBlock)
+        for(j=0;j<wordBlock;j++)
+        {
+            temp = CompareWords(pInOut[i-j],pInOut[i-j-wordDif]);
+            if(temp == 0)
+                continue;
+            else if(temp == -1)
+            {
+                *pDifStart = i+1;
+                return 0;
+            }
+            else
+            {
+                *pDifStart = i+1;
+                return 3;
+            }
+        }
+    *pDifStart=0;
+    return 0;
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+    int i, j, temp;
+    int  wordBlock = 1<<(iVar-6);
+    int  shiftBlock = wordBlock*4;
+    for(i=nWords - wordBlock - 1; i>=0; i-=shiftBlock)
+        for(j=0;j<wordBlock;j++)
+        {
+            temp = CompareWords(pInOut[i-j],pInOut[i-j-wordBlock]);
+            if(temp == 0)
+                continue;
+            else if(temp == -1)
+            {
+                *pDifStart = i+wordBlock+1;
+                return 1;
+            }
+            else
+            {
+                *pDifStart = i+wordBlock+1;
+                return 2;
+            }
+        }
+    *pDifStart=0;
+    return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+inline int minTemp2_fast_moreThen5(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
+{
+    int i, j, temp;
+    int  wordBlock = 1<<(iVar-6);
+    int  shiftBlock = wordBlock*4;
+    for(i=nWords - 1; i>=0; i-=shiftBlock)
+        for(j=0;j<wordBlock;j++)
+        {
+            temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
+            if(temp == 0)
+                continue;
+            else if(temp == -1)
+            {
+                *pDifStart = i+1;
+                return 0;
+            }
+            else
+            {
+                *pDifStart = i+1;
+                return 1;
+            }
+        }
+    *pDifStart=0;
+    return iQ;
+}
+
+// same as minTemp2_fast but this one has a start position
+inline int minTemp3_fast_moreThen5(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
+{
+    int i, j, temp;
+    int  wordBlock = 1<<(iVar-6);
+    int  shiftBlock = wordBlock*4;
+    for(i=start-1; i>=finish; i-=shiftBlock)
+        for(j=0;j<wordBlock;j++)
+        {
+            temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
+            if(temp == 0)
+                continue;
+            else if(temp == -1)
+            {
+                *pDifStart = i+1;
+                return 0;
+            }
+            else
+            {
+                *pDifStart = i+1;
+                return 1;
+            }
+        }
+    *pDifStart=0;
+    return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them 
+inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int min1, min2, DifStart0, DifStart1, DifStartMin;
+    int M[2];
+    word temp[1024];
+    int  blockSize = 1<<(iVar-6);
+    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)
+            arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], iVar, pCanonPerm, pCanonPhase);
+        else
+            arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], iVar, pCanonPerm, pCanonPhase);
+    }
+    else
+    {
+        if(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
+        {
+            min2 = minTemp3_fast_moreThen5(pInOut, iVar, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1);  // reuse DifStart1 because DifStart1 = DifStart1=0
+            if(DifStart1>DifStartMin)
+                arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, pCanonPerm, pCanonPhase);
+            else
+                arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
+        }
+    }
+}
+
+/////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
+inline void minimalInitialFlip_fast_16Vars(word* pInOut, int  nVars, unsigned* pCanonPhase)
+{
+    word oneWord=1;
+    if(  (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
+    {
+        Kit_TruthNot_64bit( pInOut, nVars );
+        (* pCanonPhase) ^=(1<<nVars);        
+    }
+
+}
+
+// this function finds minimal for all TIED(and tied only) iVars 
+//it finds tied vars based on rearranged  Store info - group of tied vars has the same bit count in Store
+inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    int i;
+    word pDuplicate[1024];    
+    int bitInfoTemp = pStore[0];
+    memcpy(pDuplicate,pInOut,nWords*sizeof(word));
+    for(i=0;i<5;i++)
+    {
+        if(bitInfoTemp == pStore[i+1])
+            minimalSwapAndFlipIVar_superFast_lessThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+        else
+        {
+            bitInfoTemp = pStore[i+1];
+            continue;
+        }
+    }
+    if(bitInfoTemp == pStore[i+1])
+        minimalSwapAndFlipIVar_superFast_iVar5((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
+    else    
+        bitInfoTemp = pStore[i+1];
+    
+    for(i=6;i<nVars-1;i++)
+    {
+        if(bitInfoTemp == pStore[i+1])
+            minimalSwapAndFlipIVar_superFast_moreThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+        else
+        {
+            bitInfoTemp = pStore[i+1];
+            continue;
+        }
+    }
+    if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
+        return 0;
+    else
+        return 1;
+}
+
+inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+    minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
+    while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
+        continue;
+}
+
+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));
+    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));
+}
+
+// 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;
+    int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
+    if ( nVars <= 6 )
+        pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
+    else if ( nVars <= 16 )
+        luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
+    else assert( 0 );
+    return uCanonPhase;
+}
+
+
+ABC_NAMESPACE_IMPL_END
+
+
+
+
diff --git a/src/bool/lucky/luckyFast6.c b/src/bool/lucky/luckyFast6.c
new file mode 100644
index 00000000..9ba6691c
--- /dev/null
+++ b/src/bool/lucky/luckyFast6.c
@@ -0,0 +1,233 @@
+/**CFile****************************************************************
+
+  FileName    [luckyFast6.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Truth table minimization procedures for 6 vars.]
+
+  Author      [Jake]
+
+  Date        [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+inline void resetPCanonPermArray_6Vars(char* x)
+{
+    x[0]='a';
+    x[1]='b';
+    x[2]='c';
+    x[3]='d';
+    x[4]='e';
+    x[5]='f';
+}
+inline void resetPCanonPermArray(char* x, int nVars)
+{
+    int i;
+    for(i=0;i<nVars;i++)
+        x[i] = 'a'+i;
+}
+
+// we need next two functions only for verification of lucky method in debugging mode 
+void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
+{
+    int Temp;
+    swap_ij(pAfter, nVars, iVarInPosition, jVar);
+    
+    Temp = pCanonPerm[iVarInPosition];
+    pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
+    pCanonPerm[jVar] = Temp;
+    
+    if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
+    {
+        *pUCanonPhase ^= (1 << iVarInPosition);
+        *pUCanonPhase ^= (1 << jVar);
+    }
+    if(*pUCanonPhase>>iVarInPosition & (unsigned)1 == 1)
+        Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
+    
+}
+int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
+{
+    int i,j;
+    char tempChar;
+    for(j=0;j<nVars;j++)
+    {
+        tempChar = 'a'+ j;
+        for(i=j;i<nVars;i++)
+        {
+            if(tempChar != pCanonPerm[i])
+                continue;
+            swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
+            break;
+        }
+    }
+    if(uCanonPhase>>nVars & (unsigned)1 == 1)
+        Kit_TruthNot_64bit(pAfter, nVars );
+    if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
+        return 0;
+    else
+        return 1;
+}
+
+inline word Abc_allFlip(word x, unsigned* pCanonPhase)
+{
+    if(  (x>>63) )
+    {
+        (* pCanonPhase) ^=(1<<6);
+        return ~x;
+    }
+    else 
+        return x;
+    
+}
+
+inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
+{    
+    if(info<4)
+        return (uCanonPhase ^= (info << iVar));
+    else
+    {
+        char temp;
+        uCanonPhase ^= ((info-4) << iVar);
+        temp=pCanonPerm[iVar];
+        pCanonPerm[iVar]=pCanonPerm[iVar+1];
+        pCanonPerm[iVar+1]=temp;
+        if ( ((uCanonPhase & (1 << iVar)) > 0) != ((uCanonPhase & (1 << (iVar+1))) > 0) )
+        {
+            uCanonPhase ^= (1 << iVar);
+            uCanonPhase ^= (1 << (iVar+1));
+        }
+        return uCanonPhase;    
+    }
+
+
+}
+
+inline word Extra_Truth6SwapAdjacent( word t, int iVar )
+{
+    // variable swapping code
+    static word PMasks[5][3] = {
+        { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+        { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+        { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+        { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+        { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+    };
+    assert( iVar < 5 );
+    return (t & PMasks[iVar][0]) | ((t & PMasks[iVar][1]) << (1 << iVar)) | ((t & PMasks[iVar][2]) >> (1 << iVar));
+}
+inline word Extra_Truth6ChangePhase( word t, int iVar)
+{
+    // elementary truth tables
+    static word Truth6[6] = {
+        0xAAAAAAAAAAAAAAAA,
+            0xCCCCCCCCCCCCCCCC,
+            0xF0F0F0F0F0F0F0F0,
+            0xFF00FF00FF00FF00,
+            0xFFFF0000FFFF0000,
+            0xFFFFFFFF00000000
+    };
+    assert( iVar < 6 );
+    return ((t & ~Truth6[iVar]) << (1 << iVar)) | ((t & Truth6[iVar]) >> (1 << iVar));
+}
+
+inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, unsigned* pCanonPhase )
+{
+    word tCur, tMin = t; // ab 
+    unsigned info =0;
+    assert( iVar >= 0 && iVar < 5 );
+    
+    tCur = Extra_Truth6ChangePhase( t, iVar );    // !a b
+    if(tCur<tMin)
+    {
+        info = 1;
+        tMin = tCur;
+    }
+    tCur = Extra_Truth6ChangePhase( t, iVar+1 );  // a !b
+    if(tCur<tMin)
+    {
+        info = 2;
+        tMin = tCur;
+    }
+    tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !a !b
+    if(tCur<tMin)
+    {
+        info = 3;
+        tMin = tCur;
+    }
+    
+    t    = Extra_Truth6SwapAdjacent( t, iVar );   // b a
+    if(t<tMin)
+    {
+        info = 4;
+        tMin = t;
+    }
+    
+    tCur = Extra_Truth6ChangePhase( t, iVar );    // !b a
+    if(tCur<tMin)
+    {
+        info = 6;
+        tMin = tCur;
+    }
+    tCur = Extra_Truth6ChangePhase( t, iVar+1 );  // b !a
+    if(tCur<tMin)
+    {
+        info = 5;
+        tMin = tCur;
+    }
+    tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !b !a
+    if(tCur<tMin)
+    {
+        (* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, 7);
+        return tCur;
+    }
+    else
+    {
+        (* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, info);
+        return tMin;
+    }
+}
+// this function finds minimal for all TIED(and tied only) iVars 
+//it finds tied vars based on rearranged  Store info - group of tied vars has the same bit count in Store
+inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+    int i, bitInfoTemp;
+    word tMin0, tMin;
+    tMin=Abc_allFlip(t, pCanonPhase);
+    do
+    {
+        bitInfoTemp = pStore[0];
+        tMin0 = tMin;
+        for ( i = 0; i < 5; i++ )
+        {
+            if(bitInfoTemp == pStore[i+1])            
+                tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );            
+            else
+                bitInfoTemp = pStore[i+1];
+        } 
+        
+    }while ( tMin0 != tMin );
+    return tMin;
+}
+
+
+inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+//    word temp, duplicat = InOut;
+    (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
+//     InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
+//      temp = InOut;
+//      assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
+//      return(InOut); 
+    return Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPerm, pCanonPhase );
+    
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 295d3c30..02dc690d 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -24,6 +24,7 @@
 #include <math.h>
 #include <time.h>
 
+
 // comment out this line to run Lucky Code outside of ABC
 #define _RUNNING_ABC_
 
@@ -80,6 +81,8 @@ typedef struct
     int totalFlips;    
 }permInfo;
 
+
+
 static inline void TimePrint( char* Message )
 {
     static int timeBegin;
@@ -89,6 +92,25 @@ static inline void TimePrint( char* Message )
     timeBegin = clock();
 }
 
+static word SFmask[5][4] = {
+    {0x8888888888888888,0x4444444444444444,0x2222222222222222,0x1111111111111111},
+    {0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
+    {0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
+    {0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
+    {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}    
+};
+
+static inline int CompareWords(word x, word  y)
+{
+    if(x>y)
+        return 1;
+    else if(x<y)
+        return -1;
+    else
+        return 0;
+    
+}
+
 extern  inline int memCompare(word* x, word*  y, int nVars);
 extern  inline int Kit_TruthWordNum_64bit( int nVars );
 extern  Abc_TtStore_t * setTtStore(char * pFileInput);
@@ -101,8 +123,16 @@ extern  inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars );
 extern  void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
 extern  permInfo* setPermInfoPtr(int var);
 extern  void freePermInfoPtr(permInfo* x);
-extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm  );
-extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm );
+extern  inline void  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
+extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
+extern  inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore );
+extern  inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase );
+extern  inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
+extern  inline void resetPCanonPermArray_6Vars(char* x);
+extern  void swap_ij( word* f,int totalVars, int varI, int varJ);
+extern  inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
+extern  inline void resetPCanonPermArray(char* x, int nVars);
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
index 46db2b0f..2a710160 100644
--- a/src/bool/lucky/luckySwap.c
+++ b/src/bool/lucky/luckySwap.c
@@ -16,6 +16,7 @@
 
 #include "luckyInt.h"
 
+
 ABC_NAMESPACE_IMPL_START
 
 
@@ -205,7 +206,7 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
-        if ( pStore[i] <= nOnes-pStore[i])
+        if ( pStore[i] >= nOnes-pStore[i])
             continue;
         uCanonPhase |= (1 << i);
         pStore[i] = nOnes-pStore[i]; 
@@ -240,11 +241,118 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
     } while ( fChange );
     return uCanonPhase;
 }
+inline unsigned  Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
+{
+    int nWords = Kit_TruthWordNum_64bit( nVars );
+    int i, fChange, nOnes;
+    int Temp;
+    unsigned  uCanonPhase=0;
+    assert( nVars <= 16 );
+    
+    nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+    //     if ( (nOnes == nWords * 32) )
+    //         return 999999;
+    
+    if ( (nOnes > nWords * 32) )
+    {
+        uCanonPhase |= (1 << nVars);
+        Kit_TruthNot_64bit( pInOut, nVars );
+        nOnes = nWords*64 - nOnes;
+    }
+    
+    // collect the minterm counts
+    Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
+    
+    // canonicize phase
+    for ( i = 0; i < nVars; i++ )
+    {
+        //         if (  pStore[i]  == nOnes-pStore[i])
+        //             return 999999;
+        if ( pStore[i] >= nOnes-pStore[i])
+            continue;
+        uCanonPhase |= (1 << i);
+        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;
+            
+            Temp = pCanonPerm[i];
+            pCanonPerm[i] = pCanonPerm[i+1];
+            pCanonPerm[i+1] = Temp;
+            
+            Temp = pStore[i];
+            pStore[i] = pStore[i+1];
+            pStore[i+1] = Temp;
+            
+            // if the polarity of variables is different, swap them
+            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+            {
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << (i+1));
+            }
+            
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
+        }
+    } while ( fChange );
+    return uCanonPhase;
+}
+
 
-inline unsigned  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
+// inline unsigned  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
+// {
+//     unsigned uCanonPhase = 0;
+//     int pStore[16];
+//     int nWords = Kit_TruthWordNum_64bit( nVars );
+//     int i, Temp, fChange, nOnes; 
+//     assert( nVars <= 16 );
+//     
+//     nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+//     
+//     if ( (nOnes > nWords * 32) )
+//     { 
+//         Kit_TruthNot_64bit( pInOut, nVars );
+//         nOnes = nWords*64 - nOnes;
+//     }
+//     
+//     // collect the minterm counts
+//     Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
+//     
+//     // canonicize phase
+//     for ( i = 0; i < nVars; i++ )
+//     {
+//         if ( pStore[i] >= nOnes-pStore[i])
+//             continue;        
+//         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;            
+//             
+//             Temp = pStore[i];
+//             pStore[i] = pStore[i+1];
+//             pStore[i+1] = Temp;
+//             
+//             Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
+//         }
+//     } while ( fChange ); 
+//     return uCanonPhase;
+// }
+
+inline void  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore )
 {
-    unsigned uCanonPhase = 0;
-    int pStore[16];
     int nWords = Kit_TruthWordNum_64bit( nVars );
     int i, Temp, fChange, nOnes; 
     assert( nVars <= 16 );
@@ -284,7 +392,6 @@ inline unsigned  Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars,
             Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );             
         }
     } while ( fChange ); 
-    return uCanonPhase;
 }
 
 
diff --git a/src/bool/lucky/luckySwapIJ.c b/src/bool/lucky/luckySwapIJ.c
new file mode 100644
index 00000000..1d598c2a
--- /dev/null
+++ b/src/bool/lucky/luckySwapIJ.c
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [luckySwapIJ.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [just for support of swap_ij() function]
+
+  Author      [Jake]
+
+  Date        [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+
+ABC_NAMESPACE_IMPL_START
+
+
+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,
+    0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 ,0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 ,
+    0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 ,0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 ,
+    0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 ,0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 ,
+    0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 ,0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 ,
+    0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 ,0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 ,
+    0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 ,0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 ,
+    0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000
+    };
+    e = 3*((9*i - i*i -2)/2 + j);          //  Exact formula for index in maskArray
+    wordsNumber = Kit_TruthWordNum_64bit(totalVars);
+    shift = (1<<j)-(1<<i);
+    for(n = 0; n < wordsNumber; n++)
+        f[n] = (f[n]&maskArray[e])+((f[n]&(maskArray[e+1]))<< shift)+((f[n]&(maskArray[e+2]))>> shift);
+}
+//  "width" - how many "Words" in a row have "1s" (or "0s")in position "i"
+//   wi - width of i
+//   wj - width of j
+//   wwi = 2*wi; wwj = 2*wj;
+
+void swap_ij_case2( word* f,int totalVars, int i, int j)
+{
+    word mask[] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
+    word temp;
+    int x,y,wj;
+    int WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
+    //    int forShift = ((Word)1)<<i;
+    int forShift = (1<<i);
+    wj = 1 << (j - 6);
+    x = 0;
+    y = wj;
+    for(y=wj; y<WORDS_IN_TT;y+=2*wj)
+        for(x=y-wj; x < y; x++)
+        {
+            temp = f[x+wj];
+            f[x+wj] = ((f[x+wj])&(mask[i])) + (((f[x]) & (mask[i])) >> forShift);
+            f[x] = ((f[x])&(~mask[i])) + ((temp&(~mask[i])) << forShift);
+        }
+}
+
+void swap_ij_case3( word* f,int totalVars, int i, int j)
+{
+    int x,y,wwi,wwj,shift;
+    int WORDS_IN_TT;
+    int SizeOfBlock;
+    word* temp;
+    wwi = 1 << (i - 5);
+    wwj = 1 << (j - 5);
+    shift = (wwj - wwi)/2;
+    WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
+    SizeOfBlock = sizeof(word)*wwi/2;
+    temp = malloc(SizeOfBlock);
+    for(y=wwj/2; y<WORDS_IN_TT; y+=wwj)
+        for(x=y-shift; x<y; x+=wwi)
+        {
+            memcpy(temp,&f[x],SizeOfBlock);
+            memcpy(&f[x],&f[x+shift],SizeOfBlock);
+            memcpy(&f[x+shift],temp,SizeOfBlock);
+        }
+}
+void swap_ij( word* f,int totalVars, int varI, int varJ)
+{
+    if (varI == varJ)
+        return;
+    else if(varI>varJ)
+        swap_ij( f,totalVars,varJ,varI);
+    else if((varI <= 4) && (varJ <= 5))
+        swap_ij_case1(f,totalVars, varI, varJ);
+    else if((varI <= 5) && (varJ > 5))
+        swap_ij_case2(f,totalVars, varI, varJ);
+    else if((varI > 5) && (varJ > 5))
+        swap_ij_case3(f,totalVars,varI,varJ);
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/module.make b/src/bool/lucky/module.make
index 70fa67f3..dad5ee61 100644
--- a/src/bool/lucky/module.make
+++ b/src/bool/lucky/module.make
@@ -1,3 +1,6 @@
 SRC +=  src/bool/lucky/lucky.c \
+    src/bool/lucky/luckyFast16.c \
+    src/bool/lucky/luckyFast6.c \
     src/bool/lucky/luckyRead.c \
+    src/bool/lucky/luckySwapIJ.c \
     src/bool/lucky/luckySwap.c