From 3c978925146b3be8ce6d3bca50a4462839b8d9fa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 30 May 2013 14:09:50 -0700 Subject: New MFS package. --- src/opt/sfm/sfmCnf.c | 13 +++-- src/opt/sfm/sfmCore.c | 8 +-- src/opt/sfm/sfmInt.h | 9 +-- src/opt/sfm/sfmNtk.c | 8 ++- src/opt/sfm/sfmSat.c | 55 +++++++++++++++++- src/opt/sfm/sfmWin.c | 155 +++++++++++++++++++++++++++++++++++--------------- 6 files changed, 183 insertions(+), 65 deletions(-) (limited to 'src/opt/sfm') diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index 02744cf4..0ab92258 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/src/opt/sfm/sfmCnf.c @@ -150,7 +150,7 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ) SeeAlso [] ***********************************************************************/ -void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap ) +void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar ) { Vec_Int_t * vClause; char Entry; @@ -159,11 +159,14 @@ void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap vClause = Vec_WecPushLevel( vRes ); Vec_StrForEachEntry( vCnf, Entry, i ) { - Lit = (int)Entry; - if ( Lit == -1 ) + if ( (int)Entry == -1 ) + { vClause = Vec_WecPushLevel( vRes ); - else - Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) ); + continue; + } + Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry ); + Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar ); + Vec_IntPush( vClause, Lit ); } } diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 865db096..55947a14 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -49,7 +49,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) pPars->nFanoutMax = 30; // the maximum number of fanouts pPars->nDepthMax = 20; // the maximum depth to try pPars->nWinSizeMax = 300; // the maximum window size - pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run + pPars->nBTLimit = 5000; // the maximum number of conflicts in one SAT run pPars->fFixLevel = 1; // does not allow level to increase pPars->fRrOnly = 0; // perform redundancy removal pPars->fArea = 0; // performs optimization for area @@ -255,13 +255,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) { int i, k, Counter = 0; p->timeTotal = Abc_Clock(); - if ( pPars->fVerbose ) + if ( pPars->fVerbose && Vec_StrSum(p->vFixed) > 0 ) printf( "Performing MFS with %d fixed objects.\n", Vec_StrSum(p->vFixed) ); p->pPars = pPars; Sfm_NtkPrepare( p ); // Sfm_ComputeInterpolantCheck( p ); // return 0; - p->nTotalNodesBeg = Vec_WecSize(&p->vFanins) - Sfm_NtkPiNum(p) - Sfm_NtkPoNum(p); + p->nTotalNodesBeg = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) ); p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p); Sfm_NtkForEachNode( p, i ) { @@ -278,7 +278,7 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) } Counter += (k > 0); } - p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p); + p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) ); p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p); p->timeTotal = Abc_Clock() - p->timeTotal; if ( pPars->fVerbose ) diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index d918077c..8ba875c1 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -42,7 +42,6 @@ ABC_NAMESPACE_HEADER_START #define SFM_FANIN_MAX 6 - #define SFM_SAT_UNDEC 0x1234567812345678 #define SFM_SAT_SAT 0x8765432187654321 @@ -77,9 +76,11 @@ struct Sfm_Ntk_t_ int nTravIds; // traversal IDs int nTravIds2; // traversal IDs // window - int iNode; + int iPivotNode; // window pivot Vec_Int_t * vLeaves; // leaves + Vec_Int_t * vLeaves2; // leaves Vec_Int_t * vNodes; // internal + Vec_Int_t * vNodes2; // internal Vec_Int_t * vDivs; // divisors Vec_Int_t * vRoots; // roots Vec_Int_t * vTfo; // TFO (excluding iNode) @@ -145,7 +146,7 @@ static inline int Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k ) { return static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); return Vec_IntEntry(&p->vId2Var, iObj); } static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Vec_IntEntry(&p->vId2Var, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num); Vec_IntWriteEntry(&p->vVar2Id, Num, iObj); } static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num ) { int iObj = Vec_IntEntry(&p->vVar2Id, Num); assert(Vec_IntEntry(&p->vId2Var, iObj) > 0); Vec_IntWriteEntry(&p->vId2Var, iObj, -1); Vec_IntWriteEntry(&p->vVar2Id, Num, -1); } -static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p ) { int i; for ( i = 1; i < p->nSatVars; i++ ) Sfm_ObjCleanSatVar( p, i ); } +static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p ) { int i; for ( i = 1; i < p->nSatVars; i++ ) if ( Vec_IntEntry(&p->vVar2Id, i) != -1 ) Sfm_ObjCleanSatVar( p, i ); } static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); } static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevels, iObj, Lev ); } @@ -171,7 +172,7 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); extern void Sfm_PrintCnf( Vec_Str_t * vCnf ); extern int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ); extern Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ); -extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap ); +extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar ); /*=== sfmCore.c ==========================================================*/ /*=== sfmNtk.c ==========================================================*/ extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos ); diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index da5b4d60..86c8390d 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -155,8 +155,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t Vec_IntFill( &p->vCounts, p->nObjs, 0 ); Vec_IntFill( &p->vTravIds, p->nObjs, 0 ); Vec_IntFill( &p->vTravIds2, p->nObjs, 0 ); - Vec_IntFill( &p->vId2Var, p->nObjs, -1 ); - Vec_IntFill( &p->vVar2Id, p->nObjs, -1 ); + Vec_IntFill( &p->vId2Var, 2*p->nObjs, -1 ); + Vec_IntFill( &p->vVar2Id, 2*p->nObjs, -1 ); p->vCover = Vec_IntAlloc( 1 << 16 ); p->vCnfs = Sfm_CreateCnf( p ); return p; @@ -164,7 +164,9 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t void Sfm_NtkPrepare( Sfm_Ntk_t * p ) { p->vLeaves = Vec_IntAlloc( 1000 ); + p->vLeaves2 = Vec_IntAlloc( 1000 ); p->vNodes = Vec_IntAlloc( 1000 ); + p->vNodes2 = Vec_IntAlloc( 1000 ); p->vDivs = Vec_IntAlloc( 100 ); p->vRoots = Vec_IntAlloc( 1000 ); p->vTfo = Vec_IntAlloc( 1000 ); @@ -197,7 +199,9 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) Vec_IntFree( p->vCover ); // other data Vec_IntFreeP( &p->vLeaves ); + Vec_IntFreeP( &p->vLeaves2 ); Vec_IntFreeP( &p->vNodes ); + Vec_IntFreeP( &p->vNodes2 ); Vec_IntFreeP( &p->vDivs ); Vec_IntFreeP( &p->vRoots ); Vec_IntFreeP( &p->vTfo ); diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index f96e2078..7dc3e565 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -53,13 +53,17 @@ static word s_Truths6[6] = { ***********************************************************************/ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) { + // p->vOrder contains all variables in the window in a good order + // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates + // p->vTfo contains TFO of the node (does not include node) + // p->vRoots contains roots of the TFO of the node (may include node) Vec_Int_t * vClause; int RetValue, iNode = -1, iFanin, i, k; abctime clk = Abc_Clock(); // if ( p->pSat ) // printf( "%d ", p->pSat->stats.learnts ); sat_solver_restart( p->pSat ); - sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 50 ); + sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vOrder) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 10 ); // create SAT variables Sfm_NtkCleanVars( p ); p->nSatVars = 1; @@ -80,7 +84,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) ); Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) ); // generate CNF - Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap ); + Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, -1 ); // add clauses Vec_WecForEachLevel( p->vClauses, vClause, k ) { @@ -90,6 +94,51 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) assert( RetValue ); } } + if ( Vec_IntSize(p->vTfo) > 0 ) + { + assert( p->pPars->nTfoLevMax > 0 ); + assert( Vec_IntSize(p->vRoots) > 0 ); + assert( Vec_IntEntry(p->vTfo, 0) != p->iPivotNode ); + // collect variables of root nodes + Vec_IntClear( p->vLits ); + Vec_IntForEachEntry( p->vRoots, iNode, i ) + Vec_IntPush( p->vLits, Sfm_ObjSatVar(p, iNode) ); + // assign new variables to the TFO nodes + Vec_IntForEachEntry( p->vTfo, iNode, i ) + { + Sfm_ObjCleanSatVar( p, Sfm_ObjSatVar(p, iNode) ); + Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ ); + } + // add CNF clauses for the TFO + Vec_IntForEachEntry( p->vTfo, iNode, i ) + { + assert( Sfm_ObjIsNode(p, iNode) ); + // collect fanin variables + Vec_IntClear( p->vFaninMap ); + Sfm_ObjForEachFanin( p, iNode, iFanin, k ) + Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) ); + Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) ); + // generate CNF + Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, Sfm_ObjSatVar(p, p->iPivotNode) ); + // add clauses + Vec_WecForEachLevel( p->vClauses, vClause, k ) + { + if ( Vec_IntSize(vClause) == 0 ) + break; + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); + assert( RetValue ); + } + } + // create XOR clauses for the roots + Vec_IntForEachEntry( p->vRoots, iNode, i ) + { + sat_solver_add_xor( p->pSat, Vec_IntEntry(p->vLits, i), Sfm_ObjSatVar(p, iNode), p->nSatVars++, 0 ); + Vec_IntWriteEntry( p->vLits, i, Abc_Var2Lit(p->nSatVars-1, 0) ); + } + // make OR clause for the last nRoots variables + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) ); + assert( RetValue ); + } // finalize RetValue = sat_solver_simplify( p->pSat ); assert( RetValue ); @@ -113,7 +162,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) int status, i, Div, iVar, nFinal, * pFinal, nIter = 0; int pLits[2], nVars = sat_solver_nvars( p->pSat ); sat_solver_setnvars( p->pSat, nVars + 1 ); - pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, Vec_IntEntryLast(p->vNodes)), 0 ); // F = 1 + pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1 pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit while ( 1 ) { diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 9f3617d1..29b9d8e1 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -114,6 +114,7 @@ int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj ) static inline void Sfm_NtkIncrementTravId( Sfm_Ntk_t * p ) { p->nTravIds++; } static inline void Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds ); } static inline int Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds); } +static inline int Sfm_ObjIsTravIdPrevious( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds-1); } static inline void Sfm_NtkIncrementTravId2( Sfm_Ntk_t * p ) { p->nTravIds2++; } static inline void Sfm_ObjSetTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds2, Id, p->nTravIds2 ); } @@ -136,7 +137,8 @@ int Sfm_NtkCheckOverlap_rec( Sfm_Ntk_t * p, int iThis, int iNode ) int i, iFanin; if ( Sfm_ObjIsTravIdCurrent2(p, iThis) || iThis == iNode ) return 0; - if ( Sfm_ObjIsTravIdCurrent(p, iThis) ) +// if ( Sfm_ObjIsTravIdCurrent(p, iThis) ) + if ( Sfm_ObjIsTravIdPrevious(p, iThis) ) return 1; Sfm_ObjSetTravIdCurrent2(p, iThis); Sfm_ObjForEachFanin( p, iThis, iFanin, i ) @@ -152,24 +154,44 @@ int Sfm_NtkCheckOverlap( Sfm_Ntk_t * p, int iFan, int iNode ) /**Function************************************************************* - Synopsis [Check fanouts of the node.] + Synopsis [Recursively collects roots of the window.] - Description [Returns 1 if they can be used instead of the node.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode ) +static inline int Sfm_NtkCheckRoot( Sfm_Ntk_t * p, int iNode, int nLevelMax ) { int i, iFanout; - if ( Sfm_ObjFanoutNum(p, iNode) >= p->pPars->nFanoutMax ) - return 0; + // the node is the root if one of the following is true: + // (1) the node has more than fanouts than the limit + if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax ) + return 1; + // (2) the node has CO fanouts + // (3) the node has fanouts above the cutoff level Sfm_ObjForEachFanout( p, iNode, iFanout, i ) - if ( !Sfm_NtkCheckOverlap( p, iFanout, iNode ) ) - return 0; - return 1; + if ( Sfm_ObjIsPo(p, iFanout) || Sfm_ObjLevel(p, iFanout) > nLevelMax )//|| !Sfm_NtkCheckOverlap(p, iFanout, iNode) ) + return 1; + return 0; +} +void Sfm_NtkComputeRoots_rec( Sfm_Ntk_t * p, int iNode, int nLevelMax, Vec_Int_t * vRoots, Vec_Int_t * vTfo ) +{ + int i, iFanout; + assert( Sfm_ObjIsNode(p, iNode) ); + if ( Sfm_ObjIsTravIdCurrent(p, iNode) ) + return; + Sfm_ObjSetTravIdCurrent(p, iNode); + if ( iNode != p->iPivotNode ) + Vec_IntPush( vTfo, iNode ); + // check if the node should be the root + if ( Sfm_NtkCheckRoot( p, iNode, nLevelMax ) ) + Vec_IntPush( vRoots, iNode ); + else // if not, explore its fanouts + Sfm_ObjForEachFanout( p, iNode, iFanout, i ) + Sfm_NtkComputeRoots_rec( p, iFanout, nLevelMax, vRoots, vTfo ); } /**Function************************************************************* @@ -244,7 +266,7 @@ static inline int Sfm_ObjIsUseful( Sfm_Ntk_t * p, int iNode ) SeeAlso [] ***********************************************************************/ -int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax ) +int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) { int i, iFanin; if ( Sfm_ObjIsTravIdCurrent( p, iNode ) ) @@ -252,50 +274,41 @@ int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax ) Sfm_ObjSetTravIdCurrent( p, iNode ); if ( Sfm_ObjIsPi( p, iNode ) ) { - Vec_IntPush( p->vLeaves, iNode ); + Vec_IntPush( vLeaves, iNode ); return 0; } Sfm_ObjForEachFanin( p, iNode, iFanin, i ) - if ( Sfm_NtkCollectTfi_rec( p, iFanin, nWinSizeMax ) ) + if ( Sfm_NtkCollectTfi_rec( p, iFanin, vLeaves, vNodes ) ) return 1; - Vec_IntPush( p->vNodes, iNode ); - return nWinSizeMax && (Vec_IntSize(p->vNodes) > nWinSizeMax); + Vec_IntPush( vNodes, iNode ); + return p->pPars->nWinSizeMax && (Vec_IntSize(vNodes) > p->pPars->nWinSizeMax); } int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) { int i, k, iTemp, nDivStart; - abctime clk = Abc_Clock(); + abctime clkDiv, clkWin = Abc_Clock(); + assert( Sfm_ObjIsNode( p, iNode ) ); + p->iPivotNode = iNode; Vec_IntClear( p->vLeaves ); // leaves + Vec_IntClear( p->vLeaves2 );// leaves Vec_IntClear( p->vNodes ); // internal + Vec_IntClear( p->vNodes2 ); // internal Vec_IntClear( p->vDivs ); // divisors Vec_IntClear( p->vRoots ); // roots Vec_IntClear( p->vTfo ); // roots + // collect transitive fanin Sfm_NtkIncrementTravId( p ); - if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) ) + if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vLeaves, p->vNodes ) ) { p->nMaxDivs++; - p->timeWin += Abc_Clock() - clk; + p->timeWin += Abc_Clock() - clkWin; return 0; } - // collect TFO (currently use only one level of TFO) -// if ( Sfm_NtkCheckFanouts(p, iNode) ) - if ( 0 ) - { - Sfm_ObjForEachFanout( p, iNode, iTemp, i ) - { - if ( Sfm_ObjIsPo(p, iTemp) ) - continue; - Vec_IntPush( p->vRoots, iTemp ); - Vec_IntPush( p->vTfo, iTemp ); - } - } - else - Vec_IntPush( p->vRoots, iNode ); - p->timeWin += Abc_Clock() - clk; - clk = Abc_Clock(); + // create divisors + clkDiv = Abc_Clock(); Vec_IntClear( p->vDivs ); Vec_IntForEachEntry( p->vLeaves, iTemp, i ) Vec_IntPush( p->vDivs, iTemp ); @@ -304,26 +317,26 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntPop( p->vDivs ); // add non-topological divisors nDivStart = Vec_IntSize(p->vDivs); - if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax ) + if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 ) { Sfm_NtkIncrementTravId2( p ); Vec_IntForEachEntry( p->vDivs, iTemp, i ) - if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax ) + if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 ) Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); } if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax ) + { +/* + k = 0; + Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nWinSizeMax ) + Vec_IntWriteEntry( p->vDivs, k++, iTemp ); + assert( k == p->pPars->nWinSizeMax ); +*/ Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax ); + } assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax ); - p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax); - // create ordering of the nodes - Vec_IntClear( p->vOrder ); - Vec_IntForEachEntryReverse( p->vNodes, iTemp, i ) - Vec_IntPush( p->vOrder, iTemp ); - Vec_IntForEachEntry( p->vLeaves, iTemp, i ) - Vec_IntPush( p->vOrder, iTemp ); - Vec_IntForEachEntryStart( p->vDivs, iTemp, i, nDivStart ) - Vec_IntPush( p->vOrder, iTemp ); - // remove fanins from divisors + p->nMaxDivs += (int)(Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax); + // remove node/fanins from divisors // mark fanins Sfm_NtkIncrementTravId2( p ); Sfm_ObjSetTravIdCurrent2( p, iNode ); @@ -336,9 +349,57 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntWriteEntry( p->vDivs, k++, iTemp ); Vec_IntShrink( p->vDivs, k ); assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax ); - // statistics + clkDiv = Abc_Clock() - clkDiv; + p->timeDiv += clkDiv; p->nTotalDivs += Vec_IntSize(p->vDivs); - p->timeDiv += Abc_Clock() - clk; + + // collect TFO and window roots + if ( p->pPars->nTfoLevMax > 0 && !Sfm_NtkCheckRoot(p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax) ) + { + // explore transitive fanout + Sfm_NtkIncrementTravId( p ); + Sfm_NtkComputeRoots_rec( p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax, p->vRoots, p->vTfo ); + assert( Vec_IntSize(p->vRoots) > 0 ); + assert( Vec_IntSize(p->vTfo) > 0 ); + // compute new leaves and nodes + Sfm_NtkIncrementTravId( p ); + Vec_IntForEachEntry( p->vRoots, iTemp, i ) + if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vLeaves2, p->vNodes2 ) ) + break; + if ( i == Vec_IntSize(p->vRoots) ) + { +// printf( "%d -> %d %d -> %d\n", Vec_IntSize(p->vLeaves), Vec_IntSize(p->vLeaves2), Vec_IntSize(p->vNodes), Vec_IntSize(p->vNodes2) ); + // swap leaves and nodes + ABC_SWAP( Vec_Int_t *, p->vLeaves, p->vLeaves2 ); + ABC_SWAP( Vec_Int_t *, p->vNodes, p->vNodes2 ); + } + else + { + Vec_IntClear( p->vRoots ); + Vec_IntClear( p->vTfo ); + } +// printf( "Roots = %d. TFO = %d.\n", Vec_IntSize(p->vRoots), Vec_IntSize(p->vTfo) ); + } + + // create ordering of the nodes, leaves and divisors that are not among nodes/leaves + Vec_IntClear( p->vOrder ); + Sfm_NtkIncrementTravId2( p ); + Vec_IntForEachEntryReverse( p->vNodes, iTemp, i ) + { + Sfm_ObjSetTravIdCurrent2( p, iTemp ); + Vec_IntPush( p->vOrder, iTemp ); + } + Vec_IntForEachEntry( p->vLeaves, iTemp, i ) + { + Sfm_ObjSetTravIdCurrent2( p, iTemp ); + Vec_IntPush( p->vOrder, iTemp ); + } + Vec_IntForEachEntry( p->vDivs, iTemp, i ) + if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) ) + Vec_IntPush( p->vOrder, iTemp ); + + // statistics + p->timeWin += Abc_Clock() - clkWin - clkDiv; if ( !fVerbose ) return 1; -- cgit v1.2.3