diff options
Diffstat (limited to 'src/opt/mfs')
-rw-r--r-- | src/opt/mfs/mfs.h | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsCore.c | 20 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 8 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 17 | ||||
-rw-r--r-- | src/opt/mfs/mfsResub.c | 307 |
5 files changed, 300 insertions, 54 deletions
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 9fc6a253..cb2da431 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -49,6 +49,8 @@ struct Mfs_Par_t_ int nGrowthLevel; // the maximum allowed growth in level int fResub; // performs resubstitution int fArea; // performs optimization for area + int fMoreEffort; // performs high-affort minimization + int fSwapEdge; // performs edge swapping int fDelay; // performs optimization for delay int fVerbose; // enable basic stats int fVeryVerbose; // enable detailed stats diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 332a6ad9..aed0abe5 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -74,10 +74,14 @@ clk = clock(); return 1; } // solve the SAT problem - if ( p->pPars->fArea ) - Abc_NtkMfsResubArea( p, pNode ); + if ( p->pPars->fSwapEdge ) + Abc_NtkMfsEdgeSwapEval( p, pNode ); else - Abc_NtkMfsResubEdge( p, pNode ); + { + Abc_NtkMfsResubNode( p, pNode ); + if ( p->pPars->fMoreEffort ) + Abc_NtkMfsResubNode2( p, pNode ); + } p->timeSat += clock() - clk; return 1; } @@ -140,12 +144,13 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; - int i, clk = clock(); + int i, nFaninMax, clk = clock(); int nTotalNodesBeg = Abc_NtkNodeNum(pNtk); int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); assert( Abc_NtkIsLogic(pNtk) ); - if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX ) + nFaninMax = Abc_NtkGetFaninMax(pNtk); + if ( nFaninMax > MFS_FANIN_MAX ) { printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX ); return 1; @@ -162,7 +167,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) // start the manager p = Mfs_ManAlloc( pPars ); - p->pNtk = pNtk; + p->pNtk = pNtk; + p->nFaninMax = nFaninMax; if ( pNtk->pExcare ) { Abc_Ntk_t * pTemp; @@ -170,7 +176,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) p->pCare = Abc_NtkToDar( pTemp, 0 ); Abc_NtkDelete( pTemp ); } - if ( pPars->fVerbose ) +// if ( pPars->fVerbose ) { if ( p->pCare != NULL ) printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) ); diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 54826bc1..ddd16407 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -49,6 +49,7 @@ struct Mfs_Man_t_ Mfs_Par_t * pPars; Abc_Ntk_t * pNtk; Aig_Man_t * pCare; + int nFaninMax; // intermeditate data for the node Vec_Ptr_t * vRoots; // the roots of the window Vec_Ptr_t * vSupp; // the support of the window @@ -78,7 +79,6 @@ struct Mfs_Man_t_ // performance statistics int nNodesTried; int nNodesResub; - int nNodesGained; int nMintsCare; int nMintsTotal; int nNodesBad; @@ -119,8 +119,10 @@ extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ); extern void Mfs_ManStop( Mfs_Man_t * p ); extern void Mfs_ManClean( Mfs_Man_t * p ); /*=== mfsResub.c ==========================================================*/ -extern int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ); -extern int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p ); +extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsSat.c ==========================================================*/ extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 67981d5a..519b855d 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -85,12 +85,12 @@ void Mfs_ManClean( Mfs_Man_t * p ) if ( p->vDivs ) Vec_PtrFree( p->vDivs ); p->pAigWin = NULL; - p->pCnf = NULL; - p->pSat = NULL; - p->vRoots = NULL; - p->vSupp = NULL; - p->vNodes = NULL; - p->vDivs = NULL; + p->pCnf = NULL; + p->pSat = NULL; + p->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; + p->vDivs = NULL; } /**Function************************************************************* @@ -117,6 +117,11 @@ void Mfs_ManPrint( Mfs_Man_t * p ) printf( "\n" ); printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls ); + if ( p->pPars->fSwapEdge ) + printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", + p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); + else + Abc_NtkMfsPrintResubStats( p ); } else { diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index ae1132f2..1e9da4d2 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -57,6 +57,35 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani /**Function************************************************************* + Synopsis [Prints resub candidate stats.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p ) +{ + Abc_Obj_t * pFanin, * pNode; + int i, k, nAreaCrits = 0, nAreaExpanse = 0; + int nFaninMax = Abc_NtkGetFaninMax(p->pNtk); + Abc_NtkForEachNode( p->pNtk, pNode, i ) + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + nAreaCrits++; + nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax); + } + } + printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", + nAreaCrits, nAreaExpanse ); +} + +/**Function************************************************************* + Synopsis [Tries resubstitution.] Description [Returns 1 if it is feasible, or 0 if c-ex is found.] @@ -68,7 +97,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani ***********************************************************************/ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) { - unsigned * pData, * pDataTot; + unsigned * pData; int RetValue, iVar, i; p->nSatCalls++; RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); @@ -77,17 +106,16 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) return 1; p->nSatCexes++; // store the counter-example - pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ ); - assert( pData[0] == 0 ); Vec_IntForEachEntry( p->vProjVars, iVar, i ) { - if ( sat_solver_var_value( p->pSat, iVar ) ) - Aig_InfoSetBit( pData, i ); + pData = Vec_PtrEntry( p->vDivCexes, i ); + if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! + { + assert( Aig_InfoHasBit(pData, p->nCexes) ); + Aig_InfoXorBit( pData, p->nCexes ); + } } - // AND the result with the previous ones - pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); - for ( i = 0; i < p->nDivWords; i++ ) - pDataTot[i] &= pData[i]; + p->nCexes++; return 0; } @@ -102,22 +130,19 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove ) +int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate ) { int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; unsigned * pData; int pCands[MFS_FANIN_MAX]; - int iVar, i, nCands, clk; + int iVar, i, nCands, nWords, w, clk; Abc_Obj_t * pFanin; Hop_Obj_t * pFunc; assert( iFanin >= 0 ); // clean simulation info - Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords ); - pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); - memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords ); + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); p->nCexes = 0; - if ( fVeryVerbose ) { printf( "\n" ); @@ -143,7 +168,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); p->nNodesResub++; -// p->nNodesGained += Abc_NodeMffcLabel(pNode); + if ( fSkipUpdate ) + return 1; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); @@ -156,11 +182,6 @@ p->timeInt += clock() - clk; if ( fOnlyRemove ) return 0; - // shift variables by 1 - for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) - p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; - p->vFanins->nSize++; - if ( fVeryVerbose ) { for ( i = 0; i < 8; i++ ) @@ -180,37 +201,52 @@ p->timeInt += clock() - clk; if ( fVeryVerbose ) { printf( "%3d: %2d ", p->nCexes, iVar ); - pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 ); -// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) ); for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) - printf( "%d", Aig_InfoHasBit(pData, i) ); + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } printf( "\n" ); } // find the next divisor to try - pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) ); + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) - if ( Aig_InfoHasBit( pData, iVar ) ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( w = 0; w < nWords; w++ ) + if ( pData[w] != ~0 ) + break; + if ( w == nWords ) break; + } if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) return 0; + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) ) { if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); p->nNodesResub++; -// p->nNodesGained += Abc_NodeMffcLabel(pNode); + if ( fSkipUpdate ) + return 1; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); - // update the network -// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) ); + // update the network Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); p->timeInt += clock() - clk; return 1; } + if ( p->nCexes >= p->pPars->nDivMax ) + break; } return 0; } @@ -226,16 +262,155 @@ p->timeInt += clock() - clk; SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 ) { + int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; + unsigned * pData, * pData2; + int pCands[MFS_FANIN_MAX]; + int iVar, iVar2, i, w, nCands, clk, nWords, fBreak; Abc_Obj_t * pFanin; - int i; + Hop_Obj_t * pFunc; + assert( iFanin >= 0 ); + assert( iFanin2 >= 0 || iFanin2 == -1 ); + + // clean simulation info + Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); + p->nCexes = 0; + if ( fVeryVerbose ) + { + printf( "\n" ); + printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n", + pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), + iFanin, iFanin2, Abc_ObjFaninNum(pNode), + Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 ); + } + + // try fanins without the critical fanin + nCands = 0; + Vec_PtrClear( p->vFanins ); Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( i == iFanin || i == iFanin2 ) + continue; + Vec_PtrPush( p->vFanins, pFanin ); + iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + } + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); + p->nNodesResub++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; + } + + if ( fVeryVerbose ) + { + for ( i = 0; i < 11; i++ ) + printf( " " ); + for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ ) + printf( "%d", i % 10 ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + if ( i == iFanin || i == iFanin2 ) + printf( "*" ); + else + printf( "%c", 'a' + i ); + printf( "\n" ); + } + iVar = iVar2 = -1; + while ( 1 ) + { + if ( fVeryVerbose ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) - return 1; + printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 ); + for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, i ); + printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + } + printf( "\n" ); + } + + // find the next divisor to try + nWords = Aig_BitWordNum(p->nCexes); + assert( nWords <= p->nDivWords ); + fBreak = 0; + for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) + { + pData = Vec_PtrEntry( p->vDivCexes, iVar ); + for ( iVar2 = 0; iVar2 < iVar; iVar2++ ) + { + pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 ); + for ( w = 0; w < nWords; w++ ) + if ( (pData[w] | pData2[w]) != ~0 ) + break; + if ( w == nWords ) + { + fBreak = 1; + break; + } + } + if ( fBreak ) + break; + } + if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) ) + return 0; + + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) ) + { + if ( fVeryVerbose ) + printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); + p->nNodesResub++; +clk = clock(); + // derive the function + pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; + // shift fanins by 1 + for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- ) + p->vFanins->pArray[i] = p->vFanins->pArray[i-1]; + p->vFanins->nSize++; + Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) ); + Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) ); + // update the network + Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); +p->timeInt += clock() - clk; + return 1; } + if ( p->nCexes >= p->pPars->nDivMax ) + break; + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the possibility of replacing given edge by another edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + int i; + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 ); return 0; } @@ -250,25 +425,81 @@ int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Abc_Obj_t * pFanin; int i; + // try replacing area critical fanins Abc_ObjForEachFanin( pNode, pFanin, i ) if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) ) + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) return 1; } + // try removing redundant edges + if ( !p->pPars->fArea ) + { + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) ) + return 1; + } + } + if ( Abc_ObjFaninNum(pNode) == p->nFaninMax ) + return 0; + // try replacing area critical fanins while adding two new fanins Abc_ObjForEachFanin( pNode, pFanin, i ) - if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) { - if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) ) + if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) ) return 1; } return 0; } +/**Function************************************************************* + + Synopsis [Performs resubstitution for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin, * pFanin2; + int i, k; +/* + Abc_ObjForEachFanin( pNode, pFanin, i ) + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) ) + return 1; + } +*/ + if ( Abc_ObjFaninNum(pNode) < 2 ) + return 0; + // try replacing one area critical fanin and one other fanin while adding two new fanins + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 ) + { + // consider second fanin to remove at the same time + Abc_ObjForEachFanin( pNode, pFanin2, k ) + { + if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) ) + return 1; + } + } + } + return 0; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |