Adding per-output logging to bmc3.

src/base/abci/abc.c

@@ -21505,7 +21505,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLaxdruvzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdruvzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21650,6 +21650,15 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             pLogFileName = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pPars->pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'a':
             pPars->fSolveAll ^= 1;
             break;
@@ -21728,7 +21737,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-L file] [-axduvzh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axduvzh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n",      pPars->nFramesMax );
@@ -21740,9 +21749,10 @@ usage:
     Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
     Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n",                   pPars->nPisAbstract );
     Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
-    Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n",               pPars->nLearnedDelta );
-    Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n",          pPars->nLearnedPerce );
+    Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n",          pPars->nLearnedDelta );
+    Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n",   pPars->nLearnedPerce );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n",                               pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-W file: the log file name with per-output details [default = %s]\n",       pPars->pLogFileName ? pPars->pLogFileName : "no logging" );
     Abc_Print( -2, "\t-a     : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",   pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dropping (replacing by 0) SAT outputs [default = %s]\n",    pPars->fDropSatOuts? "yes": "no" );

src/sat/bmc/bmc.h

@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
     int         nLearnedPerce;  // ratio of learned clause limit
     int         fVerbose;       // verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
+    char *      pLogFileName;   // log file name
     int         fSilent;        // completely silent
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs

src/sat/bmc/bmcBmc3.c

@@ -1392,13 +1392,16 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
     Abc_Cex_t * pCexNew, * pCexNew0;
+    FILE * pLogFile = NULL;
     unsigned * pInfo;
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
     int i, f, k, Lit, status;
-    abctime clk, clk2, clkOther = 0, clkTotal = Abc_Clock();
+    abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
     abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
     abctime nTimeToStopNG, nTimeToStop;
+    if ( pPars->pLogFileName )
+        pLogFile = fopen( pPars->pLogFileName, "wb" );
     if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
         pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
     if ( pPars->nTimeOutOne && !pPars->fSolveAll )
@@ -1542,15 +1545,17 @@ clkOther += Abc_Clock() - clk2;
             // solve this output
             fUnfinished = 0;
             sat_solver_compress( p->pSat );
-clk2 = Abc_Clock();
             if ( p->pTime4Outs )
             {
                 assert( p->pTime4Outs[i] > 0 );
                 clkOne = Abc_Clock();
                 sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
             }
-//            status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+clk2 = Abc_Clock();
             status = Saig_ManCallSolver( p, Lit );
+clkSatRun = Abc_Clock() - clk2;
+            if ( pLogFile )
+                fprintf( pLogFile, "Frame %5d  Output %5d  Time(ms) %8d\n", f, i, Lit < 2 ? 0 : clkSatRun );
             if ( p->pTime4Outs )
             {
                 abctime timeSince = Abc_Clock() - clkOne;
@@ -1561,7 +1566,7 @@ clk2 = Abc_Clock();
             }
             if ( status == l_False )
             {
-nTimeUnsat += Abc_Clock() - clk2;
+nTimeUnsat += clkSatRun;
                 if ( Lit != 0 )
                 {
                     // add final unit clause
@@ -1584,7 +1589,7 @@ nTimeUnsat += Abc_Clock() - clk2;
             }
             else if ( status == l_True )
             {
-nTimeSat += Abc_Clock() - clk2;
+nTimeSat += clkSatRun;
                 RetValue = 0;
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
@@ -1671,7 +1676,7 @@ nTimeSat += Abc_Clock() - clk2;
             }
             else 
             {
-nTimeUndec += Abc_Clock() - clk2;
+nTimeUndec += clkSatRun;
                 assert( status == l_Undef );
                 if ( pPars->nFramesJump )
                 {
@@ -1735,6 +1740,8 @@ finish:
     }
     Saig_Bmc3ManStop( p );
     fflush( stdout );
+    if ( pLogFile )
+        fclose( pLogFile );
     return RetValue;
 }