luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Debugging a proof error.

This commit is contained in:
Alan Mishchenko 2012-07-13 16:25:07 -07:00
parent b7b60ebdcb
commit da525b2a23
1 changed files with 9 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/misc/vec/vecSet.h
View File

@ -178,25 +178,6 @@ static inline void Vec_SetFree( Vec_Set_t * p )
ABC_FREE( p ); ABC_FREE( p );
} }
/**Function*************************************************************
Synopsis [Returns memory in bytes occupied by the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline double Vec_ReportMemory( Vec_Set_t * p )
{
double Mem = sizeof(Vec_Set_t);
Mem += p->nPagesAlloc * sizeof(void *);
Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
return Mem;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Appending entries to vector.] Synopsis [Appending entries to vector.]
@ -210,11 +191,10 @@ static inline double Vec_ReportMemory( 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 )
{ {
word * pPage = p->pPages[p->iPage];
int nWords = Vec_SetWordNum( nSize ); int nWords = Vec_SetWordNum( nSize );
assert( nWords + 3 < (1 << p->nPageSize) ); assert( nWords < (1 << p->nPageSize) );
// need two extra at the begining of the page and one extra in the end p->nEntries++;
if ( Vec_SetLimit(pPage) + nWords >= (1 << p->nPageSize) ) if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) )
{ {
if ( ++p->iPage == p->nPagesAlloc ) if ( ++p->iPage == p->nPagesAlloc )
{ {
@ -224,21 +204,19 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
} }
if ( p->pPages[p->iPage] == NULL ) if ( p->pPages[p->iPage] == NULL )
p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) ); p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) );
pPage = p->pPages[p->iPage]; Vec_SetWriteLimit( p->pPages[p->iPage], 2 );
Vec_SetWriteLimit(pPage, 2); p->pPages[p->iPage][1] = ~0;
pPage[1] = ~0;
} }
if ( pArray ) if ( pArray )
memcpy( pPage + Vec_SetLimit(pPage), pArray, sizeof(int) * nSize ); memcpy( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
p->nEntries++; Vec_SetIncLimit( p->pPages[p->iPage], nWords );
Vec_SetIncLimit( pPage, nWords );
return Vec_SetHandCurrent(p) - nWords; return Vec_SetHandCurrent(p) - nWords;
} }
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 + 3 < (1 << p->nPageSize) ); assert( nWords < (1 << p->nPageSize) );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords >= (1 << p->nPageSize) ) if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << p->nPageSize) )
Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 ); Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 );
Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
return Vec_SetHandCurrentS(p) - nWords; return Vec_SetHandCurrentS(p) - nWords;