diff options
Diffstat (limited to 'src/bool/lucky')
-rw-r--r-- | src/bool/lucky/lucky.c | 487 | ||||
-rw-r--r-- | src/bool/lucky/lucky.h | 27 | ||||
-rw-r--r-- | src/bool/lucky/luckyInt.h | 123 | ||||
-rw-r--r-- | src/bool/lucky/luckyRead.c | 332 | ||||
-rw-r--r-- | src/bool/lucky/luckySwap.c | 278 |
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 |