diff options
author | Mathias Soeken <mathias.soeken@gmail.com> | 2016-08-02 11:21:51 +0200 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@gmail.com> | 2016-08-02 11:21:51 +0200 |
commit | 160c697f32d0722c7b09e74d70df8ebe82475f62 (patch) | |
tree | caa23f569f410a75ca0447ca2cc37592a530eb7f | |
parent | 8246af894d77b52829d2470f7f5e726a52588aed (diff) | |
parent | 8bc4894ccbf295d1e1863d44880e27f30f29972c (diff) | |
download | abc-160c697f32d0722c7b09e74d70df8ebe82475f62.tar.gz abc-160c697f32d0722c7b09e74d70df8ebe82475f62.tar.bz2 abc-160c697f32d0722c7b09e74d70df8ebe82475f62.zip |
Merged alanmi/abc into default
-rw-r--r-- | src/opt/fxch/Fxch.c | 129 | ||||
-rw-r--r-- | src/opt/fxch/Fxch.h | 73 | ||||
-rw-r--r-- | src/opt/fxch/FxchDiv.c | 18 | ||||
-rw-r--r-- | src/opt/fxch/FxchMan.c | 363 | ||||
-rw-r--r-- | src/opt/fxch/FxchSCHashTable.c | 256 |
5 files changed, 551 insertions, 288 deletions
diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c index 6c3983ef..84a4c566 100644 --- a/src/opt/fxch/Fxch.c +++ b/src/opt/fxch/Fxch.c @@ -15,7 +15,6 @@ Revision [] ***********************************************************************/ - #include "Fxch.h" ABC_NAMESPACE_IMPL_START @@ -26,6 +25,128 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_CubesGruping(Fxch_Man_t* pFxchMan) +{ + Vec_Int_t* vCube; + int iCube, nOutputs, SizeOutputID; + Hsh_VecMan_t* pCubeHash; + + /* Identify the number of Outputs and create the translation table */ + pFxchMan->vTranslation = Vec_IntAlloc( 32 ); + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube ) + { + int Id = Vec_IntEntry( vCube, 0 ); + int iTranslation = Vec_IntFind( pFxchMan->vTranslation, Id ); + + if ( iTranslation == -1 ) + Vec_IntPush( pFxchMan->vTranslation, Id ); + } + nOutputs = Vec_IntSize( pFxchMan->vTranslation ); + + /* Size of the OutputID in number o ints */ + SizeOutputID = ( nOutputs >> 5 ) + ( ( nOutputs & 31 ) > 0 ); + + /* Initialize needed structures */ + pFxchMan->vOutputID = Vec_IntAlloc( 4096 ); + pFxchMan->pTempOutputID = ABC_CALLOC( int, SizeOutputID ); + pFxchMan->nSizeOutputID = SizeOutputID; + + pCubeHash = Hsh_VecManStart( 1024 ); + + /* Identify equal cubes */ + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube ) + { + int Id = Vec_IntEntry( vCube, 0 ); + int iTranslation = Vec_IntFind( pFxchMan->vTranslation, Id ); + int i, iCubeNoID, Temp, * pEntry; + Vec_IntWriteEntry( vCube, 0, 0 ); // Clear ID, Outputs will be identified by it later + + iCubeNoID = Hsh_VecManAdd( pCubeHash, vCube ); + Temp = ( 1 << ( iTranslation & 31 ) ); + if ( iCubeNoID == Vec_IntSize( pFxchMan->vOutputID ) / SizeOutputID ) + { + for ( i = 0; i < SizeOutputID; i++ ) + pFxchMan->pTempOutputID[i] = 0; + + pFxchMan->pTempOutputID[ iTranslation >> 5 ] = Temp; + Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, SizeOutputID ); + } + else + { + Vec_IntClear( vCube ); + pEntry = Vec_IntEntryP( pFxchMan->vOutputID, ( iCubeNoID * SizeOutputID ) + ( iTranslation >> 5 ) ); + *pEntry |= Temp; + } + } + + Hsh_VecManStop( pCubeHash ); + Vec_WecRemoveEmpty( pFxchMan->vCubes ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_CubesUnGruping(Fxch_Man_t* pFxchMan) +{ + int iCube; + int i, j; + Vec_Int_t* vCube; + Vec_Int_t* vNewCube; + + assert( Vec_WecSize( pFxchMan->vCubes ) == ( Vec_IntSize( pFxchMan->vOutputID ) / pFxchMan->nSizeOutputID ) ); + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube ) + { + int * pOutputID, nOnes; + if ( Vec_IntSize( vCube ) == 0 || Vec_IntEntry( vCube, 0 ) != 0 ) + continue; + + pOutputID = Vec_IntEntryP( pFxchMan->vOutputID, iCube * pFxchMan->nSizeOutputID ); + nOnes = 0; + + for ( i = 0; i < pFxchMan->nSizeOutputID; i++ ) + nOnes += Fxch_CountOnes( (unsigned int) pOutputID[i] ); + + for ( i = 0; i < pFxchMan->nSizeOutputID && nOnes; i++ ) + for ( j = 0; j < 32 && nOnes; j++ ) + if ( pOutputID[i] & ( 1 << j ) ) + { + if ( nOnes == 1 ) + Vec_IntWriteEntry( vCube, 0, Vec_IntEntry( pFxchMan->vTranslation, ( i << 5 ) | j ) ); + else + { + vNewCube = Vec_WecPushLevel( pFxchMan->vCubes ); + Vec_IntAppend( vNewCube, vCube ); + Vec_IntWriteEntry( vNewCube, 0, Vec_IntEntry( pFxchMan->vTranslation, (i << 5 ) | j ) ); + } + nOnes -= 1; + } + } + + Vec_IntFree( pFxchMan->vTranslation ); + Vec_IntFree( pFxchMan->vOutputID ); + ABC_FREE( pFxchMan->pTempOutputID ); + return; +} + +/**Function************************************************************* + Synopsis [ Performs fast extract with cube hashing on a set of covers. ] @@ -47,6 +168,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes, int i; TempTime = Abc_Clock(); + Fxch_CubesGruping( pFxchMan ); Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax ); Fxch_ManGenerateLitHashKeys( pFxchMan ); Fxch_ManComputeLevel( pFxchMan ); @@ -61,6 +183,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes, Fxch_ManPrintStats( pFxchMan ); TempTime = Abc_Clock(); + for ( i = 0; (!nMaxDivExt || i < nMaxDivExt) && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ ) { int iDiv = Vec_QuePop( pFxchMan->vDivPrio ); @@ -70,6 +193,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes, Fxch_ManUpdate( pFxchMan, iDiv ); } + pFxchMan->timeExt = Abc_Clock() - TempTime; if ( fVerbose ) @@ -80,9 +204,12 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes, Abc_PrintTime( 1, "[FXCH] +-> Extr", pFxchMan->timeExt ); } + Fxch_CubesUnGruping( pFxchMan ); Fxch_ManSCHashTablesFree( pFxchMan ); Fxch_ManFree( pFxchMan ); + Vec_WecRemoveEmpty( vCubes ); + Vec_WecSortByFirstInt( vCubes, 0 ); return 1; } diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h index 5781846c..8291e042 100644 --- a/src/opt/fxch/Fxch.h +++ b/src/opt/fxch/Fxch.h @@ -28,6 +28,9 @@ ABC_NAMESPACE_HEADER_START +typedef unsigned char uint8_t; +typedef unsigned int uint32_t; + //////////////////////////////////////////////////////////////////////// /// TYPEDEF DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -52,25 +55,22 @@ typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t; * its literals. * */ + struct Fxch_SubCube_t_ { - unsigned int Id, - iCube; - unsigned int iLit0 : 16, - iLit1 : 16; + uint32_t Id, + iCube; + uint32_t iLit0 : 16, + iLit1 : 16; }; /* Sub-cube Hash Table - * */ struct Fxch_SCHashTable_Entry_t_ { - Fxch_SubCube_t SCData; - - unsigned int iTable : 31, - Used : 1; - unsigned int iPrev, - iNext; + Fxch_SubCube_t* vSCData; + uint32_t Size : 16, + Cap : 16; }; struct Fxch_SCHashTable_t_ @@ -80,7 +80,6 @@ struct Fxch_SCHashTable_t_ Fxch_SCHashTable_Entry_t* pBins; unsigned int nEntries, SizeMask; - Vec_Int_t* vCubeLinks; /* Temporary data */ Vec_Int_t vSubCube0; @@ -91,6 +90,7 @@ struct Fxch_Man_t_ { /* user's data */ Vec_Wec_t* vCubes; + int nCubesInit; int LitCountMax; /* internal data */ @@ -107,12 +107,21 @@ struct Fxch_Man_t_ Vec_Int_t* vLevels; /* variable levels */ + // Cube Grouping + Vec_Int_t* vTranslation; + Vec_Int_t* vOutputID; + int* pTempOutputID; + int nSizeOutputID; + // temporary data to update the data-structure when a divisor is extracted - Vec_Int_t* vCubesS; /* cubes for the given single cube divisor */ - Vec_Int_t* vPairs; /* cube pairs for the given double cube divisor */ - Vec_Int_t* vCubeFree; // cube-free divisor - Vec_Int_t* vDiv; // selected divisor - Vec_Int_t* vSCC; + Vec_Int_t* vCubesS; /* cubes for the given single cube divisor */ + Vec_Int_t* vPairs; /* cube pairs for the given double cube divisor */ + Vec_Int_t* vCubeFree; // cube-free divisor + Vec_Int_t* vDiv; // selected divisor + + Vec_Int_t* vCubesToRemove; + Vec_Int_t* vCubesToUpdate; + Vec_Int_t* vSCC; /* Statistics */ abctime timeInit; /* Initialization time */ @@ -135,6 +144,15 @@ extern Vec_Wec_t* Abc_NtkFxRetrieve( Abc_Ntk_t* pNtk ); extern void Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes ); extern int Abc_NtkFxCheck( Abc_Ntk_t* pNtk ); +static inline int Fxch_CountOnes( unsigned num ) +{ + num = ( num & 0x55555555 ) + ( ( num >> 1) & 0x55555555 ); + num = ( num & 0x33333333 ) + ( ( num >> 2) & 0x33333333 ); + num = ( num & 0x0F0F0F0F ) + ( ( num >> 4) & 0x0F0F0F0F ); + num = ( num & 0x00FF00FF ) + ( ( num >> 8) & 0x00FF00FF ); + return ( num & 0x0000FFFF ) + ( num >> 16 ); +} + /*===== Fxch.c =======================================================*/ int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose ); int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int fVerbose, int fVeryVerbose ); @@ -177,26 +195,25 @@ static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan, } /*===== FxchSCHashTable.c ============================================*/ -Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeLinks, int nEntries ); +Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, int nEntries ); void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* ); 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, + uint32_t SubCubeID, + uint32_t iCube, + uint32_t iLit0, + uint32_t iLit1, char fUpdate ); + 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, + uint32_t SubCubeID, + uint32_t iCube, + uint32_t iLit0, + uint32_t iLit1, char fUpdate ); unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* ); diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c index 18c8bbfb..99c260c6 100644 --- a/src/opt/fxch/FxchDiv.c +++ b/src/opt/fxch/FxchDiv.c @@ -142,10 +142,20 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan, SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 ); SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 ); - Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) ); - Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) ); - Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) ); - Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) ); + if ( SC0_Lit0 < SC1_Lit0 ) + { + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) ); + } + else + { + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) ); + } RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree ); if ( RetValue == -1 ) diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c index 44695f91..19ce1461 100644 --- a/src/opt/fxch/FxchMan.c +++ b/src/opt/fxch/FxchMan.c @@ -15,7 +15,6 @@ Revision [] ***********************************************************************/ - #include "Fxch.h" ABC_NAMESPACE_IMPL_START @@ -25,7 +24,6 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan, unsigned int SubCubeID, - unsigned int iSubCube, unsigned int iCube, unsigned int iLit0, unsigned int iLit1, @@ -37,13 +35,13 @@ static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan, if ( fAdd ) { ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes, - SubCubeID, iSubCube, + SubCubeID, iCube, iLit0, iLit1, fUpdate ); } else { ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes, - SubCubeID, iSubCube, + SubCubeID, iCube, iLit0, iLit1, fUpdate ); } @@ -63,26 +61,38 @@ static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan, fSingleCube = 1, fBase = 0; - if ( Vec_IntSize(vCube) < 2 ) + if ( Vec_IntSize( vCube ) < 2 ) return 0; Vec_IntForEachEntryStart( vCube, Lit0, i, 1) Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) ) { + int * pOutputID, nOnes, j, z; assert( Lit0 < Lit1 ); Vec_IntClear( pFxchMan->vCubeFree ); Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit0 ), 0 ) ); Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit1 ), 1 ) ); + pOutputID = Vec_IntEntryP( pFxchMan->vOutputID, iCube * pFxchMan->nSizeOutputID ); + nOnes = 0; + + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + nOnes += Fxch_CountOnes( pOutputID[j] ); + + if ( nOnes == 0 ) + nOnes = 1; + if (fAdd) { - Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase ); + for ( z = 0; z < nOnes; z++ ) + Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase ); pFxchMan->nPairsS++; } else { - Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase ); + for ( z = 0; z < nOnes; z++ ) + Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase ); pFxchMan->nPairsS--; } } @@ -98,15 +108,13 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan, Vec_Int_t* vLitHashKeys = pFxchMan->vLitHashKeys, * vCube = Vec_WecEntry( pFxchMan->vCubes, iCube ); int SubCubeID = 0, - nHashedSC = 0, iLit0, Lit0; Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1) SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 ); - Fxch_ManSCAddRemove( pFxchMan, - SubCubeID, nHashedSC++, + Fxch_ManSCAddRemove( pFxchMan, SubCubeID, iCube, 0, 0, (char)fAdd, (char)fUpdate ); @@ -115,8 +123,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan, /* 1 Lit remove */ SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 ); - pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, - SubCubeID, nHashedSC++, + pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID, iCube, iLit0, 0, (char)fAdd, (char)fUpdate ); @@ -130,8 +137,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan, /* 2 Lit remove */ SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 ); - pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, - SubCubeID, nHashedSC++, + pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID, iCube, iLit0, iLit1, (char)fAdd, (char)fUpdate ); @@ -165,14 +171,20 @@ Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ) Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 ); pFxchMan->vCubes = vCubes; - pFxchMan->pDivHash = Hsh_VecManStart( 1000 ); - pFxchMan->vDivWeights = Vec_FltAlloc( 1000 ); - pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 ); - pFxchMan->vCubeFree = Vec_IntAlloc( 100 ); - pFxchMan->vDiv = Vec_IntAlloc( 100 ); + pFxchMan->nCubesInit = Vec_WecSize( vCubes ); + + pFxchMan->pDivHash = Hsh_VecManStart( 1024 ); + pFxchMan->vDivWeights = Vec_FltAlloc( 1024 ); + pFxchMan->vDivCubePairs = Vec_WecAlloc( 1024 ); + + pFxchMan->vCubeFree = Vec_IntAlloc( 4 ); + pFxchMan->vDiv = Vec_IntAlloc( 4 ); + + pFxchMan->vCubesS = Vec_IntAlloc( 128 ); + pFxchMan->vPairs = Vec_IntAlloc( 128 ); + pFxchMan->vCubesToUpdate = Vec_IntAlloc( 64 ); + pFxchMan->vCubesToRemove = Vec_IntAlloc( 64 ); pFxchMan->vSCC = Vec_IntAlloc( 64 ); - pFxchMan->vCubesS = Vec_IntAlloc( 100 ); - pFxchMan->vPairs = Vec_IntAlloc( 100 ); return pFxchMan; } @@ -187,11 +199,16 @@ void Fxch_ManFree( Fxch_Man_t* pFxchMan ) Vec_QueFree( pFxchMan->vDivPrio ); Vec_WecFree( pFxchMan->vDivCubePairs ); Vec_IntFree( pFxchMan->vLevels ); + Vec_IntFree( pFxchMan->vCubeFree ); Vec_IntFree( pFxchMan->vDiv ); - Vec_IntFree( pFxchMan->vSCC ); + Vec_IntFree( pFxchMan->vCubesS ); Vec_IntFree( pFxchMan->vPairs ); + Vec_IntFree( pFxchMan->vCubesToUpdate ); + Vec_IntFree( pFxchMan->vCubesToRemove ); + Vec_IntFree( pFxchMan->vSCC ); + ABC_FREE( pFxchMan ); } @@ -248,22 +265,19 @@ void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan ) void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan ) { Vec_Wec_t* vCubes = pFxchMan->vCubes; - Vec_Int_t* vCube, - * vCubeLinks; + Vec_Int_t* vCube; int iCube, nTotalHashed = 0; - vCubeLinks = Vec_IntAlloc( Vec_WecSize( vCubes ) + 1 ); Vec_WecForEachLevel( vCubes, vCube, iCube ) { int nLits = Vec_IntSize( vCube ) - 1, nSubCubes = nLits <= 2? nLits + 1: ( nLits * nLits + nLits ) / 2; - Vec_IntPush( vCubeLinks, ( nTotalHashed + 1 ) ); nTotalHashed += nSubCubes + 1; } - pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, vCubeLinks, nTotalHashed ); + pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, nTotalHashed ); } void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan ) @@ -364,56 +378,135 @@ static inline void Fxch_ManExtractDivFromCube( Fxch_Man_t* pFxchMan, Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 ); pFxchMan->nLits--; } } /* Extract divisor from cube pairs */ -static inline int Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan, +static inline void Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan, const int iVarNew ) { /* For each pair (Ci, Cj) */ - int k = 0, - iCube0, iCube1, i; + int iCube0, iCube1, i; - Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ), - * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 ); Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) { - int RetValue, + int j, Lit, + RetValue, fCompl = 0; + int * pOutputID0, * pOutputID1; - Vec_Int_t* vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ), - * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ); + Vec_Int_t* vCube = NULL, + * vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ), + * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ), + * vCube0Copy = Vec_IntDup( vCube0 ), + * vCube1Copy = Vec_IntDup( vCube1 ); - RetValue = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl ); + RetValue = Fxch_DivRemoveLits( vCube0Copy, vCube1Copy, pFxchMan->vDiv, &fCompl ); assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) ); pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2; - /* Remove second cube */ - Vec_IntClear( vCube1 ); - Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + /* Identify type of Extraction */ + pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID ); + pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID ); + RetValue = 1; + for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ ) + RetValue = ( pOutputID0[j] == pOutputID1[j] ); + + /* Exact Extractraion */ + if ( RetValue ) + { + Vec_IntClear( vCube0 ); + Vec_IntAppend( vCube0, vCube0Copy ); + vCube = vCube0; + + Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 ); + Vec_IntClear( vCube1 ); + + /* Update Lit -> Cube mapping */ + Vec_IntForEachEntry( pFxchMan->vDiv, Lit, j ) + { + Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit ) ), + Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit ) ) ), + Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + } + + } + /* Unexact Extraction */ + else + { + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + pFxchMan->pTempOutputID[j] = ( pOutputID0[j] & pOutputID1[j] ); + + /* Create new cube */ + vCube = Vec_WecPushLevel( pFxchMan->vCubes ); + Vec_IntAppend( vCube, vCube0Copy ); + Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID ); + Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube ) ); + + /* Update Lit -> Cube mapping */ + Vec_IntForEachEntryStart( vCube, Lit, j, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube ) ); + + /*********************************************************/ + RetValue = 0; + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + { + pFxchMan->pTempOutputID[j] = pOutputID0[j]; + RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) ); + pOutputID0[j] &= ~( pOutputID1[j] ); + } + + if ( RetValue != 0 ) + Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 ); + else + Vec_IntClear( vCube0 ); + + /*********************************************************/ + RetValue = 0; + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + { + RetValue |= ( pOutputID1[j] & ~( pFxchMan->pTempOutputID[j] ) ); + pOutputID1[j] &= ~( pFxchMan->pTempOutputID[j] ); + } + + if ( RetValue != 0 ) + Vec_IntPush( pFxchMan->vCubesToUpdate, iCube1 ); + else + Vec_IntClear( vCube1 ); + + } + Vec_IntFree( vCube0Copy ); + Vec_IntFree( vCube1Copy ); if ( iVarNew ) { + Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ), + * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 ); + + assert( vCube ); if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl ) { - Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) ); - Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 1 ) ); + Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube ) ); + Vec_IntSort( vLitN, 0 ); } else { - Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); - Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 0 ) ); + Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube ) ); + Vec_IntSort( vLitP, 0 ); } } } - return k; + return; } static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, @@ -421,7 +514,8 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, int Lit1 ) { int Level, - iVarNew; + iVarNew, + j; Vec_Int_t* vCube0, * vCube1; @@ -429,6 +523,10 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, iVarNew = pFxchMan->nVars; pFxchMan->nVars++; + /* Clear temporary outputID vector */ + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + pFxchMan->pTempOutputID[j] = 0; + /* Create new Lit hash keys */ Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF ); Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF ); @@ -436,6 +534,7 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, /* Create new Cube */ vCube0 = Vec_WecPushLevel( pFxchMan->vCubes ); Vec_IntPush( vCube0, iVarNew ); + Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID ); if ( Vec_IntSize( pFxchMan->vDiv ) == 2 ) { @@ -448,12 +547,27 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, } else { + int i; + int Lit; + vCube1 = Vec_WecPushLevel( pFxchMan->vCubes ); - vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 ); Vec_IntPush( vCube1, iVarNew ); + Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID ); + + vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 ); Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 ); Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ), Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) ); + + Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) ); + + /* Update Lit -> Cube mapping */ + Vec_IntForEachEntryStart( vCube0, Lit, i, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + + Vec_IntForEachEntryStart( vCube1, Lit, i, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) ); } assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew ); Vec_IntPush( pFxchMan->vLevels, Level ); @@ -470,7 +584,7 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, int iDiv ) { - int i, k, iCube0, iCube1, + int i, iCube0, iCube1, Lit0 = -1, Lit1 = -1, iVarNew; @@ -519,89 +633,128 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, /* subtract cost of single-cube divisors */ Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ - - Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1), /* remove (fAdd = 0) - fUpdate = 1 */ - Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ + { + Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); - /* subtract cost of double-cube divisors */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); + } Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + { + Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); - k = 0; + if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); + } + + Vec_IntClear( pFxchMan->vCubesToUpdate ); if ( Fxch_DivIsNotConstant1( pFxchMan->vDiv ) ) { iVarNew = Fxch_ManCreateCube( pFxchMan, Lit0, Lit1 ); Fxch_ManExtractDivFromCube( pFxchMan, Lit0, Lit1, iVarNew ); - k = Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew ); + Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew ); } else - k = Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 ); + Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 ); - assert( k == Vec_IntSize( pFxchMan->vPairs ) / 2 ); - Vec_IntShrink( pFxchMan->vPairs, k ); - - /* Add cost of single-cube divisors */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ - - Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + assert( Vec_IntSize( pFxchMan->vCubesToUpdate ) ); - /* Add cost of double-cube divisors */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + /* Add cost */ + Vec_IntForEachEntry( pFxchMan->vCubesToUpdate, iCube0, i ) + { + Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); - Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); + } /* Deal with SCC */ - if ( Vec_IntSize( pFxchMan->vSCC ) ) + if ( Vec_IntSize( pFxchMan->vSCC ) && pFxchMan->nExtDivs < 17 ) { - Vec_IntUniqify( pFxchMan->vSCC ); - Vec_IntForEachEntry( pFxchMan->vSCC, iCube0, i ) - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + Vec_IntUniqifyPairs( pFxchMan->vSCC ); + assert( Vec_IntSize( pFxchMan->vSCC ) % 2 == 0 ); + + Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i ) + { + int j, RetValue = 1; + int* pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID ); + int* pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID ); + vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 ); + vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 ); + + if ( !Vec_WecIntHasMark( vCube0 ) ) { - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ - vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ), - Vec_IntClear( vCube0 ); + Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1 ); + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); + Vec_WecIntSetMark( vCube0 ); } - Vec_IntClear( pFxchMan->vSCC ); - } + if ( !Vec_WecIntHasMark( vCube1 ) ) + { + Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1 ); + Fxch_ManDivDoubleCube( pFxchMan, iCube1, 0, 1 ); + Vec_WecIntSetMark( vCube1 ); + } + if ( Vec_IntSize( vCube0 ) == Vec_IntSize( vCube1 ) ) + { + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + { + pOutputID1[j] |= pOutputID0[j]; + pOutputID0[j] = 0; + } + Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) ); + Vec_WecIntXorMark( vCube0 ); + continue; + } - /* If it's a double-cube devisor add its cost */ - if ( Vec_IntSize( pFxchMan->vDiv ) > 2 ) - { - iCube0 = Vec_WecSize( pFxchMan->vCubes ) - 2; - iCube1 = Vec_WecSize( pFxchMan->vCubes ) - 1; + for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ ) + RetValue = ( pOutputID0[j] == pOutputID1[j] ); - Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ - Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + if ( RetValue ) + { + Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) ); + Vec_WecIntXorMark( vCube0 ); + } + else + { + RetValue = 0; + for ( j = 0; j < pFxchMan->nSizeOutputID; j++ ) + { + RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) ); + pOutputID0[j] &= ~( pOutputID1[j] ); + } + + if ( RetValue == 0 ) + { + Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) ); + Vec_WecIntXorMark( vCube0 ); + } + } + } - vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 ); - Vec_IntForEachEntryStart( vCube0, Lit0, i, 1 ) - Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i ) + { + vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 ); + vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 ); - vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 ); - Vec_IntForEachEntryStart( vCube1, Lit0, i, 1 ) - Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) ); - } + if ( Vec_WecIntHasMark( vCube0 ) ) + { + Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); + Vec_WecIntXorMark( vCube0 ); + } - /* remove these cubes from the lit array of the divisor */ - Vec_IntForEachEntry( pFxchMan->vDiv, Lit0, i ) - { - Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit0 ) ), pFxchMan->vPairs ); - Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit0 ) ) ), pFxchMan->vPairs ); + if ( Vec_WecIntHasMark( vCube1 ) ) + { + Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 ); + Fxch_ManDivDoubleCube( pFxchMan, iCube1, 1, 1 ); + Vec_WecIntXorMark( vCube1 ); + } + } + + Vec_IntClear( pFxchMan->vSCC ); } pFxchMan->nExtDivs++; diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c index a37009eb..0796a28c 100644 --- a/src/opt/fxch/FxchSCHashTable.c +++ b/src/opt/fxch/FxchSCHashTable.c @@ -19,11 +19,6 @@ ABC_NAMESPACE_IMPL_START -//#ifdef _WIN32 -typedef unsigned int uint32_t; -typedef unsigned char uint8_t; -//#endif - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -92,7 +87,6 @@ static inline void MurmurHash3_x86_32 ( const void* key, } 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 ); @@ -101,7 +95,6 @@ Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, pSCHashTable->pFxchMan = pFxchMan; pSCHashTable->SizeMask = (1 << nBits) - 1; - pSCHashTable->vCubeLinks = vCubeLinks; pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 ); return pSCHashTable; @@ -109,7 +102,6 @@ Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* pSCHashTable ) { - Vec_IntFree( pSCHashTable->vCubeLinks ); Vec_IntErase( &pSCHashTable->vSubCube0 ); Vec_IntErase( &pSCHashTable->vSubCube1 ); ABC_FREE( pSCHashTable->pBins ); @@ -122,49 +114,6 @@ static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t* 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( (int)pEntry0->iNext == iEntry1 ); - assert( (int)pEntry1->iPrev == iEntry0 ); - assert( (int)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, @@ -173,12 +122,22 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ), * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube ); + int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData0->iCube * pSCHashTable->pFxchMan->nSizeOutputID ), + * pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData1->iCube * pSCHashTable->pFxchMan->nSizeOutputID ); + int i, Result = 0; + if ( !Vec_IntSize( vCube0 ) || !Vec_IntSize( vCube1 ) || Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) || pSCData0->Id != pSCData1->Id ) return 0; + for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID && Result == 0; i++ ) + Result = ( pOutputID0[i] & pOutputID1[i] ); + + if ( Result == 0 ) + return 0; + Vec_IntClear( &pSCHashTable->vSubCube0 ); Vec_IntClear( &pSCHashTable->vSubCube1 ); @@ -189,7 +148,6 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) ) return 0; - if ( pSCData0->iLit0 > 0 ) Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 ); else @@ -200,7 +158,6 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable else Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 ); - if ( pSCData0->iLit1 > 0) Vec_IntDrop( &pSCHashTable->vSubCube0, pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 ); @@ -209,167 +166,169 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable 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, + uint32_t SubCubeID, + uint32_t iCube, + uint32_t iLit0, + uint32_t iLit1, char fUpdate ) { - unsigned int BinID; - unsigned int iNewEntry; - Fxch_SCHashTable_Entry_t* pBin,* pNewEntry; - - Fxch_SCHashTable_Entry_t* pEntry; - unsigned int iEntry; - char Pairs = 0, - fStart = 1; + int iNewEntry; + int Pairs = 0; + uint32_t BinID; + Fxch_SCHashTable_Entry_t* pBin; + Fxch_SubCube_t* pNewEntry; + int iEntry; MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID); - - iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube; 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; + + if ( pBin->vSCData == NULL ) + { + pBin->vSCData = ABC_CALLOC( Fxch_SubCube_t, 16 ); + pBin->Size = 0; + pBin->Cap = 16; + } + else if ( pBin->Size == pBin->Cap ) + { + pBin->Cap = 2 * pBin->Size; + pBin->vSCData = ABC_REALLOC( Fxch_SubCube_t, pBin->vSCData, pBin->Cap ); + } - pNewEntry->Used = 1; + iNewEntry = pBin->Size++; + pBin->vSCData[iNewEntry].Id = SubCubeID; + pBin->vSCData[iNewEntry].iCube = iCube; + pBin->vSCData[iNewEntry].iLit0 = iLit0; + pBin->vSCData[iNewEntry].iLit1 = iLit1; pSCHashTable->nEntries++; - if ( pBin->iTable == 0 ) - { - pBin->iTable = iNewEntry; - pNewEntry->iNext = iNewEntry; - pNewEntry->iPrev = iNewEntry; + + if ( pBin->Size == 1 ) return 0; - } - for ( iEntry = pBin->iTable; iEntry != pBin->iTable || fStart; iEntry = pEntry->iNext, fStart = 0 ) + pNewEntry = &( pBin->vSCData[iNewEntry] ); + for ( iEntry = 0; iEntry < (int)pBin->Size - 1; iEntry++ ) { + Fxch_SubCube_t* pEntry = &( pBin->vSCData[iEntry] ); + int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID ); + int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNewEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID ); + int Result = 0; int Base; - int iNewDiv; + int iNewDiv, i, z; - pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry ); - - if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) ) + if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNewEntry ) ) continue; - if ( ( pEntry->SCData.iLit0 == 0 ) || ( pNewEntry->SCData.iLit0 == 0 ) ) + if ( ( pEntry->iLit0 == 0 ) || ( pNewEntry->iLit0 == 0 ) ) { - Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube ), - * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube ); + Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->iCube ), + * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pNewEntry->iCube ); if ( Vec_IntSize( vCube0 ) > Vec_IntSize( vCube1 ) ) - Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->SCData.iCube ); + { + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube ); + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube ); + } else - Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->SCData.iCube ); + { + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube ); + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube ); + } continue; } - 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 ) ); + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pEntry, pNewEntry ); if ( Base < 0 ) continue; - iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base ); + for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ ) + Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] ); - Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube ); - Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube ); + for ( z = 0; z < Result; z++ ) + iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base ); + + Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->iCube ); + Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->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, + uint32_t SubCubeID, + uint32_t iCube, + uint32_t iLit0, + uint32_t iLit1, char fUpdate ) { - unsigned int BinID; - unsigned int iEntry; - Fxch_SCHashTable_Entry_t* pBin,* pEntry; - Fxch_SCHashTable_Entry_t* pNextEntry; - int iNextEntry, - Pairs = 0, - fStart = 1; + int iEntry; + int Pairs = 0; + uint32_t BinID; + Fxch_SCHashTable_Entry_t* pBin; + Fxch_SubCube_t* pEntry; + int idx; MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID); - iEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube; pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ); - pEntry = Fxch_SCHashTableEntry( pSCHashTable, iEntry ); - - assert( pEntry->Used == 1 ); - assert( pEntry->SCData.iCube == iCube ); - if ( pEntry->iNext == iEntry ) + if ( pBin->Size == 1 ) { - assert( pEntry->iPrev == iEntry ); - pBin->iTable = 0; - pEntry->iNext = 0; - pEntry->iPrev = 0; - pEntry->Used = 0; + pBin->Size = 0; return 0; } - for ( iNextEntry = (int)pEntry->iNext; iNextEntry != (int)iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 ) + for ( iEntry = 0; iEntry < (int)pBin->Size; iEntry++ ) + if ( pBin->vSCData[iEntry].iCube == iCube ) + break; + + assert( ( iEntry != pBin->Size ) && ( pBin->Size != 0 ) ); + + pEntry = &( pBin->vSCData[iEntry] ); + for ( idx = 0; idx < (int)pBin->Size; idx++ ) + if ( idx != iEntry ) { int Base, iDiv; - int i, + int i, z, iCube0, iCube1; + Fxch_SubCube_t* pNextEntry = &( pBin->vSCData[idx] ); Vec_Int_t* vDivCubePairs; + int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID ); + int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNextEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID ); + int Result = 0; - pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry ); - - if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) ) - || pEntry->SCData.iLit0 == 0 - || pNextEntry->SCData.iLit0 == 0 ) + if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNextEntry ) + || pEntry->iLit0 == 0 + || pNextEntry->iLit0 == 0 ) continue; - 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 ) ); + Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pNextEntry, pEntry ); if ( Base < 0 ) continue; - iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base ); + for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ ) + Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] ); + + for ( z = 0; z < Result; z++ ) + iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base ); vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv ); Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i ) - if ( ( iCube0 == (int)pNextEntry->SCData.iCube && iCube1 == (int)pEntry->SCData.iCube ) || - ( iCube0 == (int)pEntry->SCData.iCube && iCube1 == (int)pNextEntry->SCData.iCube ) ) + if ( ( iCube0 == (int)pNextEntry->iCube && iCube1 == (int)pEntry->iCube ) || + ( iCube0 == (int)pEntry->iCube && iCube1 == (int)pNextEntry->iCube ) ) { Vec_IntDrop( vDivCubePairs, i+1 ); Vec_IntDrop( vDivCubePairs, i ); @@ -379,12 +338,10 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable, Pairs++; } + + memmove(pBin->vSCData + iEntry, pBin->vSCData + iEntry + 1, (pBin->Size - iEntry - 1) * sizeof(*pBin->vSCData)); + pBin->Size -= 1; - if ( pBin->iTable == iEntry ) - pBin->iTable = ( pEntry->iNext != iEntry ) ? pEntry->iNext : 0; - - pEntry->Used = 0; - Fxch_SCHashTableRemoveLink( pSCHashTable, pEntry->iPrev, iEntry ); return Pairs; } @@ -392,7 +349,6 @@ 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; |