From 5ace683835f29e3b4db24f9f7d0a8a4a223a164f Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 30 Mar 2013 13:02:32 -0700
Subject: Updating bmc3 printout to show the number of failed outputs.

---
 src/sat/bmc/bmcBmc3.c | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'src/sat/bmc/bmcBmc3.c')

diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index a6a7e71b..48028f76 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/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 );
-- 
cgit v1.2.3