Moving binary IO streams to the vector package.

src/map/scl/sclFile.c

@@ -35,121 +35,6 @@ extern void Extra_PrintHex( FILE * pFile, unsigned Sign[], int nBits );
 
 /**Function*************************************************************
 
-  Synopsis    [Binary I/O for numbers (int/float/etc) and strings (char *).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrPutI_ne( Vec_Str_t * vOut, int Val )
-{
-    int i;
-    for ( i = 0; i < 4; i++ )
-        Vec_StrPush( vOut, (char)(Val >> (8*i)) );
-}
-static inline int Vec_StrGetI_ne( Vec_Str_t * vOut, int * pPos )
-{
-    int i;
-    int Val = 0;
-    for ( i = 0; i < 4; i++ )
-        Val |= (int)(unsigned char)Vec_StrEntry(vOut, (*pPos)++) << (8*i);
-    return Val;
-}
-
-static inline void Vec_StrPutI( Vec_Str_t * vOut, int Val )
-{
-    for ( ; Val >= 0x80; Val >>= 7 )
-        Vec_StrPush( vOut, (unsigned char)(Val | 0x80) );
-    Vec_StrPush( vOut, (unsigned char)Val );
-}
-static inline int Vec_StrGetI( Vec_Str_t * vOut, int * pPos )
-{
-    unsigned char ch;
-    int i = 0, Val = 0;
-    while ( (ch = Vec_StrEntry(vOut, (*pPos)++)) & 0x80 )
-        Val |= (ch & 0x7f) << (7 * i++);
-    return Val | (ch << (7 * i));
-}
-
-static inline void Vec_StrPutW( Vec_Str_t * vOut, word Val )
-{
-    int i;
-    for ( i = 0; i < 8; i++ )
-        Vec_StrPush( vOut, (char)(Val >> (8*i)) );
-}
-static inline word Vec_StrGetW( Vec_Str_t * vOut, int * pPos )
-{
-    int i;
-    word Val = 0;
-    for ( i = 0; i < 8; i++ )
-        Val |= (word)(unsigned char)Vec_StrEntry(vOut, (*pPos)++) << (8*i);
-    return Val;
-}
-
-static inline void Vec_StrPutF( Vec_Str_t * vOut, float Val )
-{
-    union { float num; unsigned char data[4]; } tmp;
-    tmp.num = Val;
-    Vec_StrPush( vOut, tmp.data[0] );
-    Vec_StrPush( vOut, tmp.data[1] );
-    Vec_StrPush( vOut, tmp.data[2] );
-    Vec_StrPush( vOut, tmp.data[3] );
-}
-static inline float Vec_StrGetF( Vec_Str_t * vOut, int * pPos )
-{
-    union { float num; unsigned char data[4]; } tmp;
-    tmp.data[0] = Vec_StrEntry( vOut, (*pPos)++ );
-    tmp.data[1] = Vec_StrEntry( vOut, (*pPos)++ );
-    tmp.data[2] = Vec_StrEntry( vOut, (*pPos)++ );
-    tmp.data[3] = Vec_StrEntry( vOut, (*pPos)++ );
-    return tmp.num;
-}
-
-static inline void Vec_StrPutD( Vec_Str_t * vOut, double Val )
-{
-    union { double num; unsigned char data[8]; } tmp;
-    int i, Lim = sizeof(double);
-    tmp.num = Val;
-    for ( i = 0; i < Lim; i++ )
-        Vec_StrPush( vOut, tmp.data[i] );
-}
-static inline double Vec_StrGetD( Vec_Str_t * vOut, int * pPos )
-{
-    union { double num; unsigned char data[8]; } tmp;
-    int i, Lim = sizeof(double);
-    for ( i = 0; i < Lim; i++ )
-        tmp.data[i] = Vec_StrEntry( vOut, (*pPos)++ );
-    return tmp.num;
-}
-
-static inline void Vec_StrPutS( Vec_Str_t * vOut, char * pStr )
-{
-    while ( *pStr )
-        Vec_StrPush( vOut, *pStr++ );
-    Vec_StrPush( vOut, (char)0 );
-}
-static inline char * Vec_StrGetS( Vec_Str_t * vOut, int * pPos )
-{
-    char * pStr = Vec_StrEntryP( vOut, *pPos );
-    while ( Vec_StrEntry(vOut, (*pPos)++) );
-    return Abc_UtilStrsav(pStr);
-}
-
-static inline void Vec_StrPutC( Vec_Str_t * vOut, char c )
-{
-    Vec_StrPush( vOut, c );
-}
-static inline char Vec_StrGetC( Vec_Str_t * vOut, int * pPos )
-{
-    return Vec_StrEntry(vOut, (*pPos)++);
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Reading library from file.]
 
   Description []

src/misc/vec/vecStr.h

@@ -720,6 +720,121 @@ static inline int Vec_StrCompareVec( Vec_Str_t * p1, Vec_Str_t * p2 )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Binary I/O for numbers (int/float/etc) and strings (char *).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPutI_ne( Vec_Str_t * vOut, int Val )
+{
+    int i;
+    for ( i = 0; i < 4; i++ )
+        Vec_StrPush( vOut, (char)(Val >> (8*i)) );
+}
+static inline int Vec_StrGetI_ne( Vec_Str_t * vOut, int * pPos )
+{
+    int i;
+    int Val = 0;
+    for ( i = 0; i < 4; i++ )
+        Val |= (int)(unsigned char)Vec_StrEntry(vOut, (*pPos)++) << (8*i);
+    return Val;
+}
+
+static inline void Vec_StrPutI( Vec_Str_t * vOut, int Val )
+{
+    for ( ; Val >= 0x80; Val >>= 7 )
+        Vec_StrPush( vOut, (unsigned char)(Val | 0x80) );
+    Vec_StrPush( vOut, (unsigned char)Val );
+}
+static inline int Vec_StrGetI( Vec_Str_t * vOut, int * pPos )
+{
+    unsigned char ch;
+    int i = 0, Val = 0;
+    while ( (ch = Vec_StrEntry(vOut, (*pPos)++)) & 0x80 )
+        Val |= (ch & 0x7f) << (7 * i++);
+    return Val | (ch << (7 * i));
+}
+
+static inline void Vec_StrPutW( Vec_Str_t * vOut, word Val )
+{
+    int i;
+    for ( i = 0; i < 8; i++ )
+        Vec_StrPush( vOut, (char)(Val >> (8*i)) );
+}
+static inline word Vec_StrGetW( Vec_Str_t * vOut, int * pPos )
+{
+    int i;
+    word Val = 0;
+    for ( i = 0; i < 8; i++ )
+        Val |= (word)(unsigned char)Vec_StrEntry(vOut, (*pPos)++) << (8*i);
+    return Val;
+}
+
+static inline void Vec_StrPutF( Vec_Str_t * vOut, float Val )
+{
+    union { float num; unsigned char data[4]; } tmp;
+    tmp.num = Val;
+    Vec_StrPush( vOut, tmp.data[0] );
+    Vec_StrPush( vOut, tmp.data[1] );
+    Vec_StrPush( vOut, tmp.data[2] );
+    Vec_StrPush( vOut, tmp.data[3] );
+}
+static inline float Vec_StrGetF( Vec_Str_t * vOut, int * pPos )
+{
+    union { float num; unsigned char data[4]; } tmp;
+    tmp.data[0] = Vec_StrEntry( vOut, (*pPos)++ );
+    tmp.data[1] = Vec_StrEntry( vOut, (*pPos)++ );
+    tmp.data[2] = Vec_StrEntry( vOut, (*pPos)++ );
+    tmp.data[3] = Vec_StrEntry( vOut, (*pPos)++ );
+    return tmp.num;
+}
+
+static inline void Vec_StrPutD( Vec_Str_t * vOut, double Val )
+{
+    union { double num; unsigned char data[8]; } tmp;
+    int i, Lim = sizeof(double);
+    tmp.num = Val;
+    for ( i = 0; i < Lim; i++ )
+        Vec_StrPush( vOut, tmp.data[i] );
+}
+static inline double Vec_StrGetD( Vec_Str_t * vOut, int * pPos )
+{
+    union { double num; unsigned char data[8]; } tmp;
+    int i, Lim = sizeof(double);
+    for ( i = 0; i < Lim; i++ )
+        tmp.data[i] = Vec_StrEntry( vOut, (*pPos)++ );
+    return tmp.num;
+}
+
+static inline void Vec_StrPutS( Vec_Str_t * vOut, char * pStr )
+{
+    while ( *pStr )
+        Vec_StrPush( vOut, *pStr++ );
+    Vec_StrPush( vOut, (char)0 );
+}
+static inline char * Vec_StrGetS( Vec_Str_t * vOut, int * pPos )
+{
+    char * pStr = Vec_StrEntryP( vOut, *pPos );
+    while ( Vec_StrEntry(vOut, (*pPos)++) );
+    return Abc_UtilStrsav(pStr);
+}
+
+static inline void Vec_StrPutC( Vec_Str_t * vOut, char c )
+{
+    Vec_StrPush( vOut, c );
+}
+static inline char Vec_StrGetC( Vec_Str_t * vOut, int * pPos )
+{
+    return Vec_StrEntry(vOut, (*pPos)++);
+}
+
+
 
 ABC_NAMESPACE_HEADER_END
 

src/proof/abs/absGla.c

@@ -1833,7 +1833,7 @@ finish:
     if ( !p->fUseNewLine )
         Abc_Print( 1, "\n" );
     if ( RetValue == 1 )
-        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryToProve );
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d  ", p->pPars->iFrameProved+1, iFrameTryToProve );
     else if ( pAig->pCexSeq == NULL )
     {
         Vec_IntFreeP( &pAig->vGateClasses );