Adding logfile dump to print_status.

2 files changed, 70 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1bae5e24..17741905 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2819,15 +2819,26 @@ usage:
 ***********************************************************************/
 int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex );
     extern void Abc_NtkPrintPoEquivs( Abc_Ntk_t * pNtk );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c, fOutStatus = 0, fShort = 1;
+    char * pLogFileName = NULL;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "osh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Losh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'o':
             fOutStatus ^= 1;
             break;
@@ -2883,7 +2894,32 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->vStatuses )
     {
-        if ( fShort )
+        if ( pLogFileName )
+        {
+            Abc_Cex_t * pTemp = NULL;
+            FILE * pFile = fopen( pLogFileName, "wb" );
+            if ( pFile == NULL )
+            {
+                printf( "Cannot open file \"%s\" for writing.\n", pLogFileName );
+                return 0;
+            }
+            Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
+            {
+                int Status = Vec_IntEntry( pAbc->vStatuses, c );
+                if ( Status == -1 ) // undec
+                    fprintf( pFile, "STATUS: ABORTED " );
+                else if ( Status == 0 )
+                    fprintf( pFile, "STATUS: SAT " );
+                else if ( Status == 1 )
+                    fprintf( pFile, "STATUS: UNSAT " );
+                fprintf( pFile, "%s\n", Abc_ObjName(Abc_NtkPo(pNtk, c)) );
+                if ( Status != 0 )
+                    continue;
+                Abc_NtkDumpOneCexSpecial( pFile, pNtk, pTemp );
+            }
+            fclose( pFile );
+        }
+        else if ( fShort )
         {
             printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).",
                 Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1),
@@ -2900,11 +2936,12 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: print_status [-osh]\n" );
-    Abc_Print( -2, "\t        prints verification status\n" );
-    Abc_Print( -2, "\t-o    : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" );
-    Abc_Print( -2, "\t-s    : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: print_status [-L file] [-osh]\n" );
+    Abc_Print( -2, "\t          prints verification status\n" );
+    Abc_Print( -2, "\t-L file : the log file name [default = %s]\n",  pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-o      : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" );
+    Abc_Print( -2, "\t-s      : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
+    Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
 }
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 669405cc..843b0ff6 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2326,6 +2326,32 @@ int Abc_NtkCheckSpecialPi( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
+{
+    Abc_Cex_t * pCare = NULL; int i, f; Abc_Obj_t * pObj;
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+    //fprintf( pFile, "# FALSIFYING OUTPUTS:");                                       
+    //fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); 
+    pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, 0, 0 );
+    Aig_ManStop( pAig );
+    if( pCare == NULL )   
+    {
+        printf( "Counter-example minimization has failed.\n" ); 
+        return;
+    }
+    // output flop values (unaffected by the minimization)
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        fprintf( pFile, "CEX: %s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+    // output PI values (while skipping the minimized ones)
+    for ( f = 0; f <= pCex->iFrame; f++ )
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
+                fprintf( pFile, "CEX: %s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+    Abc_CexFreeP( &pCare );
+}
+
+
 void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, 
     int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, 
     int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose )