Improvements to the SMTLIB parser.

2 files changed, 687 insertions, 533 deletions

diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 4a935f6b..a4e5459e 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -107,6 +107,8 @@ void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift,
     int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
     int Fill = fSticky ? pNum[nNum-1] : 0;
     int i, j, fShort = 0;
+    if ( nShift > 32 )
+        nShift = 32;
     assert( nShift <= 32 );
     for( i = 0; i < nShift; i++ ) 
         for( j = 0; j < nNum - fSticky; j++ ) 
@@ -126,6 +128,8 @@ void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, i
     int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
     int Fill = fSticky ? pNum[0] : 0;
     int i, j, fShort = 0;
+    if ( nShift > 32 )
+        nShift = 32;
     assert( nShift <= 32 );
     for( i = 0; i < nShift; i++ ) 
         for( j = nNum-1; j >= fSticky; j-- ) 
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 7093d79d..8143be6c 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [wlcReadSmt.c]
+  FileName    [wlcParse.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,11 +14,12 @@
 
   Date        [Ver. 1.0. Started - August 22, 2014.]
 
-  Revision    [$Id: wlcReadSmt.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+  Revision    [$Id: wlcParse.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
 #include "wlc.h"
+#include "misc/vec/vecWec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -26,19 +27,9 @@ 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_SMT_VALUE
-} Prs_ManType_t; 
-
 // parser
-typedef struct Prs_Smt_t_ Prs_Smt_t;
-struct Prs_Smt_t_
+typedef struct Smt_Prs_t_ Smt_Prs_t;
+struct Smt_Prs_t_
 {
     // input data
     char *       pName;       // file name
@@ -47,81 +38,77 @@ struct Prs_Smt_t_
     char *       pCur;        // current position
     Abc_Nam_t *  pStrs;       // string manager
     // network structure
-    Vec_Int_t    vData;
-    Vec_Int_t    vValues;
+    Vec_Int_t    vStack;      // current node on each level
+    //Vec_Wec_t    vDepth;      // objects on each level
+    Vec_Wec_t    vObjs;       // objects
     // error handling
-    char ErrorStr[1000];      
+    char ErrorStr[1000];     
 };
 
-
-// create error message
-static inline int Prs_SmtErrorSet( Prs_Smt_t * p, char * pError, int Value )
+// parser name types
+typedef enum { 
+    SMT_PRS_NONE = 0, 
+    SMT_PRS_SET_OPTION,    
+    SMT_PRS_SET_LOGIC,    
+    SMT_PRS_SET_INFO,    
+    SMT_PRS_DEFINE_FUN,
+    SMT_PRS_DECLARE_FUN,   
+    SMT_PRS_ASSERT,   
+    SMT_PRS_LET,   
+    SMT_PRS_CHECK_SAT,   
+    SMT_PRS_GET_VALUE,   
+    SMT_PRS_EXIT,
+    SMT_PRS_END
+} Smt_LineType_t; 
+
+typedef struct Smt_Pair_t_ Smt_Pair_t;
+struct Smt_Pair_t_
 {
-    assert( !p->ErrorStr[0] );
-    sprintf( p->ErrorStr, "%s", pError );
-    return Value;
-}
-// clear error message
-static inline void Prs_SmtErrorClear( Prs_Smt_t * p )
+    Smt_LineType_t Type;
+    char *         pName;
+};
+static Smt_Pair_t s_Types[SMT_PRS_END] =
 {
-    p->ErrorStr[0] = '\0';
-}
-// print error message
-static inline int Prs_SmtErrorPrint( Prs_Smt_t * p )
+    { SMT_PRS_NONE,         NULL         },
+    { SMT_PRS_SET_OPTION,  "set-option"  },
+    { SMT_PRS_SET_LOGIC,   "set-logic"   },
+    { SMT_PRS_SET_INFO,    "set-info"    },
+    { SMT_PRS_DEFINE_FUN,  "define-fun"  },
+    { SMT_PRS_DECLARE_FUN, "declare-fun" },
+    { SMT_PRS_ASSERT,      "assert"      },
+    { SMT_PRS_LET,         "let"         },
+    { SMT_PRS_CHECK_SAT,   "check-sat"   },
+    { SMT_PRS_GET_VALUE,   "get-value"   },
+    { SMT_PRS_EXIT,        "exit"        }
+};
+static inline char * Smt_GetTypeName( Smt_LineType_t Type )
 {
-    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;
+    Smt_LineType_t i;
+    for ( i = 1; i < SMT_PRS_END; i++ )
+        if ( s_Types[i].Type == Type )
+            return s_Types[i].pName;
+    return NULL;
 }
-static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit )
+static inline void Smt_AddTypes( Abc_Nam_t * p )
 {
-    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, char * pBuffer, char * pLimit )
-{
-    Prs_Smt_t * p;
-    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;
+    Smt_LineType_t Type;
+    for ( Type = 1; Type < SMT_PRS_END; Type++ )
+        Abc_NamStrFindOrAdd( p, Smt_GetTypeName(Type), NULL );
+    assert( Abc_NamObjNumMax(p) == SMT_PRS_END );
 }
 
-static inline void Prs_SmtFree( Prs_Smt_t * p )
-{
-    if ( p->pStrs )
-        Abc_NamDeref( p->pStrs );
-    Vec_IntErase( &p->vData );
-    Vec_IntErase( &p->vValues );
-    ABC_FREE( p );
-}
+static inline int         Smt_EntryIsName( int Fan )                          { return Abc_LitIsCompl(Fan);                                                         }
+static inline int         Smt_EntryIsType( int Fan, Smt_LineType_t Type )     { assert(Smt_EntryIsName(Fan));  return Abc_Lit2Var(Fan) == Type;                     }
+static inline char *      Smt_EntryName( Smt_Prs_t * p, int Fan )             { assert(Smt_EntryIsName(Fan));  return Abc_NamStr( p->pStrs, Abc_Lit2Var(Fan) );     }
+static inline Vec_Int_t * Smt_EntryNode( Smt_Prs_t * p, int Fan )             { assert(!Smt_EntryIsName(Fan)); return Vec_WecEntry( &p->vObjs, Abc_Lit2Var(Fan) );  }
+
+static inline int         Smt_VecEntryIsType( Vec_Int_t * vFans, int i, Smt_LineType_t Type ) { return i < Vec_IntSize(vFans) && Smt_EntryIsName(Vec_IntEntry(vFans, i)) && Smt_EntryIsType(Vec_IntEntry(vFans, i), Type); }
+static inline char *      Smt_VecEntryName( Smt_Prs_t * p, Vec_Int_t * vFans, int i )         { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? Smt_EntryName(p, Vec_IntEntry(vFans, i)) : NULL;                          }
+static inline Vec_Int_t * Smt_VecEntryNode( Smt_Prs_t * p, Vec_Int_t * vFans, int i )         { return Smt_EntryIsName(Vec_IntEntry(vFans, i)) ? NULL : Smt_EntryNode(p, Vec_IntEntry(vFans, i));                          }
+
+#define Smt_ManForEachDir( p, Type, vVec, i )                                                       \
+    for ( i = 0; (i < Vec_WecSize(&p->vObjs)) && (((vVec) = Vec_WecEntry(&p->vObjs, i)), 1); i++ )  \
+        if ( !Smt_VecEntryIsType(vVec, 0, Type) ) {} else
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -138,306 +125,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p )
   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;
-}
-static inline int Prs_SmtParseValue( Prs_Smt_t * p, char * pLimit, int Type )
-{
-    char * pToken;
-    assert( *pLimit == ')' );
-    *pLimit = 0;
-    pToken = strtok( p->pCur, " ()" );
-    assert( pToken != NULL );
-    Vec_IntPush( &p->vValues, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
-    pToken = strtok( NULL, " ()" );
-    assert( pToken == NULL );
-    assert( *pLimit == 0 );
-    *pLimit = ')';
-    p->pCur = pLimit;
-    return 1;
-}
-int Prs_SmtReadLines( Prs_Smt_t * p )
-{
-    int fAssert = 0;
-    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, "get-value") )
-        {
-            if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) )
-                return 0;
-            assert( *p->pCur == ')' );
-            p->pCur++;
-        }
-        else if ( Prs_SmtIsWord(p, "assert") )
-            fAssert = 1;
-        else if ( Prs_SmtIsWord(p, "check-sat") )
-            break;
-        else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") )
-            p->pCur = Prs_SmtFindNextPar(p) + 1;
-//        else
-            //return Prs_SmtErrorSet(p, "Unsupported directive.", 0);
-        Prs_SmtSkipSpaces( p );
-        if ( *p->pCur != '(' && fAssert == 1 )
-        {
-            fAssert = 0;
-            // finish parsing assert
-            if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) )
-                return 0;
-            assert( *p->pCur == ')' );
-            Vec_IntPush( &p->vData, 0 );
-            // skip closing
-            while ( *p->pCur == ')' )
-                p->pCur++;
-            Prs_SmtSkipSpaces( p );
-        }
-    }
-    assert( fAssert == 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) );
-    }
-    Vec_IntForEachEntry( &p->vValues, Entry, i )
-        printf( "get-value %s\n", 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 * pfSigned )
+static inline int Smt_StrToType( char * pName, int * pfSigned )
 {
     int Type = 0; *pfSigned = 0;
     if ( !strcmp(pName, "ite") )
@@ -534,209 +222,670 @@ static inline int Prs_SmtStrToType( char * pName, int * pfSigned )
     }
     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 * pfSigned )
+static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int * Value1, int * Value2 )
 {
-    int Type, NameId;
-    char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) );
-    // read type
-    Type = Prs_SmtStrToType( pName, pfSigned );
-    if ( Type == 0 )
-        return 0;
-    *pRange = 0;
-    Vec_IntClear( vFanins );
-    if ( Type == WLC_OBJ_COMP_EQU )
+    if ( Smt_EntryIsName(iSig) )
+        return Smt_StrToType( Smt_EntryName(p, iSig), pfSigned );
+    else
     {
-        *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;
+        Vec_Int_t * vFans = Smt_EntryNode( p, iSig );
+        char * pStr = Smt_VecEntryName( p, vFans, 0 );  int Type;
+        assert( Vec_IntSize(vFans) >= 3 );
+        assert( !strcmp(pStr, "_") ); // special op
+        *Value1 = *Value2 = -1;
+        assert( pStr[0] != 'b' || pStr[1] != 'v' );
+        // read type
+        Type = Smt_StrToType( Smt_VecEntryName(p, vFans, 1), pfSigned );
+        if ( Type == 0 )
+            return 0;
+        *Value1 = atoi( Smt_VecEntryName(p, vFans, 2) );
+        if ( Vec_IntSize(vFans) > 3 )
+            *Value2 = atoi( Smt_VecEntryName(p, vFans, 3) );
+        return Type;
     }
-    else if ( Type == WLC_OBJ_LOGIC_NOT )
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName )
+{
+    char Buffer[100];
+    int NameId, fFound;
+    int iObj = Wlc_ObjAlloc( pNtk, Type, fSigned, Range-1, 0 );
+    assert( Type > 0 );
+    assert( Range >= 0 );
+    assert( fSigned >= 0 );
+    Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+    if ( fSigned )
     {
-        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--;
+        Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
+        if ( Vec_IntSize(vFanins) > 0 )
+            Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
+        if ( Vec_IntSize(vFanins) > 1 )
+            Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
     }
-    else if ( Type == WLC_OBJ_BIT_SELECT )
+    if ( pName == NULL )
     {
-        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;
+        sprintf( Buffer, "_n%d_", iObj );
+        pName = Buffer;
     }
-    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 )
+    // add node's name
+    NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+    assert( !fFound );
+    assert( iObj == NameId );
+    return iObj;
+}
+static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName )
+{
+    int i, nDigits, iObj;
+    Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
+    if ( pStr[0] != '#' ) // decimal
     {
-        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 Number = atoi( pStr );
+        nBits = Abc_Base2Log( Number+1 );
+        assert( nBits < 32 );
+        Vec_IntPush( vFanins, Number );
+    }
+    else if ( pStr[1] == 'b' ) // binary
     {
-        int k;
-        Vec_IntForEachEntry( vFanins, NameId, k )
-            *pRange += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+        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 ( Type == WLC_OBJ_MUX )
+    else if ( pStr[1] == 'x' ) // hexadecimal
     {
-        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) );
+        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 )
+            return 0;
     }
-    else // to determine range, look at the first argument
+    else return 0;
+    // create constant node
+    iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, vFanins, pName );
+    Vec_IntFree( vFanins );
+    return iObj;
+}
+int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, char * pName )
+{
+    if ( Smt_EntryIsName(iNode) ) // name or constant
     {
-        NameId = Vec_IntEntry(vFanins, 0);
-        *pRange = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+        char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
+        if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' )
+        { 
+            // (_ BitVec 8) #x19
+            return Smt_PrsBuildConstant( pNtk, pStr, RangeOut, pName );
+        }
+        else
+        {
+            // s3087
+            int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
+            assert( fFound );
+            return iObj;
+        }
+    }
+    else // node
+    {
+        Vec_Int_t * vFans = Smt_EntryNode( p, iNode );
+        char * pStr0 = Smt_VecEntryName( p, vFans, 0 );
+        char * pStr1 = Smt_VecEntryName( p, vFans, 1 );
+        if ( pStr0 && pStr1 && pStr0[0] == '_' && pStr1[0] == 'b' && pStr1[1] == 'v' )
+        {
+            // (_ bv1 32)
+            char * pStr2 = Smt_VecEntryName( p, vFans, 2 );
+            assert( Vec_IntSize(vFans) == 3 );
+            return Smt_PrsBuildConstant( pNtk, pStr2+2, atoi(pStr2), pName );
+        }
+        else if ( pStr0 && pStr0[0] == '=' )
+        {
+            assert( Vec_IntSize(vFans) == 3 );
+            iNode = Vec_IntEntry(vFans, 2);
+            assert( Smt_EntryIsName(iNode) );
+            pStr0 = Smt_EntryName(p, iNode);
+            // check the last one is "#b1"
+            if ( !strcmp("#b1", pStr0) )
+            {
+                iNode = Vec_IntEntry(vFans, 1);
+                return Smt_PrsBuildNode( pNtk, p, iNode, -1, pName );
+            }
+            else
+            {
+                Vec_Int_t * vFanins = Vec_IntAlloc( 2 );
+                // get the constant
+                int iObj, iOper, iConst = Smt_PrsBuildConstant( pNtk, pStr0, -1, NULL );
+                // check the middle one is an operator
+                iNode = Vec_IntEntry(vFans, 1);
+                iOper = Smt_PrsBuildNode( pNtk, p, iNode, -1, pName );
+                // build comparator
+                Vec_IntPushTwo( vFanins, iOper, iConst );
+                iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_COMP_EQU, 0, 1, vFanins, pName );
+                Vec_IntFree( vFanins );
+                return iObj;
+            }
+        }
+        else
+        {
+            int i, Fan, NameId, iFanin, fSigned, Range, Value1 = -1, Value2 = -1;
+            int Type = Smt_PrsReadType( p, Vec_IntEntry(vFans, 0), &fSigned, &Value1, &Value2 );
+            // collect fanins
+            Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
+            Vec_IntForEachEntryStart( vFans, Fan, i, 1 )
+            {
+                iFanin = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL );
+                if ( iFanin == 0 )
+                {
+                    Vec_IntFree( vFanins );
+                    return 0;
+                }
+                Vec_IntPush( vFanins, iFanin );
+            }
+            // update specialized nodes
+            assert( Type != WLC_OBJ_BIT_SIGNEXT && Type != WLC_OBJ_BIT_ZEROPAD );
+            if ( Type == WLC_OBJ_BIT_SELECT )
+            {
+                assert( Value1 >= 0 && Value2 >= 0 && Value1 >= Value2 );
+                Vec_IntPush( vFanins, (Value1 << 16) | Value2 );
+            }
+            else if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L )
+            {
+                char Buffer[10];
+                assert( Value1 >= 0 );
+                sprintf( Buffer, "%d", Value1 ); 
+                NameId = Smt_PrsBuildConstant( pNtk, Buffer, -1, NULL );
+                Vec_IntPush( vFanins, NameId );
+            }
+            // find range
+            Range = 0;
+            if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR )
+                Range = 1;
+            else if ( Type == WLC_OBJ_BIT_SELECT )
+                Range = Value1 - Value2 + 1;
+            else if ( Type == WLC_OBJ_BIT_CONCAT )
+            {
+                Vec_IntForEachEntry( vFanins, NameId, i )
+                    Range += 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);
+                Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+            }
+            else // to determine range, look at the first argument
+            {
+                NameId = Vec_IntEntry(vFanins, 0);
+                Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
+            }
+            // create node
+            assert( Range > 0 );
+            NameId = Smt_PrsCreateNode( pNtk, Type, fSigned, Range, vFanins, pName );
+            Vec_IntFree( vFanins );
+            return NameId;
+        }
     }
