/**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 unsigned char uint8_t; typedef unsigned int uint32_t; //////////////////////////////////////////////////////////////////////// /// 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_ { uint32_t Id, iCube; uint32_t iLit0 : 16, iLit1 : 16; }; /* Sub-cube Hash Table */ struct Fxch_SCHashTable_Entry_t_ { Fxch_SubCube_t* vSCData; uint32_t Size : 16, Cap : 16; }; struct Fxch_SCHashTable_t_ { Fxch_Man_t* pFxchMan; /* Internal data */ Fxch_SCHashTable_Entry_t* pBins; unsigned int nEntries, SizeMask; /* Temporary data */ Vec_Int_t vSubCube0; Vec_Int_t vSubCube1; }; struct Fxch_Man_t_ { /* user's data */ Vec_Wec_t* vCubes; int nCubesInit; 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 */ // 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* vCubesToRemove; Vec_Int_t* vCubesToUpdate; Vec_Int_t* vSCC; /* 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 ); 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 ); /*===== 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 ); int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv ); /*===== FxchMan.c ====================================================================================================*/ Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ); 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, int nEntries ); void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* ); int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, Vec_Wec_t* vCubes, 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, uint32_t SubCubeID, uint32_t iCube, uint32_t iLit0, uint32_t iLit1, char fUpdate ); unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* ); void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////