Modifications to read SMTLIB file from stdin.

4 files changed, 75 insertions, 11 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 5954ec18..f789c03c 100644
--- a/src/base/wlc/wlc.h
+++ b/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 );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 88c91c51..84afb394 100644
--- a/src/base/wlc/wlcCom.c
+++ b/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********************************************************************
 
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 8c09467e..48171c35 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/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 );
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 35d3ed87..ec1ec567 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/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                                ///