| /**CFile**************************************************************** |
| |
| FileName [abcCollapse.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Collapsing the network into two-levels.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "aig/gia/gia.h" |
| #include "misc/vec/vecWec.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satStore.h" |
| |
| #ifdef ABC_USE_CUDD |
| #include "bdd/extrab/extraBdd.h" |
| #endif |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #ifdef ABC_USE_CUDD |
| |
| extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Makes nodes minimum base.] |
| |
| Description [Returns the number of changed nodes.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NodeMinimumBase2( Abc_Obj_t * pNode ) |
| { |
| Vec_Str_t * vSupport; |
| Vec_Ptr_t * vFanins; |
| DdNode * bTemp; |
| int i, nVars; |
| |
| assert( Abc_NtkIsBddLogic(pNode->pNtk) ); |
| assert( Abc_ObjIsNode(pNode) ); |
| |
| // compute support |
| vSupport = Vec_StrAlloc( 10 ); |
| nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) ); |
| if ( nVars == Abc_ObjFaninNum(pNode) ) |
| { |
| Vec_StrFree( vSupport ); |
| return 0; |
| } |
| |
| // add fanins |
| vFanins = Vec_PtrAlloc( Abc_ObjFaninNum(pNode) ); |
| Abc_NodeCollectFanins( pNode, vFanins ); |
| Vec_IntClear( &pNode->vFanins ); |
| for ( i = 0; i < vFanins->nSize; i++ ) |
| if ( vSupport->pArray[i] != 0 ) // useful |
| Vec_IntPush( &pNode->vFanins, Abc_ObjId((Abc_Obj_t *)vFanins->pArray[i]) ); |
| assert( nVars == Abc_ObjFaninNum(pNode) ); |
| |
| // update the function of the node |
| pNode->pData = Extra_bddRemapUp( (DdManager *)pNode->pNtk->pManFunc, bTemp = (DdNode *)pNode->pData ); Cudd_Ref( (DdNode *)pNode->pData ); |
| Cudd_RecursiveDeref( (DdManager *)pNode->pNtk->pManFunc, bTemp ); |
| Vec_PtrFree( vFanins ); |
| Vec_StrFree( vSupport ); |
| return 1; |
| } |
| int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk ) |
| { |
| Abc_Obj_t * pNode, * pFanin; |
| int i, k, Counter; |
| assert( Abc_NtkIsBddLogic(pNtk) ); |
| // remove all fanouts |
| Abc_NtkForEachObj( pNtk, pNode, i ) |
| Vec_IntClear( &pNode->vFanouts ); |
| // add useful fanins |
| Counter = 0; |
| Abc_NtkForEachNode( pNtk, pNode, i ) |
| Counter += Abc_NodeMinimumBase2( pNode ); |
| // add fanouts |
| Abc_NtkForEachObj( pNtk, pNode, i ) |
| Abc_ObjForEachFanin( pNode, pFanin, k ) |
| Vec_IntPush( &pFanin->vFanouts, Abc_ObjId(pNode) ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collapses the network.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) |
| { |
| Abc_Obj_t * pNodeNew, * pTemp; |
| int i; |
| // create a new node |
| pNodeNew = Abc_NtkCreateNode( pNtkNew ); |
| // add the fanins in the order, in which they appear in the reordered manager |
| Abc_NtkForEachCi( pNtkNew, pTemp, i ) |
| Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) ); |
| // transfer the function |
| pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData ); |
| return pNodeNew; |
| } |
| Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) |
| { |
| ProgressBar * pProgress; |
| Abc_Ntk_t * pNtkNew; |
| Abc_Obj_t * pNode, * pDriver, * pNodeNew; |
| DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); |
| int i; |
| |
| // extract don't-care and compute ISOP |
| if ( pNtk->pExdc ) |
| { |
| DdManager * ddExdc = NULL; |
| DdNode * bBddMin, * bBddDc, * bBddL, * bBddU; |
| assert( Abc_NtkIsStrash(pNtk->pExdc) ); |
| assert( Abc_NtkCoNum(pNtk->pExdc) == 1 ); |
| // compute the global BDDs |
| if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0) == NULL ) |
| return NULL; |
| // transfer tot the same manager |
| ddExdc = (DdManager *)Abc_NtkGlobalBddMan( pNtk->pExdc ); |
| bBddDc = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkCo(pNtk->pExdc, 0)); |
| bBddDc = Cudd_bddTransfer( ddExdc, dd, bBddDc ); Cudd_Ref( bBddDc ); |
| Abc_NtkFreeGlobalBdds( pNtk->pExdc, 1 ); |
| // minimize the output |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| { |
| bBddMin = (DdNode *)Abc_ObjGlobalBdd(pNode); |
| // derive lower and uppwer bound |
| bBddL = Cudd_bddAnd( dd, bBddMin, Cudd_Not(bBddDc) ); Cudd_Ref( bBddL ); |
| bBddU = Cudd_bddAnd( dd, Cudd_Not(bBddMin), Cudd_Not(bBddDc) ); Cudd_Ref( bBddU ); |
| Cudd_RecursiveDeref( dd, bBddMin ); |
| // compute new one |
| bBddMin = Cudd_bddIsop( dd, bBddL, Cudd_Not(bBddU) ); Cudd_Ref( bBddMin ); |
| Cudd_RecursiveDeref( dd, bBddL ); |
| Cudd_RecursiveDeref( dd, bBddU ); |
| // update global BDD |
| Abc_ObjSetGlobalBdd( pNode, bBddMin ); |
| //Extra_bddPrint( dd, bBddMin ); printf( "\n" ); |
| } |
| Cudd_RecursiveDeref( dd, bBddDc ); |
| } |
| |
| // start the new network |
| pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); |
| // make sure the new manager has the same number of inputs |
| Cudd_bddIthVar( (DdManager *)pNtkNew->pManFunc, dd->size-1 ); |
| // process the POs |
| pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| { |
| Extra_ProgressBarUpdate( pProgress, i, NULL ); |
| pDriver = Abc_ObjFanin0(pNode); |
| if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) ) |
| { |
| Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy ); |
| continue; |
| } |
| pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) ); |
| Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); |
| |
| } |
| Extra_ProgressBarStop( pProgress ); |
| return pNtkNew; |
| } |
| Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkNew; |
| abctime clk = Abc_Clock(); |
| |
| assert( Abc_NtkIsStrash(pNtk) ); |
| // compute the global BDDs |
| if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL ) |
| return NULL; |
| if ( fVerbose ) |
| { |
| DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); |
| printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); |
| ABC_PRT( "BDD construction time", Abc_Clock() - clk ); |
| } |
| |
| // create the new network |
| pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); |
| Abc_NtkFreeGlobalBdds( pNtk, 1 ); |
| if ( pNtkNew == NULL ) |
| return NULL; |
| |
| // make the network minimum base |
| Abc_NtkMinimumBase2( pNtkNew ); |
| |
| if ( pNtk->pExdc ) |
| pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); |
| |
| // make sure that everything is okay |
| if ( !Abc_NtkCheck( pNtkNew ) ) |
| { |
| printf( "Abc_NtkCollapse: The network check has failed.\n" ); |
| Abc_NtkDelete( pNtkNew ); |
| return NULL; |
| } |
| return pNtkNew; |
| } |
| |
| |
| #else |
| |
| Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) |
| { |
| return NULL; |
| } |
| |
| #endif |
| |
| |
| #if 0 |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives GIA for the cone of one output and computes its SOP.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) |
| { |
| int iLit0, iLit1; |
| if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) ) |
| return pNode->iTemp; |
| assert( Abc_ObjIsNode( pNode ) ); |
| Abc_NodeSetTravIdCurrent( pNode ); |
| iLit0 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); |
| iLit1 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin1(pNode) ); |
| iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); |
| iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); |
| return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1)); |
| } |
| Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp ) |
| { |
| int i, iCi, iLit; |
| Abc_Obj_t * pNode; |
| Gia_Man_t * pNew, * pTemp; |
| pNew = Gia_ManStart( 1000 ); |
| pNew->pName = Abc_UtilStrsav( pNtk->pName ); |
| pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); |
| Gia_ManHashStart( pNew ); |
| // primary inputs |
| Abc_AigConst1(pNtk)->iTemp = 1; |
| Vec_IntForEachEntry( vSupp, iCi, i ) |
| Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManAppendCi(pNew); |
| // create the first cone |
| Abc_NtkIncrementTravId( pNtk ); |
| pNode = Abc_NtkCo( pNtk, iCo ); |
| iLit = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); |
| iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) ); |
| Gia_ManAppendCo( pNew, iLit ); |
| // perform cleanup |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, 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 = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); |
| 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; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Collect structural support for all nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Wec_t * Abc_NtkCreateCoSupps( Abc_Ntk_t * pNtk, int fVerbose ) |
| { |
| abctime clk = Abc_Clock(); |
| Abc_Obj_t * pNode; int i; |
| Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) ); |
| Abc_NtkForEachCi( pNtk, pNode, i ) |
| Vec_IntPush( Vec_WecEntry(vSupps, pNode->Id), i ); |
| Abc_NtkForEachNode( pNtk, pNode, i ) |
| Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), |
| Vec_WecEntry(vSupps, Abc_ObjFanin1(pNode)->Id), |
| Vec_WecEntry(vSupps, pNode->Id) ); |
| if ( fVerbose ) |
| Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); |
| return vSupps; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derive array of COs sorted by cone size in the reverse order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NodeCompareByTemp( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) |
| { |
| int Diff = (*pp2)->iTemp - (*pp1)->iTemp; |
| if ( Diff < 0 ) |
| return -1; |
| if ( Diff > 0 ) |
| return 1; |
| Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) ); |
| if ( Diff < 0 ) |
| return -1; |
| if ( Diff > 0 ) |
| return 1; |
| return 0; |
| } |
| Vec_Ptr_t * Abc_NtkCreateCoOrder( Abc_Ntk_t * pNtk, Vec_Wec_t * vSupps ) |
| { |
| Abc_Obj_t * pNode; int i; |
| Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| { |
| pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFaninId0(pNode)) ); |
| Vec_PtrPush( vNodes, pNode ); |
| } |
| // order objects alphabetically |
| qsort( (void *)Vec_PtrArray(vNodes), Vec_PtrSize(vNodes), sizeof(Abc_Obj_t *), |
| (int (*)(const void *, const void *)) Abc_NodeCompareByTemp ); |
| // cleanup |
| // Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) |
| // printf( "%s %d ", Abc_ObjName(pNode), pNode->iTemp ); |
| // printf( "\n" ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [SAT-based collapsing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) |
| { |
| Abc_Obj_t * pNodeNew; |
| Vec_Str_t * vSop; |
| int i, iCi; |
| // compute SOP of the node |
| vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, vSupp ); |
| if ( vSop == NULL ) |
| return NULL; |
| // create a new node |
| pNodeNew = Abc_NtkCreateNode( pNtkNew ); |
| // add fanins |
| if ( Vec_StrSize(vSop) > 4 ) // non-constant SOP |
| Vec_IntForEachEntry( vSupp, iCi, i ) |
| Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); |
| // transfer the function |
| pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ); |
| Vec_StrFree( vSop ); |
| return pNodeNew; |
| } |
| Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) |
| { |
| ProgressBar * pProgress; |
| Abc_Ntk_t * pNtkNew; |
| Abc_Obj_t * pNode, * pDriver, * pNodeNew; |
| Vec_Ptr_t * vDriverCopy, * vCoNodes, * vDfsNodes; |
| Vec_Int_t * vNodeCoIds, * vLevel; |
| Vec_Wec_t * vSupps; |
| int i; |
| |
| // Abc_NtkForEachCi( pNtk, pNode, i ) |
| // printf( "%d ", Abc_ObjFanoutNum(pNode) ); |
| // printf( "\n" ); |
| |
| // compute structural supports |
| vSupps = Abc_NtkCreateCoSupps( pNtk, fVerbose ); |
| // order CO nodes by support size |
| vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps ); |
| // compute cost of the largest node |
| if ( nCubeLim > 0 ) |
| { |
| word Cost; |
| pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 ); |
| vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); |
| vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) ); |
| Cost = (word)Vec_PtrSize(vDfsNodes) * (word)Vec_IntSize(vLevel) * (word)nCubeLim; |
| if ( Cost > (word)nCostMax ) |
| { |
| printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", |
| Vec_PtrSize(vDfsNodes), Vec_IntSize(vLevel), nCubeLim, nCostMax ); |
| Vec_PtrFree( vDfsNodes ); |
| Vec_PtrFree( vCoNodes ); |
| Vec_WecFree( vSupps ); |
| return NULL; |
| } |
| Vec_PtrFree( vDfsNodes ); |
| } |
| // collect CO IDs in this order |
| vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) ); |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| pNode->iTemp = i; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i ) |
| Vec_IntPush( vNodeCoIds, pNode->iTemp ); |
| |
| // start the new network |
| pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); |
| // collect driver copies |
| vDriverCopy = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); |
| // Abc_NtkForEachCo( pNtk, pNode, i ) |
| Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i ) |
| Vec_PtrPush( vDriverCopy, Abc_ObjFanin0(pNode)->pCopy ); |
| // process the POs |
| pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); |
| // Abc_NtkForEachCo( pNtk, pNode, i ) |
| Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i ) |
| { |
| Extra_ProgressBarUpdate( pProgress, i, NULL ); |
| pDriver = Abc_ObjFanin0(pNode); |
| if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) ) |
| { |
| Abc_ObjAddFanin( pNode->pCopy, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) ); |
| continue; |
| } |
| if ( Abc_ObjIsCi(pDriver) ) |
| { |
| pNodeNew = Abc_NtkCreateNode( pNtkNew ); |
| Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) ); |
| 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_NtkFromSopsOne( pNtkNew, pNtk, Vec_IntEntry(vNodeCoIds, i), Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), nCubeLim, nBTLimit, fCanon, fReverse, i ? 0 : fVerbose ); |
| if ( pNodeNew == NULL ) |
| { |
| Abc_NtkDelete( pNtkNew ); |
| pNtkNew = NULL; |
| break; |
| } |
| Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); |
| } |
| Vec_PtrFree( vDriverCopy ); |
| Vec_PtrFree( vCoNodes ); |
| Vec_IntFree( vNodeCoIds ); |
| Vec_WecFree( vSupps ); |
| Extra_ProgressBarStop( pProgress ); |
| 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) ); |
| // create the new network |
| pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); |
| if ( pNtkNew == NULL ) |
| return NULL; |
| if ( pNtk->pExdc ) |
| pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); |
| // make sure that everything is okay |
| if ( !Abc_NtkCheck( pNtkNew ) ) |
| { |
| printf( "Abc_NtkCollapseSat: The network check has failed.\n" ); |
| Abc_NtkDelete( pNtkNew ); |
| return NULL; |
| } |
| 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 [Minimize SOP by removing redundant variables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| #define Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) |
| |
| int Abc_NtkCollapseReduce( Vec_Str_t * vSop, Vec_Int_t * vSupp, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) |
| { |
| int j = 0, i, k, iCo, iVar, nVars = Vec_IntSize(vSupp); |
| char * pCube, * pSop = Vec_StrArray(vSop); |
| Vec_Int_t * vPres; |
| if ( Vec_StrSize(vSop) == 4 ) // constant |
| { |
| Vec_IntForEachEntry( vClass, iCo, i ) |
| Vec_IntClear( Vec_WecEntry(vSupps, iCo) ); |
| return 1; |
| } |
| vPres = Vec_IntStart( nVars ); |
| Abc_NtkSopForEachCube( pSop, nVars, pCube ) |
| for ( k = 0; k < nVars; k++ ) |
| if ( pCube[k] != '-' ) |
| Vec_IntWriteEntry( vPres, k, 1 ); |
| if ( Vec_IntCountZero(vPres) == 0 ) |
| { |
| Vec_IntFree( vPres ); |
| return 0; |
| } |
| // reduce cubes |
| Abc_NtkSopForEachCube( pSop, nVars, pCube ) |
| for ( k = 0; k < nVars + 3; k++ ) |
| if ( k >= nVars || Vec_IntEntry(vPres, k) ) |
| Vec_StrWriteEntry( vSop, j++, pCube[k] ); |
| Vec_StrWriteEntry( vSop, j++, '\0' ); |
| Vec_StrShrink( vSop, j ); |
| // reduce support |
| Vec_IntForEachEntry( vClass, iCo, i ) |
| { |
| j = 0; |
| vSupp = Vec_WecEntry( vSupps, iCo ); |
| Vec_IntForEachEntry( vSupp, iVar, k ) |
| if ( Vec_IntEntry(vPres, k) ) |
| Vec_IntWriteEntry( vSupp, j++, iVar ); |
| Vec_IntShrink( vSupp, j ); |
| } |
| Vec_IntFree( vPres ); |
| // if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) ) |
| // printf( "Mismatch!!!\n" ); |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives SAT solver for one output from the shared CNF.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 ) |
| { |
| int i, k, iObj, status, nVars = 2; |
| // int i, k, iObj, status, nVars = 1; |
| Vec_Int_t * vLits = Vec_IntAlloc( 16 ); |
| sat_solver * pSat = sat_solver_new(); |
| if ( ppSat1 ) *ppSat1 = sat_solver_new(); |
| if ( ppSat2 ) *ppSat2 = sat_solver_new(); |
| if ( ppSat3 ) *ppSat3 = sat_solver_new(); |
| // assign SAT variable numbers |
| Vec_IntWriteEntry( vMap, iCoObjId, nVars++ ); |
| Vec_IntForEachEntry( vSupp, iObj, k ) |
| Vec_IntWriteEntry( vMap, iObj, nVars++ ); |
| Vec_IntForEachEntry( vAnds, iObj, k ) |
| if ( pCnf->pObj2Clause[iObj] != -1 ) |
| Vec_IntWriteEntry( vMap, iObj, nVars++ ); |
| // Vec_IntForEachEntry( vSupp, iObj, k ) |
| // Vec_IntWriteEntry( vMap, iObj, nVars++ ); |
| // create clauses for the internal nodes and for the output |
| sat_solver_setnvars( pSat, nVars ); |
| if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars ); |
| if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars ); |
| if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars ); |
| Vec_IntPush( vAnds, iCoObjId ); |
| Vec_IntForEachEntry( vAnds, iObj, k ) |
| { |
| int iClaBeg, iClaEnd, * pLit; |
| if ( pCnf->pObj2Clause[iObj] == -1 ) |
| continue; |
| iClaBeg = pCnf->pObj2Clause[iObj]; |
| iClaEnd = iClaBeg + pCnf->pObj2Count[iObj]; |
| assert( iClaBeg < iClaEnd ); |
| for ( i = iClaBeg; i < iClaEnd; i++ ) |
| { |
| Vec_IntClear( vLits ); |
| for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ ) |
| Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) ); |
| status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); |
| assert( status ); |
| (void) status; |
| if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); |
| if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); |
| if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); |
| } |
| } |
| Vec_IntPop( vAnds ); |
| Vec_IntFree( vLits ); |
| assert( nVars == sat_solver_nvars(pSat) ); |
| return pSat; |
| } |
| |
| /**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 fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) |
| { |
| Vec_Str_t * vSop; |
| abctime clk = Abc_Clock(); |
| extern Vec_Str_t * Bmc_CollapseOneOld( 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_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); |
| Gia_ManStop( pGia ); |
| if ( vSop == NULL ) |
| return NULL; |
| Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps ); |
| if ( fVerbose ) |
| printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); |
| if ( fVerbose ) |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| return vSop; |
| } |
| Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) |
| { |
| Vec_Str_t * vSop; |
| sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; |
| Gia_Obj_t * pObj; |
| abctime clk = Abc_Clock(); |
| extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); |
| extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); |
| extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); |
| int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) ); |
| Vec_Int_t * vAnds = Vec_IntAlloc( 100 ); |
| Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 ); |
| Gia_ManForEachCiVec( vSupp, p, pObj, i ) |
| Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) ); |
| Gia_ManIncrementTravId( p ); |
| Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds, NULL ); |
| assert( Vec_IntSize(vAnds) > 0 ); |
| // pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 ); |
| pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL ); |
| Vec_IntFree( vSuppObjs ); |
| if ( fVerbose ) |
| printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) ); |
| // vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); |
| // vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); |
| vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); |
| sat_solver_delete( pSat ); |
| if ( pSat1 ) sat_solver_delete( pSat1 ); |
| if ( pSat2 ) sat_solver_delete( pSat2 ); |
| if ( pSat3 ) sat_solver_delete( pSat3 ); |
| Vec_IntFree( vAnds ); |
| if ( vSop == NULL ) |
| return NULL; |
| Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps ); |
| if ( fVerbose ) |
| printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); |
| 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 fCnfShared, int fVerbose ) |
| { |
| ProgressBar * pProgress; |
| abctime clk = Abc_Clock(); |
| Vec_Ptr_t * vSops = NULL, * vSopsRepr; |
| Vec_Int_t * vReprs, * vClass, * vReprSuppSizes; |
| int i, k, Entry, iCo, * pOrder; |
| Vec_Wec_t * vClasses; |
| Cnf_Dat_t * pCnf = NULL; |
| Vec_Int_t * vMap = NULL; |
| // derive classes of outputs |
| vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 ); |
| if ( fVerbose ) |
| { |
| printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) ); |
| Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); |
| } |
| // 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 |
| if ( fCnfShared ) |
| { |
| vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); |
| pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 1, 0, 0, 0 ); |
| } |
| 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; |
| if ( Vec_IntSize(vSupp) < 2 ) |
| { |
| Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 ); |
| continue; |
| } |
| if ( fCnfShared && !fCanon ) |
| vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps ); |
| else |
| vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps ); |
| 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 ); |
| if ( fCnfShared ) |
| { |
| Cnf_DataFree( pCnf ); |
| Vec_IntFree( vMap ); |
| } |
| // 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 fCnfShared, 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 ); |
| // check the largest output |
| if ( nCubeLim > 0 && nCostMax > 0 ) |
| { |
| int iCoMax = Gia_ManCoLargestSupp( pGia, vSupps ); |
| int iObjMax = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) ); |
| int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) ); |
| int nNodeMax = Gia_ManConeSize( pGia, &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 ); |
| Gia_ManStop( pGia ); |
| Vec_WecFree( vSupps ); |
| return NULL; |
| } |
| } |
| pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); |
| vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, 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 = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, (const char*)Vec_PtrEntry( vSops, i ) ); |
| assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 ); |
| Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); |
| } |
| Vec_WecFree( vSupps ); |
| Vec_PtrFree( vSops ); |
| Abc_NtkSortSops( pNtkNew ); |
| return pNtkNew; |
| } |
| Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkNew; |
| assert( Abc_NtkIsStrash(pNtk) ); |
| pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, 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 /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