-    return Type;
 }
-Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_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, fSigned, nBits = 0;
+    Vec_Int_t * vFans, * vFans2, * vFans3; 
+    Vec_Int_t * vAsserts = Vec_IntAlloc(100);
+    char * pName, * pRange, * pValue;
+    int i, k, Fan, Fan3, iObj, Status, Range, NameId, nBits = 0;
+    // issue warnings about unknown dirs
+    vFans = Vec_WecEntry( &p->vObjs, 0 );
+    Vec_IntForEachEntry( vFans, Fan, i )
+    {
+        assert( !Smt_EntryIsName(Fan) );
+        vFans2 = Smt_VecEntryNode( p, vFans, i );
+        Fan = Vec_IntEntry(vFans2, 0);
+        assert( Smt_EntryIsName(Fan) );
+        if ( Abc_Lit2Var(Fan) >= SMT_PRS_END )
+            printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) );
+    }
     // start network and create primary inputs
-    pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 );
+    pNtk = Wlc_NtkAlloc( p->pName, 1000 );
     pNtk->pManName = Abc_NamStart( 1000, 24 );
-    for ( i = 0; i < Vec_IntSize(&p->vData) - 1; )
+    Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i )
     {
-        assert( Vec_IntEntry(&p->vData, i) == 0 );
-        if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT )
+        assert( Vec_IntSize(vFans) == 4 );
+        assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
+        // get name
+        Fan = Vec_IntEntry(vFans, 1);
+        assert( Smt_EntryIsName(Fan) );
+        pName = Smt_EntryName(p, Fan);
+        // skip ()
+        Fan = Vec_IntEntry(vFans, 2);
+        assert( !Smt_EntryIsName(Fan) );
+        // check type (Bool or BitVec)
+        Fan = Vec_IntEntry(vFans, 3);
+        if ( Smt_EntryIsName(Fan) ) 
         {
-            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 );
-            // save values
-            Vec_IntPush( &pNtk->vValues, NameId );
-            Vec_IntPush( &pNtk->vValues, nBits );
-            Vec_IntPush( &pNtk->vValues, atoi(pBits) );
-            nBits += atoi(pBits);
+            //(declare-fun s1 () Bool)
+            assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
+            Range = 1;
         }
-        while ( Vec_IntEntry(&p->vData, ++i) );
+        else
+        {
+            // (declare-fun s1 () (_ BitVec 64))
+            // get range
+            Fan = Vec_IntEntry(vFans, 3);
+            assert( !Smt_EntryIsName(Fan) );
+            vFans2 = Smt_EntryNode(p, Fan);
+            assert( Vec_IntSize(vFans2) == 3 );
+            assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
+            assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
+            Fan = Vec_IntEntry(vFans2, 2);
+            assert( Smt_EntryIsName(Fan) );
+            pRange = Smt_EntryName(p, Fan);
+            Range = atoi(pRange);
+        }
+        // create node
+        iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 );
+        NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL );
+        assert( iObj == NameId );
+        // save values
+        Vec_IntPush( &pNtk->vValues, NameId );
+        Vec_IntPush( &pNtk->vValues, nBits );
+        Vec_IntPush( &pNtk->vValues, Range );
+        nBits += Range;
     }
