From ff938c7141206e61139b3e851ccd5f8b966fa72a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 22 Nov 2011 18:48:03 -0800 Subject: Modifications to the matching procedure --- src/map/if/ifDec16.c | 132 ++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 126 insertions(+), 6 deletions(-) (limited to 'src/map/if/ifDec16.c') diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c index 606fb912..415f4a03 100644 --- a/src/map/if/ifDec16.c +++ b/src/map/if/ifDec16.c @@ -727,6 +727,99 @@ void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t } + +void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar ) +{ + word low2High, high2Low, temp; + int nWords = If_CluWordNum(nVars); + int shift, step, iStep, jStep; + int w = 0, i = 0, j = 0; + static word PPMasks[6][6] = { + { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA }, + { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC }, + { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 }, + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 }, + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 }, + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 } + }; + if( iVar == jVar ) + return; + if( jVar < iVar ) + { + int varTemp = jVar; + jVar = iVar; + iVar = varTemp; + } + if ( iVar <= 5 && jVar <= 5 ) + { + shift = (1 << jVar) - (1 << iVar); + for ( w = 0; w < nWords; w++ ) + { + low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift; + pTruth[w] &= ~PPMasks[iVar][jVar - 1]; + high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift; + pTruth[w] &= ~ (PPMasks[iVar][jVar - 1] << shift); + pTruth[w] = pTruth[w] | low2High | high2Low; + } + } + else if( iVar <= 5 && jVar > 5 ) + { + step = If_CluWordNum(jVar + 1)/2; + shift = 1 << iVar; + for ( w = 0; w < nWords; w += 2*step ) + { + for (j = 0; j < step; j++) + { + low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift; + pTruth[w + j] &= ~PPMasks[iVar][5]; + high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift; + pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift); + pTruth[w + j] |= high2Low; + pTruth[w + step + j] |= low2High; + } + } + } + else + { + iStep = If_CluWordNum(iVar + 1)/2; + jStep = If_CluWordNum(jVar + 1)/2; + for ( w = 0; w < nWords; w += 2*jStep ) + { + for ( i = 0; i < jStep; i += 2*iStep ) + { + temp = pTruth[w + iStep + i]; + pTruth[w + iStep + i] = pTruth[w + jStep + i]; + pTruth[w + jStep + i] = temp; + } + + } + } + if ( V2P && P2V ) + { + V2P[P2V[iVar]] = jVar; + V2P[P2V[jVar]] = iVar; + P2V[iVar] ^= P2V[jVar]; + P2V[jVar] ^= P2V[iVar]; + P2V[iVar] ^= P2V[jVar]; + } +} +void If_CluReverseOrder( word * pTruth, int nVars, int * V2P, int * P2V, int iVarStart ) +{ + int i, j, k; + for ( k = 0; k < (nVars-iVarStart)/2 ; k++ ) + { + i = iVarStart + k; + j = nVars - 1 - k; + If_CluSwapVars( pTruth, nVars, V2P, P2V, i, j ); + } +} + +// moves one var (v) to the given position (p) +void If_CluMoveVar2( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p ) +{ + If_CluSwapVars( pF, nVars, Var2Pla, Pla2Var, Var2Pla[v], p ); +} + // moves one var (v) to the given position (p) void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p ) { @@ -772,11 +865,15 @@ void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v ); } + // reverses the variable order -void If_CluReverseOrder( word * pF, int nVars, int * V2P, int * P2V, int iVarStart ) +void If_CluReverseOrder_old( word * pF, int nVars, int * V2P, int * P2V, int iVarStart ) { + word pG[CLU_WRD_MAX]; int v; + If_CluCopy( pG, pF, nVars ); + // for ( v = 0; v < nVars; v++ ) // printf( "%c ", 'a' + P2V[v] ); // printf( " --- " ); @@ -787,6 +884,25 @@ void If_CluReverseOrder( word * pF, int nVars, int * V2P, int * P2V, int iVarSta // for ( v = 0; v < nVars; v++ ) // printf( "%c ", 'a' + P2V[v] ); // printf( "\n" ); + +// if ( iVarStart > 0 ) +// return; + + If_CluReverseOrder( pG, nVars, NULL, NULL, iVarStart ); + if ( If_CluEqual( pG, pF, nVars ) ) + { +// printf( "+" ); + } + else + { +/* + printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pG, nVars ); + printf( "\n" ); +*/ + printf( "%d ", nVars ); + } } // return the number of cofactors w.r.t. the topmost vars (nBSsize) @@ -1191,7 +1307,7 @@ int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_ return 0; } - + // finds a good var group (cof count < 6; vars are MSBs) If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint ) { @@ -1236,7 +1352,8 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); for ( v = nVars-2-nBSsize; v >= iVarStart; v-- ) { - If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); +// If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); + If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); if ( nCofsBest2 >= nCofs ) { @@ -1245,7 +1362,8 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * } } // go back - If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); +// If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); + If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); // update best bound set nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); assert( nCofs == nCofsBest2 ); @@ -1256,7 +1374,8 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); for ( v = nVars-nBSsize; v < nVars; v++ ) { - If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); +// If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); + If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); if ( nCofsBest2 >= nCofs ) { @@ -1266,7 +1385,8 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * } // go back - If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); +// If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); + If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); // update best bound set nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); assert( nCofs == nCofsBest2 ); -- cgit v1.2.3