Various usability changes (second round).

3 files changed, 82 insertions, 2 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e26be80b..753bf2ae 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10992,6 +10992,11 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Reachability analysis works only for AIGs (run \"strash\").\n" );
         return 1;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     pAbc->Status  = Abc_NtkDarReach( pNtk, pPars );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -23901,12 +23906,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         Abc_Print( -1, "This command works only for structrally hashed networks. Run \"st\".\n" );
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
 
     // perform verification
     pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar, nBmcFramesMax, nBmcConfMax );
@@ -25605,6 +25614,11 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Does not work for combinational networks.\n" );
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     pAbc->Status = Abc_NtkDarBmc( pNtk, 0, nFrames, nSizeMax, nNodeDelta, 0, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, nCofFanLit, fVerbose, &iFrames, fUseSatoko );
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -25800,6 +25814,11 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Does not work for combinational networks.\n" );
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     pAbc->Status = Abc_NtkDarBmc( pNtk, nStart, nFrames, nSizeMax, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fOrDecomp, 0, fVerbose, &iFrames, fUseSatoko );
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -26054,6 +26073,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" );
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     pPars->fUseBridge = pAbc->fBridgeMode;
     pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
     pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
@@ -26260,6 +26284,11 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         Abc_Print( -1, "Does not work for combinational networks.\n" );
@@ -27991,6 +28020,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n");
         return 0;
     }
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         pNtkFlop = Abc_NtkDup( pNtk );
@@ -44473,6 +44507,11 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 */
+    if ( pAbc->fBatchMode && (pAbc->Status == 0 || pAbc->Status == 1) ) 
+    { 
+        Abc_Print( 1, "The miters is already solved; skipping the command.\n" ); 
+        return 0;
+    }
     if ( pAbc->pGia->vGateClasses == NULL )
     {
         Abc_Print( -1, "Abstraction gate map is missing.\n" );
diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c
index 31bfef75..f33c0125 100644
--- a/src/base/main/mainReal.c
+++ b/src/base/main/mainReal.c
@@ -44,6 +44,14 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 
 ***********************************************************************/
 
+#ifndef WIN32
+#include <sys/time.h>    
+#include <sys/times.h>   
+#include <sys/resource.h>
+#include <unistd.h>      
+#include <signal.h>      
+#include <malloc.h>      
+#endif
 
 #include "base/abc/abc.h"
 #include "mainInt.h"
@@ -62,6 +70,7 @@ static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+unsigned enable_dbg_outs = 1;  
 
 /**Function*************************************************************
 
@@ -115,8 +124,37 @@ int Abc_RealMain( int argc, char * argv[] )
     sprintf( sWriteCmd, "write" );
 
     Extra_UtilGetoptReset();
-    while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:Q:S:hf:F:o:st:T:xb")) != EOF) {
+    while ((c = Extra_UtilGetopt(argc, argv, "dm:l:c:q:C:Q:S:hf:F:o:st:T:xb")) != EOF) {
         switch(c) {
+
+            case 'd':                                          
+                enable_dbg_outs ^= 1;                            
+                break;                                          
+
+            case 'm':
+#ifndef WIN32
+                int maxMb = atoi(globalUtilOptarg);             
+                printf("Limiting memory use to %d MB\n", maxMb);
+                struct rlimit limit = {                         
+                    maxMb * (1llu << 20), /* soft limit */      
+                    maxMb * (1llu << 20)  /* hard limit */      
+                };                                              
+                setrlimit(RLIMIT_AS, &limit);                   
+#endif
+                break;                                          
+
+            case 'l':
+#ifndef WIN32
+                int maxTime = atoi(globalUtilOptarg);           
+                printf("Limiting time to %d seconds\n", maxTime);
+                struct rlimit limit = {                         
+                    maxTime,             /* soft limit */       
+                    maxTime              /* hard limit */       
+                };                                              
+                setrlimit(RLIMIT_CPU, &limit);                  
+#endif
+                break;                                          
+
             case 'c':
                 if( Vec_StrSize(sCommandUsr) > 0 )
                 {
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 14523abd..c27b907e 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -357,6 +357,9 @@ static inline void Abc_Print( int level, const char * format, ... )
 {
     extern ABC_DLL int Abc_FrameIsBridgeMode();
     va_list args;
+    extern unsigned enable_dbg_outs;  
+    if ( !enable_dbg_outs )
+        return;
 
     if ( ! Abc_FrameIsBridgeMode() ){
         if ( level == ABC_ERROR )