Updating bmc3 printout to show the number of failed outputs.

src/base/abci/abc.c

@@ -20906,6 +20906,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp );
     Saig_ParBmc_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
+    Vec_Ptr_t * vSeqModelVec = NULL;
     char * pLogFileName = NULL;
     int fOrDecomp = 0;
     int c;
@@ -21056,18 +21057,19 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+    vSeqModelVec = pNtk->vSeqModelVec;  pNtk->vSeqModelVec = NULL;
     if ( pLogFileName )
         Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
     if ( pPars->fSolveAll && pPars->fDropSatOuts )
     {
-        if ( pNtk->vSeqModelVec == NULL )
+        if ( vSeqModelVec == NULL )
             Abc_Print( 1,"The array of counter-examples is not available.\n" );
-        else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) )
+        else if ( Vec_PtrSize(vSeqModelVec) != Abc_NtkPoNum(pNtk) )
             Abc_Print( 1,"The array size does not match the number of outputs.\n" );
         else
         {
             extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
-            Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose );
+            Abc_NtkDropSatOutputs( pNtk, vSeqModelVec, pPars->fVerbose );
             pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
             if ( pNtkRes == NULL )
             {
@@ -21077,9 +21079,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
     }
-    if ( pNtk->vSeqModelVec )
+    if ( vSeqModelVec )
     {
-        Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+        Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
         pAbc->nFrames = -1;
     }
     return 0;

src/sat/bmc/bmcBmc3.c

@@ -1358,6 +1358,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     clock_t clk, clk2, clkOther = 0, clkTotal = clock();
     clock_t nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     clock_t nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
+    clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0;
     // create BMC manager
     p = Saig_Bmc3ManStart( pAig );
     p->pPars = pPars;
@@ -1478,9 +1479,11 @@ clkOther += clock() - clk2;
             // solve th is output
             fUnfinished = 0;
             sat_solver_compress( p->pSat );
+clk2 = 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 );
             if ( status == l_False )
             {
+nTimeUnsat += clock() - clk2;
                 if ( 1 )
                 {
                     // add final unit clause
@@ -1501,6 +1504,7 @@ clkOther += clock() - clk2;
             }
             else if ( status == l_True )
             {
+nTimeSat += clock() - clk2;
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
                 {
@@ -1555,6 +1559,7 @@ clkOther += clock() - clk2;
             }
             else 
             {
+nTimeUndec += clock() - clk2;
                 assert( status == l_Undef );
                 if ( pPars->nFramesJump )
                 {
@@ -1605,11 +1610,12 @@ clkOther += clock() - clk2;
 //ABC_PRT( "CNF generation runtime", clkOther );
     if ( pPars->fVerbose )
     {
-//    ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
-//    ABC_PRMn( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-//    printf( "Simples = %6d. ", p->nBufNum );
-//    printf( "Dups = %6d. ", p->nDupNum );
-//    printf( "\n" );
+        printf( "Runtime:  " );
+        printf( "CNF = %.1f sec (%.1f %%)  ",   1.0*clkOther/CLOCKS_PER_SEC,   100.0*clkOther/(clock() - clkTotal)   );
+        printf( "UNSAT = %.1f sec (%.1f %%)  ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(clock() - clkTotal) );
+        printf( "SAT = %.1f sec (%.1f %%)  ",   1.0*nTimeSat/CLOCKS_PER_SEC,   100.0*nTimeSat/(clock() - clkTotal)   );
+        printf( "UNDEC = %.1f sec (%.1f %%)",   1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(clock() - clkTotal) );
+        printf( "\n" );
     }
     Saig_Bmc3ManStop( p );
     fflush( stdout );