| /**CFile**************************************************************** |
| |
| FileName [luckyFast16.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Semi-canonical form computation package.] |
| |
| Synopsis [Truth table minimization procedures for up to 16 vars.] |
| |
| Author [Jake] |
| |
| Date [Started - September 2012] |
| |
| ***********************************************************************/ |
| |
| #include "luckyInt.h" |
| //#define LUCKY_VERIFY |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| static word SFmask[5][4] = { |
| {ABC_CONST(0x8888888888888888),ABC_CONST(0x4444444444444444),ABC_CONST(0x2222222222222222),ABC_CONST(0x1111111111111111)}, |
| {ABC_CONST(0xC0C0C0C0C0C0C0C0),ABC_CONST(0x3030303030303030),ABC_CONST(0x0C0C0C0C0C0C0C0C),ABC_CONST(0x0303030303030303)}, |
| {ABC_CONST(0xF000F000F000F000),ABC_CONST(0x0F000F000F000F00),ABC_CONST(0x00F000F000F000F0),ABC_CONST(0x000F000F000F000F)}, |
| {ABC_CONST(0xFF000000FF000000),ABC_CONST(0x00FF000000FF0000),ABC_CONST(0x0000FF000000FF00),ABC_CONST(0x000000FF000000FF)}, |
| {ABC_CONST(0xFFFF000000000000),ABC_CONST(0x0000FFFF00000000),ABC_CONST(0x00000000FFFF0000),ABC_CONST(0x000000000000FFFF)} |
| }; |
| |
| // we need next two functions only for verification of lucky method in debugging mode |
| void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase) |
| { |
| int Temp; |
| swap_ij(pAfter, nVars, iVarInPosition, jVar); |
| |
| Temp = pCanonPerm[iVarInPosition]; |
| pCanonPerm[iVarInPosition] = pCanonPerm[jVar]; |
| pCanonPerm[jVar] = Temp; |
| |
| if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) ) |
| { |
| *pUCanonPhase ^= (1 << iVarInPosition); |
| *pUCanonPhase ^= (1 << jVar); |
| } |
| if((*pUCanonPhase>>iVarInPosition) & 1) |
| Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition ); |
| |
| } |
| int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase) |
| { |
| int i,j; |
| char tempChar; |
| for(j=0;j<nVars;j++) |
| { |
| tempChar = 'a'+ j; |
| for(i=j;i<nVars;i++) |
| { |
| if(tempChar != pCanonPerm[i]) |
| continue; |
| swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase); |
| break; |
| } |
| } |
| if((uCanonPhase>>nVars) & 1) |
| Kit_TruthNot_64bit(pAfter, nVars ); |
| if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0) |
| return 0; |
| else |
| return 1; |
| } |
| |
| ////////////////////////////////////lessThen5///////////////////////////////////////////////////////////////////////////////////////////// |
| |
| // there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q) |
| //updataInfo updates CanonPerm and CanonPhase based on what quoter in position iQ and jQ |
| void updataInfo(int iQ, int jQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| *pCanonPhase = adjustInfoAfterSwap(pCanonPerm, *pCanonPhase, iVar, ((abs(iQ-jQ)-1)<<2) + iQ ); |
| |
| } |
| |
| // returns the first shift from the left in word x that has One bit in it. |
| // blockSize = ShiftSize/4 |
| int firstShiftWithOneBit(word x, int blockSize) |
| { |
| int n = 0; |
| if(blockSize == 16){ return 0;} |
| if (x >= ABC_CONST(0x0000000100000000)) {n = n + 32; x = x >> 32;} |
| if(blockSize == 8){ return (64-n)/32;} |
| if (x >= ABC_CONST(0x0000000000010000)) {n = n + 16; x = x >> 16;} |
| if(blockSize == 4){ return (64-n)/16;} |
| if (x >= ABC_CONST(0x0000000000000100)) {n = n + 8; x = x >> 8;} |
| if(blockSize == 2){ return (64-n)/8;} |
| if (x >= ABC_CONST(0x0000000000000010)) {n = n + 4; x = x >> 4;} |
| return (64-n)/4; |
| |
| } |
| |
| // It rearranges InOut (swaps and flips through rearrangement of quoters) |
| // It updates Info at the end |
| void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int i, blockSize = 1<<iVar; |
| // printf("in arrangeQuoters_superFast_lessThen5\n"); |
| // printf("start = %d, iQ = %d,jQ = %d,kQ = %d,lQ = %d, iVar = %d, nWords = %d\n", start, iQ, jQ, kQ , lQ, iVar, nWords); |
| for(i=start;i>=0;i--) |
| { |
| assert( iQ*blockSize < 64 ); |
| assert( jQ*blockSize < 64 ); |
| assert( kQ*blockSize < 64 ); |
| assert( lQ*blockSize < 64 ); |
| assert( 3*blockSize < 64 ); |
| pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) | |
| (((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) | |
| (((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) | |
| (((pInOut[i] & SFmask[iVar][lQ])<<(lQ*blockSize))>>3*blockSize); |
| } |
| updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase); |
| // printf("out arrangeQuoters_superFast_lessThen5\n"); |
| |
| } |
| // static word SFmask[5][4] = { |
| // {0x8888888888888888,0x4444444444444444,0x2222222222222222,0x1111111111111111}, |
| // {0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303}, |
| // {0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F}, |
| // {0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF}, |
| // {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF} |
| // }; |
| //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 0Q and 3Q |
| int minTemp0_fast(word* pInOut, int iVar, int nWords, int* pDifStart) |
| { |
| int i, blockSize = 1<<iVar; |
| word temp; |
| for(i=nWords - 1; i>=0; i--) |
| { |
| assert( 3*blockSize < 64 ); |
| temp = ((pInOut[i] & SFmask[iVar][0])) ^ ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)); |
| if( temp == 0) |
| continue; |
| else |
| { |
| *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize); |
| if( ((pInOut[i] & SFmask[iVar][0])) < ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)) ) |
| return 0; |
| else |
| return 3; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| |
| } |
| |
| //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 1Q and 2Q |
| int minTemp1_fast(word* pInOut, int iVar, int nWords, int* pDifStart) |
| { |
| int i, blockSize = 1<<iVar; |
| word temp; |
| for(i=nWords - 1; i>=0; i--) |
| { |
| assert( 2*blockSize < 64 ); |
| temp = ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) ^ ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)); |
| if( temp == 0) |
| continue; |
| else |
| { |
| *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize); |
| if( ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) < ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)) ) |
| return 1; |
| else |
| return 2; |
| } |
| } |
| *pDifStart=0; |
| return 1; |
| } |
| |
| //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and 1 if jQ is |
| // DifStart contains the information about the first different bit in iQ and jQ |
| int minTemp2_fast(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart) |
| { |
| int i, blockSize = 1<<iVar; |
| word temp; |
| for(i=nWords - 1; i>=0; i--) |
| { |
| assert( jQ*blockSize < 64 ); |
| temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)); |
| if( temp == 0) |
| continue; |
| else |
| { |
| *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize); |
| if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) ) |
| return 0; |
| else |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| } |
| // same as minTemp2_fast but this one has a start position |
| int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart) |
| { |
| int i, blockSize = 1<<iVar; |
| word temp; |
| for(i=start; i>=finish; i--) |
| { |
| assert( jQ*blockSize < 64 ); |
| temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)); |
| if( temp == 0) |
| continue; |
| else |
| { |
| *pDifStart = i*100 + 20 - firstShiftWithOneBit(temp, blockSize); |
| if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) ) |
| return 0; |
| else |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| } |
| |
| // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them |
| void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int min1, min2, DifStart0, DifStart1, DifStartMin, DifStart4=0; |
| int M[2]; |
| 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); |
| // printf("\nDifStart0 = %d, DifStart1 = %d, DifStartMin = %d\n",DifStart0, DifStart1, DifStartMin); |
| // printf("M[0] = %d, M[1] = %d, min1 = %d\n", M[0], M[1], min1); |
| if(DifStart0 != DifStart1) |
| { |
| // printf("if\n"); |
| if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 ) |
| arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase); |
| else if( DifStart0 > DifStart1) |
| arrangeQuoters_superFast_lessThen5(pInOut,luckyMax(DifStartMin/100, DifStart0/100), M[0], M[1], 3 - M[1], 3 - M[0], iVar, nWords, pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_lessThen5(pInOut,luckyMax(DifStartMin/100, DifStart1/100), M[1], M[0], 3 - M[0], 3 - M[1], iVar, nWords, pCanonPerm, pCanonPhase); |
| } |
| else |
| { |
| // printf("else\n"); |
| if(DifStartMin>=DifStart0) |
| arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase); |
| else |
| { |
| min2 = minTemp3_fast(pInOut, iVar, DifStart0/100, DifStartMin/100, 3-M[0], 3-M[1], &DifStart4); // no reuse DifStart1 because DifStart1 = DifStart1=0 |
| // printf("after minTemp3_fast min2 = %d, DifStart4 = %d\n", min2, DifStart4); |
| if(DifStart4>DifStartMin) |
| arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], iVar, nWords, pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase); |
| } |
| } |
| } |
| |
| void minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int DifStart1; |
| if(minTemp1_fast(pInOut, iVar, nWords, &DifStart1) == 2) |
| arrangeQuoters_superFast_lessThen5(pInOut, DifStart1/100, 0, 2, 1, 3, iVar, nWords, pCanonPerm, pCanonPhase); |
| } |
| ////////////////////////////////////iVar = 5///////////////////////////////////////////////////////////////////////////////////////////// |
| |
| // It rearranges InOut (swaps and flips through rearrangement of quoters) |
| // It updates Info at the end |
| void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int start, int iQ, int jQ, int kQ, int lQ, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int i,blockSize,shiftSize; |
| unsigned* tempPtr = temp+start; |
| // printf("in arrangeQuoters_superFast_iVar5\n"); |
| |
| if(iQ == 0 && jQ == 1) |
| return; |
| blockSize = sizeof(unsigned); |
| shiftSize = 4; |
| for(i=start-1;i>0;i-=shiftSize) |
| { |
| tempPtr -= 1; |
| memcpy(tempPtr, pInOut+i-iQ, blockSize); |
| tempPtr -= 1; |
| memcpy(tempPtr, pInOut+i-jQ, blockSize); |
| tempPtr -= 1; |
| memcpy(tempPtr, pInOut+i-kQ, blockSize); |
| tempPtr -= 1; |
| memcpy(tempPtr, pInOut+i-lQ, blockSize); |
| } |
| memcpy(pInOut, temp, start*sizeof(unsigned)); |
| updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase); |
| } |
| |
| //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 0Q and 3Q |
| int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart) |
| { |
| int i, temp; |
| // printf("in minTemp0_fast_iVar5\n"); |
| for(i=(nWords)*2 - 1; i>=0; i-=4) |
| { |
| temp = CompareWords(pInOut[i],pInOut[i-3]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 3; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| } |
| |
| //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 1Q and 2Q |
| int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart) |
| { |
| int i, temp; |
| // printf("in minTemp1_fast_iVar5\n"); |
| for(i=(nWords)*2 - 2; i>=0; i-=4) |
| { |
| temp = CompareWords(pInOut[i],pInOut[i-1]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+2; |
| return 1; |
| } |
| else |
| { |
| *pDifStart = i+2; |
| return 2; |
| } |
| } |
| *pDifStart=0; |
| return 1; |
| } |
| |
| //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in iQ and jQ |
| int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart) |
| { |
| int i, temp; |
| // printf("in minTemp2_fast_iVar5\n"); |
| |
| for(i=(nWords)*2 - 1; i>=0; i-=4) |
| { |
| temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| } |
| |
| // same as minTemp2_fast but this one has a start position |
| int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart) |
| { |
| int i, temp; |
| // printf("in minTemp3_fast_iVar5\n"); |
| |
| for(i=start-1; i>=finish; i-=4) |
| { |
| temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| return 0; |
| } |
| |
| // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them |
| void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int min1, min2, DifStart0, DifStart1, DifStartMin; |
| int M[2]; |
| unsigned temp[2048]; |
| // printf("in minimalSwapAndFlipIVar_superFast_iVar5\n"); |
| M[0] = minTemp0_fast_iVar5(pInOut, nWords, &DifStart0); // 0, 3 |
| M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2 |
| min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin); |
| if(DifStart0 != DifStart1) |
| { |
| if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 ) |
| arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase); |
| else if( DifStart0 > DifStart1) |
| arrangeQuoters_superFast_iVar5(pInOut, temp, luckyMax(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_iVar5(pInOut, temp, luckyMax(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], pCanonPerm, pCanonPhase); |
| } |
| else |
| { |
| if(DifStartMin>=DifStart0) |
| arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase); |
| else |
| { |
| min2 = minTemp3_fast_iVar5(pInOut, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0 |
| if(DifStart1>DifStartMin) |
| arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], pCanonPerm, pCanonPhase); |
| } |
| } |
| } |
| |
| void minimalSwapAndFlipIVar_superFast_iVar5_noEBFC(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int DifStart1; |
| unsigned temp[2048]; |
| if(minTemp1_fast_iVar5(pInOut, nWords, &DifStart1) == 2) |
| arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart1, 0, 2, 1, 3, pCanonPerm, pCanonPhase); |
| } |
| |
| ////////////////////////////////////moreThen5///////////////////////////////////////////////////////////////////////////////////////////// |
| |
| // It rearranges InOut (swaps and flips through rearrangement of quoters) |
| // It updates Info at the end |
| void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int start, int iQ, int jQ, int kQ, int lQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int i,wordBlock,blockSize,shiftSize; |
| word* tempPtr = temp+start; |
| // printf("in arrangeQuoters_superFast_moreThen5\n"); |
| |
| if(iQ == 0 && jQ == 1) |
| return; |
| wordBlock = (1<<(iVar-6)); |
| blockSize = wordBlock*sizeof(word); |
| shiftSize = wordBlock*4; |
| for(i=start-wordBlock;i>0;i-=shiftSize) |
| { |
| tempPtr -= wordBlock; |
| memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize); |
| tempPtr -= wordBlock; |
| memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize); |
| tempPtr -= wordBlock; |
| memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize); |
| tempPtr -= wordBlock; |
| memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize); |
| } |
| memcpy(pInOut, temp, start*sizeof(word)); |
| updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase); |
| // printf("out arrangeQuoters_superFast_moreThen5\n"); |
| |
| } |
| |
| //It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 0Q and 3Q |
| int minTemp0_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart) |
| { |
| int i, j, temp; |
| int wordBlock = 1<<(iVar-6); |
| int wordDif = 3*wordBlock; |
| int shiftBlock = wordBlock*4; |
| // printf("in minTemp0_fast_moreThen5\n"); |
| |
| for(i=nWords - 1; i>=0; i-=shiftBlock) |
| for(j=0;j<wordBlock;j++) |
| { |
| temp = CompareWords(pInOut[i-j],pInOut[i-j-wordDif]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 3; |
| } |
| } |
| *pDifStart=0; |
| // printf("out minTemp0_fast_moreThen5\n"); |
| |
| return 0; |
| } |
| |
| //It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in 1Q and 2Q |
| int minTemp1_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart) |
| { |
| int i, j, temp; |
| int wordBlock = 1<<(iVar-6); |
| int shiftBlock = wordBlock*4; |
| // printf("in minTemp1_fast_moreThen5\n"); |
| |
| for(i=nWords - wordBlock - 1; i>=0; i-=shiftBlock) |
| for(j=0;j<wordBlock;j++) |
| { |
| temp = CompareWords(pInOut[i-j],pInOut[i-j-wordBlock]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+wordBlock+1; |
| return 1; |
| } |
| else |
| { |
| *pDifStart = i+wordBlock+1; |
| return 2; |
| } |
| } |
| *pDifStart=0; |
| // printf("out minTemp1_fast_moreThen5\n"); |
| |
| return 1; |
| } |
| |
| //It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa |
| // DifStart contains the information about the first different bit in iQ and jQ |
| int minTemp2_fast_moreThen5(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart) |
| { |
| int i, j, temp; |
| int wordBlock = 1<<(iVar-6); |
| int shiftBlock = wordBlock*4; |
| // printf("in minTemp2_fast_moreThen5\n"); |
| |
| for(i=nWords - 1; i>=0; i-=shiftBlock) |
| for(j=0;j<wordBlock;j++) |
| { |
| temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| // printf("out minTemp2_fast_moreThen5\n"); |
| |
| return 0; |
| } |
| |
| // same as minTemp2_fast but this one has a start position |
| int minTemp3_fast_moreThen5(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart) |
| { |
| int i, j, temp; |
| int wordBlock = 1<<(iVar-6); |
| int shiftBlock = wordBlock*4; |
| // printf("in minTemp3_fast_moreThen5\n"); |
| |
| for(i=start-1; i>=finish; i-=shiftBlock) |
| for(j=0;j<wordBlock;j++) |
| { |
| temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]); |
| if(temp == 0) |
| continue; |
| else if(temp == -1) |
| { |
| *pDifStart = i+1; |
| return 0; |
| } |
| else |
| { |
| *pDifStart = i+1; |
| return 1; |
| } |
| } |
| *pDifStart=0; |
| // printf("out minTemp3_fast_moreThen5\n"); |
| |
| return 0; |
| } |
| |
| // It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them |
| void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int min1, min2, DifStart0, DifStart1, DifStartMin; |
| int M[2]; |
| word temp[1024]; |
| // printf("in minimalSwapAndFlipIVar_superFast_moreThen5\n"); |
| 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)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase); |
| else if( DifStart0 > DifStart1) |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, luckyMax(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], iVar, pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, luckyMax(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], iVar, pCanonPerm, pCanonPhase); |
| } |
| else |
| { |
| if(DifStartMin>=DifStart0) |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase); |
| else |
| { |
| min2 = minTemp3_fast_moreThen5(pInOut, iVar, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0 |
| if(DifStart1>DifStartMin) |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[(min2+1)&1], M[min2], 3 - M[min2], 3 - M[(min2+1)&1], iVar, pCanonPerm, pCanonPhase); |
| else |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[min1], M[(min1+1)&1], 3 - M[(min1+1)&1], 3 - M[min1], iVar, pCanonPerm, pCanonPhase); |
| } |
| } |
| // printf("out minimalSwapAndFlipIVar_superFast_moreThen5\n"); |
| |
| } |
| |
| void minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int DifStart1; |
| word temp[1024]; |
| if(minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1) == 2) |
| arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart1, 0, 2, 1, 3, iVar, pCanonPerm, pCanonPhase); |
| } |
| |
| /////////////////////////////////// for all ///////////////////////////////////////////////////////////////////////////////////////////// |
| void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase) |
| { |
| word oneWord=1; |
| if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord ) |
| { |
| Kit_TruthNot_64bit( pInOut, nVars ); |
| (* pCanonPhase) ^=(1<<nVars); |
| } |
| |
| } |
| |
| // this function finds minimal for all TIED(and tied only) iVars |
| //it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store |
| int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int i; |
| word pDuplicate[1024]; |
| int bitInfoTemp = pStore[0]; |
| memcpy(pDuplicate,pInOut,nWords*sizeof(word)); |
| // printf("in minimalSwapAndFlipIVar_superFast_all\n"); |
| for(i=0;i<5;i++) |
| { |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_lessThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase); |
| else |
| { |
| bitInfoTemp = pStore[i+1]; |
| continue; |
| } |
| } |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_iVar5((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase); |
| else |
| bitInfoTemp = pStore[i+1]; |
| |
| for(i=6;i<nVars-1;i++) |
| { |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_moreThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase); |
| else |
| { |
| bitInfoTemp = pStore[i+1]; |
| continue; |
| } |
| } |
| // printf("out minimalSwapAndFlipIVar_superFast_all\n"); |
| |
| if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0) |
| return 0; |
| else |
| return 1; |
| } |
| |
| int minimalSwapAndFlipIVar_superFast_all_noEBFC(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| int i; |
| word pDuplicate[1024]; |
| int bitInfoTemp = pStore[0]; |
| memcpy(pDuplicate,pInOut,nWords*sizeof(word)); |
| for(i=0;i<5;i++) |
| { |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase); |
| else |
| { |
| bitInfoTemp = pStore[i+1]; |
| continue; |
| } |
| } |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_iVar5_noEBFC((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase); |
| else |
| bitInfoTemp = pStore[i+1]; |
| |
| for(i=6;i<nVars-1;i++) |
| { |
| if(bitInfoTemp == pStore[i+1]) |
| minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase); |
| else |
| { |
| bitInfoTemp = pStore[i+1]; |
| continue; |
| } |
| } |
| if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0) |
| return 0; |
| else |
| return 1; |
| } |
| |
| |
| // old version with out noEBFC |
| // void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| // { |
| // while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0) |
| // continue; |
| // } |
| |
| void luckyCanonicizerS_F_first_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| if(((* pCanonPhase) >> (nVars+1)) & 1) |
| while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0) |
| continue; |
| else |
| while( minimalSwapAndFlipIVar_superFast_all_noEBFC(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0) |
| continue; |
| } |
| |
| void luckyCanonicizerS_F_first_16Vars11(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| word duplicate[1024]; |
| char pCanonPerm1[16]; |
| unsigned uCanonPhase1; |
| |
| if((* pCanonPhase) >> (nVars+2) ) |
| { |
| memcpy(duplicate, pInOut, sizeof(word)*nWords); |
| Kit_TruthNot_64bit(duplicate, nVars); |
| uCanonPhase1 = *pCanonPhase; |
| uCanonPhase1 ^= (1 << nVars); |
| memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16); |
| luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase); |
| luckyCanonicizerS_F_first_16Vars1(duplicate, nVars, nWords, pStore, pCanonPerm1, &uCanonPhase1); |
| if(memCompare(pInOut, duplicate,nVars) == 1) |
| { |
| *pCanonPhase = uCanonPhase1; |
| memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16); |
| memcpy(pInOut, duplicate, sizeof(word)*nWords); |
| } |
| } |
| else |
| { |
| luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase); |
| } |
| } |
| |
| void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| assert( nVars > 6 && nVars <= 16 ); |
| (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore ); |
| luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); |
| } |
| |
| void bitReverceOrder(word* x, int nVars) |
| { |
| int i; |
| for(i= nVars-1;i>=0;i--) |
| Kit_TruthChangePhase_64bit( x, nVars, i ); |
| } |
| |
| |
| void luckyCanonicizer_final_fast_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase) |
| { |
| assert( nVars > 6 && nVars <= 16 ); |
| (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore ); |
| luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); |
| bitReverceOrder(pInOut, nVars); |
| (*pCanonPhase) ^= (1<<nVars) -1; |
| luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); |
| // bitReverceOrder(pInOut, nVars); |
| // (*pCanonPhase) ^= (1<<nVars) -1; |
| // luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase ); |
| } |
| |
| |
| // top-level procedure calling two special cases (nVars <= 6 and nVars <= 16) |
| unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm ) |
| { |
| int nWords; |
| int pStore[16]; |
| unsigned uCanonPhase = 0; |
| #ifdef LUCKY_VERIFY |
| word temp[1024] = {0}; |
| word duplicate[1024] = {0}; |
| Kit_TruthCopy_64bit( duplicate, pInOut, nVars ); |
| #endif |
| if ( nVars <= 6 ) |
| pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase); |
| else if ( nVars <= 16 ) |
| { |
| nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6)); |
| luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase ); |
| } |
| else assert( 0 ); |
| #ifdef LUCKY_VERIFY |
| Kit_TruthCopy_64bit( temp, pInOut, nVars ); |
| assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) ); |
| #endif |
| return uCanonPhase; |
| } |
| |
| unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm) |
| { |
| int nWords; |
| int pStore[16]; |
| unsigned uCanonPhase = 0; |
| #ifdef LUCKY_VERIFY |
| word temp[1024] = {0}; |
| word duplicate[1024] = {0}; |
| Kit_TruthCopy_64bit( duplicate, pInOut, nVars ); |
| #endif |
| if ( nVars <= 6 ) |
| pInOut[0] = luckyCanonicizer_final_fast_6Vars1( pInOut[0], pStore, pCanonPerm, &uCanonPhase); |
| else if ( nVars <= 16 ) |
| { |
| nWords = 1 << (nVars - 6); |
| luckyCanonicizer_final_fast_16Vars1( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase ); |
| } |
| else assert( 0 ); |
| #ifdef LUCKY_VERIFY |
| Kit_TruthCopy_64bit( temp, pInOut, nVars ); |
| assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) ); |
| #endif |
| return uCanonPhase; |
| } |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
| |
| |