-    // create logic nodes
-    for ( i = 0; i < Vec_IntSize(&p->vData) - 1; )
+    // create constants
+    Smt_ManForEachDir( p, SMT_PRS_DEFINE_FUN, vFans, i )
     {
-        assert( Vec_IntEntry(&p->vData, i) == 0 );
-        Entry = Vec_IntEntry(&p->vData, ++i);
-        if ( Entry == PRS_SMT_INPUT )
-        {}
-        else if ( Entry == PRS_SMT_CONST )
+        assert( Vec_IntSize(vFans) == 5 );
+        assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
+        // get name
+        Fan = Vec_IntEntry(vFans, 1);
+        assert( Smt_EntryIsName(Fan) );
+        pName = Smt_EntryName(p, Fan);
+        // skip ()
+        Fan = Vec_IntEntry(vFans, 2);
+        assert( !Smt_EntryIsName(Fan) );
+        // check type (Bool or BitVec)
+        Fan = Vec_IntEntry(vFans, 3);
+        if ( Smt_EntryIsName(Fan) ) 
         {
-            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;
+            // (define-fun s_2 () Bool false)
+            assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
+            Range = 1;
+            pValue = Smt_VecEntryName(p, vFans, 4);
+            if ( !strcmp("false", pValue) )
+                pValue = "#b0";
+            else if ( !strcmp("true", pValue) )
+                pValue = "#b1";
+            else assert( 0 );
+            Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
         }
-        else if ( Entry == PRS_SMT_LET )
+        else
         {
-            pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
-            Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range, &fSigned );
-            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 );
-            if ( fSigned )
-            {
-                Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
-                if ( Vec_IntSize(vFanins) > 0 )
-                    Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
-                if ( Vec_IntSize(vFanins) > 1 )
-                    Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
-            }
-            // add node's name
-            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
-            assert( !fFound );
-            assert( iObj == NameId );
+            // (define-fun s702 () (_ BitVec 4) #xe)
+            // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
+            // get range
+            Fan = Vec_IntEntry(vFans, 3);
+            assert( !Smt_EntryIsName(Fan) );
+            vFans2 = Smt_VecEntryNode(p, vFans, 3);
+            assert( Vec_IntSize(vFans2) == 3 );
+            assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
+            assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
+            // get range
+            Fan = Vec_IntEntry(vFans2, 2);
+            assert( Smt_EntryIsName(Fan) );
+            pRange = Smt_EntryName(p, Fan);
+            Range = atoi(pRange);
+            // get constant
+            Fan = Vec_IntEntry(vFans, 4);
+            Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
+        }        
+        if ( !Status )
+        {
+            Wlc_NtkFree( pNtk ); pNtk = NULL;
+            goto finish;
         }
-        else if ( Entry == PRS_SMT_ASSERT )
+    }
+    // process let-statements
+    Smt_ManForEachDir( p, SMT_PRS_LET, vFans, i )
+    {
+        // let ((s35550 (bvor s48 s35549)))
+        assert( Vec_IntSize(vFans) == 3 );
+        assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_LET) );
+        // get parts
+        Fan = Vec_IntEntry(vFans, 1);
+        assert( !Smt_EntryIsName(Fan) );
+        vFans2 = Smt_EntryNode(p, Fan);
+        if ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) )
+            continue;
+        // iterate through the parts
+        Vec_IntForEachEntry( vFans2, Fan, k )
         {
-            Type = WLC_OBJ_BUF;
-            Vec_IntClear( vFanins );
-            pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
-            if ( !strcmp(pName, "not") )
+            // s35550 (bvor s48 s35549)
+            Fan = Vec_IntEntry(vFans2, 0);
+            assert( !Smt_EntryIsName(Fan) );
+            vFans3 = Smt_EntryNode(p, Fan);
+            // get the name
+            Fan3 = Vec_IntEntry(vFans3, 0);
+            assert( Smt_EntryIsName(Fan3) );
+            pName = Smt_EntryName(p, Fan3);
+            // get function
+            Fan3 = Vec_IntEntry(vFans3, 1);
+            assert( !Smt_EntryIsName(Fan3) );
+            Status = Smt_PrsBuildNode( pNtk, p, Fan3, -1, pName );
+            if ( !Status )
             {
-                Type = WLC_OBJ_LOGIC_NOT;
-                pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
-                Range = 1;
+                Wlc_NtkFree( pNtk ); pNtk = NULL;
+                goto finish;
             }
-            // add fanin
-            NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
-            assert( fFound );
-            Vec_IntPush( vFanins, NameId );
-            // find range
-            if ( Type == WLC_OBJ_BUF )
+        }
+    }
+    // process assert-statements
+    Vec_IntClear( vAsserts );
+    Smt_ManForEachDir( p, SMT_PRS_ASSERT, vFans, i )
+    {
+        //(assert ; no quantifiers
+        //   (let ((s2 (bvsge s0 s1)))
+        //   (not s2)))
+        //(assert (not (= s0 #x00)))
+        assert( Vec_IntSize(vFans) == 2 );
+        assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
+        // get second directive
+        Fan = Vec_IntEntry(vFans, 1);
+        if ( !Smt_EntryIsName(Fan) )
+        {
+            // find the final let-statement
+            vFans2 = Smt_VecEntryNode(p, vFans, 1);
+            while ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) )
             {
-                // find range
-                iObj = Vec_IntEntry(vFanins, 0);
-                Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
-                assert( Range == 1 );
+                Fan = Vec_IntEntry(vFans2, 2);
+                if ( Smt_EntryIsName(Fan) )
+                    break;
+                vFans2 = Smt_VecEntryNode(p, vFans2, 2);
             }
-            // 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) );
+        // find name or create node
+        iObj = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL );
+        if ( !iObj )
+        {
+            Wlc_NtkFree( pNtk ); pNtk = NULL;
+            goto finish;
+        }
+        Vec_IntPush( vAsserts, iObj );
     }
-    Vec_IntFree( vFanins );
+    // build AND of asserts
+    if ( Vec_IntSize(vAsserts) == 1 )
+        iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" );
+    else
+    {
+        iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
+        Vec_IntFill( vAsserts, 1, iObj );
+        iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" );
+    }
+    Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
     // create nameIDs
-    vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
-    Vec_IntAppend( &pNtk->vNameIds, vFanins );
-    Vec_IntFree( vFanins );
+    vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
+    Vec_IntAppend( &pNtk->vNameIds, vFans );
+    Vec_IntFree( vFans );
     //Wlc_NtkReport( pNtk, NULL );
+finish:
+    // cleanup
+    Vec_IntFree(vAsserts);
     return pNtk;
 }
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// create error message
+static inline int Smt_PrsErrorSet( Smt_Prs_t * p, char * pError, int Value )
+{
+    assert( !p->ErrorStr[0] );
+    sprintf( p->ErrorStr, "%s", pError );
+    return Value;
+}
+// print error message
+static inline int Smt_PrsErrorPrint( Smt_Prs_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 * Smt_PrsLoadFile( 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 int Smt_PrsRemoveComments( char * pBuffer, char * pLimit )
+{
+    char * pTemp; int nCount1 = 0, nCount2 = 0;
+    for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
+    {
+        if ( *pTemp == '(' )
+            nCount1++;
+        else if ( *pTemp == ')' )
+            nCount2++;
+        else if ( *pTemp == ';' )
+            while ( *pTemp && *pTemp != '\n' )
+                *pTemp++ = ' ';
+    }
+    if ( nCount1 != nCount2 )
+        printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", nCount1, nCount2 );
+    else if ( nCount1 == 0 )
+        printf( "The input SMTLIB file has no opening or closing parentheses.\n" );
+    return nCount1 == nCount2 ? nCount1 : 0;
+}
+static inline Smt_Prs_t * Smt_PrsAlloc( char * pFileName, char * pBuffer, char * pLimit, int nObjs )
+{
+    Smt_Prs_t * p;
+    if ( nObjs == 0 )
+        return NULL;
+    p = ABC_CALLOC( Smt_Prs_t, 1 );
+    p->pName   = pFileName;
+    p->pBuffer = pBuffer;
+    p->pLimit  = pLimit;
+    p->pCur    = pBuffer;
+    p->pStrs   = Abc_NamStart( 1000, 24 );
+    Smt_AddTypes( p->pStrs );
+    Vec_IntGrow( &p->vStack, 100 );
+    //Vec_WecGrow( &p->vDepth, 100 );
+    Vec_WecGrow( &p->vObjs, nObjs+1 );
+    return p;
+}
+static inline void Smt_PrsFree( Smt_Prs_t * p )
+{
+    if ( p->pStrs )
+        Abc_NamDeref( p->pStrs );
+    Vec_IntErase( &p->vStack );
+    //Vec_WecErase( &p->vDepth );
+    Vec_WecErase( &p->vObjs );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Smt_PrsIsSpace( char c )
+{
+    return c == ' ' || c == '\t' || c == '\r' || c == '\n';
+}
+static inline void Smt_PrsSkipSpaces( Smt_Prs_t * p )
+{
+    while ( Smt_PrsIsSpace(*p->pCur) )
+        p->pCur++;
+}
+static inline void Smt_PrsSkipNonSpaces( Smt_Prs_t * p )
+{
+    while ( p->pCur < p->pLimit && !Smt_PrsIsSpace(*p->pCur) && *p->pCur != '(' && *p->pCur != ')' )
+        p->pCur++;
+}
+void Smt_PrsReadLines( Smt_Prs_t * p )
+{
+    assert( Vec_IntSize(&p->vStack) == 0 );
+    //assert( Vec_WecSize(&p->vDepth) == 0 );
+    assert( Vec_WecSize(&p->vObjs) == 0 );
+    // add top node at level 0
+    //Vec_WecPushLevel( &p->vDepth );
+    //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) );
+    // add top node
+    Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) );
+    Vec_WecPushLevel( &p->vObjs );
+    // add other nodes
+    for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ )
+    {
+        Smt_PrsSkipSpaces( p );
+        if ( *p->pCur == '(' )
+        {
+            // add new node at this depth
+            //assert( Vec_WecSize(&p->vDepth) >= Vec_IntSize(&p->vStack) );
+            //if ( Vec_WecSize(&p->vDepth) == Vec_IntSize(&p->vStack) )
+            //    Vec_WecPushLevel(&p->vDepth);
+            //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) );
+            // add fanin to node on the previous level
+            Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(Vec_WecSize(&p->vObjs), 0) );            
+            // add node to the stack
+            Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) );
+            Vec_WecPushLevel( &p->vObjs );
+        }
+        else if ( *p->pCur == ')' )
+        {
+            Vec_IntPop( &p->vStack );
+        }
+        else  // token
+        {
+            char * pStart = p->pCur; 
+            Smt_PrsSkipNonSpaces( p );
+            if ( p->pCur < p->pLimit )
+            {
+                // add fanin
+                int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
+                Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) );
+            }
+        }
+    }
+    assert( Vec_IntSize(&p->vStack) == 1 );
+    assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) );
+}
+void Smt_PrsPrintParser_rec( Smt_Prs_t * p, int iObj, int Depth )
+{
+    Vec_Int_t * vFans; int i, Fan;
+    printf( "%*s(\n", Depth, "" );
+    vFans = Vec_WecEntry( &p->vObjs, iObj );
+    Vec_IntForEachEntry( vFans, Fan, i )
+    {
+        if ( Abc_LitIsCompl(Fan) )
+        {
+            printf( "%*s", Depth+2, "" );
+            printf( "%s\n", Abc_NamStr(p->pStrs, Abc_Lit2Var(Fan)) );
+        }
+        else
+            Smt_PrsPrintParser_rec( p, Abc_Lit2Var(Fan), Depth+4 );
+    }
+    printf( "%*s)\n", Depth, "" );
+}
+void Smt_PrsPrintParser( Smt_Prs_t * p )
+{
+//    Vec_WecPrint( &p->vDepth, 0 );
+    Smt_PrsPrintParser_rec( p, 0, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
 {
     Wlc_Ntk_t * pNtk = NULL;
-    Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit );
+    int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
+    Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount );
     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 );
+    Smt_PrsReadLines( p );
+    //Smt_PrsPrintParser( p );
+    if ( Smt_PrsErrorPrint(p) )
+        pNtk = Smt_PrsBuild( p );
+    Smt_PrsFree( p );
     return pNtk;
 }
 Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
 {
     Wlc_Ntk_t * pNtk = NULL;
-    char * pBuffer, * pLimit;
-    pBuffer = Prs_SmtLoadFile( pFileName, &pLimit );
+    char * pBuffer, * pLimit; 
+    pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
     if ( pBuffer == NULL )
         return NULL;
     pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit );
@@ -744,6 +893,7 @@ Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
     return pNtk;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////