diff options
Diffstat (limited to 'src/aig/mfx/mfxMan.c')
| -rw-r--r-- | src/aig/mfx/mfxMan.c | 186 |
1 files changed, 186 insertions, 0 deletions
diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c new file mode 100644 index 00000000..1b536f8c --- /dev/null +++ b/src/aig/mfx/mfxMan.c @@ -0,0 +1,186 @@ +/**CFile**************************************************************** + + FileName [mfxMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [The good old minimization with complete don't-cares.] + + Synopsis [Procedures working with the manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: mfxMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "mfxInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ) +{ + Mfx_Man_t * p; + // start the manager + p = ALLOC( Mfx_Man_t, 1 ); + memset( p, 0, sizeof(Mfx_Man_t) ); + p->pPars = pPars; + p->vProjVars = Vec_IntAlloc( 100 ); + p->vDivLits = Vec_IntAlloc( 100 ); + p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX); + p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords ); + p->pMan = Int_ManAlloc(); + p->vMem = Vec_IntAlloc( 0 ); + p->vLevels = Vec_VecStart( 32 ); + p->vFanins = Vec_PtrAlloc( 32 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManClean( Mfx_Man_t * p ) +{ + if ( p->pAigWin ) + Aig_ManStop( p->pAigWin ); + if ( p->pCnf ) + Cnf_DataFree( p->pCnf ); + if ( p->pSat ) + sat_solver_delete( p->pSat ); + if ( p->vRoots ) + Vec_PtrFree( p->vRoots ); + if ( p->vSupp ) + Vec_PtrFree( p->vSupp ); + if ( p->vNodes ) + Vec_PtrFree( p->vNodes ); + if ( p->vDivs ) + Vec_PtrFree( p->vDivs ); + p->pAigWin = NULL; + p->pCnf = NULL; + p->pSat = NULL; + p->vRoots = NULL; + p->vSupp = NULL; + p->vNodes = NULL; + p->vDivs = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManPrint( Mfx_Man_t * p ) +{ + if ( p->pPars->fResub ) + { + printf( "Reduction in nodes = %5d. (%.2f %%) ", + p->nTotalNodesBeg-p->nTotalNodesEnd, + 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg ); + printf( "Reduction in edges = %5d. (%.2f %%) ", + p->nTotalEdgesBeg-p->nTotalEdgesEnd, + 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg ); + printf( "\n" ); + printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", + Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); + if ( p->pPars->fSwapEdge ) + printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", + p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) ); + else + Mfx_PrintResubStats( p ); +// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); + } + else + { + printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", + Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, + 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); +// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", +// 1.0-(p->dTotalRatios/p->nNodesTried) ); + printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); + } +/* + PRTP( "Win", p->timeWin , p->timeTotal ); + PRTP( "Div", p->timeDiv , p->timeTotal ); + PRTP( "Aig", p->timeAig , p->timeTotal ); + PRTP( "Cnf", p->timeCnf , p->timeTotal ); + PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); + PRTP( "Int", p->timeInt , p->timeTotal ); + PRTP( "ALL", p->timeTotal , p->timeTotal ); +*/ +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mfx_ManStop( Mfx_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Mfx_ManPrint( p ); + if ( p->vTruth ) + Vec_IntFree( p->vTruth ); + if ( p->pManDec ) + Bdc_ManFree( p->pManDec ); + if ( p->pCare ) + Aig_ManStop( p->pCare ); + if ( p->vSuppsInv ) + Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv ); + Mfx_ManClean( p ); + Int_ManFree( p->pMan ); + Vec_IntFree( p->vMem ); + Vec_VecFree( p->vLevels ); + Vec_PtrFree( p->vFanins ); + Vec_IntFree( p->vProjVars ); + Vec_IntFree( p->vDivLits ); + Vec_PtrFree( p->vDivCexes ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |