summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c57
-rw-r--r--src/sat/bsat/satProof.c2
-rw-r--r--src/sat/bsat/satSolver.c2
-rw-r--r--src/sat/bsat/satSolver2.c2
-rw-r--r--src/sat/bsat/satTruth.c2
-rw-r--r--src/sat/bsat/vecSet.h75
6 files changed, 44 insertions, 96 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 08087c98..04f4b6d7 100644
--- a/src/base/abci/abc.c
+++ b/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*************************************************************
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 2c172ff6..8fbac191 100644
--- a/src/sat/bsat/satProof.c
+++ b/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;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1f86f2d3..cc5156d5 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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 );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 2cfadadc..f014b6fc 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/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 );
diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c
index dc5644b3..dabb404f 100644
--- a/src/sat/bsat/satTruth.c
+++ b/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++ )
diff --git a/src/sat/bsat/vecSet.h b/src/sat/bsat/vecSet.h
index bc98aeaf..d508bf2f 100644
--- a/src/sat/bsat/vecSet.h
+++ b/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 )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 19:57:35 +0000