diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 15:57:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 15:57:18 -0700 |
| commit | c265d2449adcfc634e6546076ec1427b21b66afe (patch) | |
| tree | c67eca250d400e50ab106a3eb67d12899e6020e4 /src/misc/vec | |
| parent | 685faae8e2e54e0d2d4a302f37ef9895073eb412 (diff) | |
| download | abc-c265d2449adcfc634e6546076ec1427b21b66afe.tar.gz abc-c265d2449adcfc634e6546076ec1427b21b66afe.tar.bz2 abc-c265d2449adcfc634e6546076ec1427b21b66afe.zip | |
Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).
Diffstat (limited to 'src/misc/vec')
| -rw-r--r-- | src/misc/vec/vecSet.h | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 72358ea1..8b031e1e 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -210,10 +210,11 @@ static inline double Vec_ReportMemory( Vec_Set_t * p ) ***********************************************************************/ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) { + word * pPage = p->pPages[p->iPage]; int nWords = Vec_SetWordNum( nSize ); - assert( nWords < (1 << p->nPageSize) ); - p->nEntries++; - if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) ) + assert( nWords + 3 < (1 << p->nPageSize) ); + // need two extra at the begining of the page and one extra in the end + if ( Vec_SetLimit(pPage) + nWords >= (1 << p->nPageSize) ) { if ( ++p->iPage == p->nPagesAlloc ) { @@ -223,12 +224,14 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) } if ( p->pPages[p->iPage] == NULL ) p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) ); - Vec_SetWriteLimit( p->pPages[p->iPage], 2 ); - p->pPages[p->iPage][1] = ~0; + pPage = p->pPages[p->iPage]; + Vec_SetWriteLimit(pPage, 2); + pPage[1] = ~0; } if ( pArray ) - memcpy( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize ); - Vec_SetIncLimit( p->pPages[p->iPage], nWords ); + memcpy( pPage + Vec_SetLimit(pPage), pArray, sizeof(int) * nSize ); + p->nEntries++; + Vec_SetIncLimit( pPage, nWords ); return Vec_SetHandCurrent(p) - nWords; } static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) |