Skip to content

A
abc
Commit 5ad0fea6 by Alan Mishchenko
Options

Extending memory page size for proof logging.

parent 12d9aaa7
Showing with 16 additions and 13 deletions
src/sat/bsat/vecSet.h
...@@ -35,12 +35,15 @@ ABC_NAMESPACE_HEADER_START ...@@ -35,12 +35,15 @@ ABC_NAMESPACE_HEADER_START
/// PARAMETERS /// /// PARAMETERS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#define VEC_SET_PAGE 20
#define VEC_SET_MASK 0xFFFFF
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// BASIC TYPES /// /// BASIC TYPES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// data-structure for logging entries // 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 'word' of each page is used storing additional data
// the first 'int' of additional data stores the word limit // the first 'int' of additional data stores the word limit
// the second 'int' of the additional data stores the shadow word limit // the second 'int' of the additional data stores the shadow word limit
...@@ -59,8 +62,8 @@ struct Vec_Set_t_ ...@@ -59,8 +62,8 @@ struct Vec_Set_t_
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline int Vec_SetHandPage( int h ) { return h >> 16; } static inline int Vec_SetHandPage( int h ) { return h >> VEC_SET_PAGE; }
static inline int Vec_SetHandShift( int h ) { return h & 0xFFFF; } 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 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); } 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* ...@@ -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_SetWriteLimit( word * p, int nWords ) { ((int*)p)[0] = nWords; }
static inline void Vec_SetWriteLimitS( word * p, int nWords ) { ((int*)p)[1] = 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_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 << 16) + Vec_SetLimitS(p->pPages[p->iPageS]); } 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_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_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 // Type is the Set type
// pVec is vector of set // pVec is vector of set
...@@ -113,7 +116,7 @@ static inline void Vec_SetAlloc_( Vec_Set_t * p ) ...@@ -113,7 +116,7 @@ static inline void Vec_SetAlloc_( Vec_Set_t * p )
memset( p, 0, sizeof(Vec_Set_t) ); memset( p, 0, sizeof(Vec_Set_t) );
p->nPagesAlloc = 256; p->nPagesAlloc = 256;
p->pPages = ABC_CALLOC( word *, p->nPagesAlloc ); 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; p->pPages[0][0] = ~0;
Vec_SetWriteLimit( p->pPages[0], 1 ); Vec_SetWriteLimit( p->pPages[0], 1 );
} }
...@@ -183,9 +186,9 @@ static inline void Vec_SetFree( Vec_Set_t * p ) ...@@ -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 ) static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
{ {
int nWords = Vec_SetWordNum( nSize ); int nWords = Vec_SetWordNum( nSize );
assert( nWords < 0x10000 ); assert( nWords < (1 << VEC_SET_PAGE) );
p->nEntries++; 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 ) if ( ++p->iPage == p->nPagesAlloc )
{ {
...@@ -194,7 +197,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) ...@@ -194,7 +197,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
p->nPagesAlloc *= 2; p->nPagesAlloc *= 2;
} }
if ( p->pPages[p->iPage] == NULL ) 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; p->pPages[p->iPage][0] = ~0;
Vec_SetWriteLimit( p->pPages[p->iPage], 1 ); Vec_SetWriteLimit( p->pPages[p->iPage], 1 );
} }
...@@ -206,8 +209,8 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) ...@@ -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 ) static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
{ {
int nWords = Vec_SetWordNum( nSize ); int nWords = Vec_SetWordNum( nSize );
assert( nWords < 0x10000 ); assert( nWords < (1 << VEC_SET_PAGE) );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > 0x10000 ) if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << VEC_SET_PAGE) )
Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 ); Vec_SetWriteLimitS( p->pPages[++p->iPageS], 1 );
Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
return Vec_SetHandCurrentS(p) - nWords; return Vec_SetHandCurrentS(p) - nWords;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment