Making 'pdr', &gla, &vta print correctly in batch mode.

10 files changed, 35 insertions, 11 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index cdfc7712..970ff26b 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1618,6 +1618,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
 ***********************************************************************/
 void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
 {
+    if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
+        return;
     Abc_Print( 1, "%3d :", nFrames-1 );
     Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) ); 
     Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
@@ -1820,7 +1822,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
                     pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
                     break;
                 }
-            }
+            } 
             Gia_GlaAddToAbs( p, vPPis, 1 );
             Gia_GlaAddOneSlice( p, f, vPPis );
             Vec_IntFree( vPPis );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index e7e5e7a6..91e609c5 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1226,6 +1226,9 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
         return fChanges;
     }
 
+    if ( Abc_FrameIsBatchMode() && !vCore )
+        return fChanges;
+
 //    Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] ); 
     Abc_Print( 1, "%3d :", nFrames-1 );
     Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) ); 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 0ab6c091..61283e09 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -412,7 +412,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
     printf( "  and =%8d", Gia_ManAndNum(p) );
     printf( "  lev =%5d", Gia_ManLevelNum(p) );
     printf( "  cut =%5d", Gia_ManCrossCut(p) );
-    printf( "  mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+    printf( "  mem =%5.2f Mb", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
+//    printf( "  mem =%5.2f Mb", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
     if ( Gia_ManHasDangling(p) )
         printf( "  ch =%5d", Gia_ManEquivCountClasses(p) );
     if ( fSwitch )
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 611d9593..c1abc54f 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -104,6 +104,7 @@ extern ABC_DLL void *          Abc_FrameReadManDd();
 extern ABC_DLL void *          Abc_FrameReadManDec();                    
 extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
 extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
+extern ABC_DLL int             Abc_FrameIsBatchMode();
 extern ABC_DLL int             Abc_FrameIsBridgeMode();
 extern ABC_DLL void            Abc_FrameSetBridgeMode();
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 50edb858..296bf7c2 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -79,6 +79,8 @@ void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateVal
 void        Abc_FrameSetCex( Abc_Cex_t * pCex )              { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex;       }
 void        Abc_FrameSetNFrames( int nFrames )               { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; }
 
+int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
+
 int         Abc_FrameIsBridgeMode()                          { return s_GlobalFrame ? s_GlobalFrame->fBridgeMode : 0;             } 
 void        Abc_FrameSetBridgeMode()                         { if ( s_GlobalFrame ) s_GlobalFrame->fBridgeMode = 1;               } 
 
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index a16d7f2e..aef02ba9 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -69,8 +69,8 @@ struct Abc_Frame_t_
     Abc_Ntk_t *     pNtkBestArea;  // the current network
     int             nSteps;        // the counter of different network processed
     int             fAutoexac;     // marks the autoexec mode
-    int                fBatchMode;       // are we invoked in batch mode?
-    int             fBridgeMode;   // are we invoked in bridge mode?
+    int                fBatchMode;       // batch mode flag
+    int             fBridgeMode;   // bridge mode flag
     // output streams
     FILE *          Out;
     FILE *          Err;
diff --git a/src/misc/bar/bar.c b/src/misc/bar/bar.c
index 565a969e..6610b415 100644
--- a/src/misc/bar/bar.c
+++ b/src/misc/bar/bar.c
@@ -144,7 +144,10 @@ void Bar_ProgressStop( Bar_Progress_t * p )
 void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
 {
     int i;
-    if ( p == NULL ) return;
+    if ( p == NULL ) 
+        return;
+    if ( Abc_FrameIsBatchMode() )
+        return;
     if ( pString )
         fprintf( p->pFile, "%s ", pString );
     for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
@@ -171,7 +174,10 @@ void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
 void Bar_ProgressClean( Bar_Progress_t * p )
 {
     int i;
-    if ( p == NULL ) return;
+    if ( p == NULL ) 
+        return;
+    if ( Abc_FrameIsBatchMode() )
+        return;
     for ( i = 0; i <= p->posTotal; i++ )
         fprintf( p->pFile, " " );
     fprintf( p->pFile, "\r" );
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
index ab0f5849..47b33196 100644
--- a/src/misc/extra/extraUtilProgress.c
+++ b/src/misc/extra/extraUtilProgress.c
@@ -136,7 +136,10 @@ void Extra_ProgressBarStop( ProgressBar * p )
 void Extra_ProgressBarShow( ProgressBar * p, char * pString )
 {
     int i;
-    if ( p == NULL ) return;
+    if ( p == NULL ) 
+        return;
+    if ( Abc_FrameIsBatchMode() )
+        return;
     if ( pString )
         fprintf( p->pFile, "%s ", pString );
     for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
@@ -163,7 +166,10 @@ void Extra_ProgressBarShow( ProgressBar * p, char * pString )
 void Extra_ProgressBarClean( ProgressBar * p )
 {
     int i;
-    if ( p == NULL ) return;
+    if ( p == NULL ) 
+        return;
+    if ( Abc_FrameIsBatchMode() )
+        return;
     for ( i = 0; i <= p->posTotal; i++ )
         fprintf( p->pFile, " " );
     fprintf( p->pFile, "\r" );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index c4a85875..f9b4a55d 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -50,6 +50,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
     int i, ThisSize, Length, LengthStart;
     if ( Vec_PtrSize(p->vSolvers) < 2 )
         return;
+    if ( Abc_FrameIsBatchMode() && !fClose )
+        return;
     // count the total length of the printout
     Length = 0;
     Vec_VecForEachLevel( p->vClauses, vVec, i )
@@ -78,7 +80,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
     for ( i = ThisSize; i < 70; i++ )
         Abc_Print( 1, " " );
     Abc_Print( 1, "%6d", p->nQueMax );
-    Abc_Print( 1, " %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+    Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     Abc_Print( 1, "%s", fClose ? "\n":"\r" );
     if ( fClose )
         p->nQueMax = 0;
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 445dda84..032bc5ba 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -20,6 +20,7 @@
 
 #include "sswInt.h"
 #include "src/aig/gia/giaAig.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1074,7 +1075,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
             if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
             {
                 if ( !fVerbose ) 
-                    printf( "\r" );
+                    printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
 //                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
                 Ssw_RarManPrepareRandom( nRandSeed );
                 Abc_CexFree( pAig->pSeqModel );
@@ -1108,7 +1109,7 @@ finish:
     if ( r == nRounds && f == nFrames )
     {
         if ( !fVerbose ) 
-            printf( "\r" );
+            printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
         printf( "Simulation did not assert POs in the first %d frames.         ", nRounds * nFrames );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }