New semi-canonical form computation package.

5 files changed, 1247 insertions, 0 deletions

diff --git a/src/bool/lucky/lucky.c b/src/bool/lucky/lucky.c
new file mode 100644
index 00000000..06894233
--- /dev/null
+++ b/src/bool/lucky/lucky.c
@@ -0,0 +1,487 @@
+/**CFile****************************************************************
+
+  FileName    [lucky.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Truth table minimization procedures.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+inline int memCompare(word* x, word*  y, int nVars)
+{
+    int i;
+    for(i=Kit_TruthWordNum_64bit( nVars )-1;i>=0;i--)
+    {
+        if(x[i]==y[i])
+            continue;
+        else if(x[i]>y[i])
+            return 1;
+        else
+            return -1;
+    }
+    return 0;
+}
+///////sort Word* a///////////////////////////////////////////////////////////////////////////////////////////////////////
+ int compareWords1 (const void * a, const void * b)
+ {
+     if( *(word*)a > *(word*)b )
+         return 1;
+     else
+         return( *(word*)a < *(word*)b ) ? -1: 0;
+     
+ }
+ 
+ void sortAndUnique1(word* a, Abc_TtStore_t* p)
+ {
+     int i, count=1, WordsN = p->nFuncs;
+     word tempWord;
+     qsort(a,WordsN,sizeof(word),compareWords1);
+     tempWord = a[0];
+     for(i=1;i<WordsN;i++)    
+         if(tempWord != a[i])
+         {
+             a[count] = a[i];
+             tempWord = a[i];
+             count++;
+         }
+         p->nFuncs = count;
+}
+//////////sort Word** a//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+int compareWords2 (const void ** x, const void ** y)
+{
+    
+    if(**(word**)x > **(word**)y)
+        return 1;
+    else if(**(word**)x < **(word**)y)
+        return -1;
+    else
+        return 0;    
+    
+}
+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;        
+}
+int compareWords3 (const void ** x, const void ** y)
+{
+    return memCompare(*(word**)x, *(word**)y, 16);     
+} 
+void sortAndUnique(word** a, Abc_TtStore_t* p)
+{
+     int i, count=1, WordsPtrN = p->nFuncs;
+     word* tempWordPtr;
+     qsort(a,WordsPtrN,sizeof(word*),compareWords3);
+     tempWordPtr = a[0];
+     for(i=1;i<WordsPtrN;i++)    
+         if(memcmp(a[i],tempWordPtr,sizeof(word)*(p->nWords)) != 0)
+         {
+             a[count] = a[i];
+             tempWordPtr = a[i];
+             count++;
+         }
+         p->nFuncs = count;
+}
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+typedef struct
+{
+     int totalCycles;
+     int maxNCycles;
+     int minNCycles;
+     
+}cycleCtr;
+cycleCtr* setCycleCtrPtr()
+{
+     cycleCtr* x = (cycleCtr*) malloc(sizeof(cycleCtr));
+     x->totalCycles=0;
+     x->maxNCycles=0;
+     x->minNCycles=111111111;
+     return x;
+}
+void freeCycleCtr(cycleCtr* x)
+{
+    free(x);
+}
+word** makeArray(Abc_TtStore_t* p)
+{
+    int i;
+    word** a;
+    a = (word**)malloc(sizeof(word*)*(p->nFuncs));
+    for(i=0;i<p->nFuncs;i++)
+    {
+        a[i] = (word*)malloc(sizeof(word)*(p->nWords));
+        memcpy(a[i],p->pFuncs[i],sizeof(word)*(p->nWords));
+
+    }
+    return a;
+}
+void freeArray(word** a,Abc_TtStore_t* p)
+{
+    int i;
+    for(i=0;i<p->nFuncs;i++)
+        free(a[i]);
+    free(a);
+}
+
+word* makeArrayB(word** a, int nFuncs)
+{
+    int i;
+    word* b;
+    b = (word*)malloc(sizeof(word)*(nFuncs));
+    for(i=0;i<nFuncs;i++)
+        b[i] = a[i][0];
+
+    return b;
+}
+void freeArrayB(word* b)
+{
+    free(b);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////
+
+// if highest bit in F ( all ones min term ) is one => inverse 
+// 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;
+// }
+// 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;
+// }
+// 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;
+// }
+// 
+// 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;
+// }
+//  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);
+//     
+//     if ( (nOnes*2 == nWords * 32) )
+//     { 
+//         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);
+//     }
+// }
+// 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;
+// }
+// luckyCanonicizer 
+
+void printCCtrInfo(cycleCtr* cCtr, int nFuncs)
+{
+    printf("maxNCycles = %d\n",cCtr->maxNCycles);
+    printf("minNCycles = %d\n",cCtr->minNCycles);
+    printf("average NCycles = %.3f\n",cCtr->totalCycles/(double)nFuncs);
+}
+////////////////////////////////////////New Faster versoin/////////////////////////////////////////////////////////
+
+// if highest bit in F ( all ones min term ) is one => inverse 
+// returns: if pInOnt changed(minimized) by function return 1 if not 0
+inline int minimalInitialFlip1(word* pInOut, int  nVars)
+{
+    word oneWord=1;
+    if(  (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
+    {
+        Kit_TruthNot_64bit( pInOut, nVars );
+        return 1;
+    }
+    return 0;
+}
+
+// compare F with  F1 = (F with changed phase in one of the vars).
+// keeps smaller.
+// same for all vars in F.
+// returns: if pInOnt changed(minimized) by function return 1 if not 0
+inline int minimalFlip1(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);
+    Kit_TruthChangePhase_64bit( pInOut, nVars, 0 );
+    for(i=1;i<nVars;i++)
+    {
+        if( memCompare(pMinimal,pInOut,nVars) == 1)
+        {
+            memcpy(pMinimal, pInOut, blockSize);
+            Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+        }
+        else
+        {
+            memcpy(pInOut, pMinimal, blockSize);
+            Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+        }
+    }
+    if( memCompare(pMinimal,pInOut,nVars) == -1)
+        memcpy(pInOut, pMinimal, blockSize);
+    if(memcmp(pInOut,PDuplicat,blockSize) == 0)
+        return 0;
+    else
+        return 1;
+}
+// compare F with  F1 = (F with swapped two adjacent vars).
+// keeps smaller.
+// same for all vars in F.
+// returns: if pInOnt changed(minimized) by function return 1 if not 0
+inline int minimalSwap1(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);
+    Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
+    for(i=1;i<nVars-1;i++)
+    {
+        if( memCompare(pMinimal,pInOut,nVars) == 1)
+        {
+            memcpy(pMinimal, pInOut, blockSize);
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+        }
+        else
+        {
+            memcpy(pInOut, pMinimal, blockSize);
+            Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+        }
+    }
+    if( memCompare(pMinimal,pInOut,nVars) == -1)
+        memcpy(pInOut, pMinimal, blockSize);
+    if(memcmp(pInOut,PDuplicat,blockSize) == 0)
+        return 0;
+    else
+        return 1;
+}
+// tries to find minimal F till F at the beginning of the loop is the same as at the end - irreducible 
+unsigned luckyCanonicizer1_simple(word* pInOut, word* pAux, word* pAux1, int  nVars, char * pCanonPerm, unsigned CanonPhase)
+{
+    int counter=1;
+    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);    
+    }
+    return CanonPhase;
+}
+
+void luckyCanonicizer_final(word* pInOut, word* pAux, word* pAux1, int  nVars)
+{
+    Kit_TruthSemiCanonicize_Yasha_simple( pInOut, nVars, NULL );
+    luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars, NULL, 0);
+}
+
+// this procedure calls internal canoniziers
+// it returns canonical phase (as return value) and canonical permutation (in pCanonPerm)
+unsigned Kit_TruthSemiCanonicize_new_internal( word * pInOut, int nVars, char * pCanonPerm )
+{
+    word pAux[1024], pAux1[1024];
+    unsigned CanonPhase;
+    assert( nVars <= 16 );
+    CanonPhase = Kit_TruthSemiCanonicize_Yasha_simple( pInOut, nVars, pCanonPerm );
+    CanonPhase = luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars, pCanonPerm, CanonPhase);
+    return CanonPhase;
+}
+
+// this procedure is translates truth table from 'unsingeds' into 'words' 
+unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
+{
+    unsigned Result;
+    if ( nVars < 6 )
+    {
+         word Temp = ((word)pInOut[0] << 32) | (word)pInOut[0];
+         Result = Kit_TruthSemiCanonicize_new_internal( &Temp, nVars, pCanonPerm );
+         pInOut[0] = (unsigned)Temp;
+    }
+    else
+         Result = Kit_TruthSemiCanonicize_new_internal( (word *)pInOut, nVars, pCanonPerm );
+    return Result;
+}
+
+
+
+// compile main() procedure only if running outside of ABC environment
+#ifndef _RUNNING_ABC_
+
+int main () 
+{
+//     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 = "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  = "nonDSDfunc16var10K.txt";
+    char * pFileInput1 = "partDSDfunc16var10K.txt";
+    char * pFileInput2 = "fullDSDfunc16var10K.txt";
+
+    int i, j, tempNF;
+    char** charArray;
+    word** a, ** b;
+    Abc_TtStore_t* p;
+    word * pAux, * pAux1;
+    short * pStore;
+//    cycleCtr* cCtr;
+    charArray = (char**)malloc(sizeof(char*)*3);
+
+    charArray[0] = pFileInput;
+    charArray[1] = pFileInput1;
+    charArray[2] = pFileInput2;
+    for(j=0;j<3;j++)
+    {
+        p = setTtStore(charArray[j]);    
+//        p = setTtStore(pFileInput);    
+        a = makeArray(p);
+        b = makeArray(p);    
+//        cCtr = setCycleCtrPtr();
+
+         pAux = (word*)malloc(sizeof(word)*(p->nWords));
+         pAux1 = (word*)malloc(sizeof(word)*(p->nWords));    
+        pStore = (short*)malloc(sizeof(short)*(p->nVars));
+        printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
+        
+         tempNF = p->nFuncs;
+
+        TimePrint("start");        
+        for(i=0;i<p->nFuncs;i++)        
+            luckyCanonicizer_final(a[i], pAux, pAux1, p->nVars, pStore);        
+         TimePrint("done with A");
+
+        sortAndUnique(a, p);
+        printf("F left in A final = %d\n",p->nFuncs);
+        freeArray(a,p);
+         TimePrint("Done with sort");
+        
+
+// delete data-structures    
+        free(pAux);
+        free(pAux1);    
+        free(pStore);
+//        freeCycleCtr(cCtr);
+        Abc_TruthStoreFree( p );
+    }
+    return 0;
+}
+
+#endif
+
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/lucky.h b/src/bool/lucky/lucky.h
new file mode 100644
index 00000000..cfe9de2e
--- /dev/null
+++ b/src/bool/lucky/lucky.h
@@ -0,0 +1,27 @@
+/**CFile****************************************************************
+
+  FileName    [lucky.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#ifndef ABC__bool__lucky__LUCKY_H_
+#define ABC__bool__lucky__LUCKY_H_
+
+
+ABC_NAMESPACE_HEADER_START
+
+extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif /* LUCKY_H_ */
\ No newline at end of file
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
new file mode 100644
index 00000000..f79e30e7
--- /dev/null
+++ b/src/bool/lucky/luckyInt.h
@@ -0,0 +1,123 @@
+/**CFile****************************************************************
+
+  FileName    [luckyInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#ifndef ABC__bool__lucky__LUCKY_INT_H_
+#define ABC__bool__lucky__LUCKY_INT_H_
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+#include <time.h>
+
+// comment out this line to run Lucky Code outside of ABC
+#define _RUNNING_ABC_
+
+#ifdef _RUNNING_ABC_
+#include "misc/util/abc_global.h"
+#else
+#define ABC_NAMESPACE_HEADER_START
+#define ABC_NAMESPACE_HEADER_END
+#define ABC_NAMESPACE_IMPL_START
+#define ABC_NAMESPACE_IMPL_END
+#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
+typedef unsigned __int64 ABC_UINT64_T;
+//typedef ABC_UINT64_T word;
+
+typedef unsigned __int64  word;
+
+#define bool int
+#define false 0
+#define true 1
+#define inline __inline  // compatible with MS VS 6.0
+#define ABC_ALLOC(type, num)    ((type *) malloc(sizeof(type) * (num)))
+static word mask1[6] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
+static word mask0[6] = { 0x5555555555555555,0x3333333333333333, 0x0F0F0F0F0F0F0F0F,0x00FF00FF00FF00FF,0x0000FFFF0000FFFF, 0x00000000FFFFFFFF};    
+static word mask[6][2] =   {
+    {0x5555555555555555,0xAAAAAAAAAAAAAAAA},
+    {0x3333333333333333,0xCCCCCCCCCCCCCCCC},
+    {0x0F0F0F0F0F0F0F0F,0xF0F0F0F0F0F0F0F0},
+    {0x00FF00FF00FF00FF,0xFF00FF00FF00FF00},
+    {0x0000FFFF0000FFFF,0xFFFF0000FFFF0000},
+    {0x00000000FFFFFFFF,0xFFFFFFFF00000000}
+};
+
+typedef struct  
+{
+    int      nVars;
+    int      nWords;
+    int      nFuncs;
+    word **  pFuncs;
+}Abc_TtStore_t;
+
+typedef struct 
+{
+    int direction; 
+    int position;
+} varInfo;
+
+
+typedef struct 
+{
+    varInfo* posArray;
+    int* realArray;
+    int varN;
+    int positionToSwap1;
+    int positionToSwap2;
+} swapInfo;
+
+typedef struct
+{
+    int varN;
+    int* swapArray;
+    int swapCtr;
+    int totalSwaps;
+    int* flipArray;
+    int flipCtr;
+    int totalFlips;    
+}permInfo;
+
+static inline void TimePrint( char* Message )
+{
+    static int timeBegin;
+    double time = 1.0*(clock() - timeBegin)/CLOCKS_PER_SEC ;
+    if ( Message != NULL)
+        printf("%s = %f sec.\n", Message, time);
+    timeBegin = clock();
+}
+
+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);
+extern  void Abc_TruthStoreFree( Abc_TtStore_t * p );
+extern  inline void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar );
+extern  inline void Kit_TruthNot_64bit(word * pIn, int nVars );
+extern  inline void Kit_TruthCopy_64bit( word * pOut, word * pIn, int nVars );
+extern  inline void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar );
+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  );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif /* LUCKY_H_ */
\ No newline at end of file
diff --git a/src/bool/lucky/luckyRead.c b/src/bool/lucky/luckyRead.c
new file mode 100644
index 00000000..0f2ab167
--- /dev/null
+++ b/src/bool/lucky/luckyRead.c
@@ -0,0 +1,332 @@
+/**CFile****************************************************************
+
+  FileName    [luckyRead.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Reading truth tables from file.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+// read/write/flip i-th bit of a bit string table:
+static inline int     Abc_TruthGetBit( word * p, int i )         { return (int)(p[i>>6] >> (i & 63)) & 1;        }
+static inline void    Abc_TruthSetBit( word * p, int i )         { p[i>>6] |= (((word)1)<<(i & 63));             }
+static inline void    Abc_TruthXorBit( word * p, int i )         { p[i>>6] ^= (((word)1)<<(i & 63));             }
+
+// read/write k-th digit d of a hexadecimal number:
+static inline int     Abc_TruthGetHex( word * p, int k )         { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15;  }
+static inline void    Abc_TruthSetHex( word * p, int k, int d )  { p[k>>4] |= (((word)d)<<((k<<2) & 63));        }
+static inline void    Abc_TruthXorHex( word * p, int k, int d )  { p[k>>4] ^= (((word)d)<<((k<<2) & 63));        }
+
+// read one hex character
+static inline int  Abc_TruthReadHexDigit( char HexChar )
+{
+    if ( HexChar >= '0' && HexChar <= '9' )
+        return HexChar - '0';
+    if ( HexChar >= 'A' && HexChar <= 'F' )
+        return HexChar - 'A' + 10;
+    if ( HexChar >= 'a' && HexChar <= 'f' )
+        return HexChar - 'a' + 10;
+    assert( 0 ); // not a hexadecimal symbol
+    return -1; // return value which makes no sense
+}
+
+// write one hex character
+static inline void Abc_TruthWriteHexDigit( FILE * pFile, int HexDigit )
+{
+    assert( HexDigit >= 0 && HexDigit < 16 );
+    if ( HexDigit < 10 )
+        fprintf( pFile, "%d", HexDigit );
+    else
+        fprintf( pFile, "%c", 'A' + HexDigit-10 );
+}
+
+// read one truth table in hexadecimal
+static inline void Abc_TruthReadHex( word * pTruth, char * pString, int nVars )
+{
+    int nWords = (nVars < 7)? 1 : (1 << (nVars-6));
+    int k, Digit, nDigits = (nWords << 4);
+    char EndSymbol;
+    // skip the first 2 symbols if they are "0x"
+    if ( pString[0] == '0' && pString[1] == 'x' )
+        pString += 2;
+    // get the last symbol
+    EndSymbol = pString[nDigits];
+    // the end symbol of the TT (the one immediately following hex digits)
+    // should be one of the following: space, a new-line, or a zero-terminator
+    // (note that on Windows symbols '\r' can be inserted before each '\n')
+    assert( EndSymbol == ' ' || EndSymbol == '\n' || EndSymbol == '\r' || EndSymbol == '\0' );
+    // read hexadecimal digits in the reverse order
+    // (the last symbol in the string is the least significant digit)
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = Abc_TruthReadHexDigit( pString[nDigits - 1 - k] );
+        assert( Digit >= 0 && Digit < 16 );
+        Abc_TruthSetHex( pTruth, k, Digit );
+    }
+}
+
+// write one truth table in hexadecimal (do not add end-of-line!)
+static inline void Abc_TruthWriteHex( FILE * pFile, word * pTruth, int nVars )
+{
+    int nDigits, Digit, k;
+    // write hexadecimal digits in the reverse order
+    // (the last symbol in the string is the least significant digit)
+    nDigits = (1 << (nVars-2));
+    for ( k = 0; k < nDigits; k++ )
+    {
+        Digit = Abc_TruthGetHex( pTruth, nDigits - 1 - k );
+        assert( Digit >= 0 && Digit < 16 );
+        Abc_TruthWriteHexDigit( pFile, Digit );
+    }
+}
+
+// allocate and clear memory to store 'nTruths' truth tables of 'nVars' variables
+static inline Abc_TtStore_t * Abc_TruthStoreAlloc( int nVars, int nFuncs )
+{
+    Abc_TtStore_t * p;
+    int i;
+    p = (Abc_TtStore_t *)malloc( sizeof(Abc_TtStore_t) );
+    p->nVars  =  nVars;
+    p->nWords = (nVars < 7) ? 1 : (1 << (nVars-6));
+    p->nFuncs =  nFuncs;
+    // alloc array of 'nFuncs' pointers to truth tables
+    p->pFuncs = (word **)malloc( sizeof(word *) * p->nFuncs );
+    // alloc storage for 'nFuncs' truth tables as one chunk of memory
+    p->pFuncs[0] = (word *)calloc( sizeof(word), p->nFuncs * p->nWords );
+    // split it up into individual truth tables
+    for ( i = 1; i < p->nFuncs; i++ )
+        p->pFuncs[i] = p->pFuncs[i-1] + p->nWords;
+    return p;
+}
+
+// free memory previously allocated for storing truth tables
+static inline void Abc_TruthStoreFree( Abc_TtStore_t * p )
+{
+    free( p->pFuncs[0] );
+    free( p->pFuncs );
+    free( p );
+}
+
+// read file contents
+static char * Abc_FileRead( char * pFileName )
+{
+    FILE * pFile;
+    char * pBuffer;
+    int nFileSize;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return NULL;
+    }
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = (char *)malloc( nFileSize + 3 );
+    fread( pBuffer, nFileSize, 1, pFile );
+    // add several empty lines at the end
+    // (these will be used to signal the end of parsing)
+    pBuffer[ nFileSize + 0] = '\n';
+    pBuffer[ nFileSize + 1] = '\n';
+    // terminate the string with '\0'
+    pBuffer[ nFileSize + 2] = '\0';
+    fclose( pFile );
+    return pBuffer;
+}
+
+// determine the number of variables by reading the first line
+// determine the number of functions by counting the lines
+static void Abc_TruthGetParams( char * pFileName, int * pnVars, int * pnTruths )
+{
+    char * pContents;
+    int i, nVars, nLines;
+    // prepare the output 
+    if ( pnVars )
+        *pnVars = 0;
+    if ( pnTruths )
+        *pnTruths = 0;
+    // read data from file
+    pContents = Abc_FileRead( pFileName );
+    if ( pContents == NULL )
+        return;
+    // count the number of symbols before the first space or new-line
+    // (note that on Windows symbols '\r' can be inserted before each '\n')
+    for ( i = 0; pContents[i]; i++ )
+        if ( pContents[i] == ' ' || pContents[i] == '\n' || pContents[i] == '\r' )
+            break;
+    if ( pContents[i] == 0 )
+        printf( "Strange, the input file does not have spaces and new-lines...\n" );
+
+    // account for the fact that truth tables may have "0x" at the beginning of each line
+    if ( pContents[0] == '0' && pContents[1] == 'x' )
+        i = i - 2;
+
+    // determine the number of variables
+    for ( nVars = 0; nVars < 32; nVars++ )
+        if ( 4 * i == (1 << nVars) ) // the number of bits equal to the size of truth table
+            break;
+    if ( nVars < 2 || nVars > 16 )
+    {
+        printf( "Does not look like the input file contains truth tables...\n" );
+        return;
+    }
+    if ( pnVars )
+        *pnVars = nVars;
+
+    // determine the number of functions by counting the lines
+    nLines = 0;
+    for ( i = 0; pContents[i]; i++ )
+        nLines += (pContents[i] == '\n');
+    if ( pnTruths )
+        *pnTruths = nLines;
+}
+
+static Abc_TtStore_t * Abc_Create_TtSpore (char * pFileInput)
+{
+    int nVars, nTruths;
+    Abc_TtStore_t * p;
+    Abc_TruthGetParams( pFileInput, &nVars, &nTruths );
+    p = Abc_TruthStoreAlloc( nVars, nTruths );
+    return p;
+
+}
+// read truth tables from file
+static void Abc_TruthStoreRead( char * pFileName, Abc_TtStore_t* p )
+{
+    char * pContents;
+    int i, nLines;
+    pContents = Abc_FileRead( pFileName );
+    if ( pContents == NULL )
+        return;
+    // here it is assumed (without checking!) that each line of the file 
+    // begins with a string of hexadecimal chars followed by space
+
+    // the file will be read till the first empty line (pContents[i] == '\n')
+    // (note that Abc_FileRead() added several empty lines at the end of the file contents)
+    for ( nLines = i = 0; pContents[i] != '\n'; )
+    {
+        // read one line
+        Abc_TruthReadHex( p->pFuncs[nLines++], &pContents[i], p->nVars );
+        // skip till after the end-of-line symbol
+        // (note that end-of-line symbol is also skipped)
+        while ( pContents[i++] != '\n' );
+    }
+    // adjust the number of functions read 
+    // (we may have allocated more storage because some lines in the file were empty)
+    assert( p->nFuncs >= nLines );
+    p->nFuncs = nLines;
+}
+
+// write truth tables into file
+// (here we write one symbol at a time - it can be optimized by writing 
+// each truth table into a string and then writing the string into a file)
+static void Abc_TruthStoreWrite( char * pFileName, Abc_TtStore_t * p )
+{
+    FILE * pFile;
+    int i;
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars );
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+}
+
+static void WriteToFile(char * pFileName, Abc_TtStore_t * p, word* a)
+{
+    FILE * pFile;
+    int i;
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        Abc_TruthWriteHex( pFile, &a[i], p->nVars );
+        fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
+}
+
+static void WriteToFile1(char * pFileName, Abc_TtStore_t * p, word** a)
+{
+    FILE * pFile;
+    int i,j;
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        fprintf( pFile, "0" );
+        fprintf( pFile, "x" );
+        for ( j=p->nWords-1; j >= 0; j-- )
+            Abc_TruthWriteHex( pFile, &a[i][j], p->nVars );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+static void WriteToFile2(char * pFileName, Abc_TtStore_t * p, word* a)
+{
+    FILE * pFile;
+    int i,j;
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        fprintf( pFile, "0" );
+        fprintf( pFile, "x" );
+        for ( j=p->nWords-1; j >= 0; j-- )
+            Abc_TruthWriteHex( pFile, a+i, p->nVars );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+
+Abc_TtStore_t * setTtStore(char * pFileInput)
+{
+    int nVars, nTruths;
+    Abc_TtStore_t * p;
+    // figure out how many truth table and how many variables
+    Abc_TruthGetParams( pFileInput, &nVars, &nTruths );
+    // allocate data-structure
+    p = Abc_TruthStoreAlloc( nVars, nTruths );
+
+    Abc_TruthStoreRead( pFileInput, p );
+    return p;
+}
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
new file mode 100644
index 00000000..cd3adaa6
--- /dev/null
+++ b/src/bool/lucky/luckySwap.c
@@ -0,0 +1,278 @@
+/**CFile****************************************************************
+
+  FileName    [luckySwap.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Semi-canonical form computation package.]
+
+  Synopsis    [Swapping variables in the truth table.]
+
+  Author      [Jake]
+
+  Date        [Started - August 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+inline int Kit_TruthWordNum_64bit( int nVars )  { return nVars <= 6 ? 1 : (1 << (nVars - 6));}
+
+inline int Kit_WordCountOnes_64bit(word x)
+{
+    x = x - ((x >> 1) & 0x5555555555555555);   
+    x = (x & 0x3333333333333333) + ((x >> 2) & 0x3333333333333333);    
+    x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0F;    
+    x = x + (x >> 8);
+    x = x + (x >> 16);
+    x = x + (x >> 32); 
+    return (int)(x & 0xFF);
+}
+
+inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars )
+{
+    int w, Counter = 0;
+    for ( w = Kit_TruthWordNum_64bit(nVars)-1; w >= 0; w-- )
+        Counter += Kit_WordCountOnes_64bit(pIn[w]);
+    return Counter;
+}
+
+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 );
+    if ( nVars <= 6 )
+    {
+        if ( nVars > 0 )        
+            pStore[0] = Kit_WordCountOnes_64bit( pTruth[0] & 0x5555555555555555 );  
+        if ( nVars > 1 )       
+            pStore[1] = Kit_WordCountOnes_64bit( pTruth[0] & 0x3333333333333333 );     
+        if ( nVars > 2 )       
+            pStore[2] = Kit_WordCountOnes_64bit( pTruth[0] & 0x0F0F0F0F0F0F0F0F );   
+        if ( nVars > 3 )       
+            pStore[3] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00FF00FF00FF00FF );     
+        if ( nVars > 4 )       
+            pStore[4] = Kit_WordCountOnes_64bit( pTruth[0] & 0x0000FFFF0000FFFF ); 
+        if ( nVars > 5 )       
+            pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00000000FFFFFFFF );         
+        return;
+    }
+    // nVars > 6
+    // count 1's for all other variables
+    for ( k = 0; k < nWords; k++ )
+    {
+        Counter = Kit_WordCountOnes_64bit( pTruth[k] );
+        for ( i = 6; i < nVars; i++ )
+            if ( (k & (1 << (i-6))) == 0)
+                pStore[i] += Counter;
+    }
+    // count 1's for the first six variables
+    for ( k = nWords/2; k>0; k-- )
+    {
+        pStore[0] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x5555555555555555) | ((pTruth[1] & 0x5555555555555555) <<  1) );
+        pStore[1] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x3333333333333333) | ((pTruth[1] & 0x3333333333333333) <<  2) );
+        pStore[2] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x0F0F0F0F0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F0F0F0F0F) <<  4) );
+        pStore[3] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x00FF00FF00FF00FF) | ((pTruth[1] & 0x00FF00FF00FF00FF) <<  8) );
+        pStore[4] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x0000FFFF0000FFFF) | ((pTruth[1] & 0x0000FFFF0000FFFF) <<  16) );
+        pStore[5] += Kit_WordCountOnes_64bit( (pTruth[0] & 0x00000000FFFFFFFF) | ((pTruth[1] & 0x00000000FFFFFFFF) <<  32) );  
+        pTruth += 2;
+    }
+}
+
+inline void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar )
+{
+    int nWords = Kit_TruthWordNum_64bit( nVars );
+    int i, Step,SizeOfBlock;
+    word Temp[512];
+    
+    assert( iVar < nVars );
+    if(iVar<=5)
+    {
+        for ( i = 0; i < nWords; i++ )
+            pInOut[i] = ((pInOut[i] & mask0[iVar]) << (1<<(iVar))) | ((pInOut[i] & ~mask0[iVar]) >> (1<<(iVar)));
+    }
+    else
+    {
+        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;            
+            pInOut += 2*Step;
+        }
+    }
+    
+}
+
+inline void Kit_TruthNot_64bit(word * pIn, int nVars )
+{
+    int w;
+    for ( w = Kit_TruthWordNum_64bit(nVars)-1; w >= 0; w-- )
+        pIn[w] = ~pIn[w];
+}
+inline void Kit_TruthCopy_64bit( word * pOut, word * pIn, int nVars )
+{ 
+    memcpy(pOut,pIn,Kit_TruthWordNum_64bit(nVars)*sizeof(word));
+}
+
+inline void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar )
+{
+    int i, Step, Shift, SizeOfBlock;                   //
+    word temp[256];                   // to make only pInOut possible
+    static word PMasks[5][3] = {
+        { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+        { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+        { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+        { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+        { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+    };
+    int nWords = Kit_TruthWordNum_64bit( nVars ); 
+    
+    assert( iVar < nVars - 1 );
+    if ( iVar < 5 )
+    {
+        Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            pInOut[i] = (pInOut[i] & PMasks[iVar][0]) | ((pInOut[i] & PMasks[iVar][1]) << Shift) | ((pInOut[i] & PMasks[iVar][2]) >> Shift);
+    }
+    else if ( iVar > 5 )
+    {
+        Step = 1 << (iVar - 6);
+        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);
+            pInOut += 4*Step;
+        }
+    }
+    else // if ( iVar == 5 )
+    {
+        for ( i = 0; i < nWords; i += 2 )
+        {
+            temp[0] = pInOut[i+1] << 32;
+            pInOut[i+1] ^= (temp[0] ^ pInOut[i]) >> 32;
+            pInOut[i] = (pInOut[i] & 0x00000000FFFFFFFF) | temp[0];
+            
+        }
+    }
+}
+
+inline unsigned  Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm )
+{
+    int pStore[16];
+    int nWords = Kit_TruthWordNum_64bit( nVars );
+    int i, Temp, fChange, nOnes;
+    unsigned  uCanonPhase=0;
+    assert( nVars <= 16 );
+    
+    nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+    
+    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])
+            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 )
+{
+    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;
+}
+
+
+ABC_NAMESPACE_IMPL_END