diff options
Diffstat (limited to 'src/aig/dar')
| -rw-r--r-- | src/aig/dar/dar.h | 29 | ||||
| -rw-r--r-- | src/aig/dar/darCore.c | 20 | ||||
| -rw-r--r-- | src/aig/dar/darInt.h | 7 | ||||
| -rw-r--r-- | src/aig/dar/darLib.c | 87 | ||||
| -rw-r--r-- | src/aig/dar/darMan.c | 2 | ||||
| -rw-r--r-- | src/aig/dar/darRefact.c | 532 | ||||
| -rw-r--r-- | src/aig/dar/darScript.c | 204 |
7 files changed, 777 insertions, 104 deletions
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index cff2785b..3106c7ad 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -37,10 +37,10 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -typedef struct Dar_Par_t_ Dar_Par_t; +typedef struct Dar_RwrPar_t_ Dar_RwrPar_t; +typedef struct Dar_RefPar_t_ Dar_RefPar_t; -// the rewriting parameters -struct Dar_Par_t_ +struct Dar_RwrPar_t_ { int nCutsMax; // the maximum number of cuts to try int nSubgMax; // the maximum number of subgraphs to try @@ -50,6 +50,18 @@ struct Dar_Par_t_ int fVeryVerbose; // enables very verbose output }; +struct Dar_RefPar_t_ +{ + int nMffcMin; // the min MFFC size for which refactoring is used + int nLeafMax; // the max number of leaves of a cut + int nCutsMax; // the max number of cuts to consider + int fExtend; // extends the cut below MFFC + int fUpdateLevel; // updates the level after each move + int fUseZeros; // perform zero-cost replacements + int fVerbose; // verbosity level + int fVeryVerbose; // enables very verbose output +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -62,10 +74,17 @@ struct Dar_Par_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== darBalance.c ========================================================*/ +extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); /*=== darCore.c ========================================================*/ -extern void Dar_ManDefaultParams( Dar_Par_t * pPars ); -extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ); +extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ); +extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ); extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig ); +/*=== darRefact.c ========================================================*/ +extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ); +extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ); +/*=== darScript.c ========================================================*/ +extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index e7186e83..7546df0b 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -39,15 +39,15 @@ SeeAlso [] ***********************************************************************/ -void Dar_ManDefaultParams( Dar_Par_t * pPars ) +void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) { - memset( pPars, 0, sizeof(Dar_Par_t) ); - pPars->nCutsMax = 8; - pPars->nSubgMax = 5; // 5 is a "magic number" - pPars->fUpdateLevel = 0; - pPars->fUseZeros = 0; - pPars->fVerbose = 0; - pPars->fVeryVerbose = 0; + memset( pPars, 0, sizeof(Dar_RwrPar_t) ); + pPars->nCutsMax = 8; + pPars->nSubgMax = 5; // 5 is a "magic number" + pPars->fUpdateLevel = 0; + pPars->fUseZeros = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; } /**Function************************************************************* @@ -61,7 +61,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ) +int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) { Dar_Man_t * p; ProgressBar * pProgress; @@ -128,7 +128,7 @@ p->timeCuts += clock() - clk; // evaluate the cuts p->GainBest = -1; - Required = 1000000; + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; Dar_ObjForEachCut( pObj, pCut, k ) Dar_LibEval( p, pObj, pCut, Required ); // check the best gain diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h index f496a73f..0acd272c 100644 --- a/src/aig/dar/darInt.h +++ b/src/aig/dar/darInt.h @@ -64,8 +64,8 @@ struct Dar_Cut_t_ // 6 words // the AIG manager struct Dar_Man_t_ { - // input data; - Dar_Par_t * pPars; // rewriting parameters + // input data + Dar_RwrPar_t * pPars; // rewriting parameters Aig_Man_t * pAig; // AIG manager // various data members Aig_MmFixed_t * pMemCuts; // memory manager for cuts @@ -125,7 +125,6 @@ static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) //////////////////////////////////////////////////////////////////////// /*=== darBalance.c ========================================================*/ -extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); /*=== darCore.c ===========================================================*/ /*=== darCut.c ============================================================*/ extern void Dar_ManCutsStart( Dar_Man_t * p ); @@ -144,7 +143,7 @@ extern void Dar_LibReturnCanonicals( unsigned * pCanons ); extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required ); extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p ); /*=== darMan.c ============================================================*/ -extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ); +extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ); extern void Dar_ManStop( Dar_Man_t * p ); extern void Dar_ManPrintStats( Dar_Man_t * p ); diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index c3d57b52..72ce0cde 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -707,65 +707,6 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut ) /**Function************************************************************* - Synopsis [Dereferences the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_NodeDeref_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) -{ - Aig_Obj_t * pFanin; - int Counter = 0; - if ( Aig_ObjIsPi(pNode) ) - return Counter; - pFanin = Aig_ObjFanin0( pNode ); - assert( pFanin->nRefs > 0 ); - if ( --pFanin->nRefs == 0 ) - Counter += Aig_NodeDeref_rec( p, pFanin ); - if ( Aig_ObjIsBuf(pNode) ) - return Counter; - pFanin = Aig_ObjFanin1( pNode ); - assert( pFanin->nRefs > 0 ); - if ( --pFanin->nRefs == 0 ) - Counter += Aig_NodeDeref_rec( p, pFanin ); - return 1 + Counter; -} - -/**Function************************************************************* - - Synopsis [References the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) -{ - Aig_Obj_t * pFanin; - int Counter = 0; - if ( Aig_ObjIsPi(pNode) ) - return Counter; - Aig_ObjSetTravIdCurrent( p, pNode ); - pFanin = Aig_ObjFanin0( pNode ); - if ( pFanin->nRefs++ == 0 ) - Counter += Aig_NodeRef_rec( p, pFanin ); - if ( Aig_ObjIsBuf(pNode) ) - return Counter; - pFanin = Aig_ObjFanin1( pNode ); - if ( pFanin->nRefs++ == 0 ) - Counter += Aig_NodeRef_rec( p, pFanin ); - return 1 + Counter; -} - -/**Function************************************************************* - Synopsis [Marks the MFFC of the node.] Description [] @@ -777,19 +718,16 @@ int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) ***********************************************************************/ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves ) { - int i, nNodes1, nNodes2; + int i, nNodes; // mark the cut leaves for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++; // label MFFC with current ID - Aig_ManIncrementTravId( p ); - nNodes1 = Aig_NodeDeref_rec( p, pRoot ); - nNodes2 = Aig_NodeRef_rec( p, pRoot ); - assert( nNodes1 == nNodes2 ); + nNodes = Aig_NodeMffsLabel( p, pRoot ); // unmark the cut leaves for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--; - return nNodes1; + return nNodes; } /**Function************************************************************* @@ -836,7 +774,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) { Dar_LibObj_t * pObj; Dar_LibDat_t * pData, * pData0, * pData1; - Aig_Obj_t * pGhost, * pFanin0, * pFanin1; + Aig_Obj_t * pFanin0, * pFanin1; int i; for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ ) { @@ -859,22 +797,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) continue; pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 ); - - // consider simple cases - if ( pFanin0 == pFanin1 ) - pData->pFunc = pFanin0; - else if ( pFanin0 == Aig_Not(pFanin1) ) - pData->pFunc = Aig_ManConst0(p->pAig); - else if ( Aig_Regular(pFanin0) == Aig_ManConst1(p->pAig) ) - pData->pFunc = pFanin0 == Aig_ManConst1(p->pAig) ? pFanin1 : Aig_ManConst0(p->pAig); - else if ( Aig_Regular(pFanin1) == Aig_ManConst1(p->pAig) ) - pData->pFunc = pFanin1 == Aig_ManConst1(p->pAig) ? pFanin0 : Aig_ManConst0(p->pAig); - else - { - pGhost = Aig_ObjCreateGhost( p->pAig, pFanin0, pFanin1, AIG_OBJ_AND ); - pData->pFunc = Aig_TableLookup( p->pAig, pGhost ); - } - + pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 ); // clear the node if it is part of MFFC if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) ) pData->fMffc = 1; diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index 8b7c5afb..ef898ea2 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ) +Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) { Dar_Man_t * p; // start the manager diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index 1bcc0466..cdfbaa01 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -19,17 +19,151 @@ ***********************************************************************/ #include "darInt.h" +#include "kit.h" //////////////////////////////////////////////////////////////////////// /// 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 + // 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 + int timeCuts; + int timeEval; + int timeOther; + int 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 = 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( 256, Kit_TruthWordNum(pPars->nLeafMax) ); + p->vMemory = Vec_IntAlloc( 1 << 16 ); + p->vCutNodes = Vec_PtrAlloc( 256 ); + p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax ); + 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.\n", + p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed ); + PRT( "Cuts ", p->timeCuts ); + PRT( "Eval ", p->timeEval ); + PRT( "Other ", p->timeOther ); + PRT( "TOTAL ", p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Stops the rewriting manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManRefStop( Ref_Man_t * p ) +{ + 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 ); + free( p ); +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -39,7 +173,405 @@ 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(pNode->pFunc)->Level; + assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-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 = pNode0->pFunc; + pAnd1 = 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 + AIG_MAX( 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; + 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( 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_ManObjIdMax(pAig) ); + Kit_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Aig_NotCond( 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( 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_ManCollectCut( pObj, vCut, p->vCutNodes ); + // get the truth table + pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); + // 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 ); + 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 ); + if ( RetValue > -1 ) + { + pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory ); + 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( vCut, pObj, i ) + if ( !Aig_ObjIsPi(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 ) +{ + ProgressBar * 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, 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_ManCreateFanout( pAig ); + if ( p->pPars->fUpdateLevel ) + Aig_ManStartReverseLevels( pAig, 0 ); + + // resynthesize each node once + clkStart = clock(); + vCut = Vec_VecEntry( p->vCuts, 0 ); + vCut2 = Vec_VecEntry( p->vCuts, 1 ); + p->nNodesInit = Aig_ManNodeNum(pAig); + nNodesOld = Vec_PtrSize( pAig->vObjs ); + pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); + Aig_ManForEachObj( pAig, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( !Aig_ObjIsNode(pObj) ) + continue; + if ( i > nNodesOld ) + break; + Vec_VecClear( p->vCuts ); + + if ( pObj->Id == 738 ) + { + int x = 0; + } + +//printf( "\nConsidering node %d.\n", pObj->Id ); + // get the bounded MFFC size +clk = clock(); + nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 ); + nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut ); + if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider + { +p->timeCuts += 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_NodeMffsLabelCut( p->pAig, pObj, vCut ); + } + else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend ) + { + if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) ) + { + if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) ) + { + nNodesSaved2 = Aig_NodeMffsLabelCut( 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 += clock() - clk; + + // try the cuts +clk = clock(); + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; + Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required ); +p->timeEval += 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, 1, p->pPars->fUpdateLevel ); + // compare the gains + nNodeAfter = Aig_ManNodeNum( pAig ); + assert( p->GainBest <= nNodeBefore - nNodeAfter ); + Kit_GraphFree( p->pGraphBest ); + p->nCutsUsed++; +// break; + } +p->timeTotal = clock() - clkStart; +p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; + + Extra_ProgressBarStop( pProgress ); + // put the nodes into the DFS order and reassign their IDs +// Aig_NtkReassignIds( p ); + // fix the levels + Aig_ManDeleteFanout( pAig ); + if ( p->pPars->fUpdateLevel ) + Aig_ManStopReverseLevels( pAig ); + + // stop the rewriting manager + Dar_ManRefStop( p ); + if ( !Aig_ManCheck( pAig ) ) + { + printf( "Dar_ManRefactor: The network check has failed.\n" ); + return 0; + } + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index c98a263e..8423a4e6 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -30,15 +30,215 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Reproduces script "compress2".] Description [] - SideEffects [] + SideEffects [This procedure does not tighten level during restructuring.] SeeAlso [] ***********************************************************************/ +Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [This procedure does not tighten level during restructuring.] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [This procedure does not tighten level during restructuring.] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); +/* + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); +*/ + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; +} //////////////////////////////////////////////////////////////////////// |