Modifications to read SMTLIB file from stdin.

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 );

src/base/wlc/wlc.h

@@ -32,6 +32,7 @@
 #include "misc/mem/mem.h"
 #include "misc/extra/extra.h"
 #include "misc/util/utilTruth.h"
+#include "base/main/mainInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -238,6 +239,10 @@ extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes
 extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
 /*=== wlcBlast.c ========================================================*/
 extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
+/*=== wlcCom.c ========================================================*/
+extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
+extern Vec_Str_t *    Wlc_GenerateSmtStdin();
+extern void           Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc );
 /*=== wlcNtk.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
@@ -253,6 +258,7 @@ extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbo
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 /*=== wlcReadSmt.c ========================================================*/
+extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit );
 extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName );
 /*=== wlcReadVer.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName );

src/base/wlc/wlcCom.c

@@ -78,6 +78,59 @@ void Wlc_End( Abc_Frame_t * pAbc )
     Wlc_AbcFreeNtk( pAbc );
 }
 
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )
+{
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads stdin and stops when "(check-sat)" is observed.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSize )
+{
+    char * pStr = Vec_StrArray(vInput) + Vec_StrSize(vInput) - LineSize;
+    if ( Vec_StrSize(vInput) < LineSize )
+        return 0;
+    return !strncmp( pStr, pLine, LineSize );
+}
+Vec_Str_t * Wlc_GenerateSmtStdin()
+{
+    char * pLine = "(check-sat)";
+    int c, LineSize = strlen(pLine);
+    Vec_Str_t * vInput = Vec_StrAlloc( 1000 );
+    while ( (c = fgetc(stdin)) != EOF )
+    {
+        Vec_StrPush( vInput, (char)c );
+        if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) )
+            break;
+    }
+    Vec_StrPush( vInput, '\0' );
+    return vInput;
+}
+void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc )
+{
+    printf( "Output produced by SMT solver will be here.\n" );
+}
 
 /**Function********************************************************************
 

src/base/wlc/wlcNtk.c

@@ -95,7 +95,7 @@ Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc )
 {
     Wlc_Ntk_t * p;
     p = ABC_CALLOC( Wlc_Ntk_t, 1 );
-    p->pName = Extra_FileNameGeneric( pName );
+    p->pName = pName ? Extra_FileNameGeneric( pName ) : NULL;
     Vec_IntGrow( &p->vPis, 111 );
     Vec_IntGrow( &p->vPos, 111 );
     Vec_IntGrow( &p->vCis, 111 );

src/base/wlc/wlcReadSmt.c

@@ -99,13 +99,9 @@ static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit )
     *ppLimit = pBuffer + nFileSize + 2;
     return pBuffer;
 }
-static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName )
+static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName, char * pBuffer, char * pLimit )
 {
     Prs_Smt_t * p;
-    char * pBuffer, * pLimit;
-    pBuffer = Prs_SmtLoadFile( pFileName, &pLimit );
-    if ( pBuffer == NULL )
-        return NULL;
     p = ABC_CALLOC( Prs_Smt_t, 1 );
     p->pName   = pFileName;
     p->pBuffer = pBuffer;
@@ -121,7 +117,6 @@ static inline void Prs_SmtFree( Prs_Smt_t * p )
     if ( p->pStrs )
         Abc_NamDeref( p->pStrs );
     Vec_IntErase( &p->vData );
-    ABC_FREE( p->pBuffer );
     ABC_FREE( p );
 }
 
@@ -655,22 +650,32 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
     Vec_IntFree( vFanins );
     return pNtk;
 }
-Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
 {
     Wlc_Ntk_t * pNtk = NULL;
-    Prs_Smt_t * p = Prs_SmtAlloc( pFileName );
+    Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit );
     if ( p == NULL )
         return NULL;
     Prs_SmtRemoveComments( p );
     Prs_SmtReadLines( p );
     //Prs_SmtPrintParser( p );
     if ( Prs_SmtErrorPrint(p) )
-    {
         pNtk = Prs_SmtBuild( p );
-    }
     Prs_SmtFree( p );
     return pNtk;
 }
+Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+{
+    Wlc_Ntk_t * pNtk = NULL;
+    Prs_Smt_t * p = NULL;
+    char * pBuffer, * pLimit;
+    pBuffer = Prs_SmtLoadFile( pFileName, &pLimit );
+    if ( pBuffer == NULL )
+        return NULL;
+    pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit );
+    ABC_FREE( pBuffer );
+    return pNtk;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///