Adding features related to the communication bridge.

6 files changed, 27 insertions, 5 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c8090460..c4d5df4c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -379,6 +379,12 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc,
 ***********************************************************************/
 void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex )
 {
+    // update bridge
+    if ( Abc_FrameIsBridgeMode() )
+    {
+        extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex );
+        Gia_ManToBridgeResult( stdout, pAbc->Status, *ppCex );
+    }
     // update CEX
     ABC_FREE( pAbc->pCex );
     pAbc->pCex = *ppCex;
@@ -23473,8 +23479,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    else
 //        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
 //    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
-    if ( pAbc->pGia->pCexSeq )
-        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 0e2ff9f4..1572af91 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -35,7 +35,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
 
 ////////////////////////////////////////////////////////////////////////
@@ -111,7 +111,7 @@ int Abc_RealMain( int argc, char * argv[] )
     sprintf( sWriteCmd, "write" );
     
     Extra_UtilGetoptReset();
-    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
+    while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:xb")) != EOF) {
         switch(c) {
             case 'c':
                 strcpy( sCommandUsr, globalUtilOptarg );
@@ -177,10 +177,20 @@ int Abc_RealMain( int argc, char * argv[] )
                 fBatch = 1;
                 break;
                 
+            case 'b':
+                Abc_FrameSetBridgeMode();
+                break;
+                
             default:
                 goto usage;
         }
     }
+
+    if ( Abc_FrameIsBridgeMode() )
+    {
+        extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
+        pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
+    }
     
     if ( fBatch )
     {
diff --git a/src/base/main/main.h b/src/base/main/main.h
index ac30f358..5d777b23 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -104,6 +104,8 @@ 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_FrameIsBridgeMode();
+extern ABC_DLL void            Abc_FrameSetBridgeMode();
 
 extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 6a63cdd6..fe9aff6a 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -78,6 +78,9 @@ void        Abc_FrameSetLibVer( void * pLib )                { s_GlobalFrame->pL
 void        Abc_FrameSetFlag( char * pFlag, char * pValue )  { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue );         } 
 void        Abc_FrameSetCex( Abc_Cex_t * pCex )              { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; }
 
+int         Abc_FrameIsBridgeMode()                          { return s_GlobalFrame->fBridgeMode;  } 
+void        Abc_FrameSetBridgeMode()                         { s_GlobalFrame->fBridgeMode = 0;     } 
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the flag is enabled without value or with value 1.]
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 2eca004e..d8a6c93e 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -70,6 +70,7 @@ struct Abc_Frame_t_
     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?
     // output streams
     FILE *          Out;
     FILE *          Err;
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index e263bc94..5b6dc893 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -120,7 +120,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
 {
     fprintf( pAbc->Err, "\n" );
     fprintf( pAbc->Err,
-             "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [file]\n", 
+             "usage: %s [-c cmd] [-f script] [-h] [-o file] [-s] [-t type] [-T type] [-x] [-b] [file]\n", 
              ProgName);
     fprintf( pAbc->Err, "    -c cmd\texecute commands `cmd'\n");
     fprintf( pAbc->Err, "    -F script\texecute commands from a script file and echo commands\n");
@@ -131,6 +131,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
     fprintf( pAbc->Err, "    -t type\tspecify input type (blif_mv (default), blif_mvs, blif, or none)\n");
     fprintf( pAbc->Err, "    -T type\tspecify output type (blif_mv (default), blif_mvs, blif, or none)\n");
     fprintf( pAbc->Err, "    -x\t\tequivalent to '-t none -T none'\n");
+    fprintf( pAbc->Err, "    -b\t\trunning in bridge mode\n");
     fprintf( pAbc->Err, "\n" );
 }