diff options
Diffstat (limited to 'src/opt/fxch/FxchSCHashTable.c')
-rw-r--r-- | src/opt/fxch/FxchSCHashTable.c | 401 |
1 files changed, 401 insertions, 0 deletions
diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c new file mode 100644 index 00000000..f9c3e7a2 --- /dev/null +++ b/src/opt/fxch/FxchSCHashTable.c @@ -0,0 +1,401 @@ +/**CFile**************************************************************** + + FileName [ FxchSCHashTable.c ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ Sub-cubes hash table implementation ] + + Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ] + + Affiliation [ UFRGS ] + + Date [ Ver. 1.0. Started - March 6, 2016. ] + + Revision [] + +***********************************************************************/ +#include "Fxch.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +static inline void MurmurHash3_x86_32 ( const void* key, + int len, + uint32_t seed, + void* out ) +{ + const uint8_t* data = (const uint8_t*)key; + const int nblocks = len / 4; + + uint32_t h1 = seed; + + const uint32_t c1 = 0xcc9e2d51; + const uint32_t c2 = 0x1b873593; + + //---------- + // body + + const uint32_t * blocks = (const uint32_t *)(data + nblocks*4); + + for(int i = -nblocks; i; i++) + { + uint32_t k1 = blocks[i]; + + k1 *= c1; + k1 = (k1 << 15) | (k1 >> (32 - 15)); + k1 *= c2; + + h1 ^= k1; + h1 = (h1 << 13) | (h1 >> (32 - 13)); + h1 = h1*5+0xe6546b64; + } + + //---------- + // tail + + const uint8_t * tail = (const uint8_t*)(data + nblocks*4); + + uint32_t k1 = 0; + + switch(len & 3) + { + case 3: k1 ^= tail[2] << 16; + case 2: k1 ^= tail[1] << 8; + case 1: k1 ^= tail[0]; + k1 *= c1; k1 = (k1 << 15) | (k1 >> (32 - 15)); k1 *= c2; h1 ^= k1; + }; + + //---------- + // finalization + + h1 ^= len; + + h1 ^= h1 >> 16; + h1 *= 0x85ebca6b; + h1 ^= h1 >> 13; + h1 *= 0xc2b2ae35; + h1 ^= h1 >> 16; + + *(uint32_t*)out = h1; +} + +Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, + Vec_Int_t* vCubeLinks, + int nEntries ) +{ + Fxch_SCHashTable_t* pSCHashTable = ABC_CALLOC( Fxch_SCHashTable_t, 1 ); + int nBits = Abc_Base2Log( nEntries + 1 ) + 1; + + + pSCHashTable->pFxchMan = pFxchMan; + pSCHashTable->SizeMask = (1 << nBits) - 1; + pSCHashTable->vCubeLinks = vCubeLinks; + pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 ); + + return pSCHashTable; +} + +void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* pSCHashTable ) +{ + Vec_IntFree( pSCHashTable->vCubeLinks ); + Vec_IntErase( &pSCHashTable->vSubCube0 ); + Vec_IntErase( &pSCHashTable->vSubCube1 ); + ABC_FREE( pSCHashTable->pBins ); + ABC_FREE( pSCHashTable ); +} + +static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t* pSCHashTable, + unsigned int SubCubeID ) +{ + return pSCHashTable->pBins + (SubCubeID & pSCHashTable->SizeMask); +} + +static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableEntry( Fxch_SCHashTable_t* pSCHashTable, + unsigned int iEntry ) +{ + if ( ( iEntry > 0 ) && ( iEntry < ( pSCHashTable->SizeMask + 1 ) ) ) + return pSCHashTable->pBins + iEntry; + + return NULL; +} + +static inline void Fxch_SCHashTableInsertLink( Fxch_SCHashTable_t* pSCHashTable, + unsigned int iEntry0, + unsigned int iEntry1 ) +{ + Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ), + * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ), + * pEntry0Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry0->iNext ); + + assert( pEntry0Next->iPrev == iEntry0 ); + + pEntry1->iNext = pEntry0->iNext; + pEntry0->iNext = iEntry1; + pEntry1->iPrev = iEntry0; + pEntry0Next->iPrev = iEntry1; +} + +static inline void Fxch_SCHashTableRemoveLink( Fxch_SCHashTable_t* pSCHashTable, + int iEntry0, + int iEntry1 ) +{ + Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ), + * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ), + * pEntry1Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry1->iNext ); + + assert( pEntry0->iNext == iEntry1 ); + assert( pEntry1->iPrev == iEntry0 ); + assert( pEntry1Next->iPrev == iEntry1 ); + + pEntry0->iNext = pEntry1->iNext; + pEntry1->iNext = 0; + pEntry1Next->iPrev = pEntry1->iPrev; + pEntry1->iPrev = 0; +} + +static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable, + Vec_Wec_t* vCubes, + Fxch_SubCube_t* pSCData0, + Fxch_SubCube_t* pSCData1 ) +{ + Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ), + * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube ); + + if ( !Vec_IntSize( vCube0 ) || + !Vec_IntSize( vCube1 ) || + Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) || + pSCData0->Id != pSCData1->Id ) + return 0; + + Vec_IntClear( &pSCHashTable->vSubCube0 ); + Vec_IntClear( &pSCHashTable->vSubCube1 ); + + if ( pSCData0->iLit1 == 0 && pSCData1->iLit1 == 0 && + Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Abc_LitNot( Vec_IntEntry( vCube1, pSCData1->iLit0 ) ) ) + return 0; + + if ( pSCData0->iLit1 > 0 && pSCData1->iLit1 > 0 && + ( Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) || + Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) || + Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) || + Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) ) + return 0; + + + if ( pSCData0->iLit0 > 0 ) + Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 ); + else + Vec_IntAppend( &pSCHashTable->vSubCube0, vCube0 ); + + if ( pSCData1->iLit0 > 0 ) + Vec_IntAppendSkip( &pSCHashTable->vSubCube1, vCube1, pSCData1->iLit0 ); + else + Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 ); + + + if ( pSCData0->iLit1 > 0) + Vec_IntDrop( &pSCHashTable->vSubCube0, + pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 ); + + if ( pSCData1->iLit1 > 0 ) + Vec_IntDrop( &pSCHashTable->vSubCube1, + pSCData1->iLit0 < pSCData1->iLit1 ? pSCData1->iLit1 - 1 : pSCData1->iLit1 ); + + Vec_IntDrop( &pSCHashTable->vSubCube0, 0 ); + Vec_IntDrop( &pSCHashTable->vSubCube1, 0 ); + + return Vec_IntEqual( &pSCHashTable->vSubCube0, &pSCHashTable->vSubCube1 ); +} + +int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, + Vec_Wec_t* vCubes, + unsigned int SubCubeID, + unsigned int iSubCube, + unsigned int iCube, + unsigned int iLit0, + unsigned int iLit1, + char fUpdate ) +{ + unsigned int BinID; + MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID); + + unsigned int iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube; + Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ), + * pNewEntry = Fxch_SCHashTableEntry( pSCHashTable, iNewEntry ); + + assert( pNewEntry->Used == 0 ); + + pNewEntry->SCData.Id = SubCubeID; + pNewEntry->SCData.iCube = iCube; + pNewEntry->SCData.iLit0 = iLit0; + pNewEntry->SCData.iLit1 = iLit1; + + pNewEntry->Used = 1; + pSCHashTable->nEntries++; + if ( pBin->iTable == 0 ) + { + pBin->iTable = iNewEntry; + pNewEntry->iNext = iNewEntry; + pNewEntry->iPrev = iNewEntry; + return 0; + } + + Fxch_SCHashTable_Entry_t* pEntry; + unsigned int iEntry; + char Pairs = 0, + fStart = 1; + for ( iEntry = pBin->iTable; iEntry != pBin->iTable || fStart; iEntry = pEntry->iNext, fStart = 0 ) + { + pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry ); + + if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) ) + continue; + + if ( pEntry->SCData.iLit0 == 0 ) + { + printf("[FXCH] SCC detected\n"); + continue; + } + if ( pNewEntry->SCData.iLit0 == 0 ) + { + printf("[FXCH] SCC detected\n"); + continue; + } + + int Base; + if ( pEntry->SCData.iCube < pNewEntry->SCData.iCube ) + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNewEntry->SCData ) ); + else + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNewEntry->SCData ), &( pEntry->SCData ) ); + + if ( Base < 0 ) + continue; + + int iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base ); + + if ( pSCHashTable->pFxchMan->SMode == 0 ) + { + Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube ); + Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube ); + } + + Pairs++; + } + assert( iEntry == (unsigned int)( pBin->iTable ) ); + + pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry ); + Fxch_SCHashTableInsertLink( pSCHashTable, pEntry->iPrev, iNewEntry ); + + return Pairs; +} + +int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable, + Vec_Wec_t* vCubes, + unsigned int SubCubeID, + unsigned int iSubCube, + unsigned int iCube, + unsigned int iLit0, + unsigned int iLit1, + char fUpdate ) +{ + unsigned int BinID; + MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID); + + unsigned int iEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube; + Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ), + * pEntry = Fxch_SCHashTableEntry( pSCHashTable, iEntry ); + + assert( pEntry->Used == 1 ); + assert( pEntry->SCData.iCube == iCube ); + + if ( pEntry->iNext == iEntry ) + { + assert( pEntry->iPrev == iEntry ); + pBin->iTable = 0; + pEntry->iNext = 0; + pEntry->iPrev = 0; + pEntry->Used = 0; + return 0; + } + + Fxch_SCHashTable_Entry_t* pNextEntry; + int iNextEntry, + Pairs = 0, + fStart = 1; + for ( iNextEntry = pEntry->iNext; iNextEntry != iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 ) + { + pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry ); + + if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) ) + || pEntry->SCData.iLit0 == 0 + || pNextEntry->SCData.iLit0 == 0 ) + continue; + + int Base; + if ( pNextEntry->SCData.iCube < pEntry->SCData.iCube ) + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNextEntry->SCData ), &( pEntry->SCData ) ); + else + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNextEntry->SCData ) ); + + if ( Base < 0 ) + continue; + + int iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base ); + + if ( pSCHashTable->pFxchMan->SMode == 0 ) + { + int i, + iCube0, + iCube1; + + Vec_Int_t* vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv ); + Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i ) + if ( ( iCube0 == pNextEntry->SCData.iCube && iCube1 == pEntry->SCData.iCube ) || + ( iCube0 == pEntry->SCData.iCube && iCube1 == pNextEntry->SCData.iCube ) ) + { + Vec_IntDrop( vDivCubePairs, i+1 ); + Vec_IntDrop( vDivCubePairs, i ); + } + if ( Vec_IntSize( vDivCubePairs ) == 0 ) + Vec_IntErase( vDivCubePairs ); + } + + Pairs++; + } + + if ( pBin->iTable == iEntry ) + pBin->iTable = ( pEntry->iNext != iEntry ) ? pEntry->iNext : 0; + + pEntry->Used = 0; + Fxch_SCHashTableRemoveLink( pSCHashTable, pEntry->iPrev, iEntry ); + return Pairs; +} + +unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* pHashTable ) +{ + unsigned int Memory = sizeof ( Fxch_SCHashTable_t ); + + Memory += Vec_IntMemory( pHashTable->vCubeLinks ); + Memory += sizeof( Fxch_SubCube_t ) * ( pHashTable->SizeMask + 1 ); + + return Memory; +} + +void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* pHashTable ) +{ + printf( "SubCube Hash Table at %p\n", ( void* )pHashTable ); + printf("%20s %20s\n", "nEntries", + "Memory Usage (MB)" ); + + int Memory = Fxch_SCHashTableMemory( pHashTable ); + printf("%20d %18.2f\n", pHashTable->nEntries, + ( ( double ) Memory / 1048576 ) ); +} +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END |