Improved bit-blasting of various operators in Wlc_Ntk_t; added SQRT operator (@).

src/base/wlc/wlc.h

@@ -85,9 +85,11 @@ typedef enum {
     WLC_OBJ_ARI_MODULUS,   // 41: arithmetic modulus
     WLC_OBJ_ARI_POWER,     // 42: arithmetic power
     WLC_OBJ_ARI_MINUS,     // 43: arithmetic minus
-    WLC_OBJ_TABLE,         // 44: bit table
-    WLC_OBJ_NUMBER         // 45: unused
+    WLC_OBJ_ARI_SQRT,      // 44: integer square root
+    WLC_OBJ_TABLE,         // 45: bit table
+    WLC_OBJ_NUMBER         // 46: unused
 } Wlc_ObjType_t;
+// when adding new types, remember to update table Wlc_Names in "wlcNtk.c"
 
 
 // Unlike AIG managers and logic networks in ABC, this network treats POs and FIs 

src/base/wlc/wlcNtk.c

@@ -73,10 +73,12 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     "%",                   // 41: arithmetic modulus
     "**",                  // 42: arithmetic power
     "-",                   // 43: arithmetic minus
-    "table",               // 44: bit table
-    NULL                   // 45: unused
+    "sqrt",                // 44: integer square root
+    "table",               // 45: bit table
+    NULL                   // 46: unused
 };
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////

src/base/wlc/wlcReadVer.c

@@ -653,12 +653,14 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
             return 0;
         Type = WLC_OBJ_CONST;
     }
-    else if ( pStr[0] == '!' || pStr[0] == '~' )
+    else if ( pStr[0] == '!' || pStr[0] == '~' || pStr[0] == '@' )
     {
         if ( pStr[0] == '!' )
             Type = WLC_OBJ_LOGIC_NOT;
         else if ( pStr[0] == '~' )
             Type = WLC_OBJ_BIT_NOT;
+        else if ( pStr[0] == '@' )
+            Type = WLC_OBJ_ARI_SQRT;
         else assert( 0 );
         // skip parentheses
         pStr = Wlc_PrsSkipSpaces( pStr+1 );

src/base/wlc/wlcWriteVer.c

@@ -324,6 +324,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                     fprintf( pFile, "%%" );
                 else if ( pObj->Type == WLC_OBJ_ARI_POWER )
                     fprintf( pFile, "**" );
+                else if ( pObj->Type == WLC_OBJ_ARI_SQRT )
+                    fprintf( pFile, "@" );
                 else assert( 0 );
                 fprintf( pFile, " %s", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, 1)) );
             }