diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 135 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 293 |
2 files changed, 330 insertions, 98 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 83077cb8..1482dc8c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -95,6 +95,7 @@ static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSatClp ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -714,6 +715,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "satclp", Abc_CommandSatClp, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "mux_struct", Abc_CommandMuxStruct, 1 ); @@ -3079,6 +3081,108 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; + int nCubeLim = 1000; + int nBTLimit = 1000000; + int fCanon = 0; + int fVerbose = 0; + int c; + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CLcvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nCubeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCubeLim < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBTLimit < 0 ) + goto usage; + break; + case 'c': + fCanon ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "Can only collapse a logic network or an AIG.\n" ); + return 1; + } + + // get the new network + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + else + { + pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + Abc_NtkDelete( pNtk ); + } + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Collapsing has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + Abc_Print( -2, "usage: satclp [-CL num] [-cvh]\n" ); + Abc_Print( -2, "\t performs SAT based collapsing\n" ); + Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); + Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk, * pNtkRes; @@ -37135,19 +37239,23 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ); int nCubeLim = 1000; int nBTLimit = 1000000; - int c, fVerbose = 0; + int fCanon = 0; + int fVerbose = 0; + int c; + + Vec_Str_t * vSop; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "LCvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CLcvh" ) ) != EOF ) { switch ( c ) { - case 'L': + case 'C': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } nCubeLim = atoi(argv[globalUtilOptind]); @@ -37155,10 +37263,10 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCubeLim < 0 ) goto usage; break; - case 'C': + case 'L': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } nBTLimit = atoi(argv[globalUtilOptind]); @@ -37166,6 +37274,9 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nBTLimit < 0 ) goto usage; break; + case 'c': + fCanon ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -37180,14 +37291,16 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SatClp(): There is no AIG.\n" ); return 0; } - Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fVerbose ); + vSop = Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fCanon, fVerbose ); + Vec_StrFree( vSop ); return 0; usage: - Abc_Print( -2, "usage: &satclp [-LC num] [-vh]\n" ); + Abc_Print( -2, "usage: &satclp [-CL num] [-cvh]\n" ); Abc_Print( -2, "\t performs SAT based collapsing\n" ); - Abc_Print( -2, "\t-L num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); - Abc_Print( -2, "\t-C num : the limit on the number of conflicts in one call [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); + Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index e0f80c60..e8ab3f7a 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "base/abc/abc.h" +#include "aig/gia/gia.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -32,9 +33,6 @@ ABC_NAMESPACE_IMPL_START #ifdef ABC_USE_CUDD -static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); -static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); - extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars ); //////////////////////////////////////////////////////////////////////// @@ -117,74 +115,24 @@ int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) { - 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 ); - Abc_NtkFreeGlobalBdds( pNtk, 1 ); - if ( pNtkNew == NULL ) - { -// Cudd_Quit( pNtk->pManGlob ); -// pNtk->pManGlob = NULL; - return NULL; - } -// Extra_StopManager( pNtk->pManGlob ); -// pNtk->pManGlob = 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; + 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; } - - -//int runtime1, runtime2; - -/**Function************************************************************* - - Synopsis [Derives the network with the given global BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) { -// extern void Extra_ShuffleTest( reo_man * p, DdManager * dd, DdNode * Func ); -// reo_man * pReo; - ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pDriver, * pNodeNew; -// DdManager * dd = pNtk->pManGlob; DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); int i; @@ -222,9 +170,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) Cudd_RecursiveDeref( dd, bBddDc ); } -// pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 ); -// runtime1 = runtime2 = 0; - // 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 @@ -240,25 +185,66 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy ); continue; } -// pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); -// Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) ); - } 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(); -// Extra_ReorderQuit( pReo ); -//ABC_PRT( "Reo ", runtime1 ); -//ABC_PRT( "Cudd", runtime2 ); + 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 + + + /**Function************************************************************* - Synopsis [Derives the network with the given global BDD.] + Synopsis [Derives GIA for the cone of one output and computes its SOP.] Description [] @@ -267,28 +253,161 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) +int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) { - Abc_Obj_t * pNodeNew, * pTemp; - int i; + int iLit0, iLit1; + if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 ) + 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, Vec_Int_t ** pvSupp ) +{ + extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo ); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ); + Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo ); + Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); + Vec_Str_t * vSop; + if ( fVerbose ) + printf( "Output %d:\n", iCo ); + vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fVerbose ); + Gia_ManStop( pGia ); + *pvSupp = vSupp; + if ( vSop == NULL ) + Vec_IntFree(vSupp); + else if ( Vec_StrSize(vSop) == 4 ) // constant + Vec_IntClear(vSupp); + return vSop; +} + +/**Function************************************************************* + + Synopsis [SAT-based collapsing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +{ + Abc_Obj_t * pNodeNew; + Vec_Int_t * vSupp; + Vec_Str_t * vSop; + int i, iCi; + // compute SOP of the node + vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, &vSupp ); + if ( vSop == NULL ) + return NULL; // 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]) ); + // add fanins + Vec_IntForEachEntry( vSupp, iCi, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); + Vec_IntFree( vSupp ); // transfer the function - pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ); + Vec_StrFree( vSop ); return pNodeNew; } - -#else - -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) { - return NULL; + ProgressBar * pProgress; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pDriver, * pNodeNew; + int i; + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // 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; + } +/* + if ( Abc_ObjIsCi(pDriver) ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); // pDriver->pCopy is removed by GIA construction... + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" ); + 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, i, nCubeLim, nBTLimit, fCanon, fVerbose ); + if ( pNodeNew == NULL ) + { + Abc_NtkDelete( pNtkNew ); + pNtkNew = NULL; + break; + } + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + Extra_ProgressBarStop( pProgress ); + return pNtkNew; +} +Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + assert( Abc_NtkIsStrash(pNtk) ); + // create the new network + pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, 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 //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |