summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abcRec2.c4
-rw-r--r--src/bool/lucky/lucky.c250
-rw-r--r--src/bool/lucky/luckyFast16.c54
-rw-r--r--src/bool/lucky/luckyFast6.c12
-rw-r--r--src/bool/lucky/luckyInt.h2
-rw-r--r--src/bool/lucky/luckySwap.c50
-rw-r--r--src/bool/lucky/luckySwapIJ.c4
7 files changed, 188 insertions, 188 deletions
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index 4edda73a..1af48247 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -1619,8 +1619,8 @@ s_pMan->timeBuild += clock() - timeBuild;
timeInsert = clock();
Abc_NtkRecInsertToLookUpTable2(s_pMan, ppSpot, pPO, nLeaves, pTruth, s_pMan->fTrim);
s_pMan->timeInsert += clock() - timeInsert;
-// if (pIfMan->pPars->fDelayOpt)
-// Abc_NtkRecAddSOPB(pIfMan, pCut, pTruth, pCanonPerm, uCanonPhase );
+// if (pIfMan->pPars->fDelayOpt)
+// Abc_NtkRecAddSOPB(pIfMan, pCut, pTruth, pCanonPerm, uCanonPhase );
return 1;
}
diff --git a/src/bool/lucky/lucky.c b/src/bool/lucky/lucky.c
index 159c54bc..bc51b751 100644
--- a/src/bool/lucky/lucky.c
+++ b/src/bool/lucky/lucky.c
@@ -49,7 +49,7 @@ inline int memCompare(word* x, word* y, int nVars)
word tempWord;
qsort(a,WordsN,sizeof(word),compareWords1);
tempWord = a[0];
- for(i=1;i<WordsN;i++)
+ for(i=1;i<WordsN;i++)
if(tempWord != a[i])
{
a[count] = a[i];
@@ -67,7 +67,7 @@ int compareWords2 (const void ** x, const void ** y)
else if(**(word**)x < **(word**)y)
return -1;
else
- return 0;
+ return 0;
}
int compareWords (const void ** a, const void ** b)
@@ -75,11 +75,11 @@ int compareWords (const void ** a, const void ** b)
if( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) > 0 )
return 1;
else
- return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;
+ return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;
}
int compareWords3 (const void ** x, const void ** y)
{
- return memCompare(*(word**)x, *(word**)y, 16);
+ return memCompare(*(word**)x, *(word**)y, 16);
}
void sortAndUnique(word** a, Abc_TtStore_t* p)
{
@@ -87,7 +87,7 @@ void sortAndUnique(word** a, Abc_TtStore_t* p)
word* tempWordPtr;
qsort(a,WordsPtrN,sizeof(word*),(int(*)(const void *,const void *))compareWords3);
tempWordPtr = a[0];
- for(i=1;i<WordsPtrN;i++)
+ for(i=1;i<WordsPtrN;i++)
if(memcmp(a[i],tempWordPtr,sizeof(word)*(p->nWords)) != 0)
{
a[count] = a[i];
@@ -159,117 +159,117 @@ void freeArrayB(word* b)
// if pInOnt changed(minimized) by function return 1 if not 0
// inline int minimalInitialFlip_propper(word* pInOut, word* pDuplicat, int nVars)
// {
-// word oneWord=1;
-// Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
-// Kit_TruthNot_64bit( pDuplicat, nVars );
-// if( memCompare(pDuplicat,pInOut,nVars) == -1)
-// {
-// Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
-// return 1;
-// }
-// return 0;
+// word oneWord=1;
+// Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
+// Kit_TruthNot_64bit( pDuplicat, nVars );
+// if( memCompare(pDuplicat,pInOut,nVars) == -1)
+// {
+// Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
+// return 1;
+// }
+// return 0;
// }
// inline int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
// {
-// int i;
-// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
-// memcpy(pMinimal, pInOut, blockSize);
-// memcpy(PDuplicat, pInOut, blockSize);
-// for(i=0;i<nVars;i++)
-// {
-// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
-// if( memCompare(pMinimal,pInOut,nVars) == 1)
-// memcpy(pMinimal, pInOut, blockSize);
-// memcpy(pInOut,PDuplicat,blockSize);
-// }
-// memcpy(pInOut,pMinimal,blockSize);
-// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
-// return 0;
-// else
-// return 1;
+// int i;
+// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
+// memcpy(pMinimal, pInOut, blockSize);
+// memcpy(PDuplicat, pInOut, blockSize);
+// for(i=0;i<nVars;i++)
+// {
+// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+// if( memCompare(pMinimal,pInOut,nVars) == 1)
+// memcpy(pMinimal, pInOut, blockSize);
+// memcpy(pInOut,PDuplicat,blockSize);
+// }
+// memcpy(pInOut,pMinimal,blockSize);
+// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
+// return 0;
+// else
+// return 1;
// }
// inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
// {
-// int i;
-// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
-// memcpy(pMinimal, pInOut, blockSize);
-// memcpy(PDuplicat, pInOut, blockSize);
-// for(i=0;i<nVars-1;i++)
-// {
-// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
-// if(memCompare(pMinimal,pInOut,nVars) == 1)
-// memcpy(pMinimal, pInOut, blockSize);
-// memcpy(pInOut,PDuplicat,blockSize);
-// }
-// memcpy(pInOut,pMinimal,blockSize);
-// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
-// return 0;
-// else
-// return 1;
+// int i;
+// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
+// memcpy(pMinimal, pInOut, blockSize);
+// memcpy(PDuplicat, pInOut, blockSize);
+// for(i=0;i<nVars-1;i++)
+// {
+// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+// if(memCompare(pMinimal,pInOut,nVars) == 1)
+// memcpy(pMinimal, pInOut, blockSize);
+// memcpy(pInOut,PDuplicat,blockSize);
+// }
+// memcpy(pInOut,pMinimal,blockSize);
+// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
+// return 0;
+// else
+// return 1;
// }
//
// void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int nVars, cycleCtr* cCtr)
// {
-// int counter=1, cycles=0;
-// assert( nVars <= 16 );
-// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
-// {
-// counter=0;
-// counter += minimalInitialFlip(pInOut, nVars);
-// counter += minimalFlip(pInOut, pAux, pAux1, nVars);
-// counter += minimalSwap(pInOut, pAux, pAux1, nVars);
-// cCtr->totalCycles++;
-// cycles++;
-// }
-// if(cycles < cCtr->minNCycles)
-// cCtr->minNCycles = cycles;
-// else if(cycles > cCtr->maxNCycles)
-// cCtr->maxNCycles = cycles;
+// int counter=1, cycles=0;
+// assert( nVars <= 16 );
+// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
+// {
+// counter=0;
+// counter += minimalInitialFlip(pInOut, nVars);
+// counter += minimalFlip(pInOut, pAux, pAux1, nVars);
+// counter += minimalSwap(pInOut, pAux, pAux1, nVars);
+// cCtr->totalCycles++;
+// cycles++;
+// }
+// if(cycles < cCtr->minNCycles)
+// cCtr->minNCycles = cycles;
+// else if(cycles > cCtr->maxNCycles)
+// cCtr->maxNCycles = cycles;
// }
// runs paralel F and ~F in luckyCanonicizer
// void luckyCanonicizer2(word* pInOut, word* pAux, word* pAux1, word* temp, int nVars)
// {
-// int nWords = Kit_TruthWordNum_64bit( nVars );
-// int counter=1, nOnes;
-// assert( nVars <= 16 );
-// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-//
+// int nWords = Kit_TruthWordNum_64bit( nVars );
+// int counter=1, nOnes;
+// assert( nVars <= 16 );
+// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+//
// if ( (nOnes*2 == nWords * 32) )
// {
-// Kit_TruthCopy_64bit( temp, pInOut, nVars );
-// Kit_TruthNot_64bit( temp, nVars );
+// Kit_TruthCopy_64bit( temp, pInOut, nVars );
+// Kit_TruthNot_64bit( temp, nVars );
// luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars);
-// luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
-// if( memCompare(temp,pInOut,nVars) == -1)
-// Kit_TruthCopy_64bit(pInOut, temp, nVars );
-// return;
-// }
-// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
-// {
-// counter=0;
-// counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
-// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
-// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+// luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
+// if( memCompare(temp,pInOut,nVars) == -1)
+// Kit_TruthCopy_64bit(pInOut, temp, nVars );
+// return;
// }
+// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
+// {
+// counter=0;
+// counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
+// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
+// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+// }
// }
// same as luckyCanonicizer + cycleCtr stutistics
// void luckyCanonicizer1(word* pInOut, word* pAux, word* pAux1, int nVars, cycleCtr* cCtr)
// {
-// int counter=1, cycles=0;
-// assert( nVars <= 16 );
-// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
-// {
-// counter=0;
-// counter += minimalInitialFlip1(pInOut, nVars);
-// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
-// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
-// cCtr->totalCycles++;
-// cycles++;
-// }
-// if(cycles < cCtr->minNCycles)
-// cCtr->minNCycles = cycles;
-// else if(cycles > cCtr->maxNCycles)
-// cCtr->maxNCycles = cycles;
+// int counter=1, cycles=0;
+// assert( nVars <= 16 );
+// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
+// {
+// counter=0;
+// counter += minimalInitialFlip1(pInOut, nVars);
+// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
+// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
+// cCtr->totalCycles++;
+// cycles++;
+// }
+// if(cycles < cCtr->minNCycles)
+// cCtr->minNCycles = cycles;
+// else if(cycles > cCtr->maxNCycles)
+// cCtr->maxNCycles = cycles;
// }
// luckyCanonicizer
@@ -404,7 +404,7 @@ inline int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int nVars
memcpy(pInOut, pMinimal, blockSize);
*p_uCanonPhase = minTemp;
}
- if(memcmp(pInOut,PDuplicat,blockSize) == 0)
+ if(memcmp(pInOut,PDuplicat,blockSize) == 0)
return 0;
else
return 1;
@@ -437,7 +437,7 @@ inline void swapInfoAdjacentVars(int iVar, char * pCanonPerm, unsigned* p_uCanon
// this version is buggy and is fixed below
inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
{
- int i;
+ int i;
int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
int blockSizeChar = nVars *sizeof(char);
memcpy(pMinimal, pInOut, blockSizeWord);
@@ -455,7 +455,7 @@ inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars
else
{
memcpy(pInOut, pMinimal, blockSizeWord);
- memcpy(pCanonPerm, tempArray, blockSizeChar);
+ memcpy(pCanonPerm, tempArray, blockSizeChar);
}
Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
@@ -474,7 +474,7 @@ inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars
inline int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
{
- int i;
+ int i;
int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
int blockSizeChar = nVars *sizeof(char);
unsigned TempuCanonPhase = *p_uCanonPhase;
@@ -570,7 +570,7 @@ inline void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int nVars,
counter=0;
counter += minimalInitialFlip(pInOut, nVars, p_uCanonPhase);
counter += minimalFlip(pInOut, pAux, pAux1, nVars, p_uCanonPhase);
- counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);
+ counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);
}
}
// tries to find minimal F till F at the beginning of the loop is the same as at the end - irreducible
@@ -629,22 +629,22 @@ unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nV
int main ()
{
-// char * pFileInput = "nonDSDfunc06var1M.txt";
-// char * pFileInput1 = "partDSDfunc06var1M.txt";
-// char * pFileInput2 = "fullDSDfunc06var1M.txt";
+// char * pFileInput = "nonDSDfunc06var1M.txt";
+// char * pFileInput1 = "partDSDfunc06var1M.txt";
+// char * pFileInput2 = "fullDSDfunc06var1M.txt";
-// char * pFileInput = "nonDSDfunc10var100K.txt";
-// char * pFileInput1 = "partDSDfunc10var100K.txt";
-// char * pFileInput2 = "fullDSDfunc10var100K.txt";
+// char * pFileInput = "nonDSDfunc10var100K.txt";
+// char * pFileInput1 = "partDSDfunc10var100K.txt";
+// char * pFileInput2 = "fullDSDfunc10var100K.txt";
-// char * pFileInput = "partDSDfunc12var100K.txt";
-// char * pFileInput = "nonDSDfunc12var100K.txt";
-// char * pFileInput1 = "partDSDfunc12var100K.txt";
-// char * pFileInput2 = "fullDSDfunc12var100K.txt";
+// char * pFileInput = "partDSDfunc12var100K.txt";
+// char * pFileInput = "nonDSDfunc12var100K.txt";
+// char * pFileInput1 = "partDSDfunc12var100K.txt";
+// char * pFileInput2 = "fullDSDfunc12var100K.txt";
-// char * pFileInput = "nonDSDfunc14var10K.txt";
-// char * pFileInput1 = "partDSDfunc14var10K.txt";
-// char * pFileInput2 = "fullDSDfunc14var10K.txt";
+// char * pFileInput = "nonDSDfunc14var10K.txt";
+// char * pFileInput1 = "partDSDfunc14var10K.txt";
+// char * pFileInput2 = "fullDSDfunc14var10K.txt";
char * pFileInput = "nonDSDfunc16var10K.txt";
char * pFileInput1 = "partDSDfunc16var10K.txt";
@@ -656,7 +656,7 @@ int main ()
Abc_TtStore_t* p;
word * pAux, * pAux1;
int * pStore;
-// cycleCtr* cCtr;
+// cycleCtr* cCtr;
charArray = (char**)malloc(sizeof(char*)*3);
charArray[0] = pFileInput;
@@ -664,35 +664,35 @@ int main ()
charArray[2] = pFileInput2;
for(j=0;j<3;j++)
{
- p = setTtStore(charArray[j]);
-// p = setTtStore(pFileInput);
+ p = setTtStore(charArray[j]);
+// p = setTtStore(pFileInput);
a = makeArray(p);
- b = makeArray(p);
-// cCtr = setCycleCtrPtr();
+ b = makeArray(p);
+// cCtr = setCycleCtrPtr();
- pAux = (word*)malloc(sizeof(word)*(p->nWords));
- pAux1 = (word*)malloc(sizeof(word)*(p->nWords));
+ pAux = (word*)malloc(sizeof(word)*(p->nWords));
+ pAux1 = (word*)malloc(sizeof(word)*(p->nWords));
pStore = (int*)malloc(sizeof(int)*(p->nVars));
printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
- tempNF = p->nFuncs;
+ tempNF = p->nFuncs;
- TimePrint("start");
+ TimePrint("start");
for(i=0;i<p->nFuncs;i++)
luckyCanonicizer_final(a[i], pAux, pAux1, p->nVars, pStore);
- TimePrint("done with A");
+ TimePrint("done with A");
sortAndUnique(a, p);
printf("F left in A final = %d\n",p->nFuncs);
freeArray(a,p);
- TimePrint("Done with sort");
+ TimePrint("Done with sort");
-// delete data-structures
+// delete data-structures
free(pAux);
free(pAux1);
free(pStore);
-// freeCycleCtr(cCtr);
+// freeCycleCtr(cCtr);
Abc_TruthStoreFree( p );
}
return 0;
diff --git a/src/bool/lucky/luckyFast16.c b/src/bool/lucky/luckyFast16.c
index d7987df5..df646599 100644
--- a/src/bool/lucky/luckyFast16.c
+++ b/src/bool/lucky/luckyFast16.c
@@ -24,7 +24,7 @@ static word SFmask[5][4] = {
{0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
{0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
{0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
- {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
+ {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
};
@@ -44,7 +44,7 @@ inline void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ,
int i;
int blockSize = 1<<iVar;
for(i=start;i>=0;i--)
- {
+ {
pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) |
(((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) |
(((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) |
@@ -174,15 +174,15 @@ inline int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ,
inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
{
int min1, min2, DifStart0, DifStart1, DifStartMin;
- int M[2];
+ int M[2];
int blockSize = 1<<iVar;
- int shiftSize = blockSize*4;
+// int shiftSize = blockSize*4;
M[0] = minTemp0_fast(pInOut, iVar, nWords, &DifStart0); // 0, 3
M[1] = minTemp1_fast(pInOut, iVar, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
- {
+ {
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
@@ -213,12 +213,12 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
int i,blockSize,shiftSize;
unsigned* tempPtr = temp+start;
if(iQ == 0 && jQ == 1)
- return;
+ return;
blockSize = sizeof(unsigned);
shiftSize = 4;
for(i=start-1;i>0;i-=shiftSize)
- {
- tempPtr -= 1;
+ {
+ tempPtr -= 1;
memcpy(tempPtr, pInOut+i-iQ, blockSize);
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-jQ, blockSize);
@@ -227,7 +227,7 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
tempPtr -= 1;
memcpy(tempPtr, pInOut+i-lQ, blockSize);
- }
+ }
memcpy(pInOut, temp, start*sizeof(unsigned));
updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
}
@@ -237,7 +237,7 @@ inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int
inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
{
int i, temp;
- for(i=(nWords)*2 - 1; i>=0; i-=4)
+ for(i=(nWords)*2 - 1; i>=0; i-=4)
{
temp = CompareWords(pInOut[i],pInOut[i-3]);
if(temp == 0)
@@ -262,7 +262,7 @@ inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
{
int i, temp;
- for(i=(nWords)*2 - 2; i>=0; i-=4)
+ for(i=(nWords)*2 - 2; i>=0; i-=4)
{
temp = CompareWords(pInOut[i],pInOut[i-1]);
if(temp == 0)
@@ -287,7 +287,7 @@ inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart)
{
int i, temp;
- for(i=(nWords)*2 - 1; i>=0; i-=4)
+ for(i=(nWords)*2 - 1; i>=0; i-=4)
{
temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
if(temp == 0)
@@ -311,7 +311,7 @@ inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int
inline int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart)
{
int i, temp;
- for(i=start-1; i>=finish; i-=4)
+ for(i=start-1; i>=finish; i-=4)
{
temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
if(temp == 0)
@@ -342,7 +342,7 @@ inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords,
M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
- {
+ {
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
@@ -379,17 +379,17 @@ inline void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int sta
blockSize = wordBlock*sizeof(word);
shiftSize = wordBlock*4;
for(i=start-wordBlock;i>0;i-=shiftSize)
- {
- tempPtr -= wordBlock;
+ {
+ tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize);
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize);
tempPtr -= wordBlock;
memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize);
tempPtr -= wordBlock;
- memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);
+ memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);
- }
+ }
memcpy(pInOut, temp, start*sizeof(word));
updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
}
@@ -513,13 +513,13 @@ inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, i
int M[2];
word temp[1024];
int blockSize = 1<<(iVar-6);
- int shiftSize = blockSize*4;
+// int shiftSize = blockSize*4;
M[0] = minTemp0_fast_moreThen5(pInOut, iVar, nWords, &DifStart0); // 0, 3
M[1] = minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1); // 1, 2
min1 = minTemp2_fast_moreThen5(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
if(DifStart0 != DifStart1)
- {
+ {
if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
else if( DifStart0 > DifStart1)
@@ -549,7 +549,7 @@ inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* p
if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
{
Kit_TruthNot_64bit( pInOut, nVars );
- (* pCanonPhase) ^=(1<<nVars);
+ (* pCanonPhase) ^=(1<<nVars);
}
}
@@ -559,7 +559,7 @@ inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* p
inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
{
int i;
- word pDuplicate[1024];
+ word pDuplicate[1024];
int bitInfoTemp = pStore[0];
memcpy(pDuplicate,pInOut,nWords*sizeof(word));
for(i=0;i<5;i++)
@@ -602,21 +602,21 @@ inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWord
inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
{
-// word pDuplicateLocal[1024]={0};
-// memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
+// word pDuplicateLocal[1024]={0};
+// memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
assert( nVars <= 16 );
assert( nVars > 6 );
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
luckyCanonicizerS_F_first_16Vars(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
-// memcpy(pDuplicate,pInOut,nWords*sizeof(word));
-// assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
+// memcpy(pDuplicate,pInOut,nWords*sizeof(word));
+// assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
}
// top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
{
int pStore[16];
- int uCanonPhase = 0;
+ unsigned uCanonPhase = 0;
int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
if ( nVars <= 6 )
pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
diff --git a/src/bool/lucky/luckyFast6.c b/src/bool/lucky/luckyFast6.c
index 9ba6691c..a32a88a4 100644
--- a/src/bool/lucky/luckyFast6.c
+++ b/src/bool/lucky/luckyFast6.c
@@ -89,7 +89,7 @@ inline word Abc_allFlip(word x, unsigned* pCanonPhase)
}
inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
-{
+{
if(info<4)
return (uCanonPhase ^= (info << iVar));
else
@@ -104,7 +104,7 @@ inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int
uCanonPhase ^= (1 << iVar);
uCanonPhase ^= (1 << (iVar+1));
}
- return uCanonPhase;
+ return uCanonPhase;
}
@@ -207,8 +207,8 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
tMin0 = tMin;
for ( i = 0; i < 5; i++ )
{
- if(bitInfoTemp == pStore[i+1])
- tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
+ if(bitInfoTemp == pStore[i+1])
+ tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
else
bitInfoTemp = pStore[i+1];
}
@@ -220,9 +220,9 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
{
-// word temp, duplicat = InOut;
+// word temp, duplicat = InOut;
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
-// InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
+// InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
// temp = InOut;
// assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
// return(InOut);
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 0e5de5c3..2e476f86 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -78,7 +78,7 @@ typedef struct
int totalSwaps;
int* flipArray;
int flipCtr;
- int totalFlips;
+ int totalFlips;
}permInfo;
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
index 2a710160..13bb489e 100644
--- a/src/bool/lucky/luckySwap.c
+++ b/src/bool/lucky/luckySwap.c
@@ -20,7 +20,7 @@
ABC_NAMESPACE_IMPL_START
-static word mask0[6] = { 0x5555555555555555,0x3333333333333333, 0x0F0F0F0F0F0F0F0F,0x00FF00FF00FF00FF,0x0000FFFF0000FFFF, 0x00000000FFFFFFFF};
+static word mask0[6] = { 0x5555555555555555,0x3333333333333333, 0x0F0F0F0F0F0F0F0F,0x00FF00FF00FF00FF,0x0000FFFF0000FFFF, 0x00000000FFFFFFFF};
/*
static word mask1[6] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
static word mask[6][2] = {
@@ -55,7 +55,7 @@ inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars )
}
inline void Kit_TruthCountOnesInCofs_64bit( word * pTruth, int nVars, int * pStore )
-{
+{
int nWords = Kit_TruthWordNum_64bit( nVars );
int i, k, Counter;
memset( pStore, 0, sizeof(int) * nVars );
@@ -72,7 +72,7 @@ inline void Kit_TruthCountOnesInCofs_64bit( word * pTruth, int nVars, int * pSto
if ( nVars > 4 )
pStore[4] = Kit_WordCountOnes_64bit( pTruth[0] & 0x0000FFFF0000FFFF );
if ( nVars > 5 )
- pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00000000FFFFFFFF );
+ pStore[5] = Kit_WordCountOnes_64bit( pTruth[0] & 0x00000000FFFFFFFF );
return;
}
// nVars > 6
@@ -114,13 +114,13 @@ inline void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar )
Step = (1 << (iVar - 6));
SizeOfBlock = sizeof(word)*Step;
for ( i = 0; i < nWords; i += 2*Step )
- {
+ {
memcpy(Temp,pInOut,SizeOfBlock);
memcpy(pInOut,pInOut+Step,SizeOfBlock);
memcpy(pInOut+Step,Temp,SizeOfBlock);
- // Temp = pInOut[i];
- // pInOut[i] = pInOut[Step+i];
- // pInOut[Step+i] = Temp;
+ // Temp = pInOut[i];
+ // pInOut[i] = pInOut[Step+i];
+ // pInOut[Step+i] = Temp;
pInOut += 2*Step;
}
}
@@ -164,7 +164,7 @@ inline void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar
SizeOfBlock = sizeof(word)*Step;
pInOut += 2*Step;
for(i=2*Step; i<nWords; i+=4*Step)
- {
+ {
memcpy(temp,pInOut-Step,SizeOfBlock);
memcpy(pInOut-Step,pInOut,SizeOfBlock);
memcpy(pInOut,temp,SizeOfBlock);
@@ -236,7 +236,7 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
uCanonPhase ^= (1 << (i+1));
}
- Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+ Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
return uCanonPhase;
@@ -250,8 +250,8 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
assert( nVars <= 16 );
nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
- // if ( (nOnes == nWords * 32) )
- // return 999999;
+ // if ( (nOnes == nWords * 32) )
+ // return 999999;
if ( (nOnes > nWords * 32) )
{
@@ -266,8 +266,8 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
- // if ( pStore[i] == nOnes-pStore[i])
- // return 999999;
+ // if ( pStore[i] == nOnes-pStore[i])
+ // return 999999;
if ( pStore[i] >= nOnes-pStore[i])
continue;
uCanonPhase |= (1 << i);
@@ -298,7 +298,7 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
uCanonPhase ^= (1 << (i+1));
}
- Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+ Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
return uCanonPhase;
@@ -311,19 +311,19 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
// int pStore[16];
// int nWords = Kit_TruthWordNum_64bit( nVars );
// int i, Temp, fChange, nOnes;
-// assert( nVars <= 16 );
-//
+// assert( nVars <= 16 );
+//
// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
-//
+//
// if ( (nOnes > nWords * 32) )
// {
// Kit_TruthNot_64bit( pInOut, nVars );
-// nOnes = nWords*64 - nOnes;
+// nOnes = nWords*64 - nOnes;
// }
-//
+//
// // collect the minterm counts
// Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
-//
+//
// // canonicize phase
// for ( i = 0; i < nVars; i++ )
// {
@@ -332,19 +332,19 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
// pStore[i] = nOnes-pStore[i];
// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
// }
-//
+//
// do {
// fChange = 0;
// for ( i = 0; i < nVars-1; i++ )
// {
// if ( pStore[i] <= pStore[i+1] )
// continue;
-// fChange = 1;
-//
+// fChange = 1;
+//
// Temp = pStore[i];
// pStore[i] = pStore[i+1];
// pStore[i+1] = Temp;
-//
+//
// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
// }
// } while ( fChange );
@@ -389,7 +389,7 @@ inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int
pStore[i] = pStore[i+1];
pStore[i+1] = Temp;
- Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+ Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
}
diff --git a/src/bool/lucky/luckySwapIJ.c b/src/bool/lucky/luckySwapIJ.c
index 1d598c2a..9901f9cb 100644
--- a/src/bool/lucky/luckySwapIJ.c
+++ b/src/bool/lucky/luckySwapIJ.c
@@ -24,7 +24,7 @@ void swap_ij_case1( word* f,int totalVars, int i, int j)
{
int e,wordsNumber,n,shift;
word maskArray[45]=
- { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
+ { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 ,0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 ,
0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 ,0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 ,
0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 ,0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 ,
@@ -51,7 +51,7 @@ void swap_ij_case2( word* f,int totalVars, int i, int j)
word temp;
int x,y,wj;
int WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
- // int forShift = ((Word)1)<<i;
+ // int forShift = ((Word)1)<<i;
int forShift = (1<<i);
wj = 1 << (j - 6);
x = 0;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 14:06:29 +0000