Added SMT parser for Wlc_Ntk_t.

8 files changed, 729 insertions, 54 deletions

diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index 9229d876..9e2e3789 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -209,7 +209,7 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" )  )
     {
-        vDes = Prs_ManReadSmt( pFileName );
+        vDes = NULL;//Prs_ManReadSmt( pFileName );
         if ( vDes && Vec_PtrSize(vDes) )
             p = Prs_ManBuildCba( pFileName, vDes );
         Prs_ManVecFree( vDes );
@@ -647,6 +647,7 @@ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Prs_ManReadBlifTest();
     extern void Prs_ManReadVerilogTest();
+    extern void Prs_SmtReadSmtTest();
     //Cba_Man_t * p = Cba_AbcGetMan(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
@@ -671,7 +672,8 @@ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
     //Cba_PtrTransformTestTest();
-    Prs_ManReadVerilogTest();
+    //Prs_ManReadVerilogTest();
+    //Prs_SmtReadSmtTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: @test [-vh]\n" );
diff --git a/src/base/cba/cbaReadSmt.c b/src/base/cba/cbaReadSmt.c
index 5099e80d..a9dd83dd 100644
--- a/src/base/cba/cbaReadSmt.c
+++ b/src/base/cba/cbaReadSmt.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "cba.h"
-#include "cbaPrs.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,29 +31,6 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Prs_ManReadSmt( char * pFileName )
-{
-    Vec_Ptr_t * vPrs = NULL;
-    Prs_Man_t * p = Prs_ManAlloc( pFileName );
-    if ( p == NULL )
-        return NULL;
-//    Prs_ManReadLines( p );
-    if ( Prs_ManErrorPrint(p) )
-        ABC_SWAP( Vec_Ptr_t *, vPrs, p->vNtks );
-    Prs_ManFree( p );
-    return vPrs;
-}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 84cc7620..717444d0 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -2,5 +2,6 @@ SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
     src/base/wlc/wlcNtk.c \
+    src/base/wlc/wlcReadSmt.c \
     src/base/wlc/wlcReadVer.c \
     src/base/wlc/wlcWriteVer.c 
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 3b7c9153..5954ec18 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -252,9 +252,11 @@ extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
-/*=== wlcReadWord.c ========================================================*/
+/*=== wlcReadSmt.c ========================================================*/
+extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName );
+/*=== wlcReadVer.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName );
-/*=== wlcWriteWord.c ========================================================*/
+/*=== wlcWriteVer.c ========================================================*/
 extern void           Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName );
 
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 68373522..88c91c51 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -28,8 +28,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int  Abc_CommandReadVer  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandWriteVer ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandReadWlc  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -55,8 +55,8 @@ static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk
 ******************************************************************************/
 void Wlc_Init( Abc_Frame_t * pAbc )
 {
-    Cmd_CommandAdd( pAbc, "Word level", "%read_ver",   Abc_CommandReadVer,   0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%write_ver",  Abc_CommandWriteVer,  0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%read",       Abc_CommandReadWlc,   0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%write",      Abc_CommandWriteWlc,  0 );
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
@@ -90,7 +90,7 @@ void Wlc_End( Abc_Frame_t * pAbc )
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
     Wlc_Ntk_t * pNtk = NULL;
@@ -112,7 +112,7 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( argc != globalUtilOptind + 1 )
     {
-        printf( "Abc_CommandReadVer(): Input file name should be given on the command line.\n" );
+        printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
         return 0;
     }
     // get the file name
@@ -120,7 +120,7 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( pFileName, "r" )) == NULL )
     {
         Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".smt", NULL, NULL, NULL )) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".smt", ".smt2", NULL, NULL )) )
             Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
         Abc_Print( 1, "\n" );
         return 0;
@@ -128,11 +128,19 @@ int Abc_CommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // perform reading
-    pNtk = Wlc_ReadVer( pFileName );
+    if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        pNtk = Wlc_ReadVer( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" )  )
+        pNtk = Wlc_ReadSmt( pFileName );
+    else
+    {
+        printf( "Abc_CommandReadWlc(): Unknown file extension.\n" );
+        return 0;
+    }
     Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%read_ver [-vh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%read [-vh] <file_name>\n" );
     Abc_Print( -2, "\t         reads word-level design from Verilog file\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -150,7 +158,7 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
-int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     char * pFileName = NULL;
@@ -171,7 +179,7 @@ int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandWriteVer(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandWriteWlc(): There is no current design.\n" );
         return 0;
     }
     if ( argc == globalUtilOptind )
@@ -186,7 +194,7 @@ int Abc_CommandWriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_WriteVer( pNtk, pFileName );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%write_ver [-vh]\n" );
+    Abc_Print( -2, "usage: %%write [-vh]\n" );
     Abc_Print( -2, "\t         writes the design into a file\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",        fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 90287781..8c09467e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -471,7 +471,9 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
         Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
         Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    if ( p->vInits )
     pNew->vInits = Vec_IntDup( p->vInits );
+    if ( p->pInits )
     pNew->pInits = Abc_UtilStrsav( p->pInits );
     Vec_IntFree( vFanins );
     return pNew;
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
new file mode 100644
index 00000000..35d3ed87
--- /dev/null
+++ b/src/base/wlc/wlcReadSmt.c
@@ -0,0 +1,681 @@
+/**CFile****************************************************************
+
+  FileName    [wlcReadSmt.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// parser name types
+typedef enum { 
+    PRS_SMT_NONE = 0, 
+    PRS_SMT_INPUT,    
+    PRS_SMT_CONST,    
+    PRS_SMT_LET,   
+    PRS_SMT_ASSERT
+} Prs_ManType_t; 
+
+// parser
+typedef struct Prs_Smt_t_ Prs_Smt_t;
+struct Prs_Smt_t_
+{
+    // input data
+    char *       pName;       // file name
+    char *       pBuffer;     // file contents
+    char *       pLimit;      // end of file
+    char *       pCur;        // current position
+    Abc_Nam_t *  pStrs;       // string manager
+    // network structure
+    Vec_Int_t    vData;       
+    // error handling
+    char ErrorStr[1000];      
+};
+
+
+// create error message
+static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value )
+{
+    assert( !p->ErrorStr[0] );
+    sprintf( p->ErrorStr, "%s", pError );
+    return Value;
+}
+// clear error message
+static inline void Prs_SmtErrorClear( Prs_Smt_t * p )
+{
+    p->ErrorStr[0] = '\0';
+}
+// print error message
+static inline int Prs_SmtErrorPrint( Prs_Smt_t * p )
+{
+    char * pThis; int iLine = 0;
+    if ( !p->ErrorStr[0] ) return 1;
+    for ( pThis = p->pBuffer; pThis < p->pCur; pThis++ )
+        iLine += (int)(*pThis == '\n');
+    printf( "Line %d: %s\n", iLine, p->ErrorStr );
+    return 0;
+}
+static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit )
+{
+    char * pBuffer;
+    int nFileSize, RetValue;
+    FILE * pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open input file.\n" );
+        return NULL;
+    }
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
+    pBuffer[0] = '\n';
+    RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[nFileSize + 0] = '\n';
+    pBuffer[nFileSize + 1] = '\0';
+    *ppLimit = pBuffer + nFileSize + 2;
+    return pBuffer;
+}
+static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName )
+{
+    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;
+    p->pLimit  = pLimit;
+    p->pCur    = pBuffer;
+    p->pStrs   = Abc_NamStart( 1000, 24 );
+    Vec_IntGrow ( &p->vData, 1000 );
+    return p;
+}
+
+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 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Prs_SmtRemoveComments( Prs_Smt_t * p )
+{
+    char * pTemp;
+    for ( pTemp = p->pBuffer; pTemp < p->pLimit; pTemp++ )
+        if ( *pTemp == ';' )
+            while ( *pTemp && *pTemp != '\n' )
+                *pTemp++ = ' ';
+}
+static inline void Prs_SmtSkipSpaces( Prs_Smt_t * p )
+{
+    while ( *p->pCur == ' ' || *p->pCur == '\t' || *p->pCur == '\r' || *p->pCur == '\n' )
+        p->pCur++;
+}
+static inline int Prs_SmtIsWord( Prs_Smt_t * p, char * pWord )
+{
+    Prs_SmtSkipSpaces( p );
+    if ( strncmp( p->pCur, pWord, strlen(pWord) ) )
+        return 0;
+    p->pCur += strlen(pWord);
+    Prs_SmtSkipSpaces( p );
+    return 1;
+}
+static inline char * Prs_SmtFindNextPar( Prs_Smt_t * p )
+{
+    char * pTemp; int Count = 1;
+    for ( pTemp = p->pCur; pTemp < p->pLimit; pTemp++ )
+    {
+        if ( *pTemp == '(' )
+            Count++;
+        else if ( *pTemp == ')' )
+            Count--;
+        if ( Count == 0 )
+            break;
+    }
+    assert( *pTemp == ')' );
+    return pTemp;
+}
+static inline int Prs_SmtParseLet( Prs_Smt_t * p, char * pLimit, int Type )
+{
+    char * pToken;
+    assert( *pLimit == ')' );
+    *pLimit = 0;
+    Vec_IntPush( &p->vData, 0 );
+    Vec_IntPush( &p->vData, Type );
+    pToken = strtok( p->pCur, " ()" );
+    while ( pToken )
+    {
+        if ( pToken[0] != '_' && pToken[0] != '=' )
+            Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
+        pToken = strtok( NULL, " ()" );
+    }
+    assert( *pLimit == 0 );
+    *pLimit = ')';
+    p->pCur = pLimit;
+    return 1;
+}
+static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type )
+{
+    char * pToken;
+    assert( *pLimit == ')' );
+    *pLimit = 0;
+    Vec_IntPush( &p->vData, 0 );
+    Vec_IntPush( &p->vData, Type );
+    pToken = strtok( p->pCur, " ()" );
+    assert( pToken != NULL );
+    Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
+    pToken = strtok( NULL, " ()" );
+    if ( pToken[0] == '_' )
+        pToken = strtok( NULL, " ()" );
+    if ( !strcmp(pToken, "Bool") )
+    {
+        Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "1", NULL) );
+        pToken = strtok( NULL, " ()" );
+        if ( !strcmp(pToken, "false") )
+            Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b0", NULL) );
+        else if ( !strcmp(pToken, "true") )
+            Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, "#b1", NULL) );
+        else assert( 0 );
+    }
+    else if ( !strcmp(pToken, "BitVec") )
+    {
+        pToken = strtok( NULL, " ()" );
+        Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
+        pToken = strtok( NULL, " ()" );
+        if ( pToken )
+        {
+            Vec_IntPush( &p->vData, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
+            pToken = strtok( NULL, " ()" );
+            if ( pToken != NULL )
+                return Prs_SmtErrorSet(p, "Trailing symbols are not recognized.", 0);
+        }
+    }
+    else 
+        return Prs_SmtErrorSet(p, "Expecting either \"Bool\" or \"BitVec\".", 0);
+    assert( *pLimit == 0 );
+    *pLimit = ')';
+    p->pCur = pLimit;
+    return 1;
+}
+int Prs_SmtReadLines( Prs_Smt_t * p )
+{
+    Prs_SmtSkipSpaces( p );
+    while ( *p->pCur == '(' )
+    {
+        p->pCur++;
+        if ( Prs_SmtIsWord(p, "let") )
+        {
+            assert( *p->pCur == '(' );
+            p->pCur++;
+            if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_LET ) )
+                return 0;
+            assert( *p->pCur == ')' );
+            p->pCur++;
+        }
+        else if ( Prs_SmtIsWord(p, "declare-fun")  )
+        {
+            if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_INPUT ) )
+                return 0;
+            assert( *p->pCur == ')' );
+            p->pCur++;
+        }
+        else if ( Prs_SmtIsWord(p, "define-fun") )
+        {
+            if ( !Prs_SmtParseFun( p, Prs_SmtFindNextPar(p), PRS_SMT_CONST ) )
+                return 0;
+            assert( *p->pCur == ')' );
+            p->pCur++;
+        }
+        else if ( Prs_SmtIsWord(p, "check-sat") )
+        {
+            Vec_IntPush( &p->vData, 0 );
+            return 1;
+        }
+        else if ( Prs_SmtIsWord(p, "assert") )
+        {}
+        else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") )
+            p->pCur = Prs_SmtFindNextPar(p) + 1;
+        else
+            break;
+            //return Prs_SmtErrorSet(p, "Unsupported directive.", 0);
+        Prs_SmtSkipSpaces( p );
+    }
+    // finish parsing assert
+    if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) )
+        return 0;
+    assert( *p->pCur == ')' );
+    Vec_IntPush( &p->vData, 0 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Prs_SmtPrintParser( Prs_Smt_t * p )
+{
+    int Entry, i;
+    Vec_IntForEachEntry( &p->vData, Entry, i )
+    {
+        if ( Entry == 0 )
+        {
+            printf( "\n" );
+            if ( i == Vec_IntSize(&p->vData) - 1 )
+                break;
+            Entry = Vec_IntEntry(&p->vData, ++i);
+            if ( Entry == PRS_SMT_INPUT )
+                printf( "declare-fun" );
+            else if ( Entry == PRS_SMT_CONST )
+                printf( "define-fun" );
+            else if ( Entry == PRS_SMT_LET )
+                printf( "let" );
+            else if ( Entry == PRS_SMT_ASSERT )
+                printf( "assert" );
+            else assert(0);
+            continue;
+        }
+        printf( " %s", Abc_NamStr(p->pStrs, Entry) );
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Prs_SmtReadConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins, char * pName )
+{
+    char Buffer[100];
+    int i, nDigits, iObj, NameId, fFound;
+    Vec_IntClear( vFanins );
+    if ( pStr[0] != '#' )
+    {
+        // handle decimal number
+        int Number = atoi( pStr );
+        nBits = Abc_Base2Log( Number+1 );
+        assert( nBits < 32 );
+        Vec_IntPush( vFanins, Number );
+    }
+    else if ( pStr[1] == 'b' )
+    {
+        if ( nBits == -1 )
+            nBits = strlen(pStr+2);
+        Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
+        for ( i = 0; i < nBits; i++ )
+            if ( pStr[2+i] == '1' )
+                Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i );
+            else if ( pStr[2+i] != '0' )
+                return 0;
+    }
+    else if ( pStr[1] == 'x' )
+    {
+        if ( nBits == -1 )
+            nBits = strlen(pStr+2)*4;
+        Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
+        nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 );
+        if ( nDigits != (nBits + 3)/4 )
+            assert( 0 );
+    }
+    else return 0;
+    // create constant node
+    iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_CONST, 0, nBits-1, 0 );
+    Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+    // add node's name
+    if ( pName == NULL )
+    {
+        sprintf( Buffer, "_c%d_", iObj );
+        pName = Buffer;
+    }
+    NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+    assert( !fFound );
+    assert( iObj == NameId );
+    return NameId;
+}
+static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec_Int_t * vFanins )
+{
+    if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' )
+    {
+        Vec_Int_t * vTemp = Vec_IntAlloc(0);
+        int NameId = Prs_SmtReadConstant( pNtk, pStr, nBits, vTemp, NULL );
+        Vec_IntFree( vTemp );
+        if ( !NameId )
+            return 0;
+        Vec_IntPush( vFanins, NameId );
+        return 1;
+    }
+    else
+    {
+        // read name
+        int fFound, NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
+        assert( fFound );
+        Vec_IntPush( vFanins, NameId );
+        return 1;
+    }
+}
+static inline int Prs_SmtStrToType( char * pName )
+{
+    int Type = 0;
+    if ( !strcmp(pName, "ite") )
+        Type = WLC_OBJ_MUX;           // 08: multiplexer
+    else if ( !strcmp(pName, "bvlshr") )
+        Type = WLC_OBJ_SHIFT_R;       // 09: shift right
+    else if ( !strcmp(pName, "bvashr") )
+        Type = WLC_OBJ_SHIFT_RA;      // 10: shift right (arithmetic)
+    else if ( !strcmp(pName, "bvshl") )
+        Type = WLC_OBJ_SHIFT_L;       // 11: shift left
+//    else if ( !strcmp(pName, "") )
+//        Type = WLC_OBJ_SHIFT_LA;    // 12: shift left (arithmetic)
+    else if ( !strcmp(pName, "rotate_right") )
+        Type = WLC_OBJ_ROTATE_R;      // 13: rotate right
+    else if ( !strcmp(pName, "rotate_left") )
+        Type = WLC_OBJ_ROTATE_L;      // 14: rotate left
+    else if ( !strcmp(pName, "bvnot") )
+        Type = WLC_OBJ_BIT_NOT;       // 15: bitwise NOT
+    else if ( !strcmp(pName, "bvand") )
+        Type = WLC_OBJ_BIT_AND;       // 16: bitwise AND
+    else if ( !strcmp(pName, "bvor") )
+        Type = WLC_OBJ_BIT_OR;        // 17: bitwise OR
+    else if ( !strcmp(pName, "bvxor") )
+        Type = WLC_OBJ_BIT_XOR;       // 18: bitwise XOR
+    else if ( !strcmp(pName, "extract") )
+        Type = WLC_OBJ_BIT_SELECT;    // 19: bit selection
+    else if ( !strcmp(pName, "concat") )
+        Type = WLC_OBJ_BIT_CONCAT;    // 20: bit concatenation
+    else if ( !strcmp(pName, "zero_extend") )
+        Type = WLC_OBJ_BIT_ZEROPAD;   // 21: zero padding
+    else if ( !strcmp(pName, "sign_extend") )
+        Type = WLC_OBJ_BIT_SIGNEXT;   // 22: sign extension
+    else if ( !strcmp(pName, "not") )
+        Type = WLC_OBJ_LOGIC_NOT;     // 23: logic NOT
+    else if ( !strcmp(pName, "and") )
+        Type = WLC_OBJ_LOGIC_AND;     // 24: logic AND
+    else if ( !strcmp(pName, "or") )
+        Type = WLC_OBJ_LOGIC_OR;      // 25: logic OR
+    else if ( !strcmp(pName, "bvcomp") )
+        Type = WLC_OBJ_COMP_EQU;      // 26: compare equal
+//    else if ( !strcmp(pName, "") )
+//        Type = WLC_OBJ_COMP_NOTEQU;   // 27: compare not equal
+    else if ( !strcmp(pName, "bvult") )
+        Type = WLC_OBJ_COMP_LESS;     // 28: compare less
+    else if ( !strcmp(pName, "bvugt") )
+        Type = WLC_OBJ_COMP_MORE;     // 29: compare more
+    else if ( !strcmp(pName, "bvule") )
+        Type = WLC_OBJ_COMP_LESSEQU;  // 30: compare less or equal
+    else if ( !strcmp(pName, "bvuge") )
+        Type = WLC_OBJ_COMP_MOREEQU;  // 31: compare more or equal
+    else if ( !strcmp(pName, "bvredand") )
+        Type = WLC_OBJ_REDUCT_AND;    // 32: reduction AND
+    else if ( !strcmp(pName, "bvredor") )
+        Type = WLC_OBJ_REDUCT_OR;     // 33: reduction OR
+    else if ( !strcmp(pName, "bvredxor") )
+        Type = WLC_OBJ_REDUCT_XOR;    // 34: reduction XOR
+    else if ( !strcmp(pName, "bvadd") )
+        Type = WLC_OBJ_ARI_ADD;       // 35: arithmetic addition
+    else if ( !strcmp(pName, "bvsub") )
+        Type = WLC_OBJ_ARI_SUB;       // 36: arithmetic subtraction
+    else if ( !strcmp(pName, "bvmul") )
+        Type = WLC_OBJ_ARI_MULTI;     // 37: arithmetic multiplier
+    else if ( !strcmp(pName, "bvdiv") )
+        Type = WLC_OBJ_ARI_DIVIDE;    // 38: arithmetic division
+    else if ( !strcmp(pName, "bvurem") )
+        Type = WLC_OBJ_ARI_MODULUS;   // 39: arithmetic modulus
+//    else if ( !strcmp(pName, "") )
+//        Type = WLC_OBJ_ARI_POWER;     // 40: arithmetic power
+    else if ( !strcmp(pName, "bvneg") )
+        Type = WLC_OBJ_ARI_MINUS;     // 41: arithmetic minus
+//    else if ( !strcmp(pName, "") )
+//        Type = WLC_OBJ_TABLE;         // 42: bit table
+    else assert( 0 );
+    return Type;
+}
+static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange )
+{
+    int Type, NameId;
+    char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) );
+    // read type
+    Type = Prs_SmtStrToType( pName );
+    if ( Type == 0 )
+        return 0;
+    *pRange = 0;
+    Vec_IntClear( vFanins );
+    if ( Type == WLC_OBJ_COMP_EQU )
+    {
+        *pRange = 1;
+        Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins );
+        Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins );
+        return WLC_OBJ_COMP_EQU;
+    }
+    else if ( Type == WLC_OBJ_LOGIC_NOT )
+    {
+        pName  = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+        if ( !strcmp(pName, "bvcomp") )
+        {
+            *pRange = 1;
+            Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins );
+            Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, ++i)), -1, vFanins );
+            return WLC_OBJ_COMP_NOTEQU;   // 26: compare equal
+        }
+        i--;
+    }
+    else if ( Type == WLC_OBJ_BIT_SELECT )
+    {
+        int End, Beg;
+        pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+        End = atoi( pName );
+        pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+        Beg = atoi( pName );
+        pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+        Prs_SmtReadName( pNtk, pName, -1, vFanins );
+        Vec_IntPush( vFanins, (End << 16) | Beg );
+        *pRange = End - Beg + 1;
+        return WLC_OBJ_BIT_SELECT;
+    }
+    while ( Vec_IntEntry(vData, ++i) )
+        Prs_SmtReadName( pNtk, Abc_NamStr(p->pStrs, Vec_IntEntry(vData, i)), -1, vFanins );
+    if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L )
+    {
+        int * pArray = Vec_IntArray(vFanins);
+        assert( Vec_IntSize(vFanins) == 2 );
+        ABC_SWAP( int, pArray[0], pArray[1] );
+    }    
+    if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR )
+        *pRange = 1;
+    else if ( Type == WLC_OBJ_BIT_CONCAT )
+    {
+        int k;
+        Vec_IntForEachEntry( vFanins, NameId, k )
+            *pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+    }
+    else if ( Type == WLC_OBJ_MUX )
+    {
+        int * pArray = Vec_IntArray(vFanins);
+        assert( Vec_IntSize(vFanins) == 3 );
+        ABC_SWAP( int, pArray[1], pArray[2] );
+        NameId = Vec_IntEntry(vFanins, 1);
+        *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+    }
+    else // to determine range, look at the first argument
+    {
+        NameId = Vec_IntEntry(vFanins, 0);
+        *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+    }
+    return Type;
+}
+Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
+{
+    Wlc_Ntk_t * pNtk;
+    char * pName, * pBits, * pConst;
+    Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
+    int i, iObj, Type, Entry, NameId, fFound, Range;
+    // start network and create primary inputs
+    pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 );
+    pNtk->pManName = Abc_NamStart( 1000, 24 );
+    for ( i = 0; i < Vec_IntSize(&p->vData) - 1; )
+    {
+        assert( Vec_IntEntry(&p->vData, i) == 0 );
+        if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT )
+        {
+            pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 );
+            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+            assert( !fFound );
+            assert( iObj == NameId );
+        }
+        while ( Vec_IntEntry(&p->vData, ++i) );
+    }
+    // create logic nodes
+    for ( i = 0; i < Vec_IntSize(&p->vData) - 1; )
+    {
+        assert( Vec_IntEntry(&p->vData, i) == 0 );
+        Entry = Vec_IntEntry(&p->vData, ++i);
+        if ( Entry == PRS_SMT_INPUT )
+        {}
+        else if ( Entry == PRS_SMT_CONST )
+        {
+            pName  = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            pBits  = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            pConst = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            // create new node
+            if ( !Prs_SmtReadConstant( pNtk, pConst, atoi(pBits), vFanins, pName ) )
+                return NULL;
+        }
+        else if ( Entry == PRS_SMT_LET )
+        {
+            pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range );
+            if ( Type == WLC_OBJ_NONE )
+                return NULL;
+            assert( Range > 0 );
+            // create new node
+            iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 );
+            Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+            // add node's name
+            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+            assert( !fFound );
+            assert( iObj == NameId );
+        }
+        else if ( Entry == PRS_SMT_ASSERT )
+        {
+            Type = WLC_OBJ_BUF;
+            Vec_IntClear( vFanins );
+            pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+            if ( !strcmp(pName, "not") )
+            {
+                Type = WLC_OBJ_LOGIC_NOT;
+                pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
+                Range = 1;
+            }
+            // add fanin
+            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+            assert( fFound );
+            Vec_IntPush( vFanins, NameId );
+            // find range
+            if ( Type == WLC_OBJ_BUF )
+            {
+                // find range
+                iObj = Vec_IntEntry(vFanins, 0);
+                Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
+                assert( Range == 1 );
+            }
+            // create new node
+            iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 );
+            Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+            Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
+            // add node's name
+            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, "miter_output", &fFound );
+            assert( !fFound );
+            assert( iObj == NameId );
+            break;
+        }
+        else assert( 0 );
+        while ( Vec_IntEntry(&p->vData, ++i) );
+    }
+    Vec_IntFree( vFanins );
+    // create nameIDs
+    vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
+    Vec_IntAppend( &pNtk->vNameIds, vFanins );
+    Vec_IntFree( vFanins );
+    return pNtk;
+}
+Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+{
+    Wlc_Ntk_t * pNtk = NULL;
+    Prs_Smt_t * p = Prs_SmtAlloc( pFileName );
+    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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 8ed33909..11d14395 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -547,7 +547,7 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t
         Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
         for ( i = 0; i < nBits; i++ )
             if ( pStr[2+i] == '1' )
-                Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), i );
+                Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i );
             else if ( pStr[2+i] != '0' )
                 return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "Wrong digit in binary constant \"%c\".", pStr[2+i] );
         *pRange = nBits;
@@ -922,19 +922,22 @@ startword:
             Vec_Int_t * vTemp = Vec_IntStartNatural( Wlc_NtkObjNumMax(p->pNtk) );
             Vec_IntAppend( &p->pNtk->vNameIds, vTemp );
             Vec_IntFree( vTemp );
-            // move FO/FI to be part of CI/CO
-            assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 );
-            assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(p->pNtk->vInits) );
-            Wlc_NtkForEachFf( p->pNtk, pObj, i )
-                if ( i & 1 )
-                    Wlc_ObjSetCo( p->pNtk, pObj, 1 );
-                else
-                    Wlc_ObjSetCi( p->pNtk, pObj );
-            Vec_IntClear( &p->pNtk->vFfs );
-            // convert init values into binary string
-            //Vec_IntPrint( &p->pNtk->vInits );
-            p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
-            //printf( "%s", p->pNtk->pInits );
+            if ( p->pNtk->vInits )
+            {
+                // move FO/FI to be part of CI/CO
+                assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 );
+                assert( Vec_IntSize(&p->pNtk->vFfs) == 2 * Vec_IntSize(p->pNtk->vInits) );
+                Wlc_NtkForEachFf( p->pNtk, pObj, i )
+                    if ( i & 1 )
+                        Wlc_ObjSetCo( p->pNtk, pObj, 1 );
+                    else
+                        Wlc_ObjSetCi( p->pNtk, pObj );
+                Vec_IntClear( &p->pNtk->vFfs );
+                // convert init values into binary string
+                //Vec_IntPrint( &p->pNtk->vInits );
+                p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
+                //printf( "%s", p->pNtk->pInits );
+            }
             break;
         }
         // these are read as part of the interface