diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 15:15:26 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 15:15:26 -0700 |
| commit | ca7c801150916cc119cab6242cb81dd63e06a1ce (patch) | |
| tree | fad6116ef6f04b43f73b08206eeb8273649d7a76 /src/proof | |
| parent | be8125f364ad80393b01a4953ae68f2158ffaa55 (diff) | |
| download | abc-ca7c801150916cc119cab6242cb81dd63e06a1ce.tar.gz abc-ca7c801150916cc119cab6242cb81dd63e06a1ce.tar.bz2 abc-ca7c801150916cc119cab6242cb81dd63e06a1ce.zip | |
Improving verbose printout of 'sim3' when solving multiple outputs.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 72e091ca..85ba67d5 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -965,8 +965,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in // if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) // return 0; if ( fVerbose ) - Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", - nWords, nFrames, nRounds, nRandSeed, TimeOut ); + Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n", + nWords, nFrames, nRounds, nRestart, nRandSeed, TimeOut ); // reset random numbers Ssw_RarManPrepareRandom( nSavedSeed ); @@ -1043,12 +1043,20 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in else Ssw_RarTransferPatterns( p, p->vInits ); // printout - if ( fVerbose && !fSolveAll ) + if ( fVerbose ) { -// Abc_Print( 1, "Round %3d: ", r ); -// Abc_PrintTime( 1, "Time", clock() - clk ); - Abc_Print( 1, "." ); + if ( fSolveAll ) + { + Abc_Print( 1, "Starts =%6d ", nNumRestart ); + Abc_Print( 1, "Rounds =%6d ", nNumRestart * nRestart + ((r==-1)?0:r) ); + Abc_Print( 1, "Frames =%6d ", (nNumRestart * nRestart + r) * nFrames ); + Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + } + else + Abc_Print( 1, "." ); } + } finish: if ( nSolved ) |