Improving print-outs of &vta and &gla.

src/aig/gia/giaAbsGla.c

@@ -131,6 +131,27 @@ static inline void        Gla_ObjClearRef( Rfn_Obj_t * p )                     {
 
 /**Function*************************************************************
 
+  Synopsis    [Prints integer number using 6 characters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_PrintInt( int i )
+{
+    if ( i > -1000 && i < 1000 )
+        printf( "%6d", i );
+    else if ( i > -1000000 && i < 1000000 )
+        printf( "%5dk", i/1000 );
+    else if ( i > -1000000000 && i < 1000000000 )
+        printf( "%5dm", i/1000000 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derive a new counter-example.]
 
   Description []
@@ -1641,8 +1662,11 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
         Abc_Print( 1, "%5c", '-' ); 
     else
         Abc_Print( 1, "%5d", nCexes ); 
-    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
-    Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
+//    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
+    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
+    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
+    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
+//    Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
     Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
     Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
@@ -1813,7 +1837,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
         Abc_Print( 1, "FrameMax = %d  ConfMax = %d  LearnMax = %d  Timeout = %d  RatioMin = %d %%.\n", 
             pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
-        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   LUT   Confl  Cex    SatVar   Core     Time\n" );
+        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   LUT   Confl  Cex  Vars  Clas  Lrns     Time      Mem\n" );
     }
     for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i )
     {

src/aig/gia/giaAbsVta.c

@@ -137,6 +137,27 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
 
 /**Function*************************************************************
 
+  Synopsis    [Prints integer number using 6 characters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_PrintInt( int i )
+{
+    if ( i > -1000 && i < 1000 )
+        printf( "%6d", i );
+    else if ( i > -1000000 && i < 1000000 )
+        printf( "%5dk", i/1000 );
+    else if ( i > -1000000000 && i < 1000000000 )
+        printf( "%5dm", i/1000000 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [This procedure sets default parameters.]
 
   Description []
@@ -1191,7 +1212,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
 {
     unsigned * pInfo;
     int * pCountAll = NULL, * pCountUni = NULL;
-    int i, k, iFrame, iObj, Entry, fChanges = 0;
+    int i, iFrame, iObj, Entry, fChanges = 0;
     // print info about frames
     if ( vCore )
     {
@@ -1240,12 +1261,15 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
         Abc_Print( 1, "%5c", '-' ); 
     else
         Abc_Print( 1, "%5d", nCexes ); 
-    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
+//    Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
+    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
+    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
+    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
     if ( vCore == NULL )
     {
         Abc_Print( 1, "    ..." ); 
-        for ( k = 0; k < 7; k++ )
-            Abc_Print( 1, "     " );
+//        for ( k = 0; k < 7; k++ )
+//            Abc_Print( 1, "     " );
         Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
         Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
         Abc_Print( 1, "\r" );
@@ -1253,6 +1277,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
     else
     {
         Abc_Print( 1, "%7d", pCountAll[0] ); 
+/*
         if ( nFrames > 7 )
         {
             for ( k = 0; k < 3; k++ )
@@ -1268,6 +1293,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
             for ( k = nFrames; k < 7; k++ )
                 Abc_Print( 1, "     " );
         }
+*/
         Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
         Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
         Abc_Print( 1, "\n" );
@@ -1572,7 +1598,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
         Abc_Print( 1, "FramePast = %d  FrameMax = %d  ConfMax = %d  LearnMax = %d  Timeout = %d  RatioMin = %d %%\n", 
             pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
-        Abc_Print( 1, "Frame   %%   Abs   %%   Confl  Cex    SatVar   Core   F0   F1   F2  ...\n" );
+//        Abc_Print( 1, "Frame   %%   Abs   %%   Confl  Cex    SatVar   Core   F0   F1   F2  ...\n" );
+        Abc_Print( 1, "Frame   %%   Abs   %%   Confl  Cex  Vars  Clas  Lrns   Core     Time      Mem\n" );
     }
     assert( Vec_PtrSize(p->vFrames) > 0 );
     for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )

src/sat/bsat/satSolver.c

@@ -1502,7 +1502,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     lbool   status        = l_Undef;
     lit*    i;
 
-//    printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+    if ( s->fVerbose )
+        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+
     ////////////////////////////////////////////////
     if ( s->fSolved )
     {

src/sat/bsat/satSolver2.c

@@ -1574,6 +1574,7 @@ void sat_solver2_rollback( sat_solver2* s )
     for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
         s->wlists[i].size = 0;
 
+
     // initialize other vars
     s->size = s->iVarPivot;
     if ( s->size == 0 )

src/sat/bsat/satSolver2.h

@@ -212,6 +212,11 @@ static inline int sat_solver2_nclauses(sat_solver2* s)
     return (int)s->stats.clauses;
 }
 
+static inline int sat_solver2_nlearnts(sat_solver2* s)
+{
+    return (int)s->stats.learnts;
+}
+
 static inline int sat_solver2_nconflicts(sat_solver2* s)
 {
     return (int)s->stats.conflicts;