diff options
| -rw-r--r-- | src/aig/gia/giaDup.c | 255 | ||||
| -rw-r--r-- | src/base/abci/abcCollapse.c | 228 |
2 files changed, 483 insertions, 0 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ff57fedb..ffb3e74d 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/tim/tim.h" +#include "misc/vec/vecWec.h" ABC_NAMESPACE_IMPL_START @@ -3236,6 +3237,260 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Computes supports for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int i, Id; + Vec_Wec_t * vSuppsCo = Vec_WecStart( Gia_ManCoNum(p) ); + Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntPush( Vec_WecEntry(vSupps, Id), i ); + Gia_ManForEachAnd( p, pObj, Id ) + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), + Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), + Vec_WecEntry(vSupps, Id) ); + Gia_ManForEachCo( p, pObj, i ) + Vec_IntAppend( Vec_WecEntry(vSuppsCo, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) ); + Vec_WecFree( vSupps ); + if ( fVerbose ) + Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); + return vSuppsCo; +} +int Gia_ManCoSuppSizeMax( Gia_Man_t * p, Vec_Wec_t * vSupps ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vSuppOne; + int i, nSuppMax = 1; + Gia_ManForEachCo( p, pObj, i ) + { + vSuppOne = Vec_WecEntry( vSupps, i ); + nSuppMax = Abc_MaxInt( nSuppMax, Vec_IntSize(vSuppOne) ); + } + return nSuppMax; +} +int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vSuppOne; + int i, iCoMax = -1, nSuppMax = -1; + Gia_ManForEachCo( p, pObj, i ) + { + vSuppOne = Vec_WecEntry( vSupps, i ); + if ( nSuppMax < Vec_IntSize(vSuppOne) ) + { + nSuppMax = Vec_IntSize(vSuppOne); + iCoMax = i; + } + } + return iCoMax; +} +Vec_Int_t * Gia_ManSortCoBySuppSize( Gia_Man_t * p, Vec_Wec_t * vSupps ) +{ + Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManCoNum(p) ); + Vec_Wrd_t * vSortData = Vec_WrdAlloc( Gia_ManCoNum(p) ); + Vec_Int_t * vSuppOne; word Entry; int i; + Vec_WecForEachLevel( vSupps, vSuppOne, i ) + Vec_WrdPush( vSortData, ((word)i << 32) | Vec_IntSize(vSuppOne) ); + Abc_QuickSort3( Vec_WrdArray(vSortData), Vec_WrdSize(vSortData), 1 ); + Vec_WrdForEachEntry( vSortData, Entry, i ) + Vec_IntPush( vOrder, (int)(Entry >> 32) ); + Vec_WrdFree( vSortData ); + return vOrder; +} + +/**Function************************************************************* + + Synopsis [Remaps each CO cone to depend on the first CI variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManDupHashDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +void Gia_ManDupCleanDfs_rec( Gia_Obj_t * pObj ) +{ + if ( !~pObj->Value ) + return; + pObj->Value = ~0; + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) ); + Gia_ManDupCleanDfs_rec( Gia_ObjFanin1(pObj) ); +} +Gia_Man_t * Gia_ManDupStrashReduce( Gia_Man_t * p, Vec_Wec_t * vSupps, Vec_Int_t ** pvCoMap ) +{ + Gia_Obj_t * pObj; + Gia_Man_t * pNew, * pTemp; + Vec_Int_t * vSuppOne, * vCoMapLit; + int i, k, iCi, iLit, nSuppMax; + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManFillValue( p ); + vCoMapLit = Vec_IntAlloc( Gia_ManCoNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps ); + for ( i = 0; i < nSuppMax; i++ ) + Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + { + vSuppOne = Vec_WecEntry( vSupps, i ); + if ( Vec_IntSize(vSuppOne) == 0 ) + Vec_IntPush( vCoMapLit, Abc_Var2Lit(0, Gia_ObjFaninC0(pObj)) ); + else if ( Vec_IntSize(vSuppOne) == 1 ) + Vec_IntPush( vCoMapLit, Abc_Var2Lit(1, Gia_ObjFaninC0(pObj)) ); + else + { + Vec_IntForEachEntry( vSuppOne, iCi, k ) + Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) ); + Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + assert( Gia_ObjFanin0Copy(pObj) < 2 * Gia_ManObjNum(pNew) ); + Vec_IntPush( vCoMapLit, Gia_ObjFanin0Copy(pObj) ); + Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) ); + } + } + Gia_ManHashStop( pNew ); + assert( Vec_IntSize(vCoMapLit) == Gia_ManCoNum(p) ); + if ( pvCoMap == NULL ) // do not remap + { + Vec_IntForEachEntry( vCoMapLit, iLit, i ) + Gia_ManAppendCo( pNew, iLit ); + } + else // remap + { + Vec_Int_t * vCoMapRes = Vec_IntAlloc( Gia_ManCoNum(p) ); // map old CO into new CO + Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(pNew) ); // map new lit into new CO + Vec_IntForEachEntry( vCoMapLit, iLit, i ) + { + if ( Vec_IntEntry(vMap, iLit) == -1 ) + { + Vec_IntWriteEntry( vMap, iLit, Gia_ManCoNum(pNew) ); + Gia_ManAppendCo( pNew, iLit ); + } + Vec_IntPush( vCoMapRes, Vec_IntEntry(vMap, iLit) ); + } + Vec_IntFree( vMap ); + *pvCoMap = vCoMapRes; + } + Vec_IntFree( vCoMapLit ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Gia_Man_t * Gia_ManIsoStrashReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) +{ + Vec_Int_t * vCoMap; + Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose ); + Gia_Man_t * pNew = Gia_ManDupStrashReduce( p, vSupps, &vCoMap ); + Vec_IntFree( vCoMap ); + Vec_WecFree( vSupps ); + *pvPosEquivs = NULL; + return pNew; +} + +int Gia_ManIsoStrashReduceOne( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) +{ + int k, iCi, iLit; + assert( Gia_ObjIsCo(pObj) ); + if ( Vec_IntSize(vSupp) == 0 ) + return Abc_Var2Lit(0, Gia_ObjFaninC0(pObj)); + if ( Vec_IntSize(vSupp) == 1 ) + return Abc_Var2Lit(1, Gia_ObjFaninC0(pObj)); + Vec_IntForEachEntry( vSupp, iCi, k ) + Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) ); + Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + iLit = Gia_ObjFanin0Copy(pObj); + Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) ); + return iLit; +} +Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 ); + Vec_Int_t * vSuppOne, * vMap = Vec_IntAlloc( 10000 ); + int i, iLit, nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps ); + // count how many times each support size appears + Vec_Int_t * vSizeCount = Vec_IntStart( nSuppMax + 1 ); + Vec_WecForEachLevel( vSupps, vSuppOne, i ) + Vec_IntAddToEntry( vSizeCount, Vec_IntSize(vSuppOne), 1 ); + // create array of unique outputs + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < nSuppMax; i++ ) + Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + { + vSuppOne = Vec_WecEntry( vSupps, i ); + if ( Vec_IntEntry(vSizeCount, Vec_IntSize(vSuppOne)) == 1 ) + { + Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i ); + continue; + } + iLit = Gia_ManIsoStrashReduceOne( pNew, p, pObj, vSuppOne ); + Vec_IntFillExtra( vMap, iLit + 1, -1 ); + if ( Vec_IntEntry(vMap, iLit) == -1 ) + { + Vec_IntWriteEntry( vMap, iLit, Vec_WecSize(vPosEquivs) ); + Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i ); + continue; + } + Vec_IntPush( Vec_WecEntry(vPosEquivs, Vec_IntEntry(vMap, iLit)), i ); + } + Gia_ManHashStop( pNew ); + Gia_ManStop( pNew ); + Vec_IntFree( vSizeCount ); + Vec_IntFree( vMap ); + return vPosEquivs; +} +Gia_Man_t * Gia_ManIsoStrashReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) +{ + Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose ); + Vec_Wec_t * vPosEquivs = Gia_ManIsoStrashReduceInt( p, vSupps, fVerbose ); + // find the first outputs and derive GIA + Vec_Int_t * vFirsts = Vec_WecCollectFirsts( vPosEquivs ); + Gia_Man_t * pNew = Gia_ManDupCones( p, Vec_IntArray(vFirsts), Vec_IntSize(vFirsts), 0 ); + Vec_IntFree( vFirsts ); + Vec_WecFree( vSupps ); + // report and return + if ( fVerbose ) + { + printf( "Nontrivial classes:\n" ); + Vec_WecPrint( vPosEquivs, 1 ); + } + if ( pvPosEquivs ) + *pvPosEquivs = Vec_WecConvertToVecPtr( vPosEquivs ); + Vec_WecFree( vPosEquivs ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 804b0bd3..d1e6be2f 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -242,6 +242,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i #endif +#if 0 /**Function************************************************************* @@ -526,6 +527,233 @@ Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in return pNtkNew; } +#endif + + + +extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ); +extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps ); +extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose ); + +/**Function************************************************************* + + Synopsis [Derives GIA for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClpGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) +{ + int iLit0, iLit1; + if ( pNode->iTemp >= 0 ) + return pNode->iTemp; + assert( Abc_ObjIsNode( pNode ) ); + iLit0 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit1 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin1(pNode) ); + iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); + iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); + return (pNode->iTemp = Gia_ManAppendAnd(pNew, iLit0, iLit1)); +} +Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ) +{ + int i, iLit; + Gia_Man_t * pNew; + Abc_Obj_t * pNode; + assert( Abc_NtkIsStrash(pNtk) ); + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pNtk->pName ); + pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->iTemp = -1; + Abc_AigConst1(pNtk)->iTemp = 1; + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->iTemp = Gia_ManAppendCi(pNew); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + iLit = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) ); + Gia_ManAppendCo( pNew, iLit ); + } + return pNew; +} + +/**Function************************************************************* + + Synopsis [Computes SOPs for each output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp ) +{ + Vec_Str_t * vSop; + abctime clk = Abc_Clock(); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 ); + if ( fVerbose ) + printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); + vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + Gia_ManStop( pGia ); + if ( vSop == NULL ) + return NULL; + if ( Vec_StrSize(vSop) == 4 ) // constant + Vec_IntClear(vSupp); + if ( fVerbose ) + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return vSop; +} +Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) +{ + ProgressBar * pProgress; + Vec_Ptr_t * vSops = NULL, * vSopsRepr; + Vec_Int_t * vReprs, * vClass, * vReprSuppSizes; + int i, k, Entry, iCo, * pOrder; + Vec_Wec_t * vClasses; + // check the largest output + if ( nCubeLim > 0 && nCostMax > 0 ) + { + int iCoMax = Gia_ManCoLargestSupp( p, vSupps ); + int iObjMax = Gia_ObjId( p, Gia_ManCo(p, iCoMax) ); + int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) ); + int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 ); + word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim; + if ( Cost > (word)nCostMax ) + { + printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", + nNodeMax, nSuppMax, nCubeLim, nCostMax ); + return NULL; + } + } + // derive classes of outputs + vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 ); + // derive representatives + vReprs = Vec_WecCollectFirsts( vClasses ); + vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) ); + Vec_IntForEachEntry( vReprs, Entry, i ) + Vec_IntPush( vReprSuppSizes, Vec_IntSize(Vec_WecEntry(vSupps, Entry)) ); + pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) ); + Vec_IntFree( vReprSuppSizes ); + // consider SOPs for representatives + vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) ); + pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) ); + Extra_ProgressBarUpdate( pProgress, 0, NULL ); + for ( i = 0; i < Vec_IntSize(vReprs); i++ ) + { + int iEntry = pOrder[Vec_IntSize(vReprs) - 1 - i]; + int iCoThis = Vec_IntEntry( vReprs, iEntry ); + Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis ); + Vec_Str_t * vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp ); + if ( vSop == NULL ) + goto finish; + assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) ); + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Vec_PtrWriteEntry( vSopsRepr, iEntry, Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ) ); + Vec_StrFree( vSop ); + } + Extra_ProgressBarStop( pProgress ); + // derive SOPs for each output + vSops = Vec_PtrStart( Gia_ManCoNum(p) ); + Vec_WecForEachLevel ( vClasses, vClass, i ) + Vec_IntForEachEntry( vClass, iCo, k ) + Vec_PtrWriteEntry( vSops, iCo, Vec_PtrEntry(vSopsRepr, i) ); + assert( Vec_PtrCountZero(vSops) == 0 ); +/* + // verify + for ( i = 0; i < Gia_ManCoNum(p); i++ ) + { + Vec_Int_t * vSupp = Vec_WecEntry( vSupps, i ); + char * pSop = (char *)Vec_PtrEntry( vSops, i ); + assert( Vec_IntSize(vSupp) == Abc_SopGetVarNum(pSop) ); + } +*/ + // cleanup +finish: + ABC_FREE( pOrder ); + Vec_IntFree( vReprs ); + Vec_WecFree( vClasses ); + Vec_PtrFree( vSopsRepr ); + return vSops; +} +Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + Gia_Man_t * pGia; + Vec_Wec_t * vSupps; + Vec_Int_t * vSupp; + Vec_Ptr_t * vSops; + Abc_Obj_t * pNode, * pNodeNew, * pDriver; + int i, k, iCi; + pGia = Abc_NtkClpGia( pNtk ); + vSupps = Gia_ManCreateCoSupps( pGia, fVerbose ); + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); + Gia_ManStop( pGia ); + if ( vSops == NULL ) + { + Vec_WecFree( vSupps ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pDriver = Abc_ObjFanin0(pNode); + if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) ) + { + Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy ); + continue; + } + if ( Abc_ObjIsCi(pDriver) ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + continue; + } + if ( pDriver == Abc_AigConst1(pNtk) ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + continue; + } + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + vSupp = Vec_WecEntry( vSupps, i ); + Vec_IntForEachEntry( vSupp, iCi, k ) + Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); + pNodeNew->pData = Vec_PtrEntry( vSops, i ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + Vec_WecFree( vSupps ); + Vec_PtrFree( vSops ); + return pNtkNew; +} +Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + assert( Abc_NtkIsStrash(pNtk) ); + pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); + if ( pNtkNew == NULL ) + return NULL; + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkCollapseSat: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |