Modifications to read SMTLIB file from stdin.

src/base/abci/abc.c

@@ -21448,6 +21448,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAlignPol;
     int fAndOuts;
     int fNewSolver;
+    int fSilent;
     int fVerbose;
     int nConfLimit;
     int nLearnedStart;
@@ -21461,6 +21462,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     fAlignPol  = 0;
     fAndOuts   = 0;
     fNewSolver = 0;
+    fSilent    = 0;
     fVerbose   = 0;
     nConfLimit = 0;
     nInsLimit  = 0;
@@ -21468,7 +21470,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     nLearnedDelta = 0;
     nLearnedPerce = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpanvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21536,6 +21538,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fNewSolver ^= 1;
             break;
+        case 's':
+            fSilent ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -21596,18 +21601,20 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
     }
     pAbc->Status = RetValue;
-    if ( RetValue == -1 )
-        Abc_Print( 1, "UNDECIDED      " );
-    else if ( RetValue == 0 )
-        Abc_Print( 1, "SATISFIABLE    " );
-    else
-        Abc_Print( 1, "UNSATISFIABLE  " );
-    //Abc_Print( -1, "\n" );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    if ( !fSilent )
+    {
+        if ( RetValue == -1 )
+            Abc_Print( 1, "UNDECIDED      " );
+        else if ( RetValue == 0 )
+            Abc_Print( 1, "SATISFIABLE    " );
+        else
+            Abc_Print( 1, "UNSATISFIABLE  " );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsat [-CILDE num] [-panvh]\n" );
+    Abc_Print( -2, "usage: dsat [-CILDE num] [-pansvh]\n" );
     Abc_Print( -2, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     Abc_Print( -2, "\t         derives CNF from the current network and leaves it unchanged\n" );
     Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
@@ -21618,6 +21625,7 @@ usage:
     Abc_Print( -2, "\t-p     : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
     Abc_Print( -2, "\t-n     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
+    Abc_Print( -2, "\t-s     : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" );
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

src/base/cba/cbaCom.c

@@ -218,7 +218,11 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         p = Cba_ManReadCba( pFileName );
     }
-    else assert( 0 );
+    else 
+    {
+        printf( "Unrecognized input file extension.\n" );
+        return 0;
+    }
     Cba_AbcUpdateMan( pAbc, p );
     return 0;
 usage:

src/base/wlc/wlc.h

@@ -68,24 +68,25 @@ typedef enum {
     WLC_OBJ_LOGIC_NOT,     // 23: logic NOT
     WLC_OBJ_LOGIC_AND,     // 24: logic AND
     WLC_OBJ_LOGIC_OR,      // 25: logic OR
-    WLC_OBJ_COMP_EQU,      // 26: compare equal
-    WLC_OBJ_COMP_NOTEQU,   // 27: compare not equal
-    WLC_OBJ_COMP_LESS,     // 28: compare less
-    WLC_OBJ_COMP_MORE,     // 29: compare more
-    WLC_OBJ_COMP_LESSEQU,  // 30: compare less or equal
-    WLC_OBJ_COMP_MOREEQU,  // 31: compare more or equal
-    WLC_OBJ_REDUCT_AND,    // 32: reduction AND
-    WLC_OBJ_REDUCT_OR,     // 33: reduction OR
-    WLC_OBJ_REDUCT_XOR,    // 34: reduction XOR
-    WLC_OBJ_ARI_ADD,       // 35: arithmetic addition
-    WLC_OBJ_ARI_SUB,       // 36: arithmetic subtraction
-    WLC_OBJ_ARI_MULTI,     // 37: arithmetic multiplier
-    WLC_OBJ_ARI_DIVIDE,    // 38: arithmetic division
-    WLC_OBJ_ARI_MODULUS,   // 39: arithmetic modulus
-    WLC_OBJ_ARI_POWER,     // 40: arithmetic power
-    WLC_OBJ_ARI_MINUS,     // 41: arithmetic minus
-    WLC_OBJ_TABLE,         // 42: bit table
-    WLC_OBJ_NUMBER         // 43: unused
+    WLC_OBJ_LOGIC_XOR,     // 26: logic XOR
+    WLC_OBJ_COMP_EQU,      // 27: compare equal
+    WLC_OBJ_COMP_NOTEQU,   // 28: compare not equal
+    WLC_OBJ_COMP_LESS,     // 29: compare less
+    WLC_OBJ_COMP_MORE,     // 30: compare more
+    WLC_OBJ_COMP_LESSEQU,  // 31: compare less or equal
+    WLC_OBJ_COMP_MOREEQU,  // 32: compare more or equal
+    WLC_OBJ_REDUCT_AND,    // 33: reduction AND
+    WLC_OBJ_REDUCT_OR,     // 34: reduction OR
+    WLC_OBJ_REDUCT_XOR,    // 35: reduction XOR
+    WLC_OBJ_ARI_ADD,       // 36: arithmetic addition
+    WLC_OBJ_ARI_SUB,       // 37: arithmetic subtraction
+    WLC_OBJ_ARI_MULTI,     // 38: arithmetic multiplier
+    WLC_OBJ_ARI_DIVIDE,    // 39: arithmetic division
+    WLC_OBJ_ARI_MODULUS,   // 40: arithmetic modulus
+    WLC_OBJ_ARI_POWER,     // 41: arithmetic power
+    WLC_OBJ_ARI_MINUS,     // 42: arithmetic minus
+    WLC_OBJ_TABLE,         // 43: bit table
+    WLC_OBJ_NUMBER         // 44: unused
 } Wlc_ObjType_t;
 
 
@@ -135,6 +136,7 @@ struct Wlc_Ntk_t_
     // object names
     Abc_Nam_t *            pManName;           // object names
     Vec_Int_t              vNameIds;           // object name IDs
+    Vec_Int_t              vValues;            // value objects
     // object attributes
     int                    nTravIds;           // counter of traversal IDs
     Vec_Int_t              vTravIds;           // trav IDs of the objects
@@ -257,6 +259,7 @@ 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 );
+extern void           Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign );
 /*=== wlcReadSmt.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit );
 extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName );

src/base/wlc/wlcBlast.c

@@ -658,6 +658,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
             for ( k = 1; k < nRange; k++ )
                 Vec_IntPush( vRes, 0 );
         }
+        else if ( pObj->Type == WLC_OBJ_LOGIC_XOR )
+        {
+            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_ManHashXor(pNew, iLit0, iLit1) );
+            for ( k = 1; k < nRange; k++ )
+                Vec_IntPush( vRes, 0 );
+        }
         else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU )
         {
             int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 );

src/base/wlc/wlcCom.c

@@ -115,21 +115,34 @@ static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSi
 }
 Vec_Str_t * Wlc_GenerateSmtStdin()
 {
-    char * pLine = "(check-sat)";
-    int c, LineSize = strlen(pLine);
-    Vec_Str_t * vInput = Vec_StrAlloc( 1000 );
+    //char * pLine = "(check-sat)";
+    //int c, LineSize = strlen(pLine);
+    Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); int c;
     while ( (c = fgetc(stdin)) != EOF )
-    {
         Vec_StrPush( vInput, (char)c );
-        if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) )
-            break;
-    }
     Vec_StrPush( vInput, '\0' );
     return vInput;
 }
 void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc )
 {
-    printf( "Output produced by SMT solver will be here.\n" );
+    if ( Abc_FrameReadProbStatus(pAbc) == -1 )
+        printf( "undecided\n" );
+    else if ( Abc_FrameReadProbStatus(pAbc) == 1 )
+        printf( "unsat\n" );
+    else if ( Abc_FrameReadProbStatus(pAbc) == 0 )
+    {
+        Vec_Int_t * vAssign = Vec_IntAlloc( 100 );
+        Abc_Cex_t * pCex = Abc_FrameReadCex( pAbc ); int i;
+        if ( pCex == NULL )
+        {
+            printf( "CEX is not found\n" );
+            return;
+        }
+        for ( i = 0; i < pCex->nPis; i++ )
+            Vec_IntPush( vAssign, Abc_InfoHasBit(pCex->pData, i) );
+        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, vAssign );
+        Vec_IntFree( vAssign );
+    }
 }
 
 /**Function********************************************************************
@@ -417,9 +430,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // transform
-    pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
-    pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
-    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
+    Wlc_GenerateSmtStdout( pAbc );
     return 0;
 usage:
     Abc_Print( -2, "usage: %%test [-vh]\n" );

src/base/wlc/wlcNtk.c

@@ -209,6 +209,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
     Vec_IntFreeP( &p->vInits );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vNameIds.pArray );
+    ABC_FREE( p->vValues.pArray );
     ABC_FREE( p->vCopies.pArray );
     ABC_FREE( p->pInits );
     ABC_FREE( p->pObjs );
@@ -496,6 +497,52 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
     pNew->vTables = p->vTables;      p->vTables = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Report results.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign )
+{
+    //sat
+//((s0 #x12000000070000000000c0000085006b))
+//((s1 #x0e008f00ff0000000000ff0000ed0040))
+//((s2 #x96008f00ff0000000000ff0000ed0040))
+
+    int i, Name, Start, nBits, k;
+    Vec_Str_t * vNum = Vec_StrAlloc( 100 );
+//    Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i )
+//        printf( "Variable %s : %d %d\n", Abc_NamStr(p->pManName, Name), Start, nBits );
+    printf( "sat\n" );
+    Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i )
+    {
+        Vec_StrClear( vNum );
+        for ( k = Start; k < Start + nBits; )
+        {
+            int j, Digit = 0;
+            for ( j = 0; j < 4 && k < Start + nBits; j++, k++ )
+                Digit += (1 << j) * Vec_IntEntry(vAssign, k);
+            assert( Digit >= 0 && Digit < 16 );
+            if ( Digit >= 0 && Digit <= 9 )
+                Vec_StrPush( vNum, (char)('0' + Digit) );
+            else
+                Vec_StrPush( vNum, (char)('a' + Digit - 10) );
+        }
+        Vec_StrPush( vNum, 'x' );
+        Vec_StrPush( vNum, '#' );
+        Vec_StrReverseOrder( vNum );
+        Vec_StrPush( vNum, '\0' );
+        printf( "((%s %s))\n", Abc_NamStr(p->pManName, Name), Vec_StrArray(vNum) );
+    }
+    Vec_StrFree( vNum );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/wlc/wlcReadSmt.c

@@ -32,7 +32,8 @@ typedef enum {
     PRS_SMT_INPUT,    
     PRS_SMT_CONST,    
     PRS_SMT_LET,   
-    PRS_SMT_ASSERT
+    PRS_SMT_ASSERT,
+    PRS_SMT_VALUE
 } Prs_ManType_t; 
 
 // parser
@@ -46,7 +47,8 @@ struct Prs_Smt_t_
     char *       pCur;        // current position
     Abc_Nam_t *  pStrs;       // string manager
     // network structure
-    Vec_Int_t    vData;       
+    Vec_Int_t    vData;
+    Vec_Int_t    vValues;
     // error handling
     char ErrorStr[1000];      
 };
@@ -117,6 +119,7 @@ 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 );
 }
 
@@ -234,8 +237,24 @@ static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type )
     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 == '(' )
     {
@@ -263,25 +282,35 @@ int Prs_SmtReadLines( Prs_Smt_t * p )
             assert( *p->pCur == ')' );
             p->pCur++;
         }
-        else if ( Prs_SmtIsWord(p, "check-sat") )
+        else if ( Prs_SmtIsWord(p, "get-value") )
         {
-            Vec_IntPush( &p->vData, 0 );
-            return 1;
+            if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) )
+                return 0;
+            assert( *p->pCur == ')' );
+            p->pCur++;
         }
         else if ( Prs_SmtIsWord(p, "assert") )
-        {}
-        else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") )
+            fAssert = 1;
+        else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") || Prs_SmtIsWord(p, "check-sat") )
             p->pCur = Prs_SmtFindNextPar(p) + 1;
-        else
-            break;
+//        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 );
+        }
     }
-    // finish parsing assert
-    if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) )
-        return 0;
-    assert( *p->pCur == ')' );
-    Vec_IntPush( &p->vData, 0 );
+    assert( fAssert == 0 );
     return 1;
 }
 
@@ -320,6 +349,8 @@ void Prs_SmtPrintParser( Prs_Smt_t * p )
         }
         printf( " %s", Abc_NamStr(p->pStrs, Entry) );
     }
+    Vec_IntForEachEntry( &p->vValues, Entry, i )
+        printf( "get-value %s\n", Abc_NamStr(p->pStrs, Entry) );
 }
 
 
@@ -404,9 +435,9 @@ static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec
         return 1;
     }
 }
-static inline int Prs_SmtStrToType( char * pName )
+static inline int Prs_SmtStrToType( char * pName, int * pfSigned )
 {
-    int Type = 0;
+    int Type = 0; *pfSigned = 0;
     if ( !strcmp(pName, "ite") )
         Type = WLC_OBJ_MUX;           // 08: multiplexer
     else if ( !strcmp(pName, "bvlshr") )
@@ -436,56 +467,77 @@ static inline int Prs_SmtStrToType( char * pName )
     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
+        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, "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, "xor") )
+        Type = WLC_OBJ_LOGIC_XOR;     // 26: logic OR
     else if ( !strcmp(pName, "bvcomp") )
-        Type = WLC_OBJ_COMP_EQU;      // 26: compare equal
+        Type = WLC_OBJ_COMP_EQU;      // 27: compare equal
 //    else if ( !strcmp(pName, "") )
-//        Type = WLC_OBJ_COMP_NOTEQU;   // 27: compare not equal
+//        Type = WLC_OBJ_COMP_NOTEQU;   // 28: compare not equal
     else if ( !strcmp(pName, "bvult") )
-        Type = WLC_OBJ_COMP_LESS;     // 28: compare less
+        Type = WLC_OBJ_COMP_LESS;     // 29: compare less
     else if ( !strcmp(pName, "bvugt") )
-        Type = WLC_OBJ_COMP_MORE;     // 29: compare more
+        Type = WLC_OBJ_COMP_MORE;     // 30: compare more
     else if ( !strcmp(pName, "bvule") )
-        Type = WLC_OBJ_COMP_LESSEQU;  // 30: compare less or equal
+        Type = WLC_OBJ_COMP_LESSEQU;  // 31: compare less or equal
     else if ( !strcmp(pName, "bvuge") )
-        Type = WLC_OBJ_COMP_MOREEQU;  // 31: compare more or equal
+        Type = WLC_OBJ_COMP_MOREEQU;  // 32: compare more or equal
+    else if ( !strcmp(pName, "bvslt") )
+        Type = WLC_OBJ_COMP_LESS, *pfSigned = 1;     // 29: compare less
+    else if ( !strcmp(pName, "bvsgt") )
+        Type = WLC_OBJ_COMP_MORE, *pfSigned = 1;     // 30: compare more
+    else if ( !strcmp(pName, "bvsle") )
+        Type = WLC_OBJ_COMP_LESSEQU, *pfSigned = 1;  // 31: compare less or equal
+    else if ( !strcmp(pName, "bvsge") )
+        Type = WLC_OBJ_COMP_MOREEQU, *pfSigned = 1;  // 32: compare more or equal
     else if ( !strcmp(pName, "bvredand") )
-        Type = WLC_OBJ_REDUCT_AND;    // 32: reduction AND
+        Type = WLC_OBJ_REDUCT_AND;    // 33: reduction AND
     else if ( !strcmp(pName, "bvredor") )
-        Type = WLC_OBJ_REDUCT_OR;     // 33: reduction OR
+        Type = WLC_OBJ_REDUCT_OR;     // 34: reduction OR
     else if ( !strcmp(pName, "bvredxor") )
-        Type = WLC_OBJ_REDUCT_XOR;    // 34: reduction XOR
+        Type = WLC_OBJ_REDUCT_XOR;    // 35: reduction XOR
     else if ( !strcmp(pName, "bvadd") )
-        Type = WLC_OBJ_ARI_ADD;       // 35: arithmetic addition
+        Type = WLC_OBJ_ARI_ADD;       // 36: arithmetic addition
     else if ( !strcmp(pName, "bvsub") )
-        Type = WLC_OBJ_ARI_SUB;       // 36: arithmetic subtraction
+        Type = WLC_OBJ_ARI_SUB;       // 37: 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
+        Type = WLC_OBJ_ARI_MULTI;     // 38: arithmetic multiplier
+    else if ( !strcmp(pName, "bvudiv") )
+        Type = WLC_OBJ_ARI_DIVIDE;    // 39: arithmetic division
     else if ( !strcmp(pName, "bvurem") )
-        Type = WLC_OBJ_ARI_MODULUS;   // 39: arithmetic modulus
+        Type = WLC_OBJ_ARI_MODULUS;   // 40: arithmetic modulus
+    else if ( !strcmp(pName, "bvsdiv") )
+        Type = WLC_OBJ_ARI_DIVIDE, *pfSigned = 1;    // 39: arithmetic division
+    else if ( !strcmp(pName, "bvsrem") )
+        Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1;   // 40: arithmetic modulus
+    else if ( !strcmp(pName, "bvsmod") )
+        Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1;   // 40: arithmetic modulus
 //    else if ( !strcmp(pName, "") )
-//        Type = WLC_OBJ_ARI_POWER;     // 40: arithmetic power
+//        Type = WLC_OBJ_ARI_POWER;     // 41: arithmetic power
     else if ( !strcmp(pName, "bvneg") )
-        Type = WLC_OBJ_ARI_MINUS;     // 41: arithmetic minus
+        Type = WLC_OBJ_ARI_MINUS;       // 42: arithmetic minus
 //    else if ( !strcmp(pName, "") )
-//        Type = WLC_OBJ_TABLE;         // 42: bit table
-    else assert( 0 );
+//        Type = WLC_OBJ_TABLE;         // 43: bit table
+    else
+    {
+        printf( "The following operations is currently not supported (%s)\n", pName );
+        fflush( stdout );
+        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 )
+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 )
 {
     int Type, NameId;
     char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) );
     // read type
-    Type = Prs_SmtStrToType( pName );
+    Type = Prs_SmtStrToType( pName, pfSigned );
     if ( Type == 0 )
         return 0;
     *pRange = 0;
@@ -499,7 +551,7 @@ static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t *
     }
     else if ( Type == WLC_OBJ_LOGIC_NOT )
     {
-        pName  = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+        pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
         if ( !strcmp(pName, "bvcomp") )
         {
             *pRange = 1;
@@ -558,7 +610,7 @@ 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;
+    int i, k, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0;
     // start network and create primary inputs
     pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 );
     pNtk->pManName = Abc_NamStart( 1000, 24 );
@@ -567,12 +619,23 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
         assert( Vec_IntEntry(&p->vData, i) == 0 );
         if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT )
         {
+            int NameOld = Vec_IntEntry(&p->vData, i+1);
             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_IntForEachEntry( &p->vValues, Entry, k )
+                if ( Entry == NameOld )
+                {
+                    Vec_IntPush( &pNtk->vValues, NameId );
+                    Vec_IntPush( &pNtk->vValues, nBits );
+                    Vec_IntPush( &pNtk->vValues, atoi(pBits) );
+                    break;
+                }
+            nBits += atoi(pBits);
         }
         while ( Vec_IntEntry(&p->vData, ++i) );
     }
@@ -595,13 +658,21 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
         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 );
+            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 );
@@ -648,6 +719,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
     vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
     Vec_IntAppend( &pNtk->vNameIds, vFanins );
     Vec_IntFree( vFanins );
+    //Wlc_NtkReport( pNtk, NULL );
     return pNtk;
 }
 Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )