summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/map/scl/sclFile.c115
-rw-r--r--src/misc/vec/vecStr.h115
-rw-r--r--src/proof/abs/absGla.c2
3 files changed, 116 insertions, 116 deletions
diff --git a/src/map/scl/sclFile.c b/src/map/scl/sclFile.c
index dd5dff47..395bcf3b 100644
--- a/src/map/scl/sclFile.c
+++ b/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 []
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 485ccbba..d64fea65 100644
--- a/src/misc/vec/vecStr.h
+++ b/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
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 1369015d..80ef6ccf 100644
--- a/src/proof/abs/absGla.c
+++ b/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 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-10 15:40:24 +0000