From 5ad0fea6060e84269bdd37526d97d0d70f5e70c5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Mar 2012 09:01:50 +0100 Subject: Extending memory page size for proof logging. --- src/sat/bsat/vecSet.h | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h index b1c4de63..d705c2ee 100644 --- a/src/sat/bsat/vecSet.h +++ b/src/sat/bsat/vecSet.h @@ -35,12 +35,15 @@ ABC_NAMESPACE_HEADER_START /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#define VEC_SET_PAGE 20 +#define VEC_SET_MASK 0xFFFFF + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// // data-structure for logging entries -// memory is allocated in 2^16 word-sized pages +// memory is allocated in 2^VEC_SET_PAGE word-sized pages // the first 'word' of each page is used storing additional data // the first 'int' of additional data stores the word limit // the second 'int' of the additional data stores the shadow word limit @@ -59,8 +62,8 @@ struct Vec_Set_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Vec_SetHandPage( int h ) { return h >> 16; } -static inline int Vec_SetHandShift( int h ) { return h & 0xFFFF; } +static inline int Vec_SetHandPage( int h ) { return h >> VEC_SET_PAGE; } +static inline int Vec_SetHandShift( int h ) { return h & VEC_SET_MASK; } static inline int Vec_SetWordNum( int nSize ) { return (nSize + 1) >> 1; } static inline word * Vec_SetEntry( Vec_Set_t * p, int h ) { return p->pPages[Vec_SetHandPage(h)] + Vec_SetHandShift(h); } @@ -76,13 +79,13 @@ static inline int Vec_SetIncLimitS( word * p, int nWords ) { return ((int* static inline void Vec_SetWriteLimit( word * p, int nWords ) { ((int*)p)[0] = nWords; } static inline void Vec_SetWriteLimitS( word * p, int nWords ) { ((int*)p)[1] = nWords; } -static inline int Vec_SetHandCurrent( Vec_Set_t * p ) { return (p->iPage << 16) + Vec_SetLimit(p->pPages[p->iPage]); } -static inline int Vec_SetHandCurrentS( Vec_Set_t * p ) { return (p->iPageS << 16) + Vec_SetLimitS(p->pPages[p->iPageS]); } +static inline int Vec_SetHandCurrent( Vec_Set_t * p ) { return (p->iPage << VEC_SET_PAGE) + Vec_SetLimit(p->pPages[p->iPage]); } +static inline int Vec_SetHandCurrentS( Vec_Set_t * p ) { return (p->iPageS << VEC_SET_PAGE) + Vec_SetLimitS(p->pPages[p->iPageS]); } -static inline int Vec_SetHandMemory( Vec_Set_t * p, int h ) { return Vec_SetHandPage(h) * 0x8FFFF + Vec_SetHandShift(h) * 8; } +static inline int Vec_SetHandMemory( Vec_Set_t * p, int h ) { return Vec_SetHandPage(h) * (1 << (VEC_SET_PAGE+3)) + Vec_SetHandShift(h) * 8; } static inline int Vec_SetMemory( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrent(p)); } static inline int Vec_SetMemoryS( Vec_Set_t * p ) { return Vec_SetHandMemory(p, Vec_SetHandCurrentS(p)); } -static inline int Vec_SetMemoryAll( Vec_Set_t * p ) { return (p->iPage+1) * 0x8FFFF; } +static inline int Vec_SetMemoryAll( Vec_Set_t * p ) { return (p->iPage+1) * (1 << (VEC_SET_PAGE+3)); } // Type is the Set type // pVec is vector of set @@ -113,7 +116,7 @@ static inline void Vec_SetAlloc_( Vec_Set_t * p ) memset( p, 0, sizeof(Vec_Set_t) ); p->nPagesAlloc = 256; p->pPages = ABC_CALLOC( word *, p->nPagesAlloc ); - p->pPages[0] = ABC_ALLOC( word, 0x10000 ); + p->pPages[0] = ABC_ALLOC( word, (1 << VEC_SET_PAGE) ); p->pPages[0][0] = ~0; Vec_SetWriteLimit( p->pPages[0], 1 ); } @@ -183,9 +186,9 @@ static inline void Vec_SetFree( Vec_Set_t * p ) static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) { int nWords = Vec_SetWordNum( nSize ); - assert( nWords < 0x10000 ); + assert( nWords < (1 << VEC_SET_PAGE) ); p->nEntries++; - if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > 0x10000 ) + if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << VEC_SET_PAGE) ) { if ( ++p->iPage == p->nPagesAlloc ) { @@ -194,7 +197,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) p->nPagesAlloc *= 2; } if ( p->pPages[p->iPage] == NULL ) - p->pPages[p->iPage] = ABC_ALLOC( word, 0x10000 ); + p->pPages[p->iPage] = ABC_ALLOC( word, (1 << VEC_SET_PAGE) ); p->pPages[p->iPage][0] = ~0; Vec_SetWriteLimit( p->pPages[p->iPage], 1 ); } @@ -206,8 +209,8 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) { int nWords = Vec_SetWordNum( nSize ); - assert( nWords < 0x10000 ); - if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 ) + assert( nWords < (1 << VEC_SET_PAGE) ); + if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << VEC_SET_PAGE) ) Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 ); Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); return Vec_SetHandCurrentS(p) - nWords; -- cgit v1.2.3