diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index 0d59399358..2319e682a9 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -321,114 +321,6 @@ float Gia_ManDelayTraceLut( Gia_Man_t * p ) return tArrival; } -#if 0 - -/**Function************************************************************* - - Synopsis [Computes the required times for the given node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float Gia_ObjComputeRequired( Gia_Man_t * p, int iObj, int fUseSorting ) -{ - If_LibLut_t * pLutLib = p->pLutLib; - int pPinPerm[32]; - float pPinDelays[32]; - Gia_Obj_t * pFanout; - float tRequired, tDelay, * pDelays; - int k, iFanin; - if ( Gia_ObjIsCo(iObj) ) - return Gia_ObjTimeRequired( p, iObj); - tRequired = TIM_ETERNITY; - if ( pLutLib == NULL ) - { - Gia_ObjForEachFanout( iObj, pFanout, k ) - { - tDelay = Gia_ObjIsCo(pFanout)? 0.0 : 1.0; - if ( tRequired > Gia_ObjTimeRequired( p, pFanout) - tDelay ) - tRequired = Gia_ObjTimeRequired( p, pFanout) - tDelay; - } - } - else if ( !pLutLib->fVarPinDelays ) - { - Gia_ObjForEachFanout( iObj, pFanout, k ) - { - pDelays = pLutLib->pLutDelays[Gia_ObjLutSize(p, pFanout)]; - tDelay = Gia_ObjIsCo(pFanout)? 0.0 : pDelays[0]; - if ( tRequired > Gia_ObjTimeRequired( p, pFanout) - tDelay ) - tRequired = Gia_ObjTimeRequired( p, pFanout) - tDelay; - } - } - else - { - if ( fUseSorting ) - { - Gia_ObjForEachFanout( iObj, pFanout, k ) - { - pDelays = pLutLib->pLutDelays[Gia_ObjLutSize(p, pFanout)]; - Gia_LutDelayTraceSortPins( p, pFanout, pPinPerm, pPinDelays ); - iFanin = Gia_LutWhereIsPin( p, pFanout, iObj, pPinPerm ); - assert( Gia_ObjLutFanin( p, pFanout, pPinPerm[iFanin]) == iObj ); - tDelay = Gia_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin]; - if ( tRequired > Gia_ObjTimeRequired( p, pFanout) - tDelay ) - tRequired = Gia_ObjTimeRequired( p, pFanout) - tDelay; - } - } - else - { - Gia_ObjForEachFanout( iObj, pFanout, k ) - { - pDelays = pLutLib->pLutDelays[Gia_ObjLutSize(p, pFanout)]; - iFanin = Gia_ObjFindFanin( p, pFanout, iObj ); - assert( Gia_ObjLutFanin(p, pFanout, iFanin) == iObj ); - tDelay = Gia_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin]; - if ( tRequired > Gia_ObjTimeRequired( p, pFanout) - tDelay ) - tRequired = Gia_ObjTimeRequired( p, pFanout) - tDelay; - } - } - } - return tRequired; -} - -/**Function************************************************************* - - Synopsis [Computes the arrival times for the given node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_LutVerifyTiming( Gia_Man_t * p ) -{ - int iObj; - float tArrival, tRequired; - int i; - Gia_LutForEachObj( p, iObj, i ) - { - if ( Gia_ObjIsCi(iObj) && Gia_ObjFanoutNum(iObj) == 0 ) - continue; - tArrival = Gia_ObjComputeArrival( p, iObj, 1 ); - tRequired = Gia_ObjComputeRequired( p, iObj, 1 ); - if ( !Gia_LutTimeEqual( tArrival, Gia_ObjTimeArrival( p, iObj), (float)0.01 ) ) - printf( "Gia_LutVerifyTiming(): Object %d has different arrival time (%.2f) from computed (%.2f).\n", - iObj->Id, Gia_ObjTimeArrival( p, iObj), tArrival ); - if ( !Gia_LutTimeEqual( tRequired, Gia_ObjTimeRequired( p, iObj), (float)0.01 ) ) - printf( "Gia_LutVerifyTiming(): Object %d has different required time (%.2f) from computed (%.2f).\n", - iObj->Id, Gia_ObjTimeRequired( p, iObj), tRequired ); - } - return 1; -} - -#endif - /**Function************************************************************* Synopsis [Prints the delay trace for the given network.] diff --git a/src/aig/ivy/ivyDsd.c b/src/aig/ivy/ivyDsd.c index 78a935be4a..d7030bd7c6 100644 --- a/src/aig/ivy/ivyDsd.c +++ b/src/aig/ivy/ivyDsd.c @@ -722,105 +722,6 @@ void Ivy_TruthTestOne( unsigned uTruth ) // Vec_IntFree( vTree ); } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_TruthTest() -{ - FILE * pFile; - char Buffer[100]; - unsigned uTruth; - int i; - - pFile = fopen( "npn4.txt", "r" ); - for ( i = 0; i < 222; i++ ) -// pFile = fopen( "npn5.txt", "r" ); -// for ( i = 0; i < 616126; i++ ) - { - fscanf( pFile, "%s", Buffer ); - Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); -// Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); - uTruth |= (uTruth << 16); -// uTruth = ~uTruth; - Ivy_TruthTestOne( uTruth ); - } - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_TruthTest3() -{ - FILE * pFile; - char Buffer[100]; - unsigned uTruth; - int i; - - pFile = fopen( "npn3.txt", "r" ); - for ( i = 0; i < 14; i++ ) - { - fscanf( pFile, "%s", Buffer ); - Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 ); - uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); - Ivy_TruthTestOne( uTruth ); - } - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_TruthTest5() -{ - FILE * pFile; - char Buffer[100]; - unsigned uTruth; - int i; - -// pFile = fopen( "npn4.txt", "r" ); -// for ( i = 0; i < 222; i++ ) - pFile = fopen( "npn5.txt", "r" ); - for ( i = 0; i < 616126; i++ ) - { - fscanf( pFile, "%s", Buffer ); -// Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); - Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); -// uTruth |= (uTruth << 16); -// uTruth = ~uTruth; - Ivy_TruthTestOne( uTruth ); - } - fclose( pFile ); -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 83797ec72f..2ca0c7f4dd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4874,134 +4874,6 @@ int Abc_CommandLutmin( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - Res_Par_t Pars, * pPars = &Pars; - int c; - - // set defaults - pPars->nWindow = 62; - pPars->nCands = 5; - pPars->nSimWords = 4; - pPars->nGrowthLevel = 0; - pPars->fArea = 0; - pPars->fVerbose = 0; - pPars->fVeryVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WSCLavwh" ) ) != EOF ) - { - switch ( c ) - { - case 'W': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nWindow = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nWindow < 1 || pPars->nWindow > 99 ) - goto usage; - break; - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nSimWords = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nCands = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nCands < 0 || pPars->nCands > ABC_INFINITY ) - goto usage; - break; - case 'L': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nGrowthLevel = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) - goto usage; - break; - case 'a': - pPars->fArea ^= 1; - break; - case 'v': - pPars->fVerbose ^= 1; - break; - case 'w': - pPars->fVeryVerbose ^= 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_Print( -1, "This command can only be applied to a logic network.\n" ); - return 1; - } - - // modify the current network - if ( !Abc_NtkResynthesize( pNtk, pPars ) ) - { - Abc_Print( -1, "Resynthesis has failed.\n" ); - return 1; - } - return 0; - -usage: - Abc_Print( -2, "usage: imfs [-W ] [-LCS ] [-avwh]\n" ); - Abc_Print( -2, "\t performs resubstitution-based resynthesis with interpolation\n" ); - Abc_Print( -2, "\t (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" ); - Abc_Print( -2, "\t-W : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 ); - Abc_Print( -2, "\t-C : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands ); - Abc_Print( -2, "\t-S : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords ); - Abc_Print( -2, "\t-L : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); - Abc_Print( -2, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - return 1; -} - -#endif - /**Function************************************************************* Synopsis [] @@ -17434,297 +17306,6 @@ int Abc_CommandTimeScale( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -#if 0 -int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - char Buffer[100]; - char LutSize[100]; - Abc_Ntk_t * pNtk, * pNtkRes; - int c; - int fRecovery; - int fSwitching; - int fLatchPaths; - int fVerbose; - int nLutSize; - float DelayTarget; - - extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fLatchPaths, int fVerbose ); - - pNtk = Abc_FrameReadNtk(pAbc); - // set defaults - fRecovery = 1; - fSwitching = 0; - fLatchPaths = 0; - fVerbose = 0; - DelayTarget =-1; - nLutSize =-1; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "aplvhDK" ) ) != EOF ) - { - switch ( c ) - { - case 'a': - fRecovery ^= 1; - break; - case 'p': - fSwitching ^= 1; - break; - case 'l': - fLatchPaths ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - case 'D': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-D\" should be followed by a floating point number.\n" ); - goto usage; - } - DelayTarget = (float)atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( DelayTarget <= 0.0 ) - goto usage; - break; - case 'K': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" ); - goto usage; - } - nLutSize = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nLutSize < 0 ) - goto usage; - break; - default: - goto usage; - } - } - - if ( pNtk == NULL ) - { - Abc_Print( -1, "Empty network.\n" ); - return 1; - } - - // create the new LUT library - if ( nLutSize >= 3 && nLutSize <= 10 ) - Fpga_SetSimpleLutLib( nLutSize ); -/* - else - { - Abc_Print( -1, "Cannot perform FPGA mapping with LUT size %d.\n", nLutSize ); - return 1; - } -*/ - if ( !Abc_NtkIsStrash(pNtk) ) - { - // strash and balance the network - pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); - if ( pNtk == NULL ) - { - Abc_Print( -1, "Strashing before FPGA mapping has failed.\n" ); - return 1; - } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 ); - Abc_NtkDelete( pNtkRes ); - if ( pNtk == NULL ) - { - Abc_Print( -1, "Balancing before FPGA mapping has failed.\n" ); - return 1; - } - Abc_Print( 1, "The network was strashed and balanced before FPGA mapping.\n" ); - // get the new network - pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fLatchPaths, fVerbose ); - if ( pNtkRes == NULL ) - { - Abc_NtkDelete( pNtk ); - Abc_Print( -1, "FPGA mapping has failed.\n" ); - return 1; - } - Abc_NtkDelete( pNtk ); - } - else - { - // get the new network - pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fLatchPaths, fVerbose ); - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "FPGA mapping has failed.\n" ); - return 1; - } - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - return 0; - -usage: - if ( DelayTarget == -1 ) - sprintf(Buffer, "best possible" ); - else - sprintf(Buffer, "%.2f", DelayTarget ); - if ( nLutSize == -1 ) - sprintf(LutSize, "library" ); - else - sprintf(LutSize, "%d", nLutSize ); - Abc_Print( -2, "usage: fpga [-D float] [-K num] [-aplvh]\n" ); - Abc_Print( -2, "\t performs FPGA mapping of the current network\n" ); - Abc_Print( -2, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" ); - Abc_Print( -2, "\t-p : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" ); - Abc_Print( -2, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", fLatchPaths? "yes": "no" ); - Abc_Print( -2, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer ); - Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < 11) [default = %s]%s\n", LutSize, (nLutSize == -1 ? " (type \"print_lut\")" : "") ); - Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : prints the command usage\n"); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - char Buffer[100]; - Abc_Ntk_t * pNtk, * pNtkRes; - int c; - int fRecovery; - int fVerbose; - int nLutSize; - float DelayTarget; - - extern Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose ); - - pNtk = Abc_FrameReadNtk(pAbc); - // set defaults - fRecovery = 1; - fVerbose = 0; - DelayTarget =-1; - nLutSize = 5; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "avhDK" ) ) != EOF ) - { - switch ( c ) - { - case 'a': - fRecovery ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - case 'D': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-D\" should be followed by a floating point number.\n" ); - goto usage; - } - DelayTarget = (float)atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( DelayTarget <= 0.0 ) - goto usage; - break; - case 'K': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" ); - goto usage; - } - nLutSize = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nLutSize < 0 ) - goto usage; - break; - default: - goto usage; - } - } - - if ( pNtk == NULL ) - { - Abc_Print( -1, "Empty network.\n" ); - return 1; - } - - if ( !Abc_NtkIsStrash(pNtk) ) - { - // strash and balance the network - pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); - if ( pNtk == NULL ) - { - Abc_Print( -1, "Strashing before FPGA mapping has failed.\n" ); - return 1; - } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 ); - Abc_NtkDelete( pNtkRes ); - if ( pNtk == NULL ) - { - Abc_Print( -1, "Balancing before FPGA mapping has failed.\n" ); - return 1; - } - Abc_Print( 1, "The network was strashed and balanced before FPGA mapping.\n" ); - // get the new network - pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose ); - if ( pNtkRes == NULL ) - { - Abc_NtkDelete( pNtk ); - Abc_Print( -1, "FPGA mapping has failed.\n" ); - return 1; - } - Abc_NtkDelete( pNtk ); - } - else - { - // get the new network - pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose ); - if ( pNtkRes == NULL ) - { - Abc_Print( -1, "FPGA mapping has failed.\n" ); - return 1; - } - } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - return 0; - -usage: - if ( DelayTarget == -1 ) - sprintf(Buffer, "not used" ); - else - sprintf(Buffer, "%.2f", DelayTarget ); - Abc_Print( -2, "usage: ffpga [-K num] [-avh]\n" ); - Abc_Print( -2, "\t performs fast FPGA mapping of the current network\n" ); - Abc_Print( -2, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" ); -// Abc_Print( -2, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer ); - Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < 32) [default = %d]\n", nLutSize ); - Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : prints the command usage\n"); - return 1; -} -#endif - /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 1542c25a55..aeb3f7c0b5 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -244,295 +244,6 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i #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 ); diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c index 3f68b8153c..76386db679 100644 --- a/src/base/abci/abcTim.c +++ b/src/base/abci/abcTim.c @@ -87,96 +87,6 @@ int Abc_NtkTestTimNodeStrash( Gia_Man_t * pGia, Abc_Obj_t * pNode ) } -#if 0 - -/**Function************************************************************* - - Synopsis [Derives GIA manager using special pins to denote box boundaries.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Abc_NtkTestPinDeriveGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose ) -{ - Gia_Man_t * pTemp; - Gia_Man_t * pGia = NULL; - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj, * pFanin; - int i, k, iPinLit = 0; - // prepare logic network - assert( Abc_NtkIsLogic(pNtk) ); - Abc_NtkToAig( pNtk ); - // construct GIA - Abc_NtkFillTemp( pNtk ); - pGia = Gia_ManStart( Abc_NtkObjNumMax(pNtk) ); - Gia_ManHashAlloc( pGia ); - // create primary inputs - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->iTemp = Gia_ManAppendCi(pGia); - // create internal nodes in a topologic order from white boxes - vNodes = Abc_NtkDfs( pNtk, 0 ); - Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) - { - // input side - if ( !fWhiteBoxOnly || Abc_NodeIsWhiteBox(pObj) ) - { - // create special pintype for this node - iPinLit = Gia_ManAppendPinType( pGia, 1 ); - // create input pins - Abc_ObjForEachFanin( pObj, pFanin, k ) - pFanin->iTemp = Gia_ManAppendAnd( pGia, pFanin->iTemp, iPinLit ); - } - // perform GIA construction - pObj->iTemp = Abc_NtkTestTimNodeStrash( pGia, pObj ); - // output side - if ( !fWhiteBoxOnly || Abc_NodeIsWhiteBox(pObj) ) - { - // create special pintype for this node - iPinLit = Gia_ManAppendPinType( pGia, 1 ); - // create output pins - pObj->iTemp = Gia_ManAppendAnd( pGia, pObj->iTemp, iPinLit ); - } - } - Vec_PtrFree( vNodes ); - // create primary outputs - Abc_NtkForEachCo( pNtk, pObj, i ) - pObj->iTemp = Gia_ManAppendCo( pGia, Abc_ObjFanin0(pObj)->iTemp ); - // finalize GIA - Gia_ManHashStop( pGia ); - Gia_ManSetRegNum( pGia, 0 ); - // clean up GIA - pGia = Gia_ManCleanup( pTemp = pGia ); - Gia_ManStop( pTemp ); - return pGia; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkTestPinGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose ) -{ - Gia_Man_t * pGia; - char * pFileName = "testpin.aig"; - pGia = Abc_NtkTestPinDeriveGia( pNtk, fWhiteBoxOnly, fVerbose ); - Gia_AigerWrite( pGia, pFileName, 0, 0 ); - Gia_ManStop( pGia ); - printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n", - Abc_NtkName(pNtk), pFileName ); -} - -#endif /**Function************************************************************* diff --git a/src/base/acb/acbCom.c b/src/base/acb/acbCom.c deleted file mode 100644 index c2eae9241b..0000000000 --- a/src/base/acb/acbCom.c +++ /dev/null @@ -1,735 +0,0 @@ -/**CFile**************************************************************** - - FileName [acbCom.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Hierarchical word-level netlist.] - - Synopsis [Command handlers.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - November 29, 2014.] - - Revision [$Id: acbCom.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "acb.h" -#include "proof/cec/cec.h" -#include "base/main/mainInt.h" - -ABC_NAMESPACE_IMPL_START - -#if 0 - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Acb_CommandRead ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandWrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandPut ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandClp ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Acb_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); - -static inline Acb_Man_t * Acb_AbcGetMan( Abc_Frame_t * pAbc ) { return (Acb_Man_t *)pAbc->pAbcCba; } -static inline void Acb_AbcFreeMan( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Acb_ManFree(Acb_AbcGetMan(pAbc)); } -static inline void Acb_AbcUpdateMan( Abc_Frame_t * pAbc, Acb_Man_t * p ) { Acb_AbcFreeMan(pAbc); pAbc->pAbcCba = p; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Acb_Init( Abc_Frame_t * pAbc ) -{ - Cmd_CommandAdd( pAbc, "New word level", "@read", Acb_CommandRead, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@write", Acb_CommandWrite, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@ps", Acb_CommandPs, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@put", Acb_CommandPut, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@get", Acb_CommandGet, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@clp", Acb_CommandClp, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@blast", Acb_CommandBlast, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@cec", Acb_CommandCec, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@test", Acb_CommandTest, 0 ); -} - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Acb_End( Abc_Frame_t * pAbc ) -{ - Acb_AbcFreeMan( pAbc ); -} - - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Acb_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - FILE * pFile; - Acb_Man_t * p = NULL; - char * pFileName = NULL; - int c, fTest = 0, fDfs = 0, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "tdvh" ) ) != EOF ) - { - switch ( c ) - { - case 't': - fTest ^= 1; - break; - case 'd': - fDfs ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( argc != globalUtilOptind + 1 ) - { - printf( "Acb_CommandRead(): Input file name should be given on the command line.\n" ); - return 0; - } - // get the file name - pFileName = argv[globalUtilOptind]; - if ( (pFile = fopen( pFileName, "r" )) == NULL ) - { - Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", ".smt", ".acb", NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); - Abc_Print( 1, "\n" ); - return 0; - } - fclose( pFile ); - if ( fTest ) - { - if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) - Prs_ManReadBlifTest( pFileName ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - Prs_ManReadVerilogTest( pFileName ); - else - { - printf( "Unrecognized input file extension.\n" ); - return 0; - } - return 0; - } - if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) - p = Acb_ManReadBlif( pFileName ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - p = Acb_ManReadVerilog( pFileName ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) ) - p = Acb_ManReadCba( pFileName ); - else - { - printf( "Unrecognized input file extension.\n" ); - return 0; - } - if ( fDfs ) - { - Acb_Man_t * pTemp; - p = Acb_ManDup( pTemp = p, Acb_NtkCollectDfs ); - Acb_ManFree( pTemp ); - } - Acb_AbcUpdateMan( pAbc, p ); - return 0; -usage: - Abc_Print( -2, "usage: @read [-tdvh] \n" ); - Abc_Print( -2, "\t reads hierarchical design\n" ); - Abc_Print( -2, "\t-t : toggle testing the parser [default = %s]\n", fTest? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle computing DFS ordering [default = %s]\n", fDfs? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * p = Acb_AbcGetMan(pAbc); - char * pFileName = NULL; - int fInclineCats = 0; - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) - { - switch ( c ) - { - case 'c': - fInclineCats ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandWrite(): There is no current design.\n" ); - return 0; - } - - if ( argc == globalUtilOptind + 1 ) - pFileName = argv[globalUtilOptind]; - else if ( argc == globalUtilOptind && p ) - { - pFileName = Extra_FileNameGenericAppend( Acb_ManSpec(p) ? Acb_ManSpec(p) : Acb_ManName(p), "_out.v" ); - printf( "Generated output file name \"%s\".\n", pFileName ); - } - else - { - printf( "Output file name should be given on the command line.\n" ); - return 0; - } - // perform writing - if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) - Acb_ManWriteBlif( pFileName, p ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - Acb_ManWriteVerilog( pFileName, p, fInclineCats ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) ) - Acb_ManWriteCba( pFileName, p ); - else - { - printf( "Unrecognized output file extension.\n" ); - return 0; - } - return 0; -usage: - Abc_Print( -2, "usage: @write [-cvh]\n" ); - Abc_Print( -2, "\t writes the design into a file in BLIF or Verilog\n" ); - Abc_Print( -2, "\t-c : toggle inlining input concatenations [default = %s]\n", fInclineCats? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * p = Acb_AbcGetMan(pAbc); - int nModules = 0; - int fShowMulti = 0; - int fShowAdder = 0; - int fDistrib = 0; - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Mmadvh" ) ) != EOF ) - { - switch ( c ) - { - case 'M': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); - goto usage; - } - nModules = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nModules < 0 ) - goto usage; - break; - case 'm': - fShowMulti ^= 1; - break; - case 'a': - fShowAdder ^= 1; - break; - case 'd': - fDistrib ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandPs(): There is no current design.\n" ); - return 0; - } - if ( nModules ) - { - Acb_ManPrintStats( p, nModules, fVerbose ); - return 0; - } - Acb_NtkPrintStatsFull( Acb_ManRoot(p), fDistrib, fVerbose ); - if ( fShowMulti ) - Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_MUL ); - if ( fShowAdder ) - Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_ADD ); - return 0; -usage: - Abc_Print( -2, "usage: @ps [-M num] [-madvh]\n" ); - Abc_Print( -2, "\t prints statistics\n" ); - Abc_Print( -2, "\t-M num : the number of first modules to report [default = %d]\n", nModules ); - Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * p = Acb_AbcGetMan(pAbc); - Gia_Man_t * pGia = NULL; - int c, fBarBufs = 1, fSeq = 0, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "bsvh" ) ) != EOF ) - { - switch ( c ) - { - case 'b': - fBarBufs ^= 1; - break; - case 's': - fSeq ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandPut(): There is no current design.\n" ); - return 0; - } - pGia = Acb_ManBlast( p, fBarBufs, fSeq, fVerbose ); - if ( pGia == NULL ) - { - Abc_Print( 1, "Acb_CommandPut(): Conversion to AIG has failed.\n" ); - return 0; - } - Abc_FrameUpdateGia( pAbc, pGia ); - return 0; -usage: - Abc_Print( -2, "usage: @put [-bsvh]\n" ); - Abc_Print( -2, "\t extracts AIG from the hierarchical design\n" ); - Abc_Print( -2, "\t-b : toggle using barrier buffers [default = %s]\n", fBarBufs? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc); - int c, fMapped = 0, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF ) - { - switch ( c ) - { - case 'm': - fMapped ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" ); - return 0; - } - - if ( fMapped ) - { - if ( pAbc->pNtkCur == NULL ) - { - Abc_Print( 1, "Acb_CommandGet(): There is no current mapped design.\n" ); - return 0; - } - pNew = Acb_ManInsertAbc( p, pAbc->pNtkCur ); - } - else - { - if ( pAbc->pGia == NULL ) - { - Abc_Print( 1, "Acb_CommandGet(): There is no current AIG.\n" ); - return 0; - } - pNew = Acb_ManInsertGia( p, pAbc->pGia ); - } - Acb_AbcUpdateMan( pAbc, pNew ); - return 0; -usage: - Abc_Print( -2, "usage: @get [-mvh]\n" ); - Abc_Print( -2, "\t extracts AIG or mapped network into the hierarchical design\n" ); - Abc_Print( -2, "\t-m : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc); - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) - { - switch ( c ) - { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" ); - return 0; - } - pNew = Acb_ManCollapse( p ); - Acb_AbcUpdateMan( pAbc, pNew ); - return 0; -usage: - Abc_Print( -2, "usage: @clp [-vh]\n" ); - Abc_Print( -2, "\t collapses the current hierarchical design\n" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Gia_Man_t * pNew = NULL; - Acb_Man_t * p = Acb_AbcGetMan(pAbc); - int c, fSeq = 0, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) - { - switch ( c ) - { - case 's': - fSeq ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandBlast(): There is no current design.\n" ); - return 0; - } - pNew = Acb_ManBlast( p, 0, fSeq, fVerbose ); - if ( pNew == NULL ) - { - Abc_Print( 1, "Acb_CommandBlast(): Bit-blasting has failed.\n" ); - return 0; - } - Abc_FrameUpdateGia( pAbc, pNew ); - return 0; -usage: - Abc_Print( -2, "usage: @blast [-svh]\n" ); - Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" ); - Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle 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 Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * p = Acb_AbcGetMan(pAbc), * pTemp; - Gia_Man_t * pFirst, * pSecond, * pMiter; - Cec_ParCec_t ParsCec, * pPars = &ParsCec; - char * pFileName, * pStr, ** pArgvNew; - int c, nArgcNew, fDumpMiter = 0; - FILE * pFile; - Cec_ManCecSetDefaultParams( pPars ); - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) - { - switch ( c ) - { - case 'v': - pPars->fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandCec(): There is no current design.\n" ); - return 0; - } - - pArgvNew = argv + globalUtilOptind; - nArgcNew = argc - globalUtilOptind; - if ( nArgcNew != 1 ) - { - if ( p->pSpec == NULL ) - { - Abc_Print( -1, "File name is not given on the command line.\n" ); - return 1; - } - pFileName = p->pSpec; - } - else - pFileName = pArgvNew[0]; - // fix the wrong symbol - for ( pStr = pFileName; *pStr; pStr++ ) - if ( *pStr == '>' ) - *pStr = '\\'; - if ( (pFile = fopen( pFileName, "r" )) == NULL ) - { - Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", NULL, NULL, NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); - Abc_Print( 1, "\n" ); - return 1; - } - fclose( pFile ); - - // extract AIG from the current design - pFirst = Acb_ManBlast( p, 0, 0, 0 ); - if ( pFirst == NULL ) - { - Abc_Print( -1, "Extracting AIG from the current design has failed.\n" ); - return 0; - } - // extract AIG from the second design - - if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) - pTemp = Acb_ManReadBlif( pFileName ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pTemp = Acb_ManReadVerilog( pFileName ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) ) - pTemp = Acb_ManReadCba( pFileName ); - else assert( 0 ); - pSecond = Acb_ManBlast( pTemp, 0, 0, 0 ); - Acb_ManFree( pTemp ); - if ( pSecond == NULL ) - { - Gia_ManStop( pFirst ); - Abc_Print( -1, "Extracting AIG from the original design has failed.\n" ); - return 0; - } - // compute the miter - pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose ); - if ( pMiter ) - { - if ( fDumpMiter ) - { - Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" ); - Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 ); - } - pAbc->Status = Cec_ManVerify( pMiter, pPars ); - //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); - Gia_ManStop( pMiter ); - } - Gia_ManStop( pFirst ); - Gia_ManStop( pSecond ); - return 0; -usage: - Abc_Print( -2, "usage: @cec [-vh]\n" ); - Abc_Print( -2, "\t combinational equivalence checking\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - return 1; -} - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Acb_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Acb_Man_t * p = Acb_AbcGetMan(pAbc); - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) - { - switch ( c ) - { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( p == NULL ) - { - Abc_Print( 1, "Acb_CommandTest(): There is no current design.\n" ); - return 0; - } - return 0; -usage: - Abc_Print( -2, "usage: @test [-vh]\n" ); - Abc_Print( -2, "\t experiments with word-level networks\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - return 1; -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/base/acb/module.make b/src/base/acb/module.make index 46294f9f48..5a1b1e5247 100644 --- a/src/base/acb/module.make +++ b/src/base/acb/module.make @@ -1,6 +1,5 @@ SRC += src/base/acb/acbAbc.c \ src/base/acb/acbAig.c \ - src/base/acb/acbCom.c \ src/base/acb/acbFunc.c \ src/base/acb/acbMfs.c \ src/base/acb/acbPush.c \ diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index a00424432e..b52d3d1eb7 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1090,56 +1090,6 @@ int CmdCommandEmpty( Abc_Frame_t * pAbc, int argc, char **argv ) } -#if 0 - -/**Function******************************************************************** - - Synopsis [Donald's version.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int CmdCommandUndo( Abc_Frame_t * pAbc, int argc, char **argv ) -{ - Abc_Ntk_t * pNtkTemp; - int id, c; - - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) - { - switch ( c ) - { - case 'h': - goto usage; - break; - default: - goto usage; - } - } - if (globalUtilOptind <= argc) { - pNtkTemp = pAbc->pNtk; - pAbc->pNtk = pAbc->pNtkSaved; - pAbc->pNtkSaved = pNtkTemp; - } - id = atoi(argv[globalUtilOptind]); - pNtkTemp = Cmd_HistoryGetSnapshot(pAbc, id); - if (!pNtkTemp) - fprintf( pAbc->Err, "Snapshot %d does not exist\n", id); - else - pAbc->pNtk = Abc_NtkDup(pNtkTemp, Abc_NtkMan(pNtkTemp)); - - return 0; -usage: - fprintf( pAbc->Err, "usage: undo\n" ); - fprintf( pAbc->Err, " swaps the current network and the backup network\n" ); - return 1; -} - -#endif - #if defined(WIN32) && !defined(__cplusplus) #include diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index 405b44d6d8..a5d52d9201 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -1668,36 +1668,6 @@ int Io_ReadBlifCreateTiming( Io_ReadBlif_t * p, Abc_Ntk_t * pNtk ) return 1; } -#if 0 - -/**Function************************************************************* - - Synopsis [Connect the boxes in the hierarchy of networks.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Io_ReadBlifNetworkConnectBoxes( Io_ReadBlif_t * p, Abc_Ntk_t * pNtkMaster ) -{ - stmm_generator * gen; - Abc_Ntk_t * pNtk; - char * pName; - // connect the master network - if ( Io_ReadBlifNetworkConnectBoxesOne( p, pNtkMaster, pNtkMaster->tName2Model ) ) - return 1; - // connect other networks - stmm_foreach_item( pNtkMaster->tName2Model, gen, &pName, (char **)&pNtk ) - if ( Io_ReadBlifNetworkConnectBoxesOne( p, pNtk, pNtkMaster->tName2Model ) ) - return 1; - return 0; -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c index 42c04c02ba..d62124e0e1 100644 --- a/src/bdd/cas/casCore.c +++ b/src/bdd/cas/casCore.c @@ -276,186 +276,6 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu return 1; } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Experiment2( BFunc * pFunc ) -{ - int i, x, RetValue; - int nVars = pFunc->nInputs; - int nOuts = pFunc->nOutputs; - DdManager * dd = pFunc->dd; - long clk1; - -// int nVarsEnc; // the number of additional variables to encode outputs -// DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars - - int nNames; // the total number of all inputs - char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names - - DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs - - char FileNameIni[100]; - char FileNameFin[100]; - char Buffer[100]; - - DdManager * DdNew; - -//pTable = fopen( "stats.txt", "a+" ); -//fprintf( pTable, "%s ", pFunc->FileGeneric ); -//fprintf( pTable, "%d ", nVars ); -//fprintf( pTable, "%d ", nOuts ); - - - // assign the file names - strcpy( FileNameIni, pFunc->FileGeneric ); - strcat( FileNameIni, "_ENC.blif" ); - - strcpy( FileNameFin, pFunc->FileGeneric ); - strcat( FileNameFin, "_LUT.blif" ); - - // derive the single-output function IN THE NEW MANAGER - clk1 = Abc_Clock(); -// aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc ); - aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew ); Cudd_Ref( aFunc ); - printf( "Single-output function derivation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); -// s_RemappingTime = Abc_Clock() - clk1; - - // dispose of the multiple-output function - Extra_Dissolve( pFunc ); - - // reorder the single output function - printf( "\nReordering variables in the new manager...\n"); - clk1 = Abc_Clock(); - printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) ); -// Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1); - Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1); -// Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1); - printf( "Node count after = %d\n", Cudd_DagSize( aFunc ) ); - printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - printf( "\n" ); - -//fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) ); -//fprintf( pTable, "%d ", Extra_ProfileWidthMax(DdNew, aFunc) ); - - - // create the names to be used with the new manager - nNames = DdNew->size; - for ( x = 0; x < nNames; x++ ) - { - sprintf( Buffer, "v%02d", x ); - pNames[x] = Extra_UtilStrsav( Buffer ); - } - - - - // write the single-output function into BLIF for verification - clk1 = Abc_Clock(); - WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni ); - printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - - - /////////////////////////////////////////////////////////////////// - // verification of single output function - clk1 = Abc_Clock(); - { - BFunc g_Func; - DdNode * aRes; - - g_Func.dd = DdNew; - g_Func.FileInput = Extra_UtilStrsav(FileNameIni); - - if ( Extra_ReadFile( &g_Func ) == 0 ) - { - printf( "\nSomething did not work out while reading the input file for verification\n"); - Extra_Dissolve( &g_Func ); - return; - } - - aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); - - if ( aRes != aFunc ) - printf( "\nVerification FAILED!\n"); - else - printf( "\nVerification okay!\n"); - - Cudd_RecursiveDeref( DdNew, aRes ); - - // delocate - Extra_Dissolve( &g_Func ); - } - printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - /////////////////////////////////////////////////////////////////// - - - CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 ); - -/* - /////////////////////////////////////////////////////////////////// - // verification of the decomposed LUT network - clk1 = Abc_Clock(); - { - BFunc g_Func; - DdNode * aRes; - - g_Func.dd = DdNew; - g_Func.FileInput = Extra_UtilStrsav(FileNameFin); - - if ( Extra_ReadFile( &g_Func ) == 0 ) - { - printf( "\nSomething did not work out while reading the input file for verification\n"); - Extra_Dissolve( &g_Func ); - return; - } - - aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] ); Cudd_Ref( aRes ); - - if ( aRes != aFunc ) - printf( "\nFinal verification FAILED!\n"); - else - printf( "\nFinal verification okay!\n"); - - Cudd_RecursiveDeref( DdNew, aRes ); - - // delocate - Extra_Dissolve( &g_Func ); - } - printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) ); - /////////////////////////////////////////////////////////////////// -*/ - - - Cudd_RecursiveDeref( DdNew, aFunc ); - - // release the names - for ( i = 0; i < nNames; i++ ) - ABC_FREE( pNames[i] ); - - - - ///////////////////////////////////////////////////////////////////// - // check for remaining references in the package - RetValue = Cudd_CheckZeroRef( DdNew ); - printf( "\nThe number of referenced nodes in the new manager = %d\n", RetValue ); - Cudd_Quit( DdNew ); - -//fprintf( pTable, "\n" ); -//fclose( pTable ); - -} - -#endif - //////////////////////////////////////////////////////////////////////// /// SINGLE OUTPUT FUNCTION /// //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdLocal.c b/src/bdd/dsd/dsdLocal.c index 552b53e9d3..5726ee2798 100644 --- a/src/bdd/dsd/dsdLocal.c +++ b/src/bdd/dsd/dsdLocal.c @@ -263,78 +263,6 @@ DdNode * Extra_bddNodePointedByCube( DdManager * dd, DdNode * bF, DdNode * bC ) return Extra_bddNodePointedByCube( dd, bF0, bC0 ); } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * dsdTreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode, int fRemap ) -{ - DdNode * bCof0, * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp; - int i; - int fAllBuffs = 1; - static int Permute[MAXINPUTS]; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->Type == DT_PRIME ); - - // transform the function of this block to depend on inputs - // corresponding to the formal inputs - - // first, substitute those inputs that have some blocks associated with them - // second, remap the inputs to the top of the manager (then, it is easy to output them) - - // start the function - bNewFunc = pNode->G; Cudd_Ref( bNewFunc ); - // go over all primary inputs - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pNode->pDecs[i]->Type != DT_BUF ) // remap only if it is not the buffer - { - bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) ); Cudd_Ref( bCube0 ); - bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 ); Cudd_Ref( bCof0 ); - Cudd_RecursiveDeref( dd, bCube0 ); - - bCube1 = Extra_bddFindOneCube( dd, pNode->pDecs[i]->G ); Cudd_Ref( bCube1 ); - bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 ); Cudd_Ref( bCof1 ); - Cudd_RecursiveDeref( dd, bCube1 ); - - Cudd_RecursiveDeref( dd, bNewFunc ); - - // use the variable in the i-th level of the manager -// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc ); - // use the first variale in the support of the component - bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 ); Cudd_Ref( bNewFunc ); - Cudd_RecursiveDeref( dd, bCof0 ); - Cudd_RecursiveDeref( dd, bCof1 ); - } - - if ( fRemap ) - { - // remap the function to the top of the manager - // remap the function to the first variables of the manager - for ( i = 0; i < pNode->nDecs; i++ ) - // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i]; - Permute[ pNode->pDecs[i]->S->index ] = i; - - bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - - Cudd_Deref( bNewFunc ); - return bNewFunc; -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/cov/covCore.c b/src/map/cov/covCore.c index b4faf308a0..9effc253fc 100644 --- a/src/map/cov/covCore.c +++ b/src/map/cov/covCore.c @@ -652,375 +652,6 @@ Min_Cube_t * Abc_NodeCovSum( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * p - - - - -#if 0 - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovPropagateEsop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) -{ - Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1; - Vec_Int_t * vSupp, * vSupp0, * vSupp1; - - if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); - if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); - - // get the resulting support - vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); - vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); - vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 ); - - // quit if support if too large - if ( vSupp->nSize > p->nFaninMax ) - { - Vec_IntFree( vSupp ); - return 0; - } - - // get the covers - pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); - pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); - - // complement the first if needed - if ( !Abc_ObjFaninC0(pObj) ) - pCover0 = pCov0; - else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube - pCover0 = pCov0->pNext; - else - pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; - - // complement the second if needed - if ( !Abc_ObjFaninC1(pObj) ) - pCover1 = pCov1; - else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube - pCover1 = pCov1->pNext; - else - pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; - - // derive and minimize the cover (quit if too large) - if ( !Abc_NodeCovProductEsop( p, pCover0, pCover1, vSupp->nSize ) ) - { - pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); - Min_CoverRecycle( p->pManMin, pCover ); - Vec_IntFree( vSupp ); - return 0; - } - - // minimize the cover - Min_EsopMinimize( p->pManMin ); - pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); - - // quit if the cover is too large - if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) - { - Min_CoverRecycle( p->pManMin, pCover ); - Vec_IntFree( vSupp ); - return 0; - } - - // count statistics - p->nSupps++; - p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps ); - - // set the covers - assert( Abc_ObjGetSupp(pObj) == NULL ); - Abc_ObjSetSupp( pObj, vSupp ); - Abc_ObjSetCover2( pObj, pCover ); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovPropagateSop( Cov_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) -{ - Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1; - Vec_Int_t * vSupp, * vSupp0, * vSupp1; - int fCompl0, fCompl1; - - if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); - if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); - - // get the resulting support - vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); - vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); - vSupp = Abc_NodeCovSupport( p, vSupp0, vSupp1 ); - - // quit if support if too large - if ( vSupp->nSize > p->nFaninMax ) - { - Vec_IntFree( vSupp ); - return 0; - } - - // get the complemented attributes - fCompl0 = Abc_ObjFaninC0(pObj); - fCompl1 = Abc_ObjFaninC1(pObj); - - // prepare the positive cover - pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); - pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); - - // derive and minimize the cover (quit if too large) - if ( !pCover0 || !pCover1 ) - pCoverP = NULL; - else if ( !Abc_NodeCovProductSop( p, pCover0, pCover1, vSupp->nSize ) ) - { - pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); - Min_CoverRecycle( p->pManMin, pCoverP ); - pCoverP = NULL; - } - else - { - Min_SopMinimize( p->pManMin ); - pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); - // quit if the cover is too large - if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax ) - { - Min_CoverRecycle( p->pManMin, pCoverP ); - pCoverP = NULL; - } - } - - // prepare the negative cover - pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); - pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); - - // derive and minimize the cover (quit if too large) - if ( !pCover0 || !pCover1 ) - pCoverN = NULL; - else if ( !Abc_NodeCovUnionSop( p, pCover0, pCover1, vSupp->nSize ) ) - { - pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); - Min_CoverRecycle( p->pManMin, pCoverN ); - pCoverN = NULL; - } - else - { - Min_SopMinimize( p->pManMin ); - pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); - // quit if the cover is too large - if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax ) - { - Min_CoverRecycle( p->pManMin, pCoverN ); - pCoverN = NULL; - } - } - - if ( pCoverP == NULL && pCoverN == NULL ) - { - Vec_IntFree( vSupp ); - return 0; - } - - // count statistics - p->nSupps++; - p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps ); - - // set the covers - assert( Abc_ObjGetSupp(pObj) == NULL ); - Abc_ObjSetSupp( pObj, vSupp ); - Abc_ObjSetCover( pObj, pCoverP, 0 ); - Abc_ObjSetCover( pObj, pCoverN, 1 ); - return 1; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovProductEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - Min_Cube_t * pCube, * pCube0, * pCube1; - int i, Val0, Val1; - - // clean storage - Min_ManClean( p->pManMin, nSupp ); - if ( pCover0 == NULL || pCover1 == NULL ) - return 1; - - // go through the cube pairs - Min_CoverForEachCube( pCover0, pCube0 ) - Min_CoverForEachCube( pCover1, pCube1 ) - { - // go through the support variables of the cubes - for ( i = 0; i < p->vPairs0->nSize; i++ ) - { - Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); - Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); - if ( (Val0 & Val1) == 0 ) - break; - } - // check disjointness - if ( i < p->vPairs0->nSize ) - continue; - - if ( p->pManMin->nCubes >= p->nCubesMax ) - return 0; - - // create the product cube - pCube = Min_CubeAlloc( p->pManMin ); - - // add the literals - pCube->nLits = 0; - for ( i = 0; i < nSupp; i++ ) - { - if ( p->vComTo0->pArray[i] == -1 ) - Val0 = 3; - else - Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); - - if ( p->vComTo1->pArray[i] == -1 ) - Val1 = 3; - else - Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); - - if ( (Val0 & Val1) == 3 ) - continue; - - Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); - pCube->nLits++; - } - // add the cube to storage - Min_EsopAddCube( p->pManMin, pCube ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovProductSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - return 1; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovUnionEsop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - Min_Cube_t * pCube, * pCube0, * pCube1; - int i, Val0, Val1; - - // clean storage - Min_ManClean( p->pManMin, nSupp ); - if ( pCover0 ) - { - Min_CoverForEachCube( pCover0, pCube0 ) - { - // create the cube - pCube = Min_CubeAlloc( p->pManMin ); - pCube->nLits = 0; - for ( i = 0; i < p->vComTo0->nSize; i++ ) - { - if ( p->vComTo0->pArray[i] == -1 ) - continue; - Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); - if ( Val0 == 3 ) - continue; - Min_CubeXorVar( pCube, i, Val0 ^ 3 ); - pCube->nLits++; - } - if ( p->pManMin->nCubes >= p->nCubesMax ) - return 0; - // add the cube to storage - Min_EsopAddCube( p->pManMin, pCube ); - } - } - if ( pCover1 ) - { - Min_CoverForEachCube( pCover1, pCube1 ) - { - // create the cube - pCube = Min_CubeAlloc( p->pManMin ); - pCube->nLits = 0; - for ( i = 0; i < p->vComTo1->nSize; i++ ) - { - if ( p->vComTo1->pArray[i] == -1 ) - continue; - Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); - if ( Val1 == 3 ) - continue; - Min_CubeXorVar( pCube, i, Val1 ^ 3 ); - pCube->nLits++; - } - if ( p->pManMin->nCubes >= p->nCubesMax ) - return 0; - // add the cube to storage - Min_EsopAddCube( p->pManMin, pCube ); - } - } - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeCovUnionSop( Cov_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) -{ - return 1; -} - - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/fpga/fpgaCutUtils.c b/src/map/fpga/fpgaCutUtils.c index 9b5b2be985..1587120e49 100644 --- a/src/map/fpga/fpgaCutUtils.c +++ b/src/map/fpga/fpgaCutUtils.c @@ -216,55 +216,6 @@ int Fpga_CutListCount( Fpga_Cut_t * pSets ) return i; } -#if 0 - -/**function************************************************************* - - synopsis [Removes the fanouts of the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Fpga_CutRemoveFanouts( Fpga_Man_t * p, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ) -{ - Fpga_NodeVec_t * vFanouts; - int i, k; - for ( i = 0; i < pCut->nLeaves; i++ ) - { - vFanouts = pCut->ppLeaves[i]->vFanouts; - for ( k = 0; k < vFanouts->nSize; k++ ) - if ( vFanouts->pArray[k] == pNode ) - break; - assert( k != vFanouts->nSize ); - for ( k++; k < vFanouts->nSize; k++ ) - vFanouts->pArray[k-1] = vFanouts->pArray[k]; - vFanouts->nSize--; - } -} - -/**function************************************************************* - - synopsis [Removes the fanouts of the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Fpga_CutInsertFanouts( Fpga_Man_t * p, Fpga_Node_t * pNode, Fpga_Cut_t * pCut ) -{ - int i; - for ( i = 0; i < pCut->nLeaves; i++ ) - Fpga_NodeVecPush( pCut->ppLeaves[i]->vFanouts, pNode ); -} -#endif - /**Function************************************************************* Synopsis [Computes the arrival time and the area flow of the cut.] diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c index 5f233533d9..624758c390 100644 --- a/src/map/fpga/fpgaMatch.c +++ b/src/map/fpga/fpgaMatch.c @@ -454,294 +454,6 @@ clk = clock(); } -#if 0 -/**function************************************************************* - - synopsis [References the cut.] - - description [This procedure is similar to the procedure NodeReclaim.] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Fpga_Experiment( Fpga_Man_t * p ) -{ - int Counter[10] = {0}; - Fpga_Node_t * pNode; - int i; - - for ( i = 0; i < p->nOutputs; i++ ) - { - pNode = Fpga_Regular(p->pOutputs[i]); - pNode->vFanouts = NULL; - } - - for ( i = 0; i < p->vAnds->nSize; i++ ) - { - pNode = p->vAnds->pArray[i]; - if ( !Fpga_NodeIsAnd( pNode ) ) - continue; - if ( pNode->vFanouts == NULL ) - continue; - if ( pNode->vFanouts->nSize >= 10 ) - continue; - Counter[pNode->vFanouts->nSize]++; - } - - printf( "Fanout stats: " ); - for ( i = 0; i < 10; i++ ) - printf( " %d=%d", i, Counter[i] ); - printf( "\n" ); - printf( "Area before = %4.2f.\n", Fpga_MappingArea(p) ); - - for ( i = 0; i < p->vAnds->nSize; i++ ) - { - Fpga_NodeVec_t * vNodesTfo; - float AreaBefore; - - pNode = p->vAnds->pArray[i]; - if ( !Fpga_NodeIsAnd( pNode ) ) - continue; - if ( pNode->vFanouts == NULL ) - continue; - if ( pNode->vFanouts->nSize != 1 && pNode->vFanouts->nSize != 2 && pNode->vFanouts->nSize != 3 ) - continue; - -// assert( pNode->nRefs > 0 ); - if ( pNode->nRefs == 0 ) - continue; - - AreaBefore = pNode->pCutBest->aFlow; - pNode->pCutBest->aFlow = FPGA_FLOAT_LARGE; - - Fpga_TimeComputeRequiredGlobal( p, 0 ); - - vNodesTfo = Fpga_CollectNodeTfo( p, pNode ); - if ( Fpga_MappingMatchesAreaArray( p, vNodesTfo ) == 0 ) - printf( "attempt failed\n" ); - else - printf( "attempt succeeded\n" ); - Fpga_NodeVecFree( vNodesTfo ); - - pNode->pCutBest->aFlow = AreaBefore; -// break; - } - printf( "Area after = %4.2f.\n", Fpga_MappingArea(p) ); -// printf( "AREA GAIN = %4.2f (%.2f %%)\n", GainTotal, 100.0 * GainTotal / Fpga_MappingArea(p) ); -} - - - -/**function************************************************************* - - synopsis [References the cut.] - - description [This procedure is similar to the procedure NodeReclaim.] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Fpga_Experiment2( Fpga_Man_t * p ) -{ - int Counter[10] = {0}; - Fpga_Cut_t * ppCutsNew[10]; - Fpga_Cut_t * ppCutsOld[10]; - Fpga_Node_t * pFanout, * pNode; - float Gain, Loss, GainTotal, Area1, Area2; - int i, k; - - for ( i = 0; i < p->nOutputs; i++ ) - { - pNode = Fpga_Regular(p->pOutputs[i]); - pNode->vFanouts = NULL; - } - - for ( i = 0; i < p->vAnds->nSize; i++ ) - { - pNode = p->vAnds->pArray[i]; - if ( !Fpga_NodeIsAnd( pNode ) ) - continue; - if ( pNode->vFanouts == NULL ) - continue; - if ( pNode->vFanouts->nSize >= 10 ) - continue; - Counter[pNode->vFanouts->nSize]++; - } - - printf( "Fanout stats: " ); - for ( i = 0; i < 10; i++ ) - printf( " %d=%d", i, Counter[i] ); - printf( "\n" ); - printf( "Area before = %4.2f.\n", Fpga_MappingArea(p) ); - - GainTotal = 0; - for ( i = 0; i < p->vAnds->nSize; i++ ) - { - pNode = p->vAnds->pArray[i]; - if ( !Fpga_NodeIsAnd( pNode ) ) - continue; - if ( pNode->vFanouts == NULL ) - continue; - if ( pNode->vFanouts->nSize != 2 )//&& pNode->vFanouts->nSize != 2 && pNode->vFanouts->nSize != 3 ) - continue; - - assert( pNode->nRefs > 0 ); - - // for all fanouts, find the best cut without this node - for ( k = 0; k < pNode->vFanouts->nSize; k++ ) - { - pFanout = pNode->vFanouts->pArray[k]; - ppCutsOld[k] = pFanout->pCutBest; - ppCutsNew[k] = Fpga_MappingAreaWithoutNode( p, pFanout, pNode ); - if ( ppCutsNew[k] == NULL ) - break; - } - if ( k != pNode->vFanouts->nSize ) - { - printf( "Node %4d: Skipped.\n", pNode->Num ); - continue; - } - - - // compute the area after replacing all the cuts - Gain = 0; - for ( k = 0; k < pNode->vFanouts->nSize; k++ ) - { - pFanout = pNode->vFanouts->pArray[k]; - // deref old cut - Area1 = Fpga_MatchAreaDeref( p, ppCutsOld[k] ); - // assign new cut - pFanout->pCutBest = ppCutsNew[k]; - // ref new cut - Area2 = Fpga_MatchAreaRef( p, ppCutsNew[k] ); - // compute the gain - Gain += Area1 - Area2; - } - - printf( "%d ", pNode->nRefs ); - - // undo the whole thing - Loss = 0; - for ( k = 0; k < pNode->vFanouts->nSize; k++ ) - { - pFanout = pNode->vFanouts->pArray[k]; - // deref old cut - Area1 = Fpga_MatchAreaDeref( p, ppCutsNew[k] ); - // assign new cut - pFanout->pCutBest = ppCutsOld[k]; - // ref new cut - Area2 = Fpga_MatchAreaRef( p, ppCutsOld[k] ); - // compute the gain - Loss += Area2 - Area1; - } - assert( Gain == Loss ); - - - printf( "Node %4d: Fanouts = %d. Cut area = %4.2f. Gain = %4.2f.\n", - pNode->Num, pNode->nRefs, pNode->pCutBest->aFlow, Gain ); - - if ( Gain > 0 ) - GainTotal += Gain; - } - printf( "Area after = %4.2f.\n", Fpga_MappingArea(p) ); - printf( "AREA GAIN = %4.2f (%.2f %%)\n", GainTotal, 100.0 * GainTotal / Fpga_MappingArea(p) ); -} - - -/**function************************************************************* - - synopsis [Computes the loss of area when node is not allowed.] - - description [Returning FPGA_FLOAT_LARGE means it does not exist.] - - sideeffects [] - - seealso [] - -***********************************************************************/ -Fpga_Cut_t * Fpga_MappingAreaWithoutNode( Fpga_Man_t * p, Fpga_Node_t * pNode, Fpga_Node_t * pNodeNo ) -{ - Fpga_Cut_t * pCut, * pCutBestOld, * pCutRes; - float aAreaCutBest; - int i; - clock_t clk; - // make sure that at least one cut other than the trivial is present - if ( pNode->pCuts->pNext == NULL ) - { - printf( "\nError: A node in the mapping graph does not have feasible cuts.\n" ); - return 0; - } - - assert( pNode->nRefs > 0 ); - - // remember the old cut - pCutBestOld = pNode->pCutBest; - // deref the old cut - aAreaCutBest = Fpga_MatchAreaDeref( p, pNode->pCutBest ); - - // search for a better cut - pNode->pCutBest = NULL; - for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext ) - { - // compute the arrival time of the cut and its area flow -clk = clock(); - Fpga_MatchCutGetArrTime( p, pCut ); -//p->time2 += clock() - clk; - // drop the cut if it does not meet the required times - if ( pCut->tArrival > pNode->tRequired ) - continue; - - // skip the cut if it contains the no-node - for ( i = 0; i < pCut->nLeaves; i++ ) - if ( pCut->ppLeaves[i] == pNodeNo ) - break; - if ( i != pCut->nLeaves ) - continue; - - // get the area of this cut - pCut->aFlow = Fpga_MatchAreaCount( p, pCut ); - // if no cut is assigned, use the current one - if ( pNode->pCutBest == NULL ) - { - pNode->pCutBest = pCut; - continue; - } - // choose the best cut as follows: exact area first, delay as a tie-breaker - if ( pNode->pCutBest->aFlow > pCut->aFlow || - pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival ) - { - pNode->pCutBest = pCut; - } - } - - // make sure the match is found - if ( pNode->pCutBest == NULL ) - { - pNode->pCutBest = pCutBestOld; - // insert the new cut - pNode->pCutBest->aFlow = Fpga_MatchAreaRef( p, pNode->pCutBest ); - return NULL; - } - - pCutRes = pNode->pCutBest; - pNode->pCutBest = pCutBestOld; - - // insert the new cut - pNode->pCutBest->aFlow = Fpga_MatchAreaRef( p, pNode->pCutBest ); - - // make sure the area selected is not worse then the original area - assert( pNode->pCutBest->aFlow == aAreaCutBest ); - assert( pNode->tRequired < FPGA_FLOAT_LARGE ); - return pCutRes; -} - -#endif - - /**function************************************************************* synopsis [Performs area minimization using a heuristic algorithm.] diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index ec172b1b8f..776991496b 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -87,190 +87,6 @@ void If_ManCleanMarkV( If_Man_t * p ) If_ManForEachObj( p, pObj, i ) pObj->fVisit = 0; } - -#if 0 - -/**Function************************************************************* - - Synopsis [Computes area, references, and nodes used in the mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float If_ManScanMapping_rec( If_Man_t * p, If_Obj_t * pObj, If_Obj_t ** ppStore ) -{ - If_Obj_t * pLeaf; - If_Cut_t * pCutBest; - float aArea; - int i; - if ( pObj->nRefs++ || If_ObjIsCi(pObj) || If_ObjIsConst1(pObj) ) - return 0.0; - // store the node in the structure by level - assert( If_ObjIsAnd(pObj) ); - pObj->pCopy = (char *)ppStore[pObj->Level]; - ppStore[pObj->Level] = pObj; - // visit the transitive fanin of the selected cut - pCutBest = If_ObjCutBest(pObj); - p->nNets += pCutBest->nLeaves; - aArea = If_CutLutArea( p, pCutBest ); - If_CutForEachLeaf( p, pCutBest, pLeaf, i ) - aArea += If_ManScanMapping_rec( p, pLeaf, ppStore ); - return aArea; -} - -/**Function************************************************************* - - Synopsis [Computes area, references, and nodes used in the mapping.] - - Description [Collects the nodes in reverse topological order in array - p->vMapping.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float If_ManScanMapping( If_Man_t * p ) -{ - If_Obj_t * pObj, ** ppStore; - float aArea; - int i; - assert( !p->pPars->fLiftLeaves ); - // clean all references - p->nNets = 0; - If_ManForEachObj( p, pObj, i ) - { - pObj->Required = IF_FLOAT_LARGE; - pObj->nVisits = pObj->nVisitsCopy; - pObj->nRefs = 0; - } - // allocate place to store the nodes - ppStore = ABC_ALLOC( If_Obj_t *, p->nLevelMax + 1 ); - memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) ); - // collect nodes reachable from POs in the DFS order through the best cuts - aArea = 0; - If_ManForEachCo( p, pObj, i ) - aArea += If_ManScanMapping_rec( p, If_ObjFanin0(pObj), ppStore ); - // reconnect the nodes in reverse topological order - Vec_PtrClear( p->vMapped ); - for ( i = p->nLevelMax; i >= 0; i-- ) - for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy ) - Vec_PtrPush( p->vMapped, pObj ); - ABC_FREE( ppStore ); - return aArea; -} - -/**Function************************************************************* - - Synopsis [Computes area, references, and nodes used in the mapping.] - - Description [Collects the nodes in reverse topological order in array - p->vMapping.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float If_ManScanMappingDirect( If_Man_t * p ) -{ - If_Obj_t * pObj, ** ppStore; - float aArea; - int i; - assert( !p->pPars->fLiftLeaves ); - // clean all references - If_ManForEachObj( p, pObj, i ) - { - pObj->Required = IF_FLOAT_LARGE; - pObj->nVisits = pObj->nVisitsCopy; - pObj->nRefs = 0; - } - // allocate place to store the nodes - ppStore = ABC_ALLOC( If_Obj_t *, p->nLevelMax + 1 ); - memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) ); - // collect nodes reachable from POs in the DFS order through the best cuts - aArea = 0; - If_ManForEachCo( p, pObj, i ) - aArea += If_ManScanMapping_rec( p, If_ObjFanin0(pObj), ppStore ); - // reconnect the nodes in reverse topological order - Vec_PtrClear( p->vMapped ); -// for ( i = p->nLevelMax; i >= 0; i-- ) - for ( i = 0; i <= p->nLevelMax; i++ ) - for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy ) - Vec_PtrPush( p->vMapped, pObj ); - ABC_FREE( ppStore ); - return aArea; -} - -/**Function************************************************************* - - Synopsis [Computes area, references, and nodes used in the mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float If_ManScanMappingSeq_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vMapped ) -{ - If_Obj_t * pLeaf; - If_Cut_t * pCutBest; - float aArea; - int i, Shift; - // treat latches transparently - if ( If_ObjIsLatch(pObj) ) - return If_ManScanMappingSeq_rec( p, If_ObjFanin0(pObj), vMapped ); - // consider trivial cases - if ( pObj->nRefs++ || If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) ) - return 0.0; - // store the node in the structure by level - assert( If_ObjIsAnd(pObj) ); - // visit the transitive fanin of the selected cut - pCutBest = If_ObjCutBest(pObj); - aArea = If_ObjIsAnd(pObj)? If_CutLutArea(p, pCutBest) : (float)0.0; - If_CutForEachLeafSeq( p, pCutBest, pLeaf, Shift, i ) - aArea += If_ManScanMappingSeq_rec( p, pLeaf, vMapped ); - // add the node - Vec_PtrPush( vMapped, pObj ); - return aArea; -} - -/**Function************************************************************* - - Synopsis [Computes area, references, and nodes used in the mapping.] - - Description [Collects the nodes in reverse topological order in array - p->vMapping.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -float If_ManScanMappingSeq( If_Man_t * p ) -{ - If_Obj_t * pObj; - float aArea; - int i; - assert( p->pPars->fLiftLeaves ); - // clean all references - If_ManForEachObj( p, pObj, i ) - pObj->nRefs = 0; - // collect nodes reachable from POs in the DFS order through the best cuts - aArea = 0; - Vec_PtrClear( p->vMapped ); - If_ManForEachPo( p, pObj, i ) - aArea += If_ManScanMappingSeq_rec( p, If_ObjFanin0(pObj), p->vMapped ); - return aArea; -} - -#endif /**Function************************************************************* diff --git a/src/map/mapper/mapperCutUtils.c b/src/map/mapper/mapperCutUtils.c index aa307368b3..fcba124131 100644 --- a/src/map/mapper/mapperCutUtils.c +++ b/src/map/mapper/mapperCutUtils.c @@ -219,56 +219,6 @@ int Map_CutListCount( Map_Cut_t * pSets ) return i; } -#if 0 - -/**function************************************************************* - - synopsis [Removes the fanouts of the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Map_CutRemoveFanouts( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ) -{ - Map_NodeVec_t * vFanouts; - int i, k; - for ( i = 0; i < pCut->nLeaves; i++ ) - { - vFanouts = pCut->ppLeaves[i]->vFanouts; - for ( k = 0; k < vFanouts->nSize; k++ ) - if ( vFanouts->pArray[k] == pNode ) - break; - assert( k != vFanouts->nSize ); - for ( k++; k < vFanouts->nSize; k++ ) - vFanouts->pArray[k-1] = vFanouts->pArray[k]; - vFanouts->nSize--; - } -} - -/**function************************************************************* - - synopsis [Removes the fanouts of the cut.] - - description [] - - sideeffects [] - - seealso [] - -***********************************************************************/ -void Map_CutInsertFanouts( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase ) -{ - int i; - for ( i = 0; i < pCut->nLeaves; i++ ) - Map_NodeVecPush( pCut->ppLeaves[i]->vFanouts, pNode ); -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c index b2ee8ab956..21b4b37f63 100644 --- a/src/map/mio/mioUtils.c +++ b/src/map/mio/mioUtils.c @@ -859,70 +859,6 @@ word Mio_DeriveTruthTable6( Mio_Gate_t * pGate ) return uTruthRes.w; } -#if 0 - -/**Function************************************************************* - - Synopsis [Recursively derives the truth table of the gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Mio_DeriveTruthTable_rec( DdNode * bFunc, unsigned uTruthsIn[][2], unsigned uTruthRes[] ) -{ - unsigned uTruthsCof0[2]; - unsigned uTruthsCof1[2]; - - // complement the resulting truth table, if the function is complemented - if ( Cudd_IsComplement(bFunc) ) - { - Mio_DeriveTruthTable_rec( Cudd_Not(bFunc), uTruthsIn, uTruthRes ); - uTruthRes[0] = ~uTruthRes[0]; - uTruthRes[1] = ~uTruthRes[1]; - return; - } - - // if the function is constant 1, return the constant 1 truth table - if ( bFunc->index == CUDD_CONST_INDEX ) - { - uTruthRes[0] = MIO_FULL; - uTruthRes[1] = MIO_FULL; - return; - } - - // solve the problem for both cofactors - Mio_DeriveTruthTable_rec( cuddE(bFunc), uTruthsIn, uTruthsCof0 ); - Mio_DeriveTruthTable_rec( cuddT(bFunc), uTruthsIn, uTruthsCof1 ); - - // derive the resulting truth table using the input truth tables - uTruthRes[0] = (uTruthsCof0[0] & ~uTruthsIn[bFunc->index][0]) | - (uTruthsCof1[0] & uTruthsIn[bFunc->index][0]); - uTruthRes[1] = (uTruthsCof0[1] & ~uTruthsIn[bFunc->index][1]) | - (uTruthsCof1[1] & uTruthsIn[bFunc->index][1]); -} - -/**Function************************************************************* - - Synopsis [Derives the truth table of the gate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Mio_DeriveTruthTable( Mio_Gate_t * pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[] ) -{ - Mio_DeriveTruthTable_rec( pGate->bFunc, uTruthsIn, uTruthRes ); -} - -#endif - /**Function************************************************************* Synopsis [Derives the truth table of the gate.] diff --git a/src/misc/mvc/mvcOpBool.c b/src/misc/mvc/mvcOpBool.c index 32339dfeee..8a54daada0 100644 --- a/src/misc/mvc/mvcOpBool.c +++ b/src/misc/mvc/mvcOpBool.c @@ -63,90 +63,6 @@ Mvc_Cover_t * Mvc_CoverBooleanOr( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 ) return pCover; } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Mvc_Cover_t * Mvc_CoverBooleanAnd( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 ) -{ - Mvc_Cover_t * pCover; - Mvc_Cube_t * pCube1, * pCube2, * pCubeCopy; - // make sure the covers are compatible - assert( pCover1->nBits == pCover2->nBits ); - // clone the cover - pCover = Mvc_CoverClone( pCover1 ); - // create the cubes by making pair-wise products - // of cubes in pCover1 and pCover2 - Mvc_CoverForEachCube( pCover1, pCube1 ) - { - Mvc_CoverForEachCube( pCover2, pCube2 ) - { - if ( Mvc_CoverDist0Cubes( p, pCube1, pCube2 ) ) - { - pCubeCopy = Mvc_CubeAlloc( pCover ); - Mvc_CubeBitAnd( pCubeCopy, pCube1, pCube2 ); - Mvc_CoverAddCubeTail( pCover, pCubeCopy ); - } - } - // if the number of cubes in the new cover is too large - // try compressing them - if ( Mvc_CoverReadCubeNum( pCover ) > 500 ) - Mvc_CoverContain( pCover ); - } - return pCover; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the two covers are equal.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Mvc_CoverBooleanEqual( Mvc_Data_t * p, Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 ) -{ - Mvc_Cover_t * pSharp; - - pSharp = Mvc_CoverSharp( p, pCover1, pCover2 ); - if ( Mvc_CoverReadCubeNum( pSharp ) ) - { -Mvc_CoverContain( pSharp ); -printf( "Sharp \n" ); -Mvc_CoverPrint( pSharp ); - Mvc_CoverFree( pSharp ); - return 0; - } - Mvc_CoverFree( pSharp ); - - pSharp = Mvc_CoverSharp( p, pCover2, pCover1 ); - if ( Mvc_CoverReadCubeNum( pSharp ) ) - { -Mvc_CoverContain( pSharp ); -printf( "Sharp \n" ); -Mvc_CoverPrint( pSharp ); - Mvc_CoverFree( pSharp ); - return 0; - } - Mvc_CoverFree( pSharp ); - - return 1; -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/mvc/mvcPrint.c b/src/misc/mvc/mvcPrint.c index b7ba494cb7..2203e756b7 100644 --- a/src/misc/mvc/mvcPrint.c +++ b/src/misc/mvc/mvcPrint.c @@ -148,74 +148,6 @@ void Mvc_CubePrintBinary( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) printf( "\n" ); } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Mvc_CoverPrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover ) -{ - Mvc_Cube_t * pCube; - int i; - // print general statistics - printf( "The cover contains %d cubes (%d bits and %d words)\n", - pCover->lCubes.nItems, pCover->nBits, pCover->nWords ); - // iterate through the cubes - Mvc_CoverForEachCube( pCover, pCube ) - Mvc_CubePrintMv( pData, pCover, pCube ); - - if ( pCover->pLits ) - { - for ( i = 0; i < pCover->nBits; i++ ) - printf( " %d", pCover->pLits[i] ); - printf( "\n" ); - } - printf( "End of cover printout\n" ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Mvc_CubePrintMv( Mvc_Data_t * pData, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) -{ - int iLit, iVar; - // iterate through the literals - printf( "Size = %2d ", Mvc_CubeReadSize(pCube) ); - iVar = 0; - for ( iLit = 0; iLit < pData->pVm->nValuesIn; iLit++ ) - { - if ( iLit == pData->pVm->pValuesFirst[iVar+1] ) - { - printf( " " ); - iVar++; - } - if ( Mvc_CubeBitValue( pCube, iLit ) ) - printf( "%c", '0' + iLit - pData->pVm->pValuesFirst[iVar] ); - else - printf( "-" ); - } - printf( "\n" ); -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c index d938169a30..77f072e41a 100644 --- a/src/misc/mvc/mvcUtils.c +++ b/src/misc/mvc/mvcUtils.c @@ -651,144 +651,6 @@ Mvc_Cover_t * Mvc_CoverUnivQuantify( Mvc_Cover_t * p, return pCover; } -#if 0 - -/**Function************************************************************* - - Synopsis [Derives the cofactors of the cover.] - - Description [Derives the cofactors w.r.t. a variable and also cubes - that do not depend on this variable.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar ) -{ - Mvc_Cover_t ** ppCofs; - Mvc_Cube_t * pCube, * pCubeNew; - int i, nValues, iValueFirst, Res; - - // start the covers for cofactors - iValueFirst = Vm_VarMapReadValuesFirst(pData->pVm, iVar); - nValues = Vm_VarMapReadValues(pData->pVm, iVar); - ppCofs = ABC_ALLOC( Mvc_Cover_t *, nValues + 1 ); - for ( i = 0; i <= nValues; i++ ) - ppCofs[i] = Mvc_CoverClone( pCover ); - - // go through the cubes - Mvc_CoverForEachCube( pCover, pCube ) - { - // if the literal if a full literal, add it to last "cofactor" - Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] ); - if ( Res ) - { - pCubeNew = Mvc_CubeDup(pCover, pCube); - Mvc_CoverAddCubeTail( ppCofs[nValues], pCubeNew ); - continue; - } - - // otherwise, add it to separate values - for ( i = 0; i < nValues; i++ ) - if ( Mvc_CubeBitValue( pCube, iValueFirst + i ) ) - { - pCubeNew = Mvc_CubeDup(pCover, pCube); - Mvc_CubeBitOr( pCubeNew, pCubeNew, pData->ppMasks[iVar] ); - Mvc_CoverAddCubeTail( ppCofs[i], pCubeNew ); - } - } - return ppCofs; -} - -/**Function************************************************************* - - Synopsis [Count the cubes with non-trivial literals with the given value.] - - Description [The data and the cover are given (pData, pCover). Also given - are the variable number and the number of a value of this variable. - This procedure returns the number of cubes having a non-trivial literal - of this variable that have the given value present.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue ) -{ - Mvc_Cube_t * pCube; - int iValueFirst, Res, Counter; - - Counter = 0; - iValueFirst = Vm_VarMapReadValuesFirst( pData->pVm, iVar ); - Mvc_CoverForEachCube( pCover, pCube ) - { - // check if the given literal is the full literal - Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] ); - if ( Res ) - continue; - // this literal is not a full literal; check if it has this value - Counter += Mvc_CubeBitValue( pCube, iValueFirst + iValue ); - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [Creates the expanded cover.] - - Description [The original cover is expanded by adding some variables. - These variables are the additional variables in pVmNew, compared to - pCvr->pVm. The resulting cover is the same as the original one, except - that it contains the additional variables present as full literals - in every cube.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Mvc_Cover_t * Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew ) -{ - Mvc_Cover_t * pCoverNew; - Mvc_Cube_t * pCube, * pCubeNew; - int i, iLast, iLastNew; - - // create the new cover - pCoverNew = Mvc_CoverAlloc( pCover->pMem, Vm_VarMapReadValuesInNum(pVmNew) ); - - // get the cube composed of extra bits - Mvc_CoverAllocateMask( pCoverNew ); - Mvc_CubeBitClean( pCoverNew->pMask ); - for ( i = pCover->nBits; i < pCoverNew->nBits; i++ ) - Mvc_CubeBitInsert( pCoverNew->pMask, i ); - - // get the indexes of the last words in both covers - iLast = pCover->nWords? pCover->nWords - 1: 0; - iLastNew = pCoverNew->nWords? pCoverNew->nWords - 1: 0; - - // create the cubes of the new cover - Mvc_CoverForEachCube( pCover, pCube ) - { - pCubeNew = Mvc_CubeAlloc( pCoverNew ); - Mvc_CubeBitClean( pCubeNew ); - // copy the bits (cannot immediately use Mvc_CubeBitCopy, - // because covers have different numbers of bits) - Mvc_CubeSetLast( pCubeNew, iLast ); - Mvc_CubeBitCopy( pCubeNew, pCube ); - Mvc_CubeSetLast( pCubeNew, iLastNew ); - // add the extra bits - Mvc_CubeBitOr( pCubeNew, pCubeNew, pCoverNew->pMask ); - // add the cube to the new cover - Mvc_CoverAddCubeTail( pCoverNew, pCubeNew ); - } - return pCoverNew; -} - -#endif - /**Function************************************************************* Synopsis [Transposes the cube cover.] diff --git a/src/misc/util/utilSort.c b/src/misc/util/utilSort.c index 4dca700c67..b6e67bf98a 100644 --- a/src/misc/util/utilSort.c +++ b/src/misc/util/utilSort.c @@ -254,119 +254,6 @@ int * Abc_MergeSortCost( int * pCosts, int nSize ) } -// this implementation uses 3x less memory but is 30% slower due to cache misses - -#if 0 - -/**Function************************************************************* - - Synopsis [Merging two lists of entries.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_MergeSortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut, int * pCost ) -{ - int nEntries = (p1End - p1Beg) + (p2End - p2Beg); - int * pOutBeg = pOut; - while ( p1Beg < p1End && p2Beg < p2End ) - { - if ( pCost[*p1Beg] == pCost[*p2Beg] ) - *pOut++ = *p1Beg++, *pOut++ = *p2Beg++; - else if ( pCost[*p1Beg] < pCost[*p2Beg] ) - *pOut++ = *p1Beg++; - else // if ( pCost[*p1Beg] > pCost[*p2Beg] ) - *pOut++ = *p2Beg++; - } - while ( p1Beg < p1End ) - *pOut++ = *p1Beg++; - while ( p2Beg < p2End ) - *pOut++ = *p2Beg++; - assert( pOut - pOutBeg == nEntries ); -} - -/**Function************************************************************* - - Synopsis [Recursive sorting.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_MergeSortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost ) -{ - int nSize = pInEnd - pInBeg; - assert( nSize > 0 ); - if ( nSize == 1 ) - return; - if ( nSize == 2 ) - { - if ( pCost[pInBeg[0]] > pCost[pInBeg[1]] ) - { - pInBeg[0] ^= pInBeg[1]; - pInBeg[1] ^= pInBeg[0]; - pInBeg[0] ^= pInBeg[1]; - } - } - else if ( nSize < 8 ) - { - int temp, i, j, best_i; - for ( i = 0; i < nSize-1; i++ ) - { - best_i = i; - for ( j = i+1; j < nSize; j++ ) - if ( pCost[pInBeg[j]] < pCost[pInBeg[best_i]] ) - best_i = j; - temp = pInBeg[i]; - pInBeg[i] = pInBeg[best_i]; - pInBeg[best_i] = temp; - } - } - else - { - Abc_MergeSortCost_rec( pInBeg, pInBeg + nSize/2, pOutBeg, pCost ); - Abc_MergeSortCost_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2, pCost ); - Abc_MergeSortCostMerge( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg, pCost ); - memcpy( pInBeg, pOutBeg, sizeof(int) * nSize ); - } -} - -/**Function************************************************************* - - Synopsis [Sorting procedure.] - - Description [Returns permutation for the non-decreasing order of costs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Abc_MergeSortCost( int * pCosts, int nSize ) -{ - int i, * pInput, * pOutput; - pInput = (int *) malloc( sizeof(int) * nSize ); - for ( i = 0; i < nSize; i++ ) - pInput[i] = i; - if ( nSize < 2 ) - return pInput; - pOutput = (int *) malloc( sizeof(int) * nSize ); - Abc_MergeSortCost_rec( pInput, pInput + nSize, pOutput, pCosts ); - free( pOutput ); - return pInput; -} - -#endif - - - /**Function************************************************************* diff --git a/src/opt/dar/darData.c b/src/opt/dar/darData.c index eaebb40dcf..d8a3d9f874 100644 --- a/src/opt/dar/darData.c +++ b/src/opt/dar/darData.c @@ -11143,146 +11143,6 @@ Vec_Int_t * Dar_LibReadPrios() return vResult; } -#if 0 - -#include "base/abc/abc.h" - -ABC_NAMESPACE_IMPL_START - - -/**Function************************************************************* - - Synopsis [Generate arrays.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_NtkGenerateArrays( Abc_Ntk_t * pNtk ) -{ - extern int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); - - Abc_Obj_t * pObj; - int i, Count = 0; - assert( Abc_NtkPiNum(pNtk) == 4 ); - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_ObjFanoutNum(Abc_AigConst1(pNtk)) == 0 ); -/* - { - unsigned char * pBuffer; - int Pos, uLit, uLit0, uLit1, Size, Digit; - - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = (void *)Count++; - - Pos = 0; - pBuffer = ABC_ALLOC( char, 200000 ); - Abc_AigForEachAnd( pNtk, pObj, i ) - { - pObj->pCopy = (void *)Count++; - uLit = ((int)pObj->pCopy << 1); - uLit0 = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj); - uLit1 = (((int)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj); - assert( uLit0 < uLit1 ); - Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); - Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); - } - // write the buffer - Size = 0; - for ( i = 0; i < Pos; i++ ) - { - if ( i % 36 == 0 ) - printf( "\n" ); - - Digit = pBuffer[i] & 0xF; - if ( Digit < 10 ) - printf( "%d", Digit ); - else - printf( "%c", Digit - 10 + 'A' ); - - - Digit = pBuffer[i]; - Digit >>= 4; - if ( Digit < 10 ) - printf( "%d", Digit ); - else - printf( "%c", Digit - 10 + 'A' ); - - } - printf( "\n" ); - printf( "Size = %d.\n", Pos ); - } -*/ - - - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = (void *)Count++; - Abc_AigForEachAnd( pNtk, pObj, i ) - { -// if ( (Count - 4) % 6 == 0 ) -// printf( "\n" ); -// printf( "%5d,", (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj) ); -// printf( "%5d,", (((int)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj) ); - pObj->pCopy = (void *)Count++; - } -// printf( "\n" ); -// printf( "Nodes = %d.\n", Count-4 ); - - - - Abc_NtkForEachPo( pNtk, pObj, i ) - { - if ( i % 12 == 0 ) - printf( "\n" ); - printf( "%5d,", (int)Abc_ObjFanin0(pObj)->pCopy ); - } - printf( "\n" ); - printf( "Outputs = %d.\n", Abc_NtkPoNum(pNtk) ); - - -/* - { - unsigned char * pBuffer; - Vec_Int_t * vOuts; - int Pos, Prev, Out; - - vOuts = Vec_IntAlloc( 25000 ); - Abc_NtkForEachPo( pNtk, pObj, i ) - Vec_IntPush( vOuts, Abc_ObjFaninId0(pObj) ); - Vec_IntSort( vOuts, 0 ); - - Pos = 0; - pBuffer = ABC_ALLOC( char, 50000 ); - Prev = 0; - Vec_IntForEachEntry( vOuts, Out, i ) - { - assert( Prev < Out ); - Pos = Io_WriteAigerEncode( pBuffer, Pos, Out - Prev ); - Prev = Out; - } - Vec_IntFree( vOuts ); - - // write the buffer - for ( i = 0; i < Pos; i++ ) - { - if ( i % 32 == 0 ) - printf( "\n" ); - printf( "%d,", pBuffer[i] ); - } - printf( "\n" ); - printf( "Size = %d.\n", Pos ); - } -*/ - -} - -#endif - - - //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dar/darMan.c b/src/opt/dar/darMan.c index e1094267ca..cf30292806 100644 --- a/src/opt/dar/darMan.c +++ b/src/opt/dar/darMan.c @@ -129,41 +129,6 @@ void Dar_ManPrintStats( Dar_Man_t * p ) } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -#if 0 - -ABC_NAMESPACE_IMPL_END - -#include "bool/kit/kit.h" - -ABC_NAMESPACE_IMPL_START - -void Dar_ManPrintScript() -{ - unsigned pCanons[222]; - int i; - Dar_LibReturnCanonicals( pCanons ); - for ( i = 1; i < 222; i++ ) - { - Kit_DsdNtk_t * pNtk; - pNtk = Kit_DsdDecompose( pCanons + i, 4 ); - printf( " \"" ); - Kit_DsdPrint( stdout, pNtk ); - printf( "\", /* %3d */\n", i ); - Kit_DsdNtkFree( pNtk ); - } -} -#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index f8508d53db..4dfa6bf2b1 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -151,240 +151,6 @@ static inline int Dss_Lit2Lit( int * pMapLit, int Lit ) { return Abc_Var2Lit( /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#if 0 - -/**Function************************************************************* - - Synopsis [Check decomposability for 666.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -// recursively collects 6-feasible supports -int Dss_ObjCheck666_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, Vec_Int_t * vSupps ) -{ - Dss_Obj_t * pFanin; - int i, uSupp = 0; - assert( !Dss_IsComplement(pObj) ); - if ( pObj->Type == DAU_DSD_VAR ) - { - assert( pObj->iVar >= 0 && pObj->iVar < 30 ); - return (1 << pObj->iVar); - } - if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR ) - { - int c0, c1, c2, uSuppTemp; - int uSuppVars[16]; - int nSuppVars = 0; - int nFanins = Dss_ObjFaninNum(pObj); - int uSupps[16], nSuppSizes[16]; - Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i ) - { - uSupps[i] = Dss_ObjCheck666_rec( p, pFanin, vSupps ); - nSuppSizes[i] = Dss_WordCountOnes( uSupps[i] ); - uSupp |= uSupps[i]; - if ( nSuppSizes[i] == 1 ) - uSuppVars[nSuppVars++] = uSupps[i]; - } - // iterate through the permutations - for ( c0 = 0; c0 < nFanins; c0++ ) - if ( nSuppSizes[c0] > 1 && nSuppSizes[c0] < 6 ) - { - uSuppTemp = uSupps[c0]; - for ( i = 0; i < nSuppVars; i++ ) - if ( nSuppSizes[c0] + i < 6 ) - uSuppTemp |= uSuppVars[i]; - else - break; - if ( Dss_WordCountOnes(uSuppTemp) <= 6 ) - Vec_IntPush( vSupps, uSuppTemp ); - - for ( c1 = c0 + 1; c1 < nFanins; c1++ ) - if ( nSuppSizes[c1] > 1 && nSuppSizes[c1] < 6 ) - { - if ( nSuppSizes[c0] + nSuppSizes[c1] <= 6 ) - Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] ); - - uSuppTemp = uSupps[c0] | uSupps[c1]; - for ( i = 0; i < nSuppVars; i++ ) - if ( nSuppSizes[c0] + nSuppSizes[c1] + i < 6 ) - uSuppTemp |= uSuppVars[i]; - else - break; - if ( Dss_WordCountOnes(uSuppTemp) <= 6 ) - Vec_IntPush( vSupps, uSuppTemp ); - - for ( c2 = c1 + 1; c2 < nFanins; c2++ ) - if ( nSuppSizes[c2] > 1 && nSuppSizes[c2] < 6 ) - { - if ( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] <= 6 ) - Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] | uSupps[c2] ); - assert( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] >= 6 ); - } - } - } - if ( nSuppVars > 1 && nSuppVars <= 6 ) - { - uSuppTemp = 0; - for ( i = 0; i < nSuppVars; i++ ) - uSuppTemp |= uSuppVars[i]; - Vec_IntPush( vSupps, uSuppTemp ); - } - else if ( nSuppVars > 6 && nSuppVars <= 12 ) - { - uSuppTemp = 0; - for ( i = 0; i < 6; i++ ) - uSuppTemp |= uSuppVars[i]; - Vec_IntPush( vSupps, uSuppTemp ); - - uSuppTemp = 0; - for ( i = 6; i < nSuppVars; i++ ) - uSuppTemp |= uSuppVars[i]; - Vec_IntPush( vSupps, uSuppTemp ); - } - } - else if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME ) - { - Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i ) - uSupp |= Dss_ObjCheck666_rec( p, pFanin, vSupps ); - } - if ( Dss_WordCountOnes( uSupp ) <= 6 ) - Vec_IntPush( vSupps, uSupp ); - return uSupp; -} -int Dss_ObjCheck666( Dss_Ntk_t * p ) -{ - Vec_Int_t * vSupps; - int i, k, SuppI, SuppK; - int nSupp = Dss_ObjSuppSize(Dss_Regular(p->pRoot)); - if ( nSupp <= 6 ) - return 1; - // compute supports - vSupps = Vec_IntAlloc( 100 ); - Dss_ObjCheck666_rec( p, Dss_Regular(p->pRoot), vSupps ); - Vec_IntUniqify( vSupps ); - Vec_IntForEachEntry( vSupps, SuppI, i ) - { - k = Dss_WordCountOnes(SuppI); - assert( k > 0 && k <= 6 ); -/* - for ( k = 0; k < 16; k++ ) - if ( (SuppI >> k) & 1 ) - printf( "%c", 'a' + k ); - else - printf( "-" ); - printf( "\n" ); -*/ - } - // consider support pairs - Vec_IntForEachEntry( vSupps, SuppI, i ) - Vec_IntForEachEntryStart( vSupps, SuppK, k, i+1 ) - { - if ( SuppI & SuppK ) - continue; - if ( Dss_WordCountOnes(SuppI | SuppK) + 4 >= nSupp ) - { - Vec_IntFree( vSupps ); - return 1; - } - } - Vec_IntFree( vSupps ); - return 0; -} -void Dau_DsdTest_() -{ -/* - extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth ); - extern void Dss_NtkFree( Dss_Ntk_t * p ); - -// char * pDsd = "(!(amn!(bh))[cdeij]!(fklg)o)"; - char * pDsd = "<[(ab)(cd)(ef)][(gh)(ij)(kl)](mn)>"; - Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, 16, NULL ); - int Status = Dss_ObjCheck666( pNtk ); - Dss_NtkFree( pNtk ); -*/ -} - -abctime if_dec_time; - -void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves ) -{ - extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth ); - extern void Dss_NtkFree( Dss_Ntk_t * p ); - - static abctime timeTt = 0; - static abctime timeDsd = 0; - abctime clkTt, clkDsd; - - char pDsd[1000]; - word Truth[1024]; - Dss_Ntk_t * pNtk; - int Status, nNonDec; - - if ( pTruth == NULL ) - { - Abc_PrintTime( 1, "TT runtime", timeTt ); - Abc_PrintTime( 1, "DSD runtime", timeDsd ); - Abc_PrintTime( 1, "Total ", if_dec_time ); - - if_dec_time = 0; - timeTt = 0; - timeDsd = 0; - return; - } - - Abc_TtCopy( Truth, pTruth, Abc_TtWordNum(nVars), 0 ); - nNonDec = Dau_DsdDecompose( Truth, nVars, 0, 0, pDsd ); - if ( nNonDec > 0 ) - return; - - pNtk = Dss_NtkCreate( pDsd, 16, NULL ); - - // measure DSD runtime - clkDsd = Abc_Clock(); - Status = Dss_ObjCheck666( pNtk ); - timeDsd += Abc_Clock() - clkDsd; - - Dss_NtkFree( pNtk ); - - // measure TT runtime - clkTt = Abc_Clock(); - { - #define CLU_VAR_MAX 16 - - // decomposition - typedef struct If_Grp_t_ If_Grp_t; - struct If_Grp_t_ - { - char nVars; - char nMyu; - char pVars[CLU_VAR_MAX]; - }; - - - int nLutLeaf = 6; - int nLutLeaf2 = 6; - int nLutRoot = 6; - - If_Grp_t G; - If_Grp_t G2, R; - word Func0, Func1, Func2; - - { - extern If_Grp_t If_CluCheck3( void * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, - If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 ); - G = If_CluCheck3( NULL, pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 ); - } - - } - timeTt += Abc_Clock() - clkTt; -} - -#endif /**Function************************************************************* diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c index dda0c8cb87..9ccaf24e9d 100644 --- a/src/proof/abs/absRef.c +++ b/src/proof/abs/absRef.c @@ -85,170 +85,6 @@ extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#if 0 - -/**Function************************************************************* - - Synopsis [Performs UNSAT-core-based refinement.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManRefineCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisited, Vec_Int_t * vFlops ) -{ - Vec_Int_t * vLeaves; - Gia_Obj_t * pFanin; - int k; - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - if ( Gia_ObjIsCi(pObj) ) - { - if ( Gia_ObjIsRo(p, pObj) ) - Vec_IntPush( vFlops, Gia_ObjId(p, pObj) ); - return; - } - assert( Gia_ObjIsAnd(pObj) ); - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) - Rnm_ManRefineCollect_rec( p, pFanin, vVisited, vFlops ); - Vec_IntPush( vVisited, Gia_ObjId(p, pObj) ); -} - -Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs ) -{ - Vec_Int_t * vCnf0, * vCnf1; - Vec_Int_t * vLeaves, * vLits, * vPpi2Map; - Vec_Int_t * vVisited, * vFlops, * vCore, * vCoreFinal; - Gia_Obj_t * pObj, * pFanin; - int i, k, f, Status, Entry, pLits[5], iBit = p->pCex->nRegs; - // map PPIs into their positions in the map // CAN BE MADE FASTER - vPpi2Map = Vec_IntAlloc( Vec_IntSize(vPPIs) ); - Vec_IntForEachEntry( vPPIs, Entry, i ) - { - Entry = Vec_IntFind( p->vMap, Entry ); - assert( Entry >= 0 ); - Vec_IntPush( vPpi2Map, Entry ); - } - // collect nodes between selected PPIs and CIs - vFlops = Vec_IntAlloc( 100 ); - vVisited = Vec_IntAlloc( 100 ); - Gia_ManIncrementTravId( p->pGia ); - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) -// if ( !Gia_ObjIsRo(p->pGia, pObj) ) // SKIP PPIs that are flops - Rnm_ManRefineCollect_rec( p->pGia, pObj, vVisited, vFlops ); - // create SAT variables and SAT solver - Vec_IntFill( p->vSat2Ids, 1, -1 ); - assert( p->pSat == NULL ); - p->pSat = sat_solver2_new(); - Vec_IntFill( p->vSatVars, Gia_ManObjNum(p->pGia), 0 ); // NO NEED TO CLEAN EACH TIME - // assign PPI variables - Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) - Rnm_ObjFindOrAddSatVar( p, pObj ); - // assign other variables - Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) - { - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - pLits[k] = Rnm_ObjFindOrAddSatVar( p, pFanin ); - vCnf0 = Ga2_ManCnfCompute( Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); - vCnf1 = Ga2_ManCnfCompute( ~Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); - Ga2_ManCnfAddStatic( p->pSat, vCnf0, vCnf1, pLits, Rnm_ObjFindOrAddSatVar(p, pObj), Rnm_ObjFindOrAddSatVar(p, pObj)/2 ); - Vec_IntFree( vCnf0 ); - Vec_IntFree( vCnf1 ); - } - -// printf( "\n" ); - - p->pSat->pPrf2 = Prf_ManAlloc(); - Prf_ManRestart( p->pSat->pPrf2, NULL, sat_solver2_nlearnts(p->pSat), Vec_IntSize(p->vSat2Ids) ); - - // iterate UNSAT core computation for each timeframe - vLits = Vec_IntAlloc( 100 ); - vCoreFinal = Vec_IntAlloc( 100 ); - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - // collect values of PPIs in this timeframe - Vec_IntClear( vLits ); - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) - { - Entry = Abc_InfoHasBit( p->pCex->pData, iBit + Vec_IntEntry(vPpi2Map, i) ); - Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), !Entry ) ); - } - - // handle the first timeframe in a special vay - if ( f == 0 ) - Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) - if ( Vec_IntFind( vPPIs, Gia_ObjId(p->pGia, pObj) ) == -1 ) - Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), 1 ) ); -/* - // uniqify literals and detect special conflicts - Vec_IntUniqify( vLits ); - Vec_IntForEachEntryStart( vLits, Entry, i, 1 ) - if ( Vec_IntEntry(vLits, i-1) == Abc_LitNot(Entry) ) - break; - if ( i < Vec_IntSize(vLits) ) - printf( "triv_unsat " ); - else -*/ - - Status = sat_solver2_solve( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( Status != l_False ) - continue; - vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); -// vCore = Vec_IntAlloc( 0 ); - // add to the UNSAT core - Vec_IntAppend( vCoreFinal, vCore ); - -// printf( "Frame %d : ", f ); -// Vec_IntPrint( vCore ); - Vec_IntFree( vCore ); - } - assert( iBit == p->pCex->nBits ); - Vec_IntUniqify( vCoreFinal ); - Vec_IntFree( vLits ); - Prf_ManStopP( &p->pSat->pPrf2 ); - sat_solver2_delete( p->pSat ); - p->pSat = NULL; - - // translate from entry into ID - Vec_IntForEachEntry( vCoreFinal, Entry, i ) - { - assert( Vec_IntEntry(p->vSat2Ids, Entry) >= 0 ); - assert( Vec_IntEntry(p->vSat2Ids, Entry) < Gia_ManObjNum(p->pGia) ); - Vec_IntWriteEntry( vCoreFinal, i, Vec_IntEntry(p->vSat2Ids, Entry) ); - } - // if there are flop outputs, add them - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) - if ( Gia_ObjIsRo(p->pGia, pObj) ) - Vec_IntPush( vCoreFinal, Gia_ObjId(p->pGia, pObj) ); - Vec_IntUniqify( vCoreFinal ); - -// printf( "\n" ); -// Vec_IntPrint( vPPIs ); -// Vec_IntPrint( vCoreFinal ); - -// printf( "\n" ); - - // clean SAT variable numbers - Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) - { - Rnm_ObjSetSatVar( p, pObj, 0 ); - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - Rnm_ObjSetSatVar( p, pFanin, 0 ); - } - Vec_IntFree( vFlops ); - Vec_IntFree( vVisited ); - Vec_IntFree( vPpi2Map ); - return vCoreFinal; -} - -#endif /**Function************************************************************* diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 5e5ca68866..6f9dfa997d 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -195,43 +195,6 @@ static inline int Ree_ManCutTruth( Gia_Obj_t * pObj, int * pCut0, int * pCut1, i return 0xFF & (Gia_ObjIsXor(pObj) ? Truth0 ^ Truth1 : Truth0 & Truth1); } -#if 0 - -int Ree_ObjComputeTruth_rec( Gia_Obj_t * pObj ) -{ - int Truth0, Truth1; - if ( pObj->Value ) - return pObj->Value; - assert( Gia_ObjIsAnd(pObj) ); - Truth0 = Ree_ObjComputeTruth_rec( Gia_ObjFanin0(pObj) ); - Truth1 = Ree_ObjComputeTruth_rec( Gia_ObjFanin1(pObj) ); - if ( Gia_ObjIsXor(pObj) ) - return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) ^ (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); - else - return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) & (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); -} -void Ree_ObjCleanTruth_rec( Gia_Obj_t * pObj ) -{ - if ( !pObj->Value ) - return; - pObj->Value = 0; - if ( !Gia_ObjIsAnd(pObj) ) - return; - Ree_ObjCleanTruth_rec( Gia_ObjFanin0(pObj) ); - Ree_ObjCleanTruth_rec( Gia_ObjFanin1(pObj) ); -} -int Ree_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut ) -{ - unsigned Truth, Truths[3] = { 0xAA, 0xCC, 0xF0 }; int i; - for ( i = 1; i <= pCut[0]; i++ ) - Gia_ManObj(p, pCut[i])->Value = Truths[i-1]; - Truth = 0xFF & Ree_ObjComputeTruth_rec( Gia_ManObj(p, iObj) ); - Ree_ObjCleanTruth_rec( Gia_ManObj(p, iObj) ); - return Truth; -} - -#endif - /**Function************************************************************* Synopsis [] diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index e2fa8ff1da..8b9de8b0c0 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -54,84 +54,6 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#if 0 // BDD code - -/**Function************************************************************* - - Synopsis [Permute primary inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip ) -{ - abctime clk = Abc_Clock(); - DdManager * dd; - DdNode * bBdd, * bBdd0, * bBdd1; - Vec_Ptr_t * vNodes; - Gia_Obj_t * pObj; - int i; - vNodes = Vec_PtrStart( Gia_ManObjNum(p) ); - dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); -// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd ); - Vec_PtrWriteEntry( vNodes, 0, bBdd ); - Gia_ManForEachPi( p, pObj, i ) - { - bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd ); - Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); - } - Gia_ManForEachAnd( p, pObj, i ) - { - bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) ); - bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) ); - bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd ); - Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); - if ( i % 10 == 0 ) - printf( "%d ", i ); -// if ( i == 3000 ) -// break; - } - printf( "\n" ); - Gia_ManForEachPo( p, pObj, i ) - { - bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) ); Cudd_Ref( bBdd ); - Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); - } - if ( bBdd == Cudd_ReadLogicZero(dd) ) - printf( "Equivalent!\n" ); - else - printf( "Not tquivalent!\n" ); - if ( pvNodes ) - *pvNodes = vNodes; - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - return dd; -} -void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes ) -{ - DdNode * bBdd; - int i; - Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i ) - if ( bBdd ) - Cudd_RecursiveDeref( dd, bBdd ); - if ( Cudd_CheckZeroRef(dd) > 0 ) - printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) ); - Cudd_PrintInfo( dd, stdout ); - Cudd_Quit( dd ); -} -void Gia_ManBuildBddTest( Gia_Man_t * p ) -{ - Vec_Ptr_t * vNodes; - DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 ); - Gia_ManDerefBdd( dd, vNodes ); -} - -#endif // BDD code - /**Function************************************************************* Synopsis [] diff --git a/src/proof/live/disjunctiveMonotone.c b/src/proof/live/disjunctiveMonotone.c index 505af77439..ca627da327 100644 --- a/src/proof/live/disjunctiveMonotone.c +++ b/src/proof/live/disjunctiveMonotone.c @@ -385,58 +385,6 @@ Vec_Int_t *createSingletonIntVector( int iElem ) return myVec; } -#if 0 -Vec_Ptr_t *generateDisjuntiveMonotone_rec() -{ - nextLevelSignals = ; - if level is not exhausted - for all x \in nextLevelSignals - { - append x in currAntecendent - recond it as a monotone predicate - resurse with level - 1 - } -} -#endif - -#if 0 -Vec_Ptr_t *generateDisjuntiveMonotoneLevels(Aig_Man_t *pAig, - struct aigPoIndices *aigPoIndicesInstance, - struct antecedentConsequentVectorsStruct *anteConsecInstanceOrig, - int level ) -{ - Vec_Int_t *firstLevelMonotone; - Vec_Int_t *currVecInt; - Vec_Ptr_t *hierarchyList; - int iElem, i; - - assert( level >= 1 ); - firstLevelMonotone = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance ); - if( firstLevelMonotone == NULL || Vec_IntSize(firstLevelMonotone) <= 0 ) - return NULL; - - hierarchyList = Vec_PtrAlloc(Vec_IntSize(firstLevelMonotone)); - - Vec_IntForEachEntry( firstLevelMonotone, iElem, i ) - { - currVecInt = createSingletonIntVector( iElem ); - Vec_PtrPush( hierarchyList, currVecInt ); - } - - if( level > 1 ) - { - Vec_IntForEachEntry( firstLevelMonotone, iElem, i ) - { - currVecInt = (Vec_Int_t *)Vec_PtrEntry( hierarchyList, i ); - - - } - } - - return hierarchyList; -} -#endif - int Vec_IntPushUniqueLocal( Vec_Int_t * p, int Entry ) { int i; diff --git a/src/proof/live/kliveness.c b/src/proof/live/kliveness.c index d9bc416b6d..6c9f489702 100644 --- a/src/proof/live/kliveness.c +++ b/src/proof/live/kliveness.c @@ -60,26 +60,6 @@ extern Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t * #define kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3 #define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4 -//unused function -#if 0 -Aig_Obj_t *readTargetPinSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk) -{ - Aig_Obj_t *pObj; - int i; - - Saig_ManForEachPo( pAig, pObj, i ) - { - if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "0Liveness_" ) != NULL ) - { - //return Aig_ObjFanin0(pObj); - return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); - } - } - - return NULL; -} -#endif - Aig_Obj_t *readLiveSignal_0( Aig_Man_t *pAig, int liveIndex_0 ) { Aig_Obj_t *pObj; @@ -96,82 +76,6 @@ Aig_Obj_t *readLiveSignal_k( Aig_Man_t *pAig, int liveIndex_k ) return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); } -//unused funtion -#if 0 -Aig_Obj_t *readTargetPoutSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int nonFirstIteration) -{ - Aig_Obj_t *pObj; - int i; - - if( nonFirstIteration == 0 ) - return NULL; - else - Saig_ManForEachPo( pAig, pObj, i ) - { - if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "kLiveness_" ) != NULL ) - { - //return Aig_ObjFanin0(pObj); - return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)); - } - } - - return NULL; -} -#endif - -//unused function -#if 0 -void updateNewNetworkNameManager_kCS( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, - Vec_Ptr_t *vLoNames, Vec_Ptr_t *vPoNames, Vec_Ptr_t *vLiNames ) -{ - Aig_Obj_t *pObj; - Abc_Obj_t *pNode; - int i, ntkObjId; - - pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) ); - - if( vPiNames ) - { - Saig_ManForEachPi( pAig, pObj, i ) - { - ntkObjId = Abc_NtkCi( pNtk, i )->Id; - Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL ); - } - } - if( vLoNames ) - { - Saig_ManForEachLo( pAig, pObj, i ) - { - ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id; - Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL ); - } - } - - if( vPoNames ) - { - Saig_ManForEachPo( pAig, pObj, i ) - { - ntkObjId = Abc_NtkCo( pNtk, i )->Id; - Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPoNames, i), NULL ); - } - } - - if( vLiNames ) - { - Saig_ManForEachLi( pAig, pObj, i ) - { - ntkObjId = Abc_NtkCo( pNtk, Saig_ManPoNum( pAig ) + i )->Id; - Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLiNames, i), NULL ); - } - } - - // assign latch input names - Abc_NtkForEachLatch(pNtk, pNode, i) - if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL ) - Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL ); -} -#endif - Aig_Man_t *introduceAbsorberLogic( Aig_Man_t *pAig, int *pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration ) { Aig_Man_t *pNewAig; @@ -405,23 +309,6 @@ int flipConePdr( Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int return RetValue; } -//unused function -#if 0 -int read0LiveIndex( Abc_Ntk_t *pNtk ) -{ - Abc_Obj_t *pObj; - int i; - - Abc_NtkForEachPo( pNtk, pObj, i ) - { - if( strstr( Abc_ObjName( pObj ), "0Liveness_" ) != NULL ) - return i; - } - - return -1; -} -#endif - int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk) { Abc_Obj_t *pObj; diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index a40671604f..689c522e4e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -459,140 +459,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) return RetValue; } -#if 0 - -/**Function************************************************************* - - Synopsis [Performs one resultion step.] - - Description [Returns ID of the resolvent if success, and -1 if failure.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_ProofCheckResolveOne( Vec_Set_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) -{ - satset * c; - int h, i, k, Var = -1, Count = 0; - // find resolution variable - for ( i = 0; i < (int)c1->nEnts; i++ ) - for ( k = 0; k < (int)c2->nEnts; k++ ) - if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) - { - Var = (c1->pEnts[i] >> 1); - Count++; - } - if ( Count == 0 ) - { - printf( "Cannot find resolution variable\n" ); - return 0; - } - if ( Count > 1 ) - { - printf( "Found more than 1 resolution variables\n" ); - return 0; - } - // perform resolution - Vec_IntClear( vTemp ); - Vec_IntPush( vTemp, 0 ); // placeholder - Vec_IntPush( vTemp, 0 ); - for ( i = 0; i < (int)c1->nEnts; i++ ) - if ( (c1->pEnts[i] >> 1) != Var ) - Vec_IntPush( vTemp, c1->pEnts[i] ); - for ( i = 0; i < (int)c2->nEnts; i++ ) - if ( (c2->pEnts[i] >> 1) != Var ) - Vec_IntPushUnique( vTemp, c2->pEnts[i] ); - // create new resolution entry - h = Vec_SetAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) ); - // return the new entry - c = Proof_NodeRead( p, h ); - c->nEnts = Vec_IntSize(vTemp)-2; - return h; -} - -/**Function************************************************************* - - Synopsis [Checks the proof for consitency.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Set_t * vResolves, int iAnt ) -{ - satset * pAnt; - if ( iAnt & 1 ) - return Proof_ClauseRead( vClauses, iAnt >> 2 ); - assert( iAnt > 0 ); - pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); - assert( pAnt->Id > 0 ); - return Proof_NodeRead( vResolves, pAnt->Id ); -} - -/**Function************************************************************* - - Synopsis [Checks the proof for consitency.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_ProofCheck( sat_solver2 * s ) -{ - Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; - Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; - Vec_Set_t * vResolves; - Vec_Int_t * vUsed, * vTemp; - satset * pSet, * pSet0 = NULL, * pSet1; - int i, k, hRoot, Handle, Counter = 0; - abctime clk = Abc_Clock(); - hRoot = s->hProofLast; - if ( hRoot == -1 ) - return; - // collect visited clauses - vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); - Proof_CleanCollected( vProof, vUsed ); - // perform resolution steps - vTemp = Vec_IntAlloc( 1000 ); - vResolves = Vec_SetAlloc( 20 ); - Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) - { - Handle = -1; - pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < (int)pSet->nEnts; k++ ) - { - pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - Handle = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp ); - pSet0 = Proof_NodeRead( vResolves, Handle ); - } - pSet->Id = Handle; - Counter++; - } - Vec_IntFree( vTemp ); - // clean the proof - Proof_CleanCollected( vProof, vUsed ); - // compare the final clause - printf( "Used %6.2f MB for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) ); - if ( pSet0->nEnts > 0 ) - printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts ); - else - printf( "Proof verification successful. " ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - // cleanup - Vec_SetFree( vResolves ); - Vec_IntFree( vUsed ); -} -#endif - /**Function************************************************************* Synopsis [Collects nodes belonging to the UNSAT core.] @@ -634,271 +500,6 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed ) return vCore; } -#if 0 - -/**Function************************************************************* - - Synopsis [Verifies that variables are labeled correctly.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars ) -{ - satset* c; - Vec_Int_t * vVarMap; - int i, k, Entry, * pMask; - int Counts[5] = {0}; - // map variables into their type (A, B, or AB) - vVarMap = Vec_IntStart( s->size ); - sat_solver_foreach_clause( s, c, i ) - for ( k = 0; k < (int)c->nEnts; k++ ) - *Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA; - // analyze variables - Vec_IntForEachEntry( vGloVars, Entry, i ) - { - pMask = Vec_IntEntryP(vVarMap, Entry); - assert( *pMask >= 0 && *pMask <= 3 ); - Counts[(*pMask & 3)]++; - *pMask = 0; - } - // count the number of global variables not listed - Vec_IntForEachEntry( vVarMap, Entry, i ) - if ( Entry == 3 ) - Counts[4]++; - Vec_IntFree( vVarMap ); - // report - if ( Counts[0] ) - printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] ); - if ( Counts[1] ) - printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] ); - if ( Counts[2] ) - printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] ); - if ( Counts[3] ) - printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) ); - if ( Counts[4] ) - printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] ); -} - -/**Function************************************************************* - - Synopsis [Computes interpolant of the proof.] - - Description [Aassuming that vars/clause of partA are marked.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) -{ - Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; - Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; - Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; - Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; - satset * pNode, * pFanin; - Aig_Man_t * pAig; - Aig_Obj_t * pObj = NULL; - int i, k, iVar, Lit, Entry, hRoot; -// if ( s->hLearntLast < 0 ) -// return NULL; -// hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; - hRoot = s->hProofLast; - if ( hRoot == -1 ) - return NULL; - - Sat_ProofInterpolantCheckVars( s, vGlobVars ); - - // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); - // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vProof, vUsed ); - // vCore arrived in terms of clause handles - - // map variables into their global numbers - vVarMap = Vec_IntStartFull( s->size ); - Vec_IntForEachEntry( vGlobVars, Entry, i ) - Vec_IntWriteEntry( vVarMap, Entry, i ); - - // start the AIG - pAig = Aig_ManStart( 10000 ); - pAig->pName = Abc_UtilStrsav( "interpol" ); - for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) - Aig_ObjCreateCi( pAig ); - - // copy the numbers out and derive interpol for clause - vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); - Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) - { - if ( pNode->partA ) - { - pObj = Aig_ManConst0( pAig ); - satset_foreach_lit( pNode, Lit, k, 0 ) - if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 ) - pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) ); - } - else - pObj = Aig_ManConst1( pAig ); - // remember the interpolant - Vec_IntPush( vCoreNums, pNode->Id ); - pNode->Id = Aig_ObjToLit(pObj); - } - Vec_IntFree( vVarMap ); - - // copy the numbers out and derive interpol for resolvents - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - { -// satset_print( pNode ); - assert( pNode->nEnts > 1 ); - Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) - { - assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); - if ( k == 0 ) - pObj = Aig_ObjFromLit( pAig, pFanin->Id ); - else if ( pNode->pEnts[k] & 2 ) // variable of A - pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - else - pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - } - // remember the interpolant - pNode->Id = Aig_ObjToLit(pObj); - } - // save the result -// assert( Proof_NodeHandle(vProof, pNode) == hRoot ); - Aig_ObjCreateCo( pAig, pObj ); - Aig_ManCleanup( pAig ); - - // move the results back - Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) - pNode->Id = Vec_IntEntry( vCoreNums, i ); - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - pNode->Id = 0; - // cleanup - Vec_IntFree( vCore ); - Vec_IntFree( vUsed ); - Vec_IntFree( vCoreNums ); - return pAig; -} - - -/**Function************************************************************* - - Synopsis [Computes interpolant of the proof.] - - Description [Aassuming that vars/clause of partA are marked.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) -{ - Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; - Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs; - Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; - Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; - Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; - satset * pNode, * pFanin; - Tru_Man_t * pTru; - int nVars = Vec_IntSize(vGlobVars); - int nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); - word * pRes = ABC_ALLOC( word, nWords ); - int i, k, iVar, Lit, Entry, hRoot; - assert( nVars > 0 && nVars <= 16 ); - hRoot = s->hProofLast; - if ( hRoot == -1 ) - return NULL; - - Sat_ProofInterpolantCheckVars( s, vGlobVars ); - - // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); - // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vProof, vUsed, 0 ); - // vCore arrived in terms of clause handles - - // map variables into their global numbers - vVarMap = Vec_IntStartFull( s->size ); - Vec_IntForEachEntry( vGlobVars, Entry, i ) - Vec_IntWriteEntry( vVarMap, Entry, i ); - - // start the AIG - pTru = Tru_ManAlloc( nVars ); - - // copy the numbers out and derive interpol for clause - vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); - Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) - { - if ( pNode->partA ) - { -// pObj = Aig_ManConst0( pAig ); - Tru_ManClear( pRes, nWords ); - satset_foreach_lit( pNode, Lit, k, 0 ) - if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 ) -// pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) ); - pRes = Tru_ManOrNotCond( pRes, Tru_ManVar(pTru, iVar), nWords, lit_sign(Lit) ); - } - else -// pObj = Aig_ManConst1( pAig ); - Tru_ManFill( pRes, nWords ); - // remember the interpolant - Vec_IntPush( vCoreNums, pNode->Id ); -// pNode->Id = Aig_ObjToLit(pObj); - pNode->Id = Tru_ManInsert( pTru, pRes ); - } - Vec_IntFree( vVarMap ); - - // copy the numbers out and derive interpol for resolvents - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - { -// satset_print( pNode ); - assert( pNode->nEnts > 1 ); - Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) - { -// assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); -// assert( pFanin->Id <= Tru_ManHandleMax(pTru) ); - if ( k == 0 ) -// pObj = Aig_ObjFromLit( pAig, pFanin->Id ); - pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); - else if ( pNode->pEnts[k] & 2 ) // variable of A -// pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - pRes = Tru_ManOrNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); - else -// pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - pRes = Tru_ManAndNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); - } - // remember the interpolant -// pNode->Id = Aig_ObjToLit(pObj); - pNode->Id = Tru_ManInsert( pTru, pRes ); - } - // save the result -// assert( Proof_NodeHandle(vProof, pNode) == hRoot ); -// Aig_ObjCreateCo( pAig, pObj ); -// Aig_ManCleanup( pAig ); - - // move the results back - Proof_ForeachClauseVec( vCore, vClauses, pNode, i ) - pNode->Id = Vec_IntEntry( vCoreNums, i ); - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - pNode->Id = 0; - // cleanup - Vec_IntFree( vCore ); - Vec_IntFree( vUsed ); - Vec_IntFree( vCoreNums ); - Tru_ManFree( pTru ); -// ABC_FREE( pRes ); - return pRes; -} - -#endif - /**Function************************************************************* Synopsis [Computes UNSAT core.] diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c index 8cb86f875c..dc99f31e8c 100644 --- a/src/sat/cnf/cnfCore.c +++ b/src/sat/cnf/cnfCore.c @@ -222,63 +222,6 @@ Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin ) return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin ); } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig ) -{ -/* - // iteratively improve area flow - for ( i = 0; i < nIters; i++ ) - { -clk = Abc_Clock(); - Cnf_ManScanMapping( p, 0 ); - Cnf_ManMapForCnf( p ); -ABC_PRT( "iter ", Abc_Clock() - clk ); - } -*/ - // write the file - vMapped = Aig_ManScanMapping( p, 1 ); - Vec_PtrFree( vMapped ); - -clk = Abc_Clock(); - Cnf_ManTransferCuts( p ); - - Cnf_ManPostprocess( p ); - Cnf_ManScanMapping( p, 0 ); -/* - Cnf_ManPostprocess( p ); - Cnf_ManScanMapping( p, 0 ); - Cnf_ManPostprocess( p ); - Cnf_ManScanMapping( p, 0 ); -*/ -ABC_PRT( "Ext ", Abc_Clock() - clk ); - -/* - vMapped = Cnf_ManScanMapping( p, 1 ); - pCnf = Cnf_ManWriteCnf( p, vMapped ); - Vec_PtrFree( vMapped ); - - // clean up - Cnf_ManFreeCuts( p ); - Dar_ManCutsFree( pAig ); - return pCnf; -*/ - Aig_MmFixedStop( pMemCuts, 0 ); - return NULL; -} - -#endif //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/cnf/cnfData.c b/src/sat/cnf/cnfData.c index 3d3cdf37aa..eba9d1cffc 100644 --- a/src/sat/cnf/cnfData.c +++ b/src/sat/cnf/cnfData.c @@ -4604,182 +4604,6 @@ void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops ) } } -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManDeriveCnfTest() -{ - int i, k, Lit; - printf( "\n" ); - for ( i = 80; i >= 0; i-- ) - { - Lit = i; - for ( k = 0; k < 4; k++ ) - { - if ( Lit % 3 == 0 ) - printf( "%c", 'A' + k ); - else if ( Lit % 3 == 1 ) - printf( "%c", 'a' + k ); - Lit = Lit / 3; - } - printf( "\n" ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManDeriveCnfTest2() -{ - char s_Data3[81] = "!#&()*+,-.0123456789:;<=>?ABCDEFGHIJKLMNOPQRSTUVWXYZ[]abcdefghijklmnopqrstuvwxyz|"; - - unsigned uMasks[4][2] = { - { 0x5555, 0xAAAA }, - { 0x3333, 0xCCCC }, - { 0x0F0F, 0xF0F0 }, - { 0x00FF, 0xFF00 } - }; - char Buffer[100], * pCur; - FILE * pFile; - int CountCur, Counter = 0, nLines = 0; - int pLines[1<<16] = {0}; - int pNums[1<<16] = {0}; - unsigned uTruth, uTruth2, uCube, cCube; - char * pSops[1<<16] = {0}; - char Sop[10]; - char Cube[4]; - int i, k; - - pFile = fopen( "cands2.txt", "r" ); - while ( fgets( Buffer, 100, pFile ) ) - { - if ( Buffer[0] == '0' ) - Extra_ReadHexadecimal( &uTruth2, Buffer+2, 4 ); - else - uTruth2 = 0xFFFFFF; - - // skip all chars till a-d or A-D - if ( Buffer[0] == '0' ) - for ( pCur = Buffer; *pCur != '\n'; pCur++ ) - { -// if ( *pCur >= 'a' && *pCur <= 'd' || *pCur >= 'A' && *pCur <= 'D' ) - if ( *pCur == ':' ) - { - pCur++; - break; - } - } - else - pCur = Buffer; - - - uTruth = 0; - CountCur = 0; - uCube = 0xFFFF; - for ( i = 0; i < 4; i++ ) - Cube[i] = 2; - - for ( ; *pCur; pCur++ ) - { - if ( *pCur == '+' || *pCur == '\n' ) - { - uTruth |= uCube; - uCube = 0xFFFF; - - // get the cube - cCube = 0; - for ( i = 0; i < 4; i++ ) - cCube = 3 * cCube + Cube[i]; - for ( i = 0; i < 4; i++ ) - Cube[i] = 2; - - assert( cCube >= 0 && cCube < 81 ); - Sop[CountCur] = cCube; - CountCur++; - if ( *pCur == '\n' ) - { - Sop[CountCur] = 0; - break; - } - } - else if ( *pCur >= 'a' && *pCur <= 'd' ) - { - uCube &= uMasks[*pCur-'a'][1]; - Cube[*pCur-'a'] = 1; - } - else if ( *pCur >= 'A' && *pCur <= 'D' ) - { - uCube &= uMasks[*pCur-'A'][0]; - Cube[*pCur-'A'] = 0; - } - } - assert( *pCur == '\n' ); - assert( uTruth2 == 0xFFFFFF || uTruth2 == uTruth ); - - Counter += CountCur; - pNums[uTruth] = CountCur; - pSops[uTruth] = ALLOC( char, CountCur ); - memcpy( pSops[uTruth], Sop, CountCur ); - pLines[nLines++] = Counter; - } - fclose( pFile ); - - printf( "Lines = %d. Counter = %d.\n", nLines, Counter ); - -/* - // write the number of cubes - for ( i = 0; i < 65536; i++ ) - printf( "%d,%d ", pNums[i], pNums[i] + pNums[0xffff & ~i] ); - printf( "\n" ); -*/ - - // write the number of cubes - Counter = 0; - for ( i = 1; i < 65536; i++ ) - { - CountCur = pNums[i]; - assert( CountCur > 0 ); - for ( k = 0; k <= CountCur; k++ ) - { - if ( k < CountCur ) - { - assert( pSops[i][k] >= 0 && pSops[i][k] < 81 ); - printf( "%c", s_Data3[pSops[i][k]] ); - } - else - printf( " " ); - if ( ++Counter == 75 ) - { - printf( "\",\n\"" ); - Counter = 0; - } - } - } - printf( "\n" ); - - return 1; -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/cnf/cnfMap.c b/src/sat/cnf/cnfMap.c index a634547172..35a9ac2af1 100644 --- a/src/sat/cnf/cnfMap.c +++ b/src/sat/cnf/cnfMap.c @@ -151,208 +151,6 @@ void Cnf_DeriveMapping( Cnf_Man_t * p ) } - -#if 0 - -/**Function************************************************************* - - Synopsis [Computes area of the first level.] - - Description [The cut need to be derefed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_CutDeref( Aig_Man_t * p, Dar_Cut_t * pCut ) -{ - Aig_Obj_t * pLeaf; - int i; - Dar_CutForEachLeaf( p, pCut, pLeaf, i ) - { - assert( pLeaf->nRefs > 0 ); - if ( --pLeaf->nRefs > 0 || !Aig_ObjIsAnd(pLeaf) ) - continue; - Aig_CutDeref( p, Aig_ObjBestCut(pLeaf) ); - } -} - -/**Function************************************************************* - - Synopsis [Computes area of the first level.] - - Description [The cut need to be derefed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_CutRef( Aig_Man_t * p, Dar_Cut_t * pCut ) -{ - Aig_Obj_t * pLeaf; - int i, Area = pCut->Value; - Dar_CutForEachLeaf( p, pCut, pLeaf, i ) - { - assert( pLeaf->nRefs >= 0 ); - if ( pLeaf->nRefs++ > 0 || !Aig_ObjIsAnd(pLeaf) ) - continue; - Area += Aig_CutRef( p, Aig_ObjBestCut(pLeaf) ); - } - return Area; -} - -/**Function************************************************************* - - Synopsis [Computes exact area of the cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_CutArea( Aig_Man_t * p, Dar_Cut_t * pCut ) -{ - int Area; - Area = Aig_CutRef( p, pCut ); - Aig_CutDeref( p, pCut ); - return Area; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the second cut is better.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cnf_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 ) -{ - if ( pC0->Area < pC1->Area - 0.0001 ) - return -1; - if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better - return 1; -// if ( pC0->NoRefs < pC1->NoRefs ) -// return -1; -// if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better -// return 1; -// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves ) -// return -1; -// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves ) -// return 1; // larger average fanin ref-counter is better -// return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns the cut with the smallest area flow.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj ) -{ - Dar_Cut_t * pCut, * pCutBest; - int i; - pCutBest = NULL; - Dar_ObjForEachCut( pObj, pCut, i ) - if ( pCutBest == NULL || Cnf_CutCompare(pCutBest, pCut) == 1 ) - pCutBest = pCut; - return pCutBest; -} - -/**Function************************************************************* - - Synopsis [Computes area flow of the cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut ) -{ - Aig_Obj_t * pLeaf; - int i; - pCut->Area = (float)pCut->Cost; - pCut->NoRefs = 0; - pCut->FanRefs = 0; - Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i ) - { - if ( !Aig_ObjIsNode(pLeaf) ) - continue; - if ( pLeaf->nRefs == 0 ) - { - pCut->Area += Aig_ObjBestCut(pLeaf)->Cost; - pCut->NoRefs++; - } - else - { - if ( pCut->FanRefs + pLeaf->nRefs > 15 ) - pCut->FanRefs = 15; - else - pCut->FanRefs += pLeaf->nRefs; - } - } -} - -/**Function************************************************************* - - Synopsis [Performs one round of "area recovery" using exact local area.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_ManMapForCnf( Cnf_Man_t * p ) -{ - Aig_Obj_t * pObj; - Dar_Cut_t * pCut, * pCutBest; - int i, k; - // visit the nodes in the topological order and update their best cuts - Aig_ManForEachNode( p->pManAig, pObj, i ) - { - // find the old best cut - pCutBest = Aig_ObjBestCut(pObj); - Dar_ObjClearBestCut(pCutBest); - // if the node is used, dereference its cut - if ( pObj->nRefs ) - Aig_CutDeref( p->pManAig, pCutBest ); - - // evaluate the cuts of this node - Dar_ObjForEachCut( pObj, pCut, k ) -// Cnf_CutAssignAreaFlow( p, pCut ); - pCut->Area = (float)Cnf_CutArea( p->pManAig, pCut ); - - // find the new best cut - pCutBest = Cnf_ObjFindBestCut(pObj); - Dar_ObjSetBestCut( pCutBest ); - // if the node is used, reference its cut - if ( pObj->nRefs ) - Aig_CutRef( p->pManAig, pCutBest ); - } - return 1; -} - -#endif - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////