| /**CFile**************************************************************** | |
| FileName [darRefact.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [DAG-aware AIG rewriting.] | |
| Synopsis [Refactoring.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - April 28, 2007.] | |
| Revision [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "darInt.h" | |
| #include "bool/kit/kit.h" | |
| #include "bool/bdc/bdc.h" | |
| #include "bool/bdc/bdcInt.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| // the refactoring manager | |
| typedef struct Ref_Man_t_ Ref_Man_t; | |
| struct Ref_Man_t_ | |
| { | |
| // input data | |
| Dar_RefPar_t * pPars; // rewriting parameters | |
| Aig_Man_t * pAig; // AIG manager | |
| // computed cuts | |
| Vec_Vec_t * vCuts; // the storage for cuts | |
| // truth table and ISOP | |
| Vec_Ptr_t * vTruthElem; // elementary truth tables | |
| Vec_Ptr_t * vTruthStore; // storage for truth tables | |
| Vec_Int_t * vMemory; // storage for ISOP | |
| Vec_Ptr_t * vCutNodes; // storage for internal nodes of the cut | |
| // various data members | |
| Vec_Ptr_t * vLeavesBest; // the best set of leaves | |
| Kit_Graph_t * pGraphBest; // the best factored form | |
| int GainBest; // the best gain | |
| int LevelBest; // the level of node with the best gain | |
| // bi-decomposition | |
| Bdc_Par_t DecPars; // decomposition parameters | |
| Bdc_Man_t * pManDec; // decomposition manager | |
| // node statistics | |
| int nNodesInit; // the initial number of nodes | |
| int nNodesTried; // the number of nodes tried | |
| int nNodesBelow; // the number of nodes below the level limit | |
| int nNodesExten; // the number of nodes with extended cut | |
| int nCutsUsed; // the number of rewriting steps | |
| int nCutsTried; // the number of cuts tries | |
| // timing statistics | |
| abctime timeCuts; | |
| abctime timeEval; | |
| abctime timeOther; | |
| abctime timeTotal; | |
| }; | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [Returns the structure with default assignment of parameters.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ) | |
| { | |
| memset( pPars, 0, sizeof(Dar_RefPar_t) ); | |
| pPars->nMffcMin = 2; // the min MFFC size for which refactoring is used | |
| pPars->nLeafMax = 12; // the max number of leaves of a cut | |
| pPars->nCutsMax = 5; // the max number of cuts to consider | |
| pPars->fUpdateLevel = 0; | |
| pPars->fUseZeros = 0; | |
| pPars->fVerbose = 0; | |
| pPars->fVeryVerbose = 0; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Starts the rewriting manager.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) | |
| { | |
| Ref_Man_t * p; | |
| // start the manager | |
| p = ABC_ALLOC( Ref_Man_t, 1 ); | |
| memset( p, 0, sizeof(Ref_Man_t) ); | |
| p->pAig = pAig; | |
| p->pPars = pPars; | |
| // other data | |
| p->vCuts = Vec_VecStart( pPars->nCutsMax ); | |
| p->vTruthElem = Vec_PtrAllocTruthTables( pPars->nLeafMax ); | |
| p->vTruthStore = Vec_PtrAllocSimInfo( 1024, Kit_TruthWordNum(pPars->nLeafMax) ); | |
| p->vMemory = Vec_IntAlloc( 1 << 16 ); | |
| p->vCutNodes = Vec_PtrAlloc( 256 ); | |
| p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax ); | |
| // alloc bi-decomposition manager | |
| p->DecPars.nVarsMax = pPars->nLeafMax; | |
| p->DecPars.fVerbose = pPars->fVerbose; | |
| p->DecPars.fVeryVerbose = 0; | |
| // p->pManDec = Bdc_ManAlloc( &p->DecPars ); | |
| return p; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Prints out the statistics of the manager.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Dar_ManRefPrintStats( Ref_Man_t * p ) | |
| { | |
| int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig); | |
| printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", | |
| p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit ); | |
| printf( "Tried = %6d. Below = %5d. Extended = %5d. Used = %5d. Levels = %4d.\n", | |
| p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed, Aig_ManLevels(p->pAig) ); | |
| ABC_PRT( "Cuts ", p->timeCuts ); | |
| ABC_PRT( "Eval ", p->timeEval ); | |
| ABC_PRT( "Other ", p->timeOther ); | |
| ABC_PRT( "TOTAL ", p->timeTotal ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Stops the rewriting manager.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Dar_ManRefStop( Ref_Man_t * p ) | |
| { | |
| if ( p->pManDec ) | |
| Bdc_ManFree( p->pManDec ); | |
| if ( p->pPars->fVerbose ) | |
| Dar_ManRefPrintStats( p ); | |
| Vec_VecFree( p->vCuts ); | |
| Vec_PtrFree( p->vTruthElem ); | |
| Vec_PtrFree( p->vTruthStore ); | |
| Vec_PtrFree( p->vLeavesBest ); | |
| Vec_IntFree( p->vMemory ); | |
| Vec_PtrFree( p->vCutNodes ); | |
| ABC_FREE( p ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Ref_ObjComputeCuts( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Vec_t * vCuts ) | |
| { | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Ref_ObjPrint( Aig_Obj_t * pObj ) | |
| { | |
| printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 ); | |
| if ( pObj ) | |
| printf( "(%d) ", Aig_IsComplement(pObj) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Counts the number of new nodes added when using this graph.] | |
| Description [AIG nodes for the fanins should be assigned to pNode->pFunc | |
| of the leaves of the graph before calling this procedure. | |
| Returns -1 if the number of nodes and levels exceeded the given limit or | |
| the number of levels exceeded the maximum allowed level.] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph, int NodeMax, int LevelMax ) | |
| { | |
| Kit_Node_t * pNode, * pNode0, * pNode1; | |
| Aig_Obj_t * pAnd, * pAnd0, * pAnd1; | |
| int i, Counter, LevelNew, LevelOld; | |
| // check for constant function or a literal | |
| if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) ) | |
| return 0; | |
| // set the levels of the leaves | |
| Kit_GraphForEachLeaf( pGraph, pNode, i ) | |
| { | |
| pNode->pFunc = Vec_PtrEntry(vCut, i); | |
| pNode->Level = Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level; | |
| assert( Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level < (1<<24)-1 ); | |
| } | |
| //printf( "Trying:\n" ); | |
| // compute the AIG size after adding the internal nodes | |
| Counter = 0; | |
| Kit_GraphForEachNode( pGraph, pNode, i ) | |
| { | |
| // get the children of this node | |
| pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node ); | |
| pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node ); | |
| // get the AIG nodes corresponding to the children | |
| pAnd0 = (Aig_Obj_t *)pNode0->pFunc; | |
| pAnd1 = (Aig_Obj_t *)pNode1->pFunc; | |
| if ( pAnd0 && pAnd1 ) | |
| { | |
| // if they are both present, find the resulting node | |
| pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl ); | |
| pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl ); | |
| pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 ); | |
| // return -1 if the node is the same as the original root | |
| if ( Aig_Regular(pAnd) == pRoot ) | |
| return -1; | |
| } | |
| else | |
| pAnd = NULL; | |
| // count the number of added nodes | |
| if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) ) | |
| { | |
| if ( ++Counter > NodeMax ) | |
| return -1; | |
| } | |
| // count the number of new levels | |
| LevelNew = 1 + Abc_MaxInt( pNode0->Level, pNode1->Level ); | |
| if ( pAnd ) | |
| { | |
| if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) ) | |
| LevelNew = 0; | |
| else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) ) | |
| LevelNew = (int)Aig_Regular(pAnd0)->Level; | |
| else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) ) | |
| LevelNew = (int)Aig_Regular(pAnd1)->Level; | |
| LevelOld = (int)Aig_Regular(pAnd)->Level; | |
| // assert( LevelNew == LevelOld ); | |
| } | |
| if ( LevelNew > LevelMax ) | |
| return -1; | |
| pNode->pFunc = pAnd; | |
| pNode->Level = LevelNew; | |
| /* | |
| printf( "Checking " ); | |
| Ref_ObjPrint( pAnd0 ); | |
| printf( " and " ); | |
| Ref_ObjPrint( pAnd1 ); | |
| printf( " Result " ); | |
| Ref_ObjPrint( pNode->pFunc ); | |
| printf( "\n" ); | |
| */ | |
| } | |
| return Counter; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph ) | |
| { | |
| Aig_Obj_t * pAnd0, * pAnd1; | |
| Kit_Node_t * pNode = NULL; | |
| int i; | |
| // check for constant function | |
| if ( Kit_GraphIsConst(pGraph) ) | |
| return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) ); | |
| // set the leaves | |
| Kit_GraphForEachLeaf( pGraph, pNode, i ) | |
| pNode->pFunc = Vec_PtrEntry(vCut, i); | |
| // check for a literal | |
| if ( Kit_GraphIsVar(pGraph) ) | |
| return Aig_NotCond( (Aig_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) ); | |
| // build the AIG nodes corresponding to the AND gates of the graph | |
| //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) ); | |
| Kit_GraphForEachNode( pGraph, pNode, i ) | |
| { | |
| pAnd0 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); | |
| pAnd1 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); | |
| pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); | |
| /* | |
| printf( "Checking " ); | |
| Ref_ObjPrint( pAnd0 ); | |
| printf( " and " ); | |
| Ref_ObjPrint( pAnd1 ); | |
| printf( " Result " ); | |
| Ref_ObjPrint( pNode->pFunc ); | |
| printf( "\n" ); | |
| */ | |
| } | |
| // complement the result if necessary | |
| return Aig_NotCond( (Aig_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required ) | |
| { | |
| Vec_Ptr_t * vCut; | |
| Kit_Graph_t * pGraphCur; | |
| int k, RetValue, GainCur, nNodesAdded; | |
| unsigned * pTruth; | |
| p->GainBest = -1; | |
| p->pGraphBest = NULL; | |
| Vec_VecForEachLevel( p->vCuts, vCut, k ) | |
| { | |
| if ( Vec_PtrSize(vCut) == 0 ) | |
| continue; | |
| // if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 ) | |
| // continue; | |
| p->nCutsTried++; | |
| // get the cut nodes | |
| Aig_ObjCollectCut( pObj, vCut, p->vCutNodes ); | |
| // get the truth table | |
| pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); | |
| if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) ) | |
| { | |
| p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL ); | |
| p->pGraphBest = Kit_GraphCreateConst0(); | |
| Vec_PtrCopy( p->vLeavesBest, vCut ); | |
| return p->GainBest; | |
| } | |
| if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) ) | |
| { | |
| p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL ); | |
| p->pGraphBest = Kit_GraphCreateConst1(); | |
| Vec_PtrCopy( p->vLeavesBest, vCut ); | |
| return p->GainBest; | |
| } | |
| // try the positive phase | |
| RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); | |
| if ( RetValue > -1 ) | |
| { | |
| pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory ); | |
| /* | |
| { | |
| int RetValue; | |
| RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 ); | |
| printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue ); | |
| } | |
| */ | |
| nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); | |
| if ( nNodesAdded > -1 ) | |
| { | |
| GainCur = nNodesSaved - nNodesAdded; | |
| if ( p->GainBest < GainCur || (p->GainBest == GainCur && | |
| (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) ) | |
| { | |
| p->GainBest = GainCur; | |
| if ( p->pGraphBest ) | |
| Kit_GraphFree( p->pGraphBest ); | |
| p->pGraphBest = pGraphCur; | |
| Vec_PtrCopy( p->vLeavesBest, vCut ); | |
| } | |
| else | |
| Kit_GraphFree( pGraphCur ); | |
| } | |
| else | |
| Kit_GraphFree( pGraphCur ); | |
| } | |
| // try negative phase | |
| Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) ); | |
| RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); | |
| // Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) ); | |
| if ( RetValue > -1 ) | |
| { | |
| pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory ); | |
| /* | |
| { | |
| int RetValue; | |
| RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 ); | |
| printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue ); | |
| } | |
| */ | |
| nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); | |
| if ( nNodesAdded > -1 ) | |
| { | |
| GainCur = nNodesSaved - nNodesAdded; | |
| if ( p->GainBest < GainCur || (p->GainBest == GainCur && | |
| (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) ) | |
| { | |
| p->GainBest = GainCur; | |
| if ( p->pGraphBest ) | |
| Kit_GraphFree( p->pGraphBest ); | |
| p->pGraphBest = pGraphCur; | |
| Vec_PtrCopy( p->vLeavesBest, vCut ); | |
| } | |
| else | |
| Kit_GraphFree( pGraphCur ); | |
| } | |
| else | |
| Kit_GraphFree( pGraphCur ); | |
| } | |
| } | |
| return p->GainBest; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Returns 1 if a non-PI node has nLevelMin or below.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin ) | |
| { | |
| Aig_Obj_t * pObj; | |
| int i; | |
| Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i ) | |
| if ( !Aig_ObjIsCi(pObj) && (int)pObj->Level <= nLevelMin ) | |
| return 1; | |
| return 0; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) | |
| { | |
| // Bar_Progress_t * pProgress; | |
| Ref_Man_t * p; | |
| Vec_Ptr_t * vCut, * vCut2; | |
| Aig_Obj_t * pObj, * pObjNew; | |
| int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2; | |
| int i, Required, nLevelMin; | |
| abctime clkStart, clk; | |
| // start the manager | |
| p = Dar_ManRefStart( pAig, pPars ); | |
| // remove dangling nodes | |
| Aig_ManCleanup( pAig ); | |
| // if updating levels is requested, start fanout and timing | |
| Aig_ManFanoutStart( pAig ); | |
| if ( p->pPars->fUpdateLevel ) | |
| Aig_ManStartReverseLevels( pAig, 0 ); | |
| // resynthesize each node once | |
| clkStart = Abc_Clock(); | |
| vCut = Vec_VecEntry( p->vCuts, 0 ); | |
| vCut2 = Vec_VecEntry( p->vCuts, 1 ); | |
| p->nNodesInit = Aig_ManNodeNum(pAig); | |
| nNodesOld = Vec_PtrSize( pAig->vObjs ); | |
| // pProgress = Bar_ProgressStart( stdout, nNodesOld ); | |
| Aig_ManForEachObj( pAig, pObj, i ) | |
| { | |
| // Bar_ProgressUpdate( pProgress, i, NULL ); | |
| if ( !Aig_ObjIsNode(pObj) ) | |
| continue; | |
| if ( i > nNodesOld ) | |
| break; | |
| if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit ) | |
| break; | |
| Vec_VecClear( p->vCuts ); | |
| //printf( "\nConsidering node %d.\n", pObj->Id ); | |
| // get the bounded MFFC size | |
| clk = Abc_Clock(); | |
| nLevelMin = Abc_MaxInt( 0, Aig_ObjLevel(pObj) - 10 ); | |
| nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut ); | |
| if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider | |
| { | |
| p->timeCuts += Abc_Clock() - clk; | |
| continue; | |
| } | |
| p->nNodesTried++; | |
| if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut | |
| { | |
| Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 ); | |
| nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut ); | |
| } | |
| else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend ) | |
| { | |
| if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) ) | |
| { | |
| if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) ) | |
| { | |
| nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut ); | |
| assert( nNodesSaved2 == nNodesSaved ); | |
| } | |
| if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax ) | |
| Vec_PtrClear(vCut2); | |
| if ( Vec_PtrSize(vCut2) > 0 ) | |
| { | |
| p->nNodesExten++; | |
| // printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) ); | |
| } | |
| } | |
| else | |
| p->nNodesBelow++; | |
| } | |
| p->timeCuts += Abc_Clock() - clk; | |
| // try the cuts | |
| clk = Abc_Clock(); | |
| Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY; | |
| Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required ); | |
| p->timeEval += Abc_Clock() - clk; | |
| // check the best gain | |
| if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) | |
| { | |
| if ( p->pGraphBest ) | |
| Kit_GraphFree( p->pGraphBest ); | |
| continue; | |
| } | |
| //printf( "\n" ); | |
| // if we end up here, a rewriting step is accepted | |
| nNodeBefore = Aig_ManNodeNum( pAig ); | |
| pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest ); | |
| assert( (int)Aig_Regular(pObjNew)->Level <= Required ); | |
| // replace the node | |
| Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel ); | |
| // compare the gains | |
| nNodeAfter = Aig_ManNodeNum( pAig ); | |
| assert( p->GainBest <= nNodeBefore - nNodeAfter ); | |
| Kit_GraphFree( p->pGraphBest ); | |
| p->nCutsUsed++; | |
| // break; | |
| } | |
| p->timeTotal = Abc_Clock() - clkStart; | |
| p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; | |
| // Bar_ProgressStop( pProgress ); | |
| // put the nodes into the DFS order and reassign their IDs | |
| // Aig_NtkReassignIds( p ); | |
| // fix the levels | |
| Aig_ManFanoutStop( pAig ); | |
| if ( p->pPars->fUpdateLevel ) | |
| Aig_ManStopReverseLevels( pAig ); | |
| /* | |
| Aig_ManForEachObj( p->pAig, pObj, i ) | |
| if ( Aig_ObjIsNode(pObj) && Aig_ObjRefs(pObj) == 0 ) | |
| { | |
| printf( "Unreferenced " ); | |
| Aig_ObjPrintVerbose( pObj, 0 ); | |
| printf( "\n" ); | |
| } | |
| */ | |
| // remove dangling nodes (they should not be here!) | |
| Aig_ManCleanup( pAig ); | |
| // stop the rewriting manager | |
| Dar_ManRefStop( p ); | |
| // Aig_ManCheckPhase( pAig ); | |
| if ( !Aig_ManCheck( pAig ) ) | |
| { | |
| printf( "Dar_ManRefactor: The network check has failed.\n" ); | |
| return 0; | |
| } | |
| return 1; | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |