Extending memory page size for proof logging.

1 files changed, 16 insertions, 13 deletions

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;