From ca7c801150916cc119cab6242cb81dd63e06a1ce Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 30 Mar 2013 15:15:26 -0700
Subject: Improving verbose printout of 'sim3' when solving multiple outputs.

---
 src/base/abci/abc.c       |  6 +++---
 src/proof/ssw/sswRarity.c | 20 ++++++++++++++------
 2 files changed, 17 insertions(+), 9 deletions(-)

(limited to 'src')

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 )
-- 
cgit v1.2.3