Fxch.h

Go to the documentation of this file.

 
#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 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;
/* 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 */
};

/* 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