Improving SMT-LIB parser.

8 files changed, 164 insertions, 107 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 305a896d..b12e239c 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -61,40 +61,41 @@ typedef enum {
     WLC_OBJ_BIT_AND,       // 16: bitwise AND
     WLC_OBJ_BIT_OR,        // 17: bitwise OR
     WLC_OBJ_BIT_XOR,       // 18: bitwise XOR
-    WLC_OBJ_BIT_NAND,      // 16: bitwise AND
-    WLC_OBJ_BIT_NOR,       // 17: bitwise OR
-    WLC_OBJ_BIT_NXOR,      // 19: bitwise NXOR
-    WLC_OBJ_BIT_SELECT,    // 20: bit selection
-    WLC_OBJ_BIT_CONCAT,    // 21: bit concatenation
-    WLC_OBJ_BIT_ZEROPAD,   // 22: zero padding
-    WLC_OBJ_BIT_SIGNEXT,   // 23: sign extension
-    WLC_OBJ_LOGIC_NOT,     // 24: logic NOT
-    WLC_OBJ_LOGIC_AND,     // 25: logic AND
-    WLC_OBJ_LOGIC_OR,      // 27: logic OR
-    WLC_OBJ_LOGIC_XOR,     // 28: logic XOR
-    WLC_OBJ_COMP_EQU,      // 29: compare equal
-    WLC_OBJ_COMP_NOTEQU,   // 30: compare not equal
-    WLC_OBJ_COMP_LESS,     // 31: compare less
-    WLC_OBJ_COMP_MORE,     // 32: compare more
-    WLC_OBJ_COMP_LESSEQU,  // 33: compare less or equal
-    WLC_OBJ_COMP_MOREEQU,  // 34: compare more or equal
-    WLC_OBJ_REDUCT_AND,    // 35: reduction AND
-    WLC_OBJ_REDUCT_OR,     // 36: reduction OR
-    WLC_OBJ_REDUCT_XOR,    // 37: reduction XOR
-    WLC_OBJ_REDUCT_NAND,   // 38: reduction NAND
-    WLC_OBJ_REDUCT_NOR,    // 39: reduction NOR
-    WLC_OBJ_REDUCT_NXOR,   // 40: reduction NXOR
-    WLC_OBJ_ARI_ADD,       // 41: arithmetic addition
-    WLC_OBJ_ARI_SUB,       // 42: arithmetic subtraction
-    WLC_OBJ_ARI_MULTI,     // 43: arithmetic multiplier
-    WLC_OBJ_ARI_DIVIDE,    // 44: arithmetic division
-    WLC_OBJ_ARI_MODULUS,   // 45: arithmetic modulus
-    WLC_OBJ_ARI_POWER,     // 46: arithmetic power
-    WLC_OBJ_ARI_MINUS,     // 47: arithmetic minus
-    WLC_OBJ_ARI_SQRT,      // 48: integer square root
-    WLC_OBJ_ARI_SQUARE,    // 49: integer square
-    WLC_OBJ_TABLE,         // 50: bit table
-    WLC_OBJ_NUMBER         // 51: unused
+    WLC_OBJ_BIT_NAND,      // 19: bitwise AND
+    WLC_OBJ_BIT_NOR,       // 20: bitwise OR
+    WLC_OBJ_BIT_NXOR,      // 21: bitwise NXOR
+    WLC_OBJ_BIT_SELECT,    // 22: bit selection
+    WLC_OBJ_BIT_CONCAT,    // 23: bit concatenation
+    WLC_OBJ_BIT_ZEROPAD,   // 24: zero padding
+    WLC_OBJ_BIT_SIGNEXT,   // 25: sign extension
+    WLC_OBJ_LOGIC_NOT,     // 26: logic NOT
+    WLC_OBJ_LOGIC_IMPL,    // 27: logic implication
+    WLC_OBJ_LOGIC_AND,     // 28: logic AND
+    WLC_OBJ_LOGIC_OR,      // 29: logic OR
+    WLC_OBJ_LOGIC_XOR,     // 30: logic XOR
+    WLC_OBJ_COMP_EQU,      // 31: compare equal
+    WLC_OBJ_COMP_NOTEQU,   // 32: compare not equal
+    WLC_OBJ_COMP_LESS,     // 33: compare less
+    WLC_OBJ_COMP_MORE,     // 34: compare more
+    WLC_OBJ_COMP_LESSEQU,  // 35: compare less or equal
+    WLC_OBJ_COMP_MOREEQU,  // 36: compare more or equal
+    WLC_OBJ_REDUCT_AND,    // 37: reduction AND
+    WLC_OBJ_REDUCT_OR,     // 38: reduction OR
+    WLC_OBJ_REDUCT_XOR,    // 39: reduction XOR
+    WLC_OBJ_REDUCT_NAND,   // 40: reduction NAND
+    WLC_OBJ_REDUCT_NOR,    // 41: reduction NOR
+    WLC_OBJ_REDUCT_NXOR,   // 42: reduction NXOR
+    WLC_OBJ_ARI_ADD,       // 43: arithmetic addition
+    WLC_OBJ_ARI_SUB,       // 44: arithmetic subtraction
+    WLC_OBJ_ARI_MULTI,     // 45: arithmetic multiplier
+    WLC_OBJ_ARI_DIVIDE,    // 46: arithmetic division
+    WLC_OBJ_ARI_MODULUS,   // 47: arithmetic modulus
+    WLC_OBJ_ARI_POWER,     // 48: arithmetic power
+    WLC_OBJ_ARI_MINUS,     // 49: arithmetic minus
+    WLC_OBJ_ARI_SQRT,      // 50: integer square root
+    WLC_OBJ_ARI_SQUARE,    // 51: integer square
+    WLC_OBJ_TABLE,         // 52: bit table
+    WLC_OBJ_NUMBER         // 53: unused
 } Wlc_ObjType_t;
 // when adding new types, remember to update table Wlc_Names in "wlcNtk.c"
 
@@ -273,8 +274,8 @@ extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkDupSingleNodes( 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 );
+extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
+extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
 /*=== wlcSim.c ========================================================*/
 extern Vec_Ptr_t *    Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int nFrames );
 extern void           Wlc_NtkDeleteSim( Vec_Ptr_t * p );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 16044e67..5ef7ef14 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -777,7 +777,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
     // blast in the topological order
     Wlc_NtkForEachObj( p, pObj, i )
     {
-//        char * pName = Wlc_ObjName(p, i);
+//        char * pName1 = Wlc_ObjName(p, i);
+//        char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
+
         nAndPrev = Gia_ManAndNum(pNew);
         nRange  = Wlc_ObjRange( pObj );
         nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
@@ -1007,7 +1009,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
         else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
         {
             int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1];
-            assert( nRange0 < nRange );
+            assert( nRange0 <= nRange );
             for ( k = 0; k < nRange0; k++ )
                 Vec_IntPush( vRes, pFans0[k] );
             for (      ; k < nRange; k++ )
@@ -1020,6 +1022,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
             for ( k = 1; k < nRange; k++ )
                 Vec_IntPush( vRes, 0 );
         }
+        else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL )
+        {
+            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
+            int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
+            Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, Abc_LitNot(iLit0), iLit1) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
         else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
         {
             int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index bbb897ea..4bdb66c2 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -119,12 +119,20 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     Wlc_Ntk_t * pNtk = NULL;
     char * pFileName = NULL;
+    int fOldParser   =    0;
+    int fPrintTree   =    0;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'o':
+            fPrintTree ^= 1;
+            break;
+        case 'p':
+            fOldParser ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -155,7 +163,7 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     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 );
+        pNtk = Wlc_ReadSmt( pFileName, fOldParser, fPrintTree );
     else
     {
         printf( "Abc_CommandReadWlc(): Unknown file extension.\n" );
@@ -164,8 +172,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%read [-vh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%read [-opvh] <file_name>\n" );
     Abc_Print( -2, "\t         reads word-level design from Verilog file\n" );
+    Abc_Print( -2, "\t-o     : toggle using old SMT-LIB parser [default = %s]\n", fOldParser? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle printing parse SMT-LIB tree [default = %s]\n", fPrintTree? "yes": "no" );
     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");
     return 1;
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index c4f9ac70..726e7bf8 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -50,40 +50,41 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     "&",                   // 16: bitwise AND
     "|",                   // 17: bitwise OR
     "^",                   // 18: bitwise XOR
-    "~&",                  // 16: bitwise NAND
-    "~|",                  // 17: bitwise NOR
-    "~^",                  // 19: bitwise NXOR
-    "[:]",                 // 20: bit selection
-    "{,}",                 // 21: bit concatenation
-    "zeroPad",             // 22: zero padding
-    "signExt",             // 23: sign extension
-    "!",                   // 24: logic NOT
-    "&&",                  // 25: logic AND
-    "||",                  // 27: logic OR
-    "^^",                  // 28: logic XOR
-    "==",                  // 29: compare equal
-    "!=",                  // 30: compare not equal
-    "<",                   // 31: compare less
-    ">",                   // 32: compare more
-    "<=",                  // 33: compare less or equal
-    ">=",                  // 34: compare more or equal
-    "&",                   // 35: reduction AND
-    "|",                   // 36: reduction OR
-    "^",                   // 37: reduction XOR
-    "~&",                  // 38: reduction NAND
-    "~|",                  // 39: reduction NOR
-    "~^",                  // 40: reduction NXOR
-    "+",                   // 41: arithmetic addition
-    "-",                   // 42: arithmetic subtraction
-    "*",                   // 43: arithmetic multiplier
-    "/",                   // 44: arithmetic division
-    "%",                   // 45: arithmetic modulus
-    "**",                  // 46: arithmetic power
-    "-",                   // 47: arithmetic minus
-    "sqrt",                // 48: integer square root
-    "square",              // 49: integer square
-    "table",               // 50: bit table
-    NULL                   // 51: unused
+    "~&",                  // 19: bitwise NAND
+    "~|",                  // 20: bitwise NOR
+    "~^",                  // 21: bitwise NXOR
+    "[:]",                 // 22: bit selection
+    "{,}",                 // 23: bit concatenation
+    "zeroPad",             // 24: zero padding
+    "signExt",             // 25: sign extension
+    "!",                   // 26: logic NOT
+    "=>",                  // 27: logic implication
+    "&&",                  // 28: logic AND
+    "||",                  // 29: logic OR
+    "^^",                  // 30: logic XOR
+    "==",                  // 31: compare equal
+    "!=",                  // 32: compare not equal
+    "<",                   // 33: compare less
+    ">",                   // 34: compare more
+    "<=",                  // 35: compare less or equal
+    ">=",                  // 36: compare more or equal
+    "&",                   // 37: reduction AND
+    "|",                   // 38: reduction OR
+    "^",                   // 39: reduction XOR
+    "~&",                  // 40: reduction NAND
+    "~|",                  // 41: reduction NOR
+    "~^",                  // 42: reduction NXOR
+    "+",                   // 43: arithmetic addition
+    "-",                   // 44: arithmetic subtraction
+    "*",                   // 45: arithmetic multiplier
+    "/",                   // 46: arithmetic division
+    "%",                   // 47: arithmetic modulus
+    "**",                  // 48: arithmetic power
+    "-",                   // 49: arithmetic minus
+    "sqrt",                // 50: integer square root
+    "square",              // 51: integer square
+    "table",               // 52: bit table
+    NULL                   // 53: unused
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -380,6 +381,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
             Vec_IntAddToEntry( vAnds, WLC_OBJ_BIT_SIGNEXT, 0 );
         else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )    
             Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_NOT,        Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+        else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL )    
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_IMPL,       Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) - 1 );
         else if ( pObj->Type == WLC_OBJ_LOGIC_AND )    
             Vec_IntAddToEntry( vAnds, WLC_OBJ_LOGIC_AND,        Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) - 1 );
         else if ( pObj->Type == WLC_OBJ_LOGIC_OR )     
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 3a782257..d68688c4 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -169,6 +169,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
         Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1;   // 22: sign extension
     else if ( !strcmp(pName, "not") )
         Type = WLC_OBJ_LOGIC_NOT;     // 23: logic NOT
+    else if ( !strcmp(pName, "=>") )
+        Type = WLC_OBJ_LOGIC_IMPL;    // 24: logic AND
     else if ( !strcmp(pName, "and") )
         Type = WLC_OBJ_LOGIC_AND;     // 24: logic AND
     else if ( !strcmp(pName, "or") )
@@ -701,17 +703,28 @@ char * Smt_PrsGenName( Smt_Prs_t * p )
     sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount );
     return Buffer;
 }
-int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev )
+int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName )
 {
     if ( Smt_EntryIsName(iNode) )
     {
         char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
+        // handle built-in constants
+        if ( !strcmp(pStr, "false") )
+            pStr = "#b0";
+        else if ( !strcmp(pStr, "true") )
+            pStr = "#b1";
         if ( pStr[0] == '#' )
-            return Smt_PrsBuildConstant( pNtk, pStr, -1, Smt_PrsGenName(p) );
+            return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) );
         else
         {
             int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
             assert( fFound );
+            // create buffer if the name of the fanin has different name
+            if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) )
+            {
+                Vec_IntFill( &p->vTempFans, 1, iObj );
+                iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName );
+            }
             return iObj;
         }
      }
@@ -724,7 +737,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
         iRoot0 = Vec_IntEntry( vRoots, 0 );
         if ( Smt_EntryIsName(iRoot0) )
         {
-            char * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
+            char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
             if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
             {
                 // let ((s35550 (bvor s48 s35549)))
@@ -744,21 +757,21 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                     // get the name
                     Fan3 = Vec_IntEntry(vFans3, 0);
                     assert( Smt_EntryIsName(Fan3) );
-                    pName = Smt_EntryName(p, Fan3);
+                    pName2 = Smt_EntryName(p, Fan3);
                     // get function
                     Fan3 = Vec_IntEntry(vFans3, 1);
-                    assert( !Smt_EntryIsName(Fan3) );
+                    //assert( !Smt_EntryIsName(Fan3) );
                     // solve the problem
-                    iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1 );
+                    iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 );
                     if ( iObj == 0 )
                         return 0;
                     // create buffer
-                    Vec_IntFill( &p->vTempFans, 1, iObj );
-                    Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName );
+                    //Vec_IntFill( &p->vTempFans, 1, iObj );
+                    //Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName2 );
                 }
-                // pricess the final part of let
+                // process the final part of let
                 iRoot2 = Vec_IntEntry(vRoots, 2);
-                return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1 );
+                return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1, pName );
             }
             else if ( pStr0[0] == '_' )
             {
@@ -768,7 +781,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                     // (_ bv1 32)
                     char * pStr2 = Smt_VecEntryName( p, vRoots, 2 );
                     assert( Vec_IntSize(vRoots) == 3 );
-                    return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), Smt_PrsGenName(p) );
+                    return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName ? pName : Smt_PrsGenName(p) );
                 }
                 else
                 {
@@ -777,16 +790,23 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                     Type1 = Smt_StrToType( pStr1, &fSigned );
                     if ( Type1 == 0 )
                         return 0;
-                    Vec_IntFill( &p->vTempFans, 1, iObjPrev );
                     // find out this branch
+                    Vec_IntFill( &p->vTempFans, 1, iObjPrev );
                     if ( Type1 == WLC_OBJ_BIT_SIGNEXT || Type1 == WLC_OBJ_BIT_ZEROPAD || Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
                     {
                         int iRoot2 = Vec_IntEntry(vRoots, 2);
                         char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
                         int Num = atoi( pStr2 );
                         fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
-                        Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
-                        Vec_IntPush( &p->vTempFans, Num );
+                        if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
+                        {
+                            int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) );
+                            Vec_IntClear( &p->vTempFans );
+                            Vec_IntPushTwo( &p->vTempFans, iObjPrev, iConst );
+                            Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
+                        }
+                        else
+                            Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
                     }
                     else if ( Type1 == WLC_OBJ_BIT_SELECT )
                     {
@@ -797,12 +817,11 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                         int Num1 = atoi( pStr2 );
                         int Num2 = atoi( pStr3 );
                         assert( Num1 >= Num2 );
-                        fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
                         Range = Num1 - Num2 + 1;
                         Vec_IntPushTwo( &p->vTempFans, Num1, Num2 );
                     }
                     else assert( 0 );
-                    iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, Smt_PrsGenName(p) );
+                    iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, pName ? pName : Smt_PrsGenName(p) );
                     return iObj;
                 }
             }
@@ -822,7 +841,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                 vFanins = Vec_IntAlloc( 100 );
                 Vec_IntForEachEntryStart( vRoots, Fan, i, 1 )
                 {
-                    iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1 );
+                    iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1, NULL );
                     if ( iObj == 0 )
                     {
                         Vec_IntFree( vFanins );
@@ -854,17 +873,17 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev
                 }
                 // create node
                 assert( Range > 0 );
-                iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, Smt_PrsGenName(p) );
+                iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, pName ? pName : Smt_PrsGenName(p) );
                 Vec_IntFree( vFanins );
                 return iObj;
             }
         }
-        else if ( Vec_IntSize(vRoots) == 2 ) // possible   ((_ extract 48 16) (bvmul ?v_5 ?v_12))
+        else if ( Vec_IntSize(vRoots) == 2 ) // could be   ((_ extract 48 16) (bvmul ?v_5 ?v_12))
         {
-            int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1 );
+            int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1, NULL );
             if ( iObjPrev == 0 )
                 return 0;
-            return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev );
+            return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev, pName );
         }
         else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 );
         return 0;
@@ -992,7 +1011,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
             //(assert (not (= s0 #x00)))
             assert( Vec_IntSize(vFans) == 2 );
             assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
-            iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1 );
+            iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL );
             if ( iObj == 0 )
             {
                 Wlc_NtkFree( pNtk ); pNtk = NULL;
@@ -1083,14 +1102,16 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit )
 }
 static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit )
 {
-    char * pTemp; int nCount1 = 0, nCount2 = 0;
+    char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0;
     for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
     {
         if ( *pTemp == '(' )
             nCount1++;
         else if ( *pTemp == ')' )
             nCount2++;
-        else if ( *pTemp == ';' )
+        else if ( *pTemp == '|' )
+            fHaveBar ^= 1;
+        else if ( *pTemp == ';' && !fHaveBar )
             while ( *pTemp && *pTemp != '\n' )
                 *pTemp++ = ' ';
     }
@@ -1191,8 +1212,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
             Smt_PrsSkipNonSpaces( p );
             if ( p->pCur < p->pLimit )
             {
-                // add fanin
-                int iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
+                // remove strange characters (this can lead to name clashes)
+                int iToken;
+                char * pTemp;
+                if ( *pStart == '?' )
+                    *pStart = '_';
+                for ( pTemp = pStart; pTemp < p->pCur; pTemp++ )
+                    if ( *pTemp == '.' )
+                        *pTemp = '_';
+                // create and save token for this string
+                iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
                 Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) );
             }
         }
@@ -1235,7 +1264,7 @@ void Smt_PrsPrintParser( Smt_Prs_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
+Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree )
 {
     Wlc_Ntk_t * pNtk = NULL;
     int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
@@ -1243,20 +1272,21 @@ Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
     if ( p == NULL )
         return NULL;
     Smt_PrsReadLines( p );
-    //Smt_PrsPrintParser( p );
+    if ( fPrintTree )
+        Smt_PrsPrintParser( p );
     if ( Smt_PrsErrorPrint(p) )
-        pNtk = Smt_PrsBuild2( p );
+        pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p);
     Smt_PrsFree( p );
     return pNtk;
 }
-Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree )
 {
     Wlc_Ntk_t * pNtk = NULL;
     char * pBuffer, * pLimit; 
     pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
     if ( pBuffer == NULL )
         return NULL;
-    pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit );
+    pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree );
     ABC_FREE( pBuffer );
     return pNtk;
 }
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index e42fac42..7683f8a6 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -781,6 +781,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
             else if ( pStr[0] == '~' && pStr[1] == '&'                   ) pStr += 2, Type = WLC_OBJ_BIT_NAND;       
             else if ( pStr[0] == '~' && pStr[1] == '|'                   ) pStr += 2, Type = WLC_OBJ_BIT_NOR;       
             else if ( pStr[0] == '~' && pStr[1] == '^'                   ) pStr += 2, Type = WLC_OBJ_BIT_NXOR;       
+            else if ( pStr[0] == '=' && pStr[1] == '>'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_IMPL;     
             else if ( pStr[0] == '&' && pStr[1] == '&'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_AND;     
             else if ( pStr[0] == '|' && pStr[1] == '|'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_OR;      
             else if ( pStr[0] == '^' && pStr[1] == '^'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_XOR;      
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index d0249d1e..86092f95 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -192,7 +192,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
     // collect stdin until (check-sat)
     Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" );
     // parse input
-    Wlc_Ntk_t * pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput) );
+    Wlc_Ntk_t * pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput), 0, 0 );
     Vec_StrFree( vInput );
     // install current network
     Wlc_SetNtk( pAbc, pNtk );
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index 5f99f81b..b15d3d38 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -314,6 +314,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                     fprintf( pFile, "~|" );
                 else if ( pObj->Type == WLC_OBJ_BIT_NXOR )
                     fprintf( pFile, "~^" );
+                else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL )
+                    fprintf( pFile, "=>" );
                 else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
                     fprintf( pFile, "&&" );
                 else if ( pObj->Type == WLC_OBJ_LOGIC_OR )