Improving SMT-LIB parser.

6 files changed, 38 insertions, 27 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index b12e239c..0165a0a4 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -89,13 +89,14 @@ typedef enum {
     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_OBJ_ARI_REM,       // 47: arithmetic remainder
+    WLC_OBJ_ARI_MODULUS,   // 48: arithmetic modulus
+    WLC_OBJ_ARI_POWER,     // 49: arithmetic power
+    WLC_OBJ_ARI_MINUS,     // 50: arithmetic minus
+    WLC_OBJ_ARI_SQRT,      // 51: integer square root
+    WLC_OBJ_ARI_SQUARE,    // 52: integer square
+    WLC_OBJ_TABLE,         // 53: bit table
+    WLC_OBJ_NUMBER         // 54: unused
 } Wlc_ObjType_t;
 // when adding new types, remember to update table Wlc_Names in "wlcNtk.c"
 
@@ -138,6 +139,7 @@ struct Wlc_Ntk_t_
     char *                 pInits;             // initial values
     int                    nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
     int                    nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
+    int                    fSmtLib;            // the network comes from an SMT-LIB file
     // memory for objects
     Wlc_Obj_t *            pObjs;
     int                    iObj;
@@ -196,7 +198,7 @@ static inline int          Wlc_ObjRangeBeg( Wlc_Obj_t * p )
 static inline int          Wlc_ObjRangeIsReversed( Wlc_Obj_t * p )                  { return p->End < p->Beg;                                                  }
 
 static inline int          Wlc_ObjIsSigned( Wlc_Obj_t * p )                         { return p->Signed;                                                        }
-static inline int          Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed; }
+static inline int          Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : (Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed); }
 static inline int          Wlc_ObjSign( Wlc_Obj_t * p )                             { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjIsSigned(p) );               }
 static inline int *        Wlc_ObjConstValue( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_CONST);      return Wlc_ObjFanins(p);          }
 static inline int          Wlc_ObjTableId( Wlc_Obj_t * p )                          { assert(p->Type == WLC_OBJ_TABLE);      return p->Fanins[1];              }
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 5ef7ef14..f6cd9310 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1130,7 +1130,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
                 assert( Vec_IntSize(vRes) == nRange );
             }
         }
-        else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
             int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 726e7bf8..5a08cd99 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -78,13 +78,14 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     "-",                   // 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
+    "%",                   // 47: arithmetic reminder
+    "mod",                 // 48: arithmetic modulus
+    "**",                  // 49: arithmetic power
+    "-",                   // 50: arithmetic minus
+    "sqrt",                // 51: integer square root
+    "square",              // 52: integer square
+    "table",               // 53: bit table
+    NULL                   // 54: unused
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -421,6 +422,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_MULTI,    9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) );
         else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE )   
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_DIVIDE,  13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 19 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) + 10 );
+        else if ( pObj->Type == WLC_OBJ_ARI_REM )  
+            Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_REM,     13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 7 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 2  );
         else if ( pObj->Type == WLC_OBJ_ARI_MODULUS )  
             Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_MODULUS, 13 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 7 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 2  );
         else if ( pObj->Type == WLC_OBJ_ARI_POWER ) 
@@ -586,6 +589,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
     Wlc_NtkCleanCopy( p );
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+    pNew->fSmtLib = p->fSmtLib;
     Wlc_NtkForEachCi( p, pObj, i )
         Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
@@ -645,6 +649,7 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
     Wlc_NtkCleanCopy( p );
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+    pNew->fSmtLib = p->fSmtLib;
     Wlc_NtkForEachObj( p, pObj, i )
     {
         if ( Wlc_ObjIsCi(pObj) )
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index d68688c4..9ebecb73 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -166,7 +166,7 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
     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, *pfSigned = 1;   // 22: sign extension
+        Type = WLC_OBJ_BIT_SIGNEXT;   // 22: sign extension
     else if ( !strcmp(pName, "not") )
         Type = WLC_OBJ_LOGIC_NOT;     // 23: logic NOT
     else if ( !strcmp(pName, "=>") )
@@ -212,11 +212,11 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
     else if ( !strcmp(pName, "bvudiv") )
         Type = WLC_OBJ_ARI_DIVIDE;    // 39: arithmetic division
     else if ( !strcmp(pName, "bvurem") )
-        Type = WLC_OBJ_ARI_MODULUS;   // 40: arithmetic modulus
+        Type = WLC_OBJ_ARI_REM;       // 40: arithmetic remainder
     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
+        Type = WLC_OBJ_ARI_REM, *pfSigned = 1;       // 40: arithmetic remainder
     else if ( !strcmp(pName, "bvsmod") )
         Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1;   // 40: arithmetic modulus
 //    else if ( !strcmp(pName, "") )
@@ -278,10 +278,10 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
     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;
+//        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;
     }
     if ( pName == NULL )
     {
@@ -499,6 +499,7 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
     // start network and create primary inputs
     pNtk = Wlc_NtkAlloc( p->pName, 1000 );
     pNtk->pManName = Abc_NamStart( 1000, 24 );
+    pNtk->fSmtLib = 1;
     Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i )
     {
         assert( Vec_IntSize(vFans) == 4 );
@@ -797,7 +798,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
                         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);
+                        //fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
                         if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
                         {
                             int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) );
@@ -899,6 +900,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
     // start network and create primary inputs
     pNtk = Wlc_NtkAlloc( p->pName, 1000 );
     pNtk->pManName = Abc_NamStart( 1000, 24 );
+    pNtk->fSmtLib = 1;
     // collect top-level asserts
     vFansRoot = Vec_WecEntry( &p->vObjs, 0 );
     Vec_IntForEachEntry( vFansRoot, Root, i )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 7683f8a6..7753d24d 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -795,7 +795,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
             else if ( pStr[0] == '-'                                     ) pStr += 1, Type = WLC_OBJ_ARI_SUB;       
             else if ( pStr[0] == '*' && pStr[1] != '*'                   ) pStr += 1, Type = WLC_OBJ_ARI_MULTI;     
             else if ( pStr[0] == '/'                                     ) pStr += 1, Type = WLC_OBJ_ARI_DIVIDE;        
-            else if ( pStr[0] == '%'                                     ) pStr += 1, Type = WLC_OBJ_ARI_MODULUS;   
+            else if ( pStr[0] == '%'                                     ) pStr += 1, Type = WLC_OBJ_ARI_REM;   
             else if ( pStr[0] == '*' && pStr[1] == '*'                   ) pStr += 2, Type = WLC_OBJ_ARI_POWER;
             else return Wlc_PrsWriteErrorMessage( p, pStr, "Unsupported operation (%c).", pStr[0] );
             if ( !(pStr = Wlc_PrsReadName(p, pStr+1, vFanins)) )
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index b15d3d38..cf0e528f 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -171,7 +171,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
             pObj->Mark = 0;
             continue;
         }
-        sprintf( Range, "%s[%d:%d]%*s", Wlc_ObjIsSigned(pObj) ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
+        sprintf( Range, "%s[%d:%d]%*s", (!p->fSmtLib && Wlc_ObjIsSigned(pObj)) ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
         fprintf( pFile, "  " );
         if ( pObj->Type == WLC_OBJ_PI || (fNoFlops && pObj->Type == WLC_OBJ_FO) )
             fprintf( pFile, "input  " );
@@ -342,6 +342,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                     fprintf( pFile, "*" );
                 else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE )
                     fprintf( pFile, "/" );
+                else if ( pObj->Type == WLC_OBJ_ARI_REM )
+                    fprintf( pFile, "%%" );
                 else if ( pObj->Type == WLC_OBJ_ARI_MODULUS )
                     fprintf( pFile, "%%" );
                 else if ( pObj->Type == WLC_OBJ_ARI_POWER )
@@ -355,7 +357,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                 fprintf( pFile, " %s", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, 1)) );
             }
         }
-        fprintf( pFile, " ;\n" );
+        fprintf( pFile, " ;%s\n", (p->fSmtLib && Wlc_ObjIsSigned(pObj)) ? " // signed SMT-LIB operator" : "" );
     }
     iFanin = 0;
     assert( !p->vInits || Wlc_NtkFfNum(p) == Vec_IntSize(p->vInits) );