Skip to content

A
abc
Commit f50ce3db by Alan Mishchenko
Options

Switching to a variable-page-size memory manager for clauses and proofs.

parent 92539a91
Showing with 44 additions and 96 deletions
src/base/abci/abc.c
......@@ -802,67 +802,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 );
// Rwt_Man4ExploreStart();
// Map_Var3Print();
// Map_Var4Test();
// Abc_NtkPrint256();
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
{
extern void Dar_LibStart();
Dar_LibStart();
}
{
// extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
// Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
}
{
// extern void Aig_ManRandomTest1();
// Aig_ManRandomTest1();
}
{
extern void Extra_MemTest();
// Extra_MemTest();
}
{
extern void Gia_SortTest();
// Gia_SortTest();
}
{
void For_ManFileExperiment();
// For_ManFileExperiment();
}
/*
{
int i1, i2, i3, i4, i5, i6, N, Counter = 0;
for ( N = 20; N < 40; N++ )
{
Counter = 0;
for ( i1 = 0; i1 < N; i1++ )
for ( i2 = i1+1; i2 < N; i2++ )
for ( i3 = i2; i3 < N; i3++ )
for ( i4 = i3; i4 < N; i4++ )
// for ( i5 = i4+1; i5 < N; i5++ )
// for ( i6 = i5+1; i6 < N; i6++ )
Counter++;
printf( "%d=%d ", N, Counter );
}
printf( "\n" );
}
*/
{
// extern void If_CluTest();
// If_CluTest();
// extern void Iso_QuickSortTest();
// Iso_QuickSortTest();
}
}
/**Function*************************************************************
......
src/sat/bsat/satProof.c
......@@ -534,7 +534,7 @@ void Sat_ProofCheck( sat_solver2 * s )
Proof_CleanCollected( vProof, vUsed );
// perform resolution steps
vTemp = Vec_IntAlloc( 1000 );
vResolves = Vec_SetAlloc();
vResolves = Vec_SetAlloc( 20 );
Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
{
Handle = -1;
......
src/sat/bsat/satSolver.c
......@@ -912,7 +912,7 @@ sat_solver* sat_solver_new(void)
{
sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
Vec_SetAlloc_(&s->Mem);
Vec_SetAlloc_(&s->Mem, 15);
s->hLearnts = -1;
s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
s->binary = clause_read( s, s->hBinary );
......
src/sat/bsat/satSolver2.c
......@@ -1155,7 +1155,7 @@ sat_solver2* sat_solver2_new(void)
veci_new(&s->claActs); veci_push(&s->claActs, -1);
veci_new(&s->claProofs); veci_push(&s->claProofs, -1);
if ( s->fProofLogging )
Vec_SetAlloc_( &s->Proofs );
Vec_SetAlloc_( &s->Proofs, 20 );
// prealloc clause
assert( !s->clauses.ptr );
......
src/sat/bsat/satTruth.c
......@@ -215,7 +215,7 @@ Tru_Man_t * Tru_ManAlloc( int nVars )
p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int);
p->nTableSize = 8147;
p->pTable = ABC_CALLOC( int, p->nTableSize );
p->pMem = Vec_SetAlloc();
p->pMem = Vec_SetAlloc( 16 );
// initialize truth tables
p->pZero = ABC_ALLOC( word, p->nWords );
for ( i = 0; i < nVars; i++ )
......
src/sat/bsat/vecSet.h
......@@ -35,15 +35,12 @@ ABC_NAMESPACE_HEADER_START
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define VEC_SET_PAGE 16
#define VEC_SET_MASK 0xFFFFF
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// data-structure for logging entries
// memory is allocated in 2^VEC_SET_PAGE word-sized pages
// memory is allocated in 2^p->nPageSize 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
......@@ -51,41 +48,44 @@ ABC_NAMESPACE_HEADER_START
typedef struct Vec_Set_t_ Vec_Set_t;
struct Vec_Set_t_
{
int nPageSize; // page size
unsigned uPageMask; // page mask
int nEntries; // entry count
int iPage; // current page
int iPageS; // shadow page
int nPagesAlloc; // page count allocated
word ** pPages; // page pointers
};
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
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_SetHandPage( Vec_Set_t * p, int h ) { return h >> p->nPageSize; }
static inline int Vec_SetHandShift( Vec_Set_t * p, int h ) { return h & p->uPageMask; }
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 ) { assert(Vec_SetHandPage(p, h) >= 0 && Vec_SetHandPage(p, h) <= p->iPage); assert(Vec_SetHandShift(p, h) >= 2 && Vec_SetHandShift(p, h) < (1 << p->nPageSize)); return p->pPages[Vec_SetHandPage(p, h)] + Vec_SetHandShift(p, h); }
static inline word * Vec_SetEntry( Vec_Set_t * p, int h ) { return p->pPages[Vec_SetHandPage(p, h)] + Vec_SetHandShift(p, h); }
static inline int Vec_SetEntryNum( Vec_Set_t * p ) { return p->nEntries; }
static inline void Vec_SetWriteEntryNum( Vec_Set_t * p, int i){ p->nEntries = i; }
static inline int Vec_SetLimit( word * p ) { return p[0]; }
static inline int Vec_SetLimitS( word * p ) { return p[1]; }
static inline int Vec_SetLimit( word * p ) { return p[0]; }
static inline int Vec_SetLimitS( word * p ) { return p[1]; }
static inline int Vec_SetIncLimit( word * p, int nWords ) { return p[0] += nWords; }
static inline int Vec_SetIncLimitS( word * p, int nWords ) { return p[1] += nWords; }
static inline int Vec_SetIncLimit( word * p, int nWords ) { return p[0] += nWords; }
static inline int Vec_SetIncLimitS( word * p, int nWords ) { return p[1] += nWords; }
static inline void Vec_SetWriteLimit( word * p, int nWords ) { p[0] = nWords; }
static inline void Vec_SetWriteLimitS( word * p, int nWords ) { p[1] = nWords; }
static inline void Vec_SetWriteLimit( word * p, int nWords ) { p[0] = nWords; }
static inline void Vec_SetWriteLimitS( word * p, int nWords ) { p[1] = nWords; }
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_SetHandCurrent( Vec_Set_t * p ) { return (p->iPage << p->nPageSize) + Vec_SetLimit(p->pPages[p->iPage]); }
static inline int Vec_SetHandCurrentS( Vec_Set_t * p ) { return (p->iPageS << p->nPageSize) + Vec_SetLimitS(p->pPages[p->iPageS]); }
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) * (1 << (VEC_SET_PAGE+3)); }
static inline int Vec_SetHandMemory( Vec_Set_t * p, int h ) { return Vec_SetHandPage(p, h) * (1 << (p->nPageSize+3)) + Vec_SetHandShift(p, 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) * (1 << (p->nPageSize+3)); }
// Type is the Set type
// pVec is vector of set
......@@ -111,20 +111,24 @@ static inline int Vec_SetMemoryAll( Vec_Set_t * p ) { return (p->iP
SeeAlso []
***********************************************************************/
static inline void Vec_SetAlloc_( Vec_Set_t * p )
static inline void Vec_SetAlloc_( Vec_Set_t * p, int nPageSize )
{
assert( nPageSize > 8 );
memset( p, 0, sizeof(Vec_Set_t) );
p->nPageSize = nPageSize;
p->uPageMask = (unsigned)((1 << nPageSize) - 1);
p->nPagesAlloc = 256;
p->pPages = ABC_CALLOC( word *, p->nPagesAlloc );
p->pPages[0] = ABC_ALLOC( word, (1 << VEC_SET_PAGE) );
p->pPages[0] = ABC_ALLOC( word, (1 << p->nPageSize) );
p->pPages[0][0] = ~0;
p->pPages[0][1] = ~0;
Vec_SetWriteLimit( p->pPages[0], 2 );
}
static inline Vec_Set_t * Vec_SetAlloc()
static inline Vec_Set_t * Vec_SetAlloc( int nPageSize )
{
Vec_Set_t * p;
p = ABC_CALLOC( Vec_Set_t, 1 );
Vec_SetAlloc_( p );
Vec_SetAlloc_( p, nPageSize );
return p;
}
......@@ -145,6 +149,7 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
p->iPage = 0;
p->iPageS = 0;
p->pPages[0][0] = ~0;
p->pPages[0][1] = ~0;
Vec_SetWriteLimit( p->pPages[0], 2 );
}
......@@ -186,9 +191,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 < (1 << VEC_SET_PAGE) );
assert( nWords < (1 << p->nPageSize) );
p->nEntries++;
if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << VEC_SET_PAGE) )
if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) )
{
if ( ++p->iPage == p->nPagesAlloc )
{
......@@ -197,20 +202,20 @@ 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, (1 << VEC_SET_PAGE) );
p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) );
Vec_SetWriteLimit( p->pPages[p->iPage], 2 );
Vec_SetWriteLimitS( p->pPages[p->iPage], 0 );
p->pPages[p->iPage][1] = ~0;
}
if ( pArray )
memmove( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
memcpy( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
Vec_SetIncLimit( p->pPages[p->iPage], nWords );
return Vec_SetHandCurrent(p) - nWords;
}
static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
{
int nWords = Vec_SetWordNum( nSize );
assert( nWords < (1 << VEC_SET_PAGE) );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << VEC_SET_PAGE) )
assert( nWords < (1 << p->nPageSize) );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << p->nPageSize) )
Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 );
Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
return Vec_SetHandCurrentS(p) - nWords;
......@@ -230,14 +235,14 @@ static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
static inline void Vec_SetShrink( Vec_Set_t * p, int h )
{
assert( h <= Vec_SetHandCurrent(p) );
p->iPage = Vec_SetHandPage(h);
Vec_SetWriteLimit( p->pPages[p->iPage], Vec_SetHandShift(h) );
p->iPage = Vec_SetHandPage(p, h);
Vec_SetWriteLimit( p->pPages[p->iPage], Vec_SetHandShift(p, h) );
}
static inline void Vec_SetShrinkS( Vec_Set_t * p, int h )
{
assert( h <= Vec_SetHandCurrent(p) );
p->iPageS = Vec_SetHandPage(h);
Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(h) );
p->iPageS = Vec_SetHandPage(p, h);
Vec_SetWriteLimitS( p->pPages[p->iPageS], Vec_SetHandShift(p, h) );
}
static inline void Vec_SetShrinkLimits( Vec_Set_t * p )
......
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