diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 88 |
1 files changed, 84 insertions, 4 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 6e74d539..a46aa67a 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -57,6 +57,12 @@ struct Ga2_Man_t_ int nSatVars; // the number of SAT variables int nCexes; // the number of counter-examples int nObjAdded; // objs added during refinement + // hash table + int * pTable; + int nTable; + int nHashHit; + int nHashMiss; + int nHashOver; // temporaries Vec_Int_t * vLits; Vec_Int_t * vIsopMem; @@ -390,6 +396,9 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->vLits = Vec_IntAlloc( 100 ); p->vIsopMem = Vec_IntAlloc( 100 ); Cnf_ReadMsops( &p->pSopSizes, &p->pSops ); + // hash table + p->nTable = 1000003; + p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB return p; } void Ga2_ManReportMemory( Ga2_Man_t * p ) @@ -427,6 +436,9 @@ void Ga2_ManStop( Ga2_Man_t * p ) sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d.\n", + p->nHashHit, p->nHashMiss, p->nHashOver ); + if( p->pSat ) sat_solver2_delete( p->pSat ); Vec_VecFree( (Vec_Vec_t *)p->vCnfs ); Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); @@ -437,6 +449,7 @@ void Ga2_ManStop( Ga2_Man_t * p ) Vec_IntFree( p->vLits ); Vec_IntFree( p->vIsopMem ); Rnm_ManStop( p->pRnm, 1 ); + ABC_FREE( p->pTable ); ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); ABC_FREE( p->pSops ); @@ -679,6 +692,43 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In SeeAlso [] ***********************************************************************/ +static inline unsigned Saig_ManBmcHashKey( int * pArray ) +{ + static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 }; + unsigned i, Key = 0; + for ( i = 0; i < 5; i++ ) + Key += pArray[i] * s_Primes[i]; + return Key; +} +static inline int * Saig_ManBmcLookup( Ga2_Man_t * p, int * pArray ) +{ + int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable); + if ( memcmp( pTable, pArray, 20 ) ) + { + if ( pTable[0] == 0 ) + p->nHashMiss++; + else + p->nHashOver++; + memcpy( pTable, pArray, 20 ); + pTable[5] = 0; + } + else + p->nHashHit++; + assert( pTable + 5 < pTable + 6 * p->nTable ); + return pTable + 5; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) { unsigned uTruth; @@ -826,15 +876,45 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i Vec_IntWriteEntry( p->vLits, i, Lit ); } } - // perform structural hashing here!!! - // add new nodes - Lit = Ga2_ObjFindOrAddLit(p, pObj, f); if ( Vec_IntSize(p->vLits) == 5 ) + { + Lit = Ga2_ObjFindOrAddLit(p, pObj, f); Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, -1 ); + } else - Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 ); + { + int fUseHash = 0; + if ( fUseHash ) + { + int * pLookup, nSize = Vec_IntSize(p->vLits); + assert( Vec_IntSize(p->vLits) < 5 ); + assert( Vec_IntEntry(p->vLits, 0) < Vec_IntEntryLast(p->vLits) ); + assert( Ga2_ObjFindLit(p, pObj, f) == -1 ); + for ( i = Vec_IntSize(p->vLits); i < 4; i++ ) + Vec_IntPush( p->vLits, GA2_BIG_NUM ); + Vec_IntPush( p->vLits, (int)uTruth ); + assert( Vec_IntSize(p->vLits) == 5 ); + + // perform structural hashing here!!! + pLookup = Saig_ManBmcLookup( p, Vec_IntArray(p->vLits) ); + if ( *pLookup == 0 ) + { + *pLookup = Ga2_ObjFindOrAddLit(p, pObj, f); + Vec_IntShrink( p->vLits, nSize ); + Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), *pLookup, -1 ); + } + else + Ga2_ObjAddLit( p, pObj, f, *pLookup ); + + } + else + { + Lit = Ga2_ObjFindOrAddLit(p, pObj, f); + Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 ); + } + } } } } |