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 | |
| 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')
| -rw-r--r-- | src/base/abci/abc.c | 6 | ||||
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 20 |
2 files changed, 17 insertions, 9 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index debedfa1..d972b506 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17904,7 +17904,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nWords = 50; int nBinSize = 8; int nRounds = 0; - int nRestart = 100; + int nRestart = 0; int nRandSeed = 0; int TimeOut = 0; int TimeOutGap = 0; @@ -24884,7 +24884,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) nWords = 50; nBinSize = 8; nRounds = 0; - nRestart = 100; + nRestart = 0; nRandSeed = 0; TimeOut = 0; TimeOutGap = 0; @@ -25449,7 +25449,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nWords = 50; int nBinSize = 8; int nRounds = 0; - int nRestart = 100; + int nRestart = 0; int nRandSeed = 0; int TimeOut = 0; int fMiter = 0; 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 ) |