From dcd37b6a25c37a546f08c1942dda2d7d64e72e48 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Wed, 27 Jul 2016 23:30:46 -0300 Subject: Make FX able to handle SCC and remove its SOP preprocessing. Some other small changes. --- src/base/abci/abcFx.c | 41 +++++++++++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 10 deletions(-) (limited to 'src/base/abci/abcFx.c') diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 445082ca..4694c394 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -103,6 +103,7 @@ struct Fx_Man_t_ Vec_Int_t * vCompls; // complemented attribute of each cube pair Vec_Int_t * vCubeFree; // cube-free divisor Vec_Int_t * vDiv; // selected divisor + Vec_Int_t * vSCC; // single cubes containment cubes // statistics abctime timeStart; // starting time int nVars; // original problem variables @@ -312,11 +313,6 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int f printf( "Abc_NtkFastExtract: Nodes have duplicated fanins. FX is not performed.\n" ); return 0; } - // sweep removes useless nodes - Abc_NtkCleanup( pNtk, 0 ); -// Abc_NtkOrderFanins( pNtk ); - // makes sure the SOPs are SCC-free and D1C-free - Abc_NtkMakeLegit( pNtk ); // collect information about the covers vCubes = Abc_NtkFxRetrieve( pNtk ); // call the fast extract procedure @@ -359,6 +355,7 @@ Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes ) p->vCompls = Vec_IntAlloc( 100 ); p->vCubeFree = Vec_IntAlloc( 100 ); p->vDiv = Vec_IntAlloc( 100 ); + p->vSCC = Vec_IntAlloc( 100 ); return p; } void Fx_ManStop( Fx_Man_t * p ) @@ -377,6 +374,7 @@ void Fx_ManStop( Fx_Man_t * p ) Vec_IntFree( p->vCompls ); Vec_IntFree( p->vCubeFree ); Vec_IntFree( p->vDiv ); + Vec_IntFree( p->vSCC ); ABC_FREE( p ); } @@ -571,10 +569,10 @@ static int Fx_ManDivNormalize( Vec_Int_t * vCubeFree ) // return 1 if complement ***********************************************************************/ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCubeFree, int * fWarning ) { - int * pBeg1 = vArr1->pArray + 1; // skip variable ID - int * pBeg2 = vArr2->pArray + 1; // skip variable ID - int * pEnd1 = vArr1->pArray + vArr1->nSize; - int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pBeg1 = Vec_IntArray( vArr1 ) + 1; // skip variable ID + int * pBeg2 = Vec_IntArray( vArr2 ) + 1; // skip variable ID + int * pEnd1 = Vec_IntLimit( vArr1 ); + int * pEnd2 = Vec_IntLimit( vArr2 ); int Counter = 0, fAttr0 = 0, fAttr1 = 1; Vec_IntClear( vCubeFree ); while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) @@ -597,7 +595,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu if ( Vec_IntSize(vCubeFree) == 0 ) printf( "The SOP has duplicated cubes.\n" ); else if ( Vec_IntSize(vCubeFree) == 1 ) - printf( "The SOP has contained cubes.\n" ); + return -1; else if ( Vec_IntSize( vCubeFree ) == 3 ) { int * pArray = Vec_IntArray( vCubeFree ); @@ -799,6 +797,17 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) ) break; Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vCubeFree, fWarning ); + if ( Base == -1 ) + { + if ( fRemove == 0 ) + { + if ( Vec_IntSize( vCube ) > Vec_IntSize( vPivot ) ) + Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vCube ) ); + else + Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vPivot ) ); + } + continue; + } if ( Vec_IntSize(p->vCubeFree) == 4 ) { int Value = Fx_ManDivNormalize( p->vCubeFree ); @@ -1103,6 +1112,17 @@ ExtractFromPairs: Vec_WecUnmarkLevels( p->vCubes, p->vCubesS ); Vec_WecUnmarkLevels( p->vCubes, p->vCubesD ); + // Deal with SCC + if ( Vec_IntSize( p->vSCC ) ) + { + Vec_IntUniqify( p->vSCC ); + Fx_ManForEachCubeVec( p->vSCC, p->vCubes, vCube, i ) + { + Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1, fWarning ); // remove - update + Vec_IntClear( vCube ); + } + Vec_IntClear( p->vSCC ); + } // add cost of the new divisor if ( Vec_IntSize(vDiv) > 2 ) { @@ -1123,6 +1143,7 @@ ExtractFromPairs: if ( (p->nCompls && i > 1) || Vec_IntSize( vDiv ) == 2 ) // the last two lits are possibly complemented Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD ); } + } /**Function************************************************************* -- cgit v1.2.3