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