summaryrefslogtreecommitdiffstats
path: root/src/bool/lucky
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool/lucky')
-rw-r--r--src/bool/lucky/lucky.c487
-rw-r--r--src/bool/lucky/lucky.h27
-rw-r--r--src/bool/lucky/luckyInt.h123
-rw-r--r--src/bool/lucky/luckyRead.c332
-rw-r--r--src/bool/lucky/luckySwap.c278
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