diff options
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/fxch/Fxch.c | 140 | ||||
-rw-r--r-- | src/opt/fxch/Fxch.h | 218 | ||||
-rw-r--r-- | src/opt/fxch/FxchDiv.c | 582 | ||||
-rw-r--r-- | src/opt/fxch/FxchMan.c | 600 | ||||
-rw-r--r-- | src/opt/fxch/FxchSCHashTable.c | 401 | ||||
-rw-r--r-- | src/opt/fxch/module.make | 4 |
6 files changed, 1945 insertions, 0 deletions
diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c new file mode 100644 index 00000000..9d674720 --- /dev/null +++ b/src/opt/fxch/Fxch.c @@ -0,0 +1,140 @@ +/**CFile**************************************************************** + + FileName [ Fxch.c ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ The entrance into the fast extract module. ] + + 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 /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [ Performs fast extract with cube hashing on a set + of covers. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_FastExtract( Vec_Wec_t* vCubes, + int ObjIdMax, + int nMaxDivExt, + int SMode, + int fVerbose, + int fVeryVerbose ) +{ + abctime TempTime; + Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, SMode ); + + TempTime = Abc_Clock(); + Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax ); + Fxch_ManGenerateLitHashKeys( pFxchMan ); + Fxch_ManComputeLevel( pFxchMan ); + Fxch_ManSCHashTablesInit( pFxchMan ); + Fxch_ManDivCreate( pFxchMan ); + pFxchMan->timeInit = Abc_Clock() - TempTime; + + if ( fVeryVerbose ) + Fxch_ManPrintDivs( pFxchMan ); + + if ( fVerbose ) + Fxch_ManPrintStats( pFxchMan ); + + TempTime = Abc_Clock(); + for ( int i = 0; i < nMaxDivExt && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ ) + { + int iDiv = Vec_QuePop( pFxchMan->vDivPrio ); + + if ( fVeryVerbose ) + Fxch_DivPrint( pFxchMan, iDiv ); + + Fxch_ManUpdate( pFxchMan, iDiv ); + } + pFxchMan->timeExt = Abc_Clock() - TempTime; + + if ( fVerbose ) + { + Fxch_ManPrintStats( pFxchMan ); + Abc_PrintTime( 1, "\n[FXCH] Elapsed Time", pFxchMan->timeInit + pFxchMan->timeExt ); + Abc_PrintTime( 1, "[FXCH] +-> Init", pFxchMan->timeInit ); + Abc_PrintTime( 1, "[FXCH] +-> Extr", pFxchMan->timeExt ); + } + + Fxch_ManSCHashTablesFree( pFxchMan ); + Fxch_ManFree( pFxchMan ); + Vec_WecRemoveEmpty( vCubes ); + + return 1; +} + +/**Function************************************************************* + + Synopsis [ Retrives the necessary information for the fast extract + with cube hashing. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, + int nMaxDivExt, + int SMode, + int fVerbose, + int fVeryVerbose ) +{ + Vec_Wec_t* vCubes; + + assert( Abc_NtkIsSopLogic( pNtk ) ); + + if ( !Abc_NtkFxCheck( pNtk ) ) + { + printf( "Abc_NtkFxchPerform(): Nodes have duplicated fanins. FXCH is not performed.\n" ); + return 0; + } + + vCubes = Abc_NtkFxRetrieve( pNtk ); + if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, SMode, fVerbose, fVeryVerbose ) > 0 ) + { + Abc_NtkFxInsert( pNtk, vCubes ); + Vec_WecFree( vCubes ); + + if ( !Abc_NtkCheck( pNtk ) ) + printf( "Abc_NtkFxchPerform(): The network check has failed.\n" ); + + return 1; + } + else + printf( "Warning: The network has not been changed by \"fxch\".\n" ); + + Vec_WecFree( vCubes ); + + return 0; +} +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h new file mode 100644 index 00000000..be229b98 --- /dev/null +++ b/src/opt/fxch/Fxch.h @@ -0,0 +1,218 @@ +/**CFile**************************************************************** + + FileName [ Fxch.h ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ External declarations of fast extract with cube hashing. ] + + Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ] + + Affiliation [ UFRGS ] + + Date [ Ver. 1.0. Started - March 6, 2016. ] + + Revision [] + +***********************************************************************/ + +#ifndef ABC__opt__fxch__fxch_h +#define ABC__opt__fxch__fxch_h + +#include "base/abc/abc.h" + +#include "misc/vec/vecHsh.h" +#include "misc/vec/vecQue.h" +#include "misc/vec/vecVec.h" +#include "misc/vec/vecWec.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// TYPEDEF DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct Fxch_Man_t_ Fxch_Man_t; +typedef struct Fxch_SubCube_t_ Fxch_SubCube_t; +typedef struct Fxch_SCHashTable_t_ Fxch_SCHashTable_t; +typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t; +//////////////////////////////////////////////////////////////////////// +/// STRUCTURES DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +/* Sub-Cube Structure + * + * In the context of this program, a sub-cube is a cube derived from + * another cube by removing one or two literals. Since a cube is represented + * as a vector of literals, one might think that a sub-cube would also be + * represented in the same way. However, in order to same memory, we only + * store a sub-cube identifier and the data necessary to generate the sub-cube: + * - The index number of the orignal cube in the cover. (iCube) + * - Identifiers of which literal(s) was(were) removed. (iLit0, iLit1) + * + * The sub-cube identifier is generated by adding the unique identifiers of + * its literals. + * + */ +struct Fxch_SubCube_t_ +{ + unsigned int Id, + iCube; + unsigned int 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; +}; + +struct Fxch_SCHashTable_t_ +{ + Fxch_Man_t* pFxchMan; + /* Internal data */ + Fxch_SCHashTable_Entry_t* pBins; + unsigned int nEntries, + SizeMask; + Vec_Int_t* vCubeLinks; + + /* Temporary data */ + Vec_Int_t vSubCube0; + Vec_Int_t vSubCube1; +}; + +struct Fxch_Man_t_ +{ + /* user's data */ + Vec_Wec_t* vCubes; + int LitCountMax; + + /* internal data */ + Fxch_SCHashTable_t* pSCHashTable; + + Vec_Wec_t* vLits; /* lit -> cube */ + Vec_Int_t* vLitCount; /* literal counts (currently not used) */ + Vec_Int_t* vLitHashKeys; /* Literal hash keys used to generate subcube hash */ + + Hsh_VecMan_t* pDivHash; + Vec_Flt_t* vDivWeights; /* divisor weights */ + Vec_Que_t* vDivPrio; /* priority queue for divisors by weight */ + Vec_Wec_t* vDivCubePairs; /* cube pairs for each div */ + + Vec_Int_t* vLevels; /* variable levels */ + + // 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 + + /* Config */ + char SMode; /* Saving Memory mode */ + + /* Statistics */ + abctime timeInit; /* Initialization time */ + abctime timeExt; /* Extraction time */ + int nVars; // original problem variables + int nLits; // the number of SOP literals + int nPairsS; // number of lit pairs + int nPairsD; // number of cube pairs + int nExtDivs; /* Number of extracted divisor */ +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +/* The following functions are from abcFx.c + * They are use in order to retrive SOP information for fast_extract + * Since I want an implementation that change only the core part of + * the algorithm I'm using this */ +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 ); + +/*===== Fxch.c =======================================================*/ +int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose ); +int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose ); + +/*===== FxchDiv.c ====================================================================================================*/ +int Fxch_DivCreate( Fxch_Man_t* pFxchMan, Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 ); +int Fxch_DivAdd( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase ); +int Fxch_DivRemove( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase ); +void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube1 ); +int Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl ); +void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv ); + +/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ +void Fxch_DivFindPivots( Vec_Int_t* vDiv, int* pLit0, int* pLit1 ); +int Fxch_DivFind( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vCubeFree ); +void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubes_Lit0, Vec_Int_t* vCubes_Lit1 ); + +/*===== FxchMan.c ====================================================================================================*/ +Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, char SMode ); +void Fxch_ManFree( Fxch_Man_t* pFxchMan ); +void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars ); +void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan ); +void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan ); +void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan ); +void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan ); +int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeFree ); +int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan, Vec_Int_t* vCube ); +void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan ); +void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, int iDiv ); +void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan ); +void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan ); + +static inline Vec_Int_t* Fxch_ManGetCube( Fxch_Man_t* pFxchMan, + int iCube ) +{ + return Vec_WecEntry( pFxchMan->vCubes, iCube ); +} + +static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan, + int iCube, + int iLit ) +{ + return Vec_IntEntry( Vec_WecEntry(pFxchMan->vCubes, iCube), iLit ); +} + +/*===== FxchSCHashTable.c ============================================*/ +Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeLinks, 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, + 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, + char fUpdate ); + +unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* ); +void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* ); + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c new file mode 100644 index 00000000..072198ef --- /dev/null +++ b/src/opt/fxch/FxchDiv.c @@ -0,0 +1,582 @@ +/**CFile**************************************************************************************************************** + + FileName [ FxchDiv.c ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ Divisor handling functions ] + + 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 int Fxch_DivNormalize( Vec_Int_t* vCubeFree ) +{ + int * L = Vec_IntArray(vCubeFree); + int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1; + assert( Vec_IntSize(vCubeFree) == 4 ); + if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars + { + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]); + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) ) + { + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) ); + LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]); + } + else + { + assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ); + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) ); + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]); + } + } + else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]); + if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]); + else + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]); + } + else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) ) + return -1; + LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]); + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]); + else + LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]); + } + else + return -1; + assert( LitA0 == Abc_LitNot(LitB0) ); + if ( Abc_LitIsCompl(LitA0) ) + { + ABC_SWAP( int, LitA0, LitB0 ); + ABC_SWAP( int, LitA1, LitB1 ); + } + assert( !Abc_LitIsCompl(LitA0) ); + if ( Abc_LitIsCompl(LitA1) ) + { + LitA1 = Abc_LitNot(LitA1); + LitB1 = Abc_LitNot(LitB1); + RetValue = 1; + } + assert( !Abc_LitIsCompl(LitA1) ); + // arrange literals in such as a way that + // - the first two literals are control literals from different cubes + // - the third literal is non-complented data input + // - the forth literal is possibly complemented data input + L[0] = Abc_Var2Lit( LitA0, 0 ); + L[1] = Abc_Var2Lit( LitB0, 1 ); + L[2] = Abc_Var2Lit( LitA1, 0 ); + L[3] = Abc_Var2Lit( LitB1, 1 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [ Creates a Divisor. ] + + Description [ This functions receive as input two sub-cubes and creates + a divisor using their information. The divisor is stored + in vCubeFree vector of the pFxchMan structure. + + It returns the base value, which is the number of elements + that the cubes pair used to generate the devisor have in + common. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivCreate( Fxch_Man_t* pFxchMan, + Fxch_SubCube_t* pSubCube0, + Fxch_SubCube_t* pSubCube1 ) +{ + int Base = 0; + + Vec_IntClear( pFxchMan->vCubeFree ); + + int SC0_Lit0, + SC0_Lit1, + SC1_Lit0, + SC1_Lit1; + + SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 ); + SC0_Lit1 = 0; + SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 ); + SC1_Lit1 = 0; + + if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 ) + { + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + } + else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 ) + { + 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 ) ); + + int RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree ); + if ( RetValue == -1 ) + return -1; + } + else + { + if ( pSubCube0->iLit1 > 0 ) + { + SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 ); + + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 ); + else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + } + else + { + SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 ); + + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 ); + else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + } + } + + if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 ) + return -1; + + if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 ) + { + Vec_IntSort( pFxchMan->vCubeFree, 0 ); + + Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) ); + Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) ); + } + + int Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) ), + Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) ); + if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 ) + { + Base = Abc_MinInt( Cube0Size, Cube1Size ) + -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */ + } + else + return -1; + + return Base; +} + +/**Function************************************************************* + + Synopsis [ Add a divisor to the divisors hash table. ] + + Description [ This functions will try to add the divisor store in + vCubeFree to the divisor hash table. If the divisor + is already present in the hash table it will just + increment its weight, otherwise it will add the divisor + and asign an initial weight. ] + + SideEffects [ If the fUpdate option is set, the function will also + update the divisor priority queue. ] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivAdd( Fxch_Man_t* pFxchMan, + int fUpdate, + int fSingleCube, + int fBase ) +{ + int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree ); + + /* Verify if the divisor already exist */ + if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) ) + { + if ( pFxchMan->SMode == 0 ) + Vec_WecPushLevel( pFxchMan->vDivCubePairs ); + + /* Assign initial weight */ + if ( fSingleCube ) + { + Vec_FltPush( pFxchMan->vDivWeights, + -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9 + -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) ); + } + else + { + Vec_FltPush( pFxchMan->vDivWeights, + -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9 + -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) ); + } + + } + + /* Increment weight */ + if ( fSingleCube ) + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 ); + else + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ); + + assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) ); + + if ( fUpdate ) + if ( pFxchMan->vDivPrio ) + { + if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) ) + Vec_QueUpdate( pFxchMan->vDivPrio, iDiv ); + else + Vec_QuePush( pFxchMan->vDivPrio, iDiv ); + } + + return iDiv; +} + +/**Function************************************************************* + + Synopsis [ Removes a divisor to the divisors hash table. ] + + Description [ This function don't effectively removes a divisor from + the hash table (the hash table implementation don't + support such operation). It only assures its existence + and decrement its weight. ] + + SideEffects [ If the fUpdate option is set, the function will also + update the divisor priority queue. ] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivRemove( Fxch_Man_t* pFxchMan, + int fUpdate, + int fSingleCube, + int fBase ) +{ + int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree ); + + assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) ); + + /* Decrement weight */ + if ( fSingleCube ) + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 ); + else + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) ); + + if ( fUpdate ) + if ( pFxchMan->vDivPrio ) + { + if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) ) + Vec_QueUpdate( pFxchMan->vDivPrio, iDiv ); + } + + return iDiv; +} + +/**Function************************************************************* + + Synopsis [ Separete the cubes in present in a divisor ] + + Description [ In this implementation *all* stored divsors are composed + of two cubes. + + In order to save space and to be able to use the Vec_Int_t + hash table both cubes are stored in the same vector - using + a little hack to differentiate which literal belongs to each + cube. + + This function separetes the two cubes in their own vectors + so that they can be added to the cover. + + *Note* that this also applies to single cube + divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, + Vec_Int_t* vCube0, + Vec_Int_t* vCube1 ) +{ + int* pArray; + int i, + Lit; + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) ); + else + Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) ); + + if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) ) + { + assert( Vec_IntSize( vCube1 ) == 3 ); + + pArray = Vec_IntArray( vCube0 ); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + + pArray = Vec_IntArray( vCube1 ); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + } +} + +/**Function************************************************************* + + Synopsis [ Removes the literals present in the divisor from their + original cubes. ] + + Description [ This function returns the numeber of removed literals + which should be equal to the size of the divisor. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivRemoveLits( Vec_Int_t* vCube0, + Vec_Int_t* vCube1, + Vec_Int_t* vDiv, + int *fCompl ) +{ + int i, + Lit, + CountP = 0, + CountN = 0, + Count = 0, + ret = 0; + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) ) + CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) ); + else + CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) ); + + if ( Vec_IntSize( vDiv ) == 2 ) + Vec_IntForEachEntry( vDiv, Lit, i ) + { + Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) ); + Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) ); + } + + ret = Count + CountP + CountN; + + if ( Vec_IntSize( vDiv ) == 4 ) + { + int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ), + Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ), + Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ), + Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) ); + + if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 ) + *fCompl = 1; + + if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 ) + { + *fCompl = 1; + + Vec_IntForEachEntry( vDiv, Lit, i ) + ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) ); + } + } + + return ret; +} + +/**Function************************************************************* + + Synopsis [ Print the divisor identified by iDiv. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_DivPrint( Fxch_Man_t* pFxchMan, + int iDiv ) +{ + Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ); + int i, + Lit; + + printf( "Div %7d : ", iDiv ); + printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( !Abc_LitIsCompl( Lit ) ) + printf( "%d(1)", Abc_Lit2Var( Lit ) ); + + printf( " + " ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl( Lit ) ) + printf( "%d(2)", Abc_Lit2Var( Lit ) ); + + printf( " Lits =%7d ", pFxchMan->nLits ); + printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) ); +} + +/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ +void Fxch_DivFindPivots( Vec_Int_t* vDiv, + int* pLit0, + int* pLit1 ) +{ + int i, + Lit; + * pLit0 = -1; + * pLit1 = -1; + + Vec_IntForEachEntry( vDiv, Lit, i ) + { + if ( Abc_LitIsCompl( Lit ) ) + { + if ( *pLit1 == -1 ) + *pLit1 = Abc_Lit2Var( Lit ); + } + else + { + if ( *pLit0 == -1 ) + *pLit0 = Abc_Lit2Var( Lit ); + } + if ( *pLit0 >= 0 && *pLit1 >= 0 ) + return; + } +} + +int Fxch_DivFind( Vec_Int_t* vCube0, + Vec_Int_t* vCube1, + Vec_Int_t* vCubeFree ) +{ + int Counter = 0, + fAttr0 = 0, + fAttr1 = 1; + int* pBeg1 = vCube0->pArray + 1, + * pBeg2 = vCube1->pArray + 1, + * pEnd1 = vCube0->pArray + vCube0->nSize, + * pEnd2 = vCube1->pArray + vCube1->nSize; + + Vec_IntClear( vCubeFree ); + + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + { + pBeg1++; + pBeg2++; + Counter++; + } + else if ( *pBeg1 < *pBeg2 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); + else + { + if ( Vec_IntSize( vCubeFree ) == 0 ) + fAttr0 = 1, fAttr1 = 0; + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1) ); + } + } + while ( pBeg1 < pEnd1 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); + while ( pBeg2 < pEnd2 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1 ) ); + + assert( !Abc_LitIsCompl( Vec_IntEntry(vCubeFree, 0) ) ); + return Counter; +} + +void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, + Vec_Int_t* vCubes_Lit0, + Vec_Int_t* vCubes_Lit1 ) +{ + int* pBeg1 = vCubes_Lit0->pArray + 1, + * pBeg2 = vCubes_Lit1->pArray + 1, + * pEnd1 = vCubes_Lit0->pArray + vCubes_Lit0->nSize, + * pEnd2 = vCubes_Lit1->pArray + vCubes_Lit1->nSize; + + Vec_IntClear( pFxchMan->vPairs ); + + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ), + CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ), + i, k; + + if ( CubeId1 == CubeId2 ) + { + for ( i = 1; pBeg1+i < pEnd1; i++ ) + if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg1[i], 0) ) + break; + + for ( k = 1; pBeg2+k < pEnd2; k++ ) + if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) ) + break; + + for ( int i_ = 0; i_ < i; i_++ ) + for ( int k_ = 0; k_ < k; k_++ ) + { + if ( pBeg1[i_] == pBeg2[k_] ) + continue; + Fxch_DivFind( Vec_WecEntry( pFxchMan->vCubes, pBeg1[i_] ), + Vec_WecEntry( pFxchMan->vCubes, pBeg2[k_] ), + pFxchMan->vCubeFree ); + + if ( Vec_IntSize( pFxchMan->vCubeFree ) == 4 ) + Fxch_DivNormalize( pFxchMan->vCubeFree ); + + if ( !Vec_IntEqual( pFxchMan->vDiv, pFxchMan->vCubeFree ) ) + continue; + + Vec_IntPush( pFxchMan->vPairs, pBeg1[i_] ); + Vec_IntPush( pFxchMan->vPairs, pBeg2[k_] ); + } + pBeg1 += i; + pBeg2 += k; + } + else if ( CubeId1 < CubeId2 ) + pBeg1++; + else + pBeg2++; + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c new file mode 100644 index 00000000..6437950d --- /dev/null +++ b/src/opt/fxch/FxchMan.c @@ -0,0 +1,600 @@ +/**CFile**************************************************************** + + FileName [ FxchMan.c ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ Fxch Manager 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 + +//////////////////////////////////////////////////////////////////////// +/// LOCAL FUNCTIONS DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan, + unsigned int SubCubeID, + unsigned int iSubCube, + unsigned int iCube, + unsigned int iLit0, + unsigned int iLit1, + char fAdd, + char fUpdate ) +{ + int ret = 0; + + if ( fAdd ) + { + ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes, + SubCubeID, iSubCube, + iCube, iLit0, iLit1, fUpdate ); + } + else + { + ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes, + SubCubeID, iSubCube, + iCube, iLit0, iLit1, fUpdate ); + } + + return ret; +} + + +static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan, + int iCube, + int fAdd, + int fUpdate ) +{ + Vec_Int_t* vCube = Vec_WecEntry( pFxchMan->vCubes, iCube ); + int i, k, + Lit0, + Lit1, + fSingleCube = 1, + fBase = 0; + + if ( Vec_IntSize(vCube) < 2 ) + return 0; + + Vec_IntForEachEntryStart( vCube, Lit0, i, 1) + Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) ) + { + 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 ) ); + + if (fAdd) + { + Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase ); + pFxchMan->nPairsS++; + } + else + { + Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase ); + pFxchMan->nPairsS--; + } + } + + return Vec_IntSize( vCube ) * ( Vec_IntSize( vCube ) - 1 ) / 2; +} + +static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan, + int iCube, + int fAdd, + int fUpdate ) +{ + 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++, + iCube, 0, 0, + fAdd, fUpdate ); + + Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1) + { + /* 1 Lit remove */ + SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 ); + + pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, + SubCubeID, nHashedSC++, + iCube, iLit0, 0, + fAdd, fUpdate ); + + if ( Vec_IntSize( vCube ) > 3 ) + { + int Lit1, + iLit1; + + Vec_IntForEachEntryStart( vCube, Lit1, iLit1, iLit0 + 1) + { + /* 2 Lit remove */ + SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 ); + + pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, + SubCubeID, nHashedSC++, + iCube, iLit0, iLit1, + fAdd, fUpdate ); + + SubCubeID += Vec_IntEntry( vLitHashKeys, Lit1 ); + } + } + + SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 ); + } +} + +static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes, + Vec_Int_t* vLit2Cube ) +{ + int i, + k = 0, + CubeId; + + Vec_IntForEachEntry( vLit2Cube, CubeId, i ) + if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 ) + Vec_IntWriteEntry( vLit2Cube, k++, CubeId ); + + Vec_IntShrink( vLit2Cube, k ); +} + +//////////////////////////////////////////////////////////////////////// +/// PUBLIC INTERFACE /// +//////////////////////////////////////////////////////////////////////// +Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, + char SMode ) +{ + Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 ); + + pFxchMan->vCubes = vCubes; + pFxchMan->pDivHash = Hsh_VecManStart( 1000 ); + pFxchMan->vDivWeights = Vec_FltAlloc( 1000 ); + + pFxchMan->SMode = SMode; + if ( pFxchMan->SMode == 0 ) + pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 ); + + pFxchMan->vCubeFree = Vec_IntAlloc( 100 ); + pFxchMan->vDiv = Vec_IntAlloc( 100 ); + pFxchMan->vCubesS = Vec_IntAlloc( 100 ); + pFxchMan->vPairs = Vec_IntAlloc( 100 ); + + return pFxchMan; +} + +void Fxch_ManFree( Fxch_Man_t* pFxchMan ) +{ + Vec_WecFree( pFxchMan->vLits ); + Vec_IntFree( pFxchMan->vLitCount ); + Vec_IntFree( pFxchMan->vLitHashKeys ); + + Hsh_VecManStop( pFxchMan->pDivHash ); + Vec_FltFree( pFxchMan->vDivWeights ); + Vec_QueFree( pFxchMan->vDivPrio ); + + if ( pFxchMan->SMode == 0 ) + Vec_WecFree( pFxchMan->vDivCubePairs ); + + Vec_IntFree( pFxchMan->vLevels ); + + Vec_IntFree( pFxchMan->vCubeFree ); + Vec_IntFree( pFxchMan->vDiv ); + Vec_IntFree( pFxchMan->vCubesS ); + Vec_IntFree( pFxchMan->vPairs ); + + ABC_FREE( pFxchMan ); +} + +void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, + int nVars ) +{ + + Vec_Int_t* vCube; + int i, k, + Lit, + Count; + + pFxchMan->nVars = 0; + pFxchMan->nLits = 0; + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i ) + { + assert( Vec_IntSize(vCube) > 0 ); + pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Vec_IntEntry( vCube, 0 ) ); + pFxchMan->nLits += Vec_IntSize(vCube) - 1; + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Abc_Lit2Var( Lit ) ); + } + + assert( pFxchMan->nVars < nVars ); + pFxchMan->nVars = nVars; + + /* Count the number of time each literal appears on the SOP */ + pFxchMan->vLitCount = Vec_IntStart( 2 * pFxchMan->nVars ); + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i ) + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Vec_IntAddToEntry( pFxchMan->vLitCount, Lit, 1 ); + + /* Allocate space to the array of arrays wich maps Literals into cubes which uses them */ + pFxchMan->vLits = Vec_WecStart( 2 * pFxchMan->nVars ); + Vec_IntForEachEntry( pFxchMan->vLitCount, Count, Lit ) + Vec_IntGrow( Vec_WecEntry( pFxchMan->vLits, Lit ), Count ); + + /* Maps Literals into cubes which uses them */ + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i ) + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit, i ); +} + +void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan ) +{ + /* Generates the random number which will be used for hashing cubes */ + Gia_ManRandom( 1 ); + pFxchMan->vLitHashKeys = Vec_IntAlloc( ( 2 * pFxchMan->nVars ) ); + for ( int i = 0; i < (2 * pFxchMan->nVars); i++ ) + Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF ); +} + +void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan ) +{ + Vec_Wec_t* vCubes = pFxchMan->vCubes; + Vec_Int_t* vCube, + * vCubeLinks; + 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 : ( nLits * nLits + nLits ) / 2; + + Vec_IntPush( vCubeLinks, ( nTotalHashed + 1 ) ); + nTotalHashed += nSubCubes + 1; + } + + pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, vCubeLinks, nTotalHashed ); +} + +void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan ) +{ + Fxch_SCHashTableDelete( pFxchMan->pSCHashTable ); +} + +void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan ) +{ + Vec_Int_t* vCube; + float Weight; + int fAdd = 1, + fUpdate = 0, + iCube; + + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube ) + { + Fxch_ManDivSingleCube( pFxchMan, iCube, fAdd, fUpdate ); + Fxch_ManDivDoubleCube( pFxchMan, iCube, fAdd, fUpdate ); + } + + pFxchMan->vDivPrio = Vec_QueAlloc( Vec_FltSize( pFxchMan->vDivWeights ) ); + Vec_QueSetPriority( pFxchMan->vDivPrio, Vec_FltArrayP( pFxchMan->vDivWeights ) ); + Vec_FltForEachEntry( pFxchMan->vDivWeights, Weight, iCube ) + { + if ( Weight > 0.0 ) + Vec_QuePush( pFxchMan->vDivPrio, iCube ); + } +} + +/* Level Computation */ +int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan, + Vec_Int_t* vCubeFree ) +{ + int i, + Lit, + Level = 0; + + Vec_IntForEachEntry( vCubeFree, Lit, i ) + Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Abc_Lit2Var( Lit ) ) ) ); + + return Abc_MinInt( Level, 800 ); +} + +int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan, + Vec_Int_t * vCube ) +{ + int k, + Lit, + Level = 0; + + Vec_IntForEachEntryStart( vCube, Lit, k, 1 ) + Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Lit ) ) ); + + return Level; +} + +void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan ) +{ + Vec_Int_t* vCube; + int i, + iVar, + iFirst = 0; + + iVar = Vec_IntEntry( Vec_WecEntry( pFxchMan->vCubes, 0 ), 0 ); + pFxchMan->vLevels = Vec_IntStart( pFxchMan->nVars ); + + Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i ) + { + if ( iVar != Vec_IntEntry( vCube, 0 ) ) + { + Vec_IntAddToEntry( pFxchMan->vLevels, iVar, i - iFirst ); + iVar = Vec_IntEntry( vCube, 0 ); + iFirst = i; + } + Vec_IntUpdateEntry( pFxchMan->vLevels, iVar, Fxch_ManComputeLevelCube( pFxchMan, vCube ) ); + } +} + +void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, + int iDiv ) +{ + int i, + iCube0, + iCube1, + Lit0 = -1, + Lit1 = -1; + + Vec_Int_t* vCube0, + * vCube1, + * vLitP, + * vLitN, + * vDivCubePairs; + + /* Get the selected candidate (divisor) */ + Vec_IntClear( pFxchMan->vDiv ); + Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) ); + + /* Find cubes associated with the single divisor */ + Vec_IntClear( pFxchMan->vCubesS ); + if ( Vec_IntSize( pFxchMan->vDiv ) == 2 ) + { + Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) ); + Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) ); + + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) ); + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) ); + Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ), + Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ), + pFxchMan->vCubesS ); + } + else + Fxch_DivFindPivots( pFxchMan->vDiv, &Lit0, &Lit1 ); + + assert( Lit0 >= 0 && Lit1 >= 0 ); + + /* Find pairs associated with the divisor */ + Vec_IntClear( pFxchMan->vPairs ); + if ( pFxchMan->SMode == 1 ) + { + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit0) ); + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit1) ); + Fxch_DivFindCubePairs( pFxchMan, Vec_WecEntry( pFxchMan->vLits, Lit0 ), Vec_WecEntry( pFxchMan->vLits, Lit1 ) ); + } + else + { + vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv ); + Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs ); + Vec_IntErase( vDivCubePairs ); + } + + Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) + { + assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) ); + if (iCube0 > iCube1) + { + Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1); + Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0); + } + } + + Vec_IntUniqifyPairs( pFxchMan->vPairs ); + assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 ); + + /* 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 */ + + /* 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 */ + } + + Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) + { + if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + + } + + /* Create a new variable */ + int iVarNew = pFxchMan->nVars; + pFxchMan->nVars++; + + /* Create new Lit hash keys */ + Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF ); + Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF ); + + /* Create new Cube */ + vCube0 = Vec_WecPushLevel( pFxchMan->vCubes ); + Vec_IntPush( vCube0, iVarNew ); + + int Level; + if ( Vec_IntSize( pFxchMan->vDiv ) == 2 ) + { + if ( Lit0 > Lit1 ) + ABC_SWAP(int, Lit0, Lit1); + + Vec_IntPush( vCube0, Abc_LitNot( Lit0 ) ); + Vec_IntPush( vCube0, Abc_LitNot( Lit1 ) ); + Level = 1 + Fxch_ManComputeLevelCube( pFxchMan, vCube0 ); + } + else + { + vCube1 = Vec_WecPushLevel( pFxchMan->vCubes ); + vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 ); + Vec_IntPush( vCube1, iVarNew ); + Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 ); + Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ), + Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) ); + } + assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew ); + Vec_IntPush( pFxchMan->vLevels, Level ); + + pFxchMan->nLits += Vec_IntSize( pFxchMan->vDiv ); + + /* Create new literals */ + vLitP = Vec_WecPushLevel( pFxchMan->vLits ); + vLitN = Vec_WecPushLevel( pFxchMan->vLits ); + vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ); + + /* Extract divisor from single-cubes */ + Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) + { + int RetValue; + + vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ); + RetValue = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) ); + RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) ); + assert( RetValue == 2 ); + + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); + Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + + pFxchMan->nLits--; + } + + /* For each pair (Ci, Cj) */ + /* Extract divisor from cube pairs */ + int k = 0, + nCompls = 0; + Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) + { + int RetValue, fCompl = 0; + + vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ); + vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ); + + RetValue = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl ); + nCompls += fCompl; + + assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) ); + + if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl ) + { + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) ); + Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + } + else + { + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); + Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + } + 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 ) ); + } + 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 */ + + /* 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 */ + + Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) + if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + + /* 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; + + Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + + vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 ); + Vec_IntForEachEntryStart( vCube0, Lit0, i, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + + vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 ); + Vec_IntForEachEntryStart( vCube1, Lit0, i, 1 ) + Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) ); + } + + /* 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 ); + } + + pFxchMan->nExtDivs++; +} + +/* Print */ +void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan ) +{ + int iDiv; + + for ( iDiv = 0; iDiv < Vec_FltSize( pFxchMan->vDivWeights ); iDiv++ ) + Fxch_DivPrint( pFxchMan, iDiv ); +} + +void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan ) +{ + printf( "[FXCH] "); + printf( "Cubes =%8d ", Vec_WecSizeUsed( pFxchMan->vCubes ) ); + printf( "Lits =%8d ", Vec_WecSizeUsed( pFxchMan->vLits ) ); + printf( "Divs =%8d ", Hsh_VecSize( pFxchMan->pDivHash ) ); + printf( "Divs+ =%8d ", Vec_QueSize( pFxchMan->vDivPrio ) ); + printf( "Extr =%7d \n", pFxchMan->nExtDivs ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END 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 diff --git a/src/opt/fxch/module.make b/src/opt/fxch/module.make new file mode 100644 index 00000000..48f36b13 --- /dev/null +++ b/src/opt/fxch/module.make @@ -0,0 +1,4 @@ +SRC += src/opt/fxch/Fxch.c \ + src/opt/fxch/FxchDiv.c \ + src/opt/fxch/FxchMan.c \ + src/opt/fxch/FxchSCHashTable.c \ |