From ea13085fe34bed2e827fe8ec6fb7e24c6e1a5d8f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 19 Feb 2012 13:33:21 -0800 Subject: Added printout of BMC tents in &ps. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaAbs.c | 8 ++++---- src/aig/gia/giaCof.c | 4 ++-- src/aig/gia/giaEquiv.c | 2 +- src/aig/gia/giaMan.c | 15 ++++++++++++++- src/aig/gia/giaReparam.c | 10 +++++----- 6 files changed, 27 insertions(+), 14 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 23beca19..96cfda34 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -742,7 +742,7 @@ extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern void Gia_ManStop( Gia_Man_t * p ); extern void Gia_ManStopP( Gia_Man_t ** p ); -extern void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); +extern void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch ); extern void Gia_ManPrintStatsShort( Gia_Man_t * p ); extern void Gia_ManPrintMiterStatus( Gia_Man_t * p ); extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index e25ff7fb..2efc73e4 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -292,7 +292,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ) Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); Vec_IntFree( vAbsFfsToAdd ); if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStats( pGia, 0, 0 ); return -1; } @@ -365,7 +365,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit } Aig_ManStop( pAig ); if ( fVerbose ) - Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStats( pGia, 0, 0 ); return RetValue; } @@ -409,7 +409,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) Vec_IntFreeP( &vGateClassesOld ); pGia->vGateClasses = vGateClasses; if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStats( pGia, 0, 0 ); return 1; } @@ -494,7 +494,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) Gia_ManStop( pGiaAbs ); } if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStats( pGia, 0, 0 ); return 1; } diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index 60dcf3af..49142683 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -862,7 +862,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose if ( fVerbose ) { printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) ); - Gia_ManPrintStats( p, 0 ); + Gia_ManPrintStats( p, 0, 0 ); } if ( Vec_IntSize( vSigs ) > 200 ) { @@ -888,7 +888,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose if ( fVerbose ) printf( "Cofactored variable %d.\n", iVar ); if ( fVerbose ) - Gia_ManPrintStats( pAig, 0 ); + Gia_ManPrintStats( pAig, 0, 0 ); } Vec_IntFree( vSigsNew ); return pAig; diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index e244ef46..3c5ad848 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1686,7 +1686,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f } // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim Gia_ManCleanMark0( pGia ); - Gia_ManPrintStats( pGia, 0 ); + Gia_ManPrintStats( pGia, 0, 0 ); for ( nIter = 0; ; nIter++ ) { if ( Gia_ManHasNoEquivs(pGia) ) diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 80fcf896..0e08341c 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -363,7 +363,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) +void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch ) { if ( p->pName ) printf( "%-8s : ", p->pName ); @@ -399,6 +399,19 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) Gia_ManPrintFlopClasses( p ); Gia_ManPrintGateClasses( p ); Gia_ManPrintObjClasses( p ); + if ( fTents ) + { + int k, Entry, Prev = 1; + Vec_Int_t * vLimit = Vec_IntAlloc( 1000 ); + Gia_Man_t * pNew = Gia_ManUnrollDup( p, vLimit ); + printf( "Tents: " ); + Vec_IntForEachEntryStart( vLimit, Entry, k, 1 ) + printf( "%d = %d ", k, Entry-Prev ), Prev = Entry; + printf( " Unused = %d.", Gia_ManObjNum(p) - Gia_ManObjNum(pNew) ); + printf( "\n" ); + Vec_IntFree( vLimit ); + Gia_ManStop( pNew ); + } } /**Function************************************************************* diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c index 10294671..59a45477 100644 --- a/src/aig/gia/giaReparam.c +++ b/src/aig/gia/giaReparam.c @@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) if ( fVerbose ) { printf( "Original AIG:\n" ); - Gia_ManPrintStats( p, 0 ); + Gia_ManPrintStats( p, 0, 0 ); } // perform input trimming @@ -155,7 +155,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) if ( fVerbose ) { printf( "After PI trimming:\n" ); - Gia_ManPrintStats( pNew, 0 ); + Gia_ManPrintStats( pNew, 0, 0 ); } // transform GIA pNew = Gia_ManDupIn2Ff( pTmp = pNew ); @@ -163,7 +163,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) if ( fVerbose ) { printf( "After PI-2-FF transformation:\n" ); - Gia_ManPrintStats( pNew, 0 ); + Gia_ManPrintStats( pNew, 0, 0 ); } // derive AIG @@ -178,7 +178,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) if ( fVerbose ) { printf( "After min-area retiming:\n" ); - Gia_ManPrintStats( pNew, 0 ); + Gia_ManPrintStats( pNew, 0, 0 ); } // transform back @@ -187,7 +187,7 @@ Gia_Man_t * Gia_ManReparam( Gia_Man_t * p, int fVerbose ) if ( fVerbose ) { printf( "After FF-2-PI tranformation:\n" ); - Gia_ManPrintStats( pNew, 0 ); + Gia_ManPrintStats( pNew, 0, 0 ); } return pNew; } -- cgit v1.2.3