diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-10 12:47:47 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-10 12:47:47 -0700 |
commit | db6e7f97c1404e8a578184de2ac137d3f3b0ea06 (patch) | |
tree | fa68e3ccff360908b93388994268289f88206fd9 /src/aig/gia | |
parent | 1d441b6489b8b9df53297ab4c115ac86ae0d448c (diff) | |
download | abc-db6e7f97c1404e8a578184de2ac137d3f3b0ea06.tar.gz abc-db6e7f97c1404e8a578184de2ac137d3f3b0ea06.tar.bz2 abc-db6e7f97c1404e8a578184de2ac137d3f3b0ea06.zip |
Improving print-outs of &vta and &gla.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 30 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 37 |
2 files changed, 59 insertions, 8 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 75aacc7d..944badc4 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -131,6 +131,27 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { /**Function************************************************************* + Synopsis [Prints integer number using 6 characters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_PrintInt( int i ) +{ + if ( i > -1000 && i < 1000 ) + printf( "%6d", i ); + else if ( i > -1000000 && i < 1000000 ) + printf( "%5dk", i/1000 ); + else if ( i > -1000000000 && i < 1000000000 ) + printf( "%5dm", i/1000000 ); +} + +/**Function************************************************************* + Synopsis [Derive a new counter-example.] Description [] @@ -1641,8 +1662,11 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl Abc_Print( 1, "%5c", '-' ); else Abc_Print( 1, "%5d", nCexes ); - Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); - Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); +// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nclauses(p->pSat) ); + Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); +// Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" ); @@ -1813,7 +1837,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" ); Abc_Print( 1, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n", pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin ); - Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex SatVar Core Time\n" ); + Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i ) { diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index d32c1a2e..98f2b536 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -137,6 +137,27 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); /**Function************************************************************* + Synopsis [Prints integer number using 6 characters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_PrintInt( int i ) +{ + if ( i > -1000 && i < 1000 ) + printf( "%6d", i ); + else if ( i > -1000000 && i < 1000000 ) + printf( "%5dk", i/1000 ); + else if ( i > -1000000000 && i < 1000000000 ) + printf( "%5dm", i/1000000 ); +} + +/**Function************************************************************* + Synopsis [This procedure sets default parameters.] Description [] @@ -1191,7 +1212,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo { unsigned * pInfo; int * pCountAll = NULL, * pCountUni = NULL; - int i, k, iFrame, iObj, Entry, fChanges = 0; + int i, iFrame, iObj, Entry, fChanges = 0; // print info about frames if ( vCore ) { @@ -1240,12 +1261,15 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo Abc_Print( 1, "%5c", '-' ); else Abc_Print( 1, "%5d", nCexes ); - Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); +// Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nvars(p->pSat) ); + Abc_PrintInt( sat_solver2_nclauses(p->pSat) ); + Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); if ( vCore == NULL ) { Abc_Print( 1, " ..." ); - for ( k = 0; k < 7; k++ ) - Abc_Print( 1, " " ); +// for ( k = 0; k < 7; k++ ) +// Abc_Print( 1, " " ); Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); Abc_Print( 1, "\r" ); @@ -1253,6 +1277,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo else { Abc_Print( 1, "%7d", pCountAll[0] ); +/* if ( nFrames > 7 ) { for ( k = 0; k < 3; k++ ) @@ -1268,6 +1293,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo for ( k = nFrames; k < 7; k++ ) Abc_Print( 1, " " ); } +*/ Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); Abc_Print( 1, "\n" ); @@ -1572,7 +1598,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" ); Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%\n", pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin ); - Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" ); +// Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" ); + Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" ); } assert( Vec_PtrSize(p->vFrames) > 0 ); for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) |