diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 12 | ||||
-rw-r--r-- | src/opt/fxch/Fxch.c | 6 | ||||
-rw-r--r-- | src/opt/fxch/Fxch.h | 14 | ||||
-rw-r--r-- | src/opt/fxch/FxchDiv.c | 125 | ||||
-rw-r--r-- | src/opt/fxch/FxchMan.c | 44 | ||||
-rw-r--r-- | src/opt/fxch/FxchSCHashTable.c | 6 |
6 files changed, 20 insertions, 187 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index aa2d5598..b09a3001 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4137,17 +4137,16 @@ usage: ***********************************************************************/ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkFxchPerform( Abc_Ntk_t * pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkFxchPerform( Abc_Ntk_t * pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c, nMaxDivExt = 0, - SMode = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "Nsvwh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "Nvwh")) != EOF ) { switch (c) { @@ -4164,10 +4163,6 @@ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; break; - case 's': - SMode ^= 1; - break; - case 'v': fVerbose ^= 1; break; @@ -4206,7 +4201,7 @@ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - Abc_NtkFxchPerform( pNtk, nMaxDivExt, SMode, fVerbose, fVeryVerbose ); + Abc_NtkFxchPerform( pNtk, nMaxDivExt, fVerbose, fVeryVerbose ); return 0; @@ -4214,7 +4209,6 @@ usage: Abc_Print( -2, "usage: fxch [-N <num>] [-svwh]\n"); Abc_Print( -2, "\t performs fast extract with cube hashing on the current network\n"); Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = unused]\n" ); - Abc_Print( -2, "\t-s : memory saving mode (slower) [default = %d]\n", SMode? "yes": "no" ); Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : print additional information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c index a9228dc6..6c3983ef 100644 --- a/src/opt/fxch/Fxch.c +++ b/src/opt/fxch/Fxch.c @@ -39,12 +39,11 @@ ABC_NAMESPACE_IMPL_START int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, - int SMode, int fVerbose, int fVeryVerbose ) { abctime TempTime; - Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, (char)SMode ); + Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes ); int i; TempTime = Abc_Clock(); @@ -102,7 +101,6 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes, ***********************************************************************/ int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, - int SMode, int fVerbose, int fVeryVerbose ) { @@ -117,7 +115,7 @@ int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, } vCubes = Abc_NtkFxRetrieve( pNtk ); - if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, SMode, fVerbose, fVeryVerbose ) > 0 ) + if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, fVerbose, fVeryVerbose ) > 0 ) { Abc_NtkFxInsert( pNtk, vCubes ); Vec_WecFree( vCubes ); diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h index be229b98..d9f9dc7e 100644 --- a/src/opt/fxch/Fxch.h +++ b/src/opt/fxch/Fxch.h @@ -113,9 +113,6 @@ struct Fxch_Man_t_ Vec_Int_t* vCubeFree; // cube-free divisor Vec_Int_t* vDiv; // selected divisor - /* Config */ - char SMode; /* Saving Memory mode */ - /* Statistics */ abctime timeInit; /* Initialization time */ abctime timeExt; /* Extraction time */ @@ -138,8 +135,8 @@ extern void Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes ); extern int Abc_NtkFxCheck( Abc_Ntk_t* pNtk ); /*===== Fxch.c =======================================================*/ -int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose ); -int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose ); +int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose ); +int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int fVerbose, int fVeryVerbose ); /*===== FxchDiv.c ====================================================================================================*/ int Fxch_DivCreate( Fxch_Man_t* pFxchMan, Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 ); @@ -149,13 +146,8 @@ void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube int Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl ); void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv ); -/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ -void Fxch_DivFindPivots( Vec_Int_t* vDiv, int* pLit0, int* pLit1 ); -int Fxch_DivFind( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vCubeFree ); -void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubes_Lit0, Vec_Int_t* vCubes_Lit1 ); - /*===== FxchMan.c ====================================================================================================*/ -Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, char SMode ); +Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ); void Fxch_ManFree( Fxch_Man_t* pFxchMan ); void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars ); void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan ); diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c index 9541d8e8..68fd569d 100644 --- a/src/opt/fxch/FxchDiv.c +++ b/src/opt/fxch/FxchDiv.c @@ -225,8 +225,7 @@ int Fxch_DivAdd( Fxch_Man_t* pFxchMan, /* Verify if the divisor already exist */ if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) ) { - if ( pFxchMan->SMode == 0 ) - Vec_WecPushLevel( pFxchMan->vDivCubePairs ); + Vec_WecPushLevel( pFxchMan->vDivCubePairs ); /* Assign initial weight */ if ( fSingleCube ) @@ -458,128 +457,6 @@ void Fxch_DivPrint( Fxch_Man_t* pFxchMan, printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) ); } -/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ -void Fxch_DivFindPivots( Vec_Int_t* vDiv, - int* pLit0, - int* pLit1 ) -{ - int i, - Lit; - * pLit0 = -1; - * pLit1 = -1; - - Vec_IntForEachEntry( vDiv, Lit, i ) - { - if ( Abc_LitIsCompl( Lit ) ) - { - if ( *pLit1 == -1 ) - *pLit1 = Abc_Lit2Var( Lit ); - } - else - { - if ( *pLit0 == -1 ) - *pLit0 = Abc_Lit2Var( Lit ); - } - if ( *pLit0 >= 0 && *pLit1 >= 0 ) - return; - } -} - -int Fxch_DivFind( Vec_Int_t* vCube0, - Vec_Int_t* vCube1, - Vec_Int_t* vCubeFree ) -{ - int Counter = 0, - fAttr0 = 0, - fAttr1 = 1; - int* pBeg1 = vCube0->pArray + 1, - * pBeg2 = vCube1->pArray + 1, - * pEnd1 = vCube0->pArray + vCube0->nSize, - * pEnd2 = vCube1->pArray + vCube1->nSize; - - Vec_IntClear( vCubeFree ); - - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) - { - if ( *pBeg1 == *pBeg2 ) - { - pBeg1++; - pBeg2++; - Counter++; - } - else if ( *pBeg1 < *pBeg2 ) - Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); - else - { - if ( Vec_IntSize( vCubeFree ) == 0 ) - fAttr0 = 1, fAttr1 = 0; - Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1) ); - } - } - while ( pBeg1 < pEnd1 ) - Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); - while ( pBeg2 < pEnd2 ) - Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1 ) ); - - assert( !Abc_LitIsCompl( Vec_IntEntry(vCubeFree, 0) ) ); - return Counter; -} - -void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, - Vec_Int_t* vCubes_Lit0, - Vec_Int_t* vCubes_Lit1 ) -{ - int* pBeg1 = vCubes_Lit0->pArray + 1, - * pBeg2 = vCubes_Lit1->pArray + 1, - * pEnd1 = vCubes_Lit0->pArray + vCubes_Lit0->nSize, - * pEnd2 = vCubes_Lit1->pArray + vCubes_Lit1->nSize; - - Vec_IntClear( pFxchMan->vPairs ); - - while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) - { - int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ), - CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ), - i, k, i_, k_; - - if ( CubeId1 == CubeId2 ) - { - for ( i = 1; pBeg1+i < pEnd1; i++ ) - if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg1[i], 0) ) - break; - - for ( k = 1; pBeg2+k < pEnd2; k++ ) - if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) ) - break; - - for ( i_ = 0; i_ < i; i_++ ) - for ( k_ = 0; k_ < k; k_++ ) - { - if ( pBeg1[i_] == pBeg2[k_] ) - continue; - Fxch_DivFind( Vec_WecEntry( pFxchMan->vCubes, pBeg1[i_] ), - Vec_WecEntry( pFxchMan->vCubes, pBeg2[k_] ), - pFxchMan->vCubeFree ); - - if ( Vec_IntSize( pFxchMan->vCubeFree ) == 4 ) - Fxch_DivNormalize( pFxchMan->vCubeFree ); - - if ( !Vec_IntEqual( pFxchMan->vDiv, pFxchMan->vCubeFree ) ) - continue; - - Vec_IntPush( pFxchMan->vPairs, pBeg1[i_] ); - Vec_IntPush( pFxchMan->vPairs, pBeg2[k_] ); - } - pBeg1 += i; - pBeg2 += k; - } - else if ( CubeId1 < CubeId2 ) - pBeg1++; - else - pBeg2++; - } -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c index a54e6c9a..83794ea9 100644 --- a/src/opt/fxch/FxchMan.c +++ b/src/opt/fxch/FxchMan.c @@ -160,23 +160,18 @@ static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes, //////////////////////////////////////////////////////////////////////// /// PUBLIC INTERFACE /// //////////////////////////////////////////////////////////////////////// -Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, - char SMode ) +Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ) { Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 ); pFxchMan->vCubes = vCubes; - pFxchMan->pDivHash = Hsh_VecManStart( 1000 ); + pFxchMan->pDivHash = Hsh_VecManStart( 1000 ); pFxchMan->vDivWeights = Vec_FltAlloc( 1000 ); - - pFxchMan->SMode = SMode; - if ( pFxchMan->SMode == 0 ) - pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 ); - + pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 ); pFxchMan->vCubeFree = Vec_IntAlloc( 100 ); - pFxchMan->vDiv = Vec_IntAlloc( 100 ); - pFxchMan->vCubesS = Vec_IntAlloc( 100 ); - pFxchMan->vPairs = Vec_IntAlloc( 100 ); + pFxchMan->vDiv = Vec_IntAlloc( 100 ); + pFxchMan->vCubesS = Vec_IntAlloc( 100 ); + pFxchMan->vPairs = Vec_IntAlloc( 100 ); return pFxchMan; } @@ -186,21 +181,15 @@ void Fxch_ManFree( Fxch_Man_t* pFxchMan ) Vec_WecFree( pFxchMan->vLits ); Vec_IntFree( pFxchMan->vLitCount ); Vec_IntFree( pFxchMan->vLitHashKeys ); - Hsh_VecManStop( pFxchMan->pDivHash ); Vec_FltFree( pFxchMan->vDivWeights ); Vec_QueFree( pFxchMan->vDivPrio ); - - if ( pFxchMan->SMode == 0 ) - Vec_WecFree( pFxchMan->vDivCubePairs ); - + Vec_WecFree( pFxchMan->vDivCubePairs ); Vec_IntFree( pFxchMan->vLevels ); - Vec_IntFree( pFxchMan->vCubeFree ); Vec_IntFree( pFxchMan->vDiv ); Vec_IntFree( pFxchMan->vCubesS ); Vec_IntFree( pFxchMan->vPairs ); - ABC_FREE( pFxchMan ); } @@ -381,6 +370,7 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, { Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) ); Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) ); + assert( Lit0 >= 0 && Lit1 >= 0 ); Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) ); Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) ); @@ -388,25 +378,13 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ), pFxchMan->vCubesS ); } - else - Fxch_DivFindPivots( pFxchMan->vDiv, &Lit0, &Lit1 ); - assert( Lit0 >= 0 && Lit1 >= 0 ); /* Find pairs associated with the divisor */ Vec_IntClear( pFxchMan->vPairs ); - if ( pFxchMan->SMode == 1 ) - { - Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit0) ); - Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit1) ); - Fxch_DivFindCubePairs( pFxchMan, Vec_WecEntry( pFxchMan->vLits, Lit0 ), Vec_WecEntry( pFxchMan->vLits, Lit1 ) ); - } - else - { - vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv ); - Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs ); - Vec_IntErase( vDivCubePairs ); - } + vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv ); + Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs ); + Vec_IntErase( vDivCubePairs ); Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) { diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c index 149169ad..669d92c2 100644 --- a/src/opt/fxch/FxchSCHashTable.c +++ b/src/opt/fxch/FxchSCHashTable.c @@ -291,11 +291,8 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base ); - if ( pSCHashTable->pFxchMan->SMode == 0 ) - { Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube ); Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube ); - } Pairs++; } @@ -365,8 +362,6 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable, iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base ); - if ( pSCHashTable->pFxchMan->SMode == 0 ) - { int i, iCube0, iCube1; @@ -381,7 +376,6 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable, } if ( Vec_IntSize( vDivCubePairs ) == 0 ) Vec_IntErase( vDivCubePairs ); - } Pairs++; } |