Modifications to read SMTLIB file from stdin.

1 files changed, 31 insertions, 2 deletions

diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c
index 204e7491..04152ae6 100644
--- a/src/base/main/mainReal.c
+++ b/src/base/main/mainReal.c
@@ -51,6 +51,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 
 #include "base/abc/abc.h"
 #include "mainInt.h"
+#include "base/wlc/wlc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -90,7 +91,8 @@ int Abc_RealMain( int argc, char * argv[] )
         INTERACTIVE, // interactive mode
         BATCH, // batch mode, run a command and quit
         BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode
-        BATCH_QUIET // as in batch mode, but don't echo the command
+        BATCH_QUIET, // as in batch mode, but don't echo the command
+        BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin
     } fBatch;
 
     // added to detect memory leaks
@@ -138,7 +140,7 @@ int Abc_RealMain( int argc, char * argv[] )
     sprintf( sWriteCmd, "write" );
 
     Extra_UtilGetoptReset();
-    while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:hf:F:o:st:T:xb")) != EOF) {
+    while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:S:hf:F:o:st:T:xb")) != EOF) {
         switch(c) {
             case 'c':
                 strcpy( sCommandUsr, globalUtilOptarg );
@@ -155,6 +157,11 @@ int Abc_RealMain( int argc, char * argv[] )
                 fBatch = BATCH_THEN_INTERACTIVE;
                 break;
 
+            case 'S':
+                strcpy( sCommandUsr, globalUtilOptarg );
+                fBatch = BATCH_SMT;
+                break;
+
             case 'f':
                 sprintf(sCommandUsr, "source %s", globalUtilOptarg);
                 fBatch = BATCH;
@@ -223,6 +230,28 @@ int Abc_RealMain( int argc, char * argv[] )
         }
     }
 
+    if ( fBatch == BATCH_SMT )
+    {
+        Wlc_Ntk_t * pNtk;
+        Vec_Str_t * vInput;
+        // collect stdin
+        vInput = Wlc_GenerateSmtStdin();
+        // parse the input
+        pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput) );
+        Vec_StrFree( vInput );
+        // install current network
+        Wlc_SetNtk( pAbc, pNtk );
+        // execute command
+        fStatus = Cmd_CommandExecute( pAbc, sCommandUsr );
+        // generate output
+        if ( !fStatus )
+            Wlc_GenerateSmtStdout( pAbc );
+        else
+            Abc_Print( 1, "Something did not work out with the command \"%s\".\n", sCommandUsr );
+        Abc_Stop();
+        return 0;
+    }
+
     if ( Abc_FrameIsBridgeMode() )
     {
         extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );