/**CFile****************************************************************

  FileName    [covInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Mapping into network of SOPs/ESOPs.]

  Synopsis    [Internal declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: covInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#ifndef ABC__map__cov__covInt_h
#define ABC__map__cov__covInt_h

#include "base/abc/abc.h"


ABC_NAMESPACE_HEADER_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Min_Man_t_  Min_Man_t;
typedef struct Min_Cube_t_ Min_Cube_t;

struct Min_Man_t_
{
    int               nVars;          // the number of vars
    int               nWords;         // the number of words
    Extra_MmFixed_t * pMemMan;        // memory manager for cubes
    // temporary cubes
    Min_Cube_t *      pOne0;          // tautology cube
    Min_Cube_t *      pOne1;          // tautology cube
    Min_Cube_t *      pTriv0[2];      // trivial cube
    Min_Cube_t *      pTriv1[2];      // trivial cube
    Min_Cube_t *      pTemp;          // cube for computing the distance
    Min_Cube_t *      pBubble;        // cube used as a separator
    // temporary storage for the new cover
    int               nCubes;         // the number of cubes
    Min_Cube_t **     ppStore;        // storage for cubes by number of literals
};

struct Min_Cube_t_
{
    Min_Cube_t *      pNext;          // the pointer to the next cube in the cover
    unsigned          nVars    : 10;  // the number of variables
    unsigned          nWords   : 12;  // the number of machine words
    unsigned          nLits    : 10;  // the number of literals in the cube
    unsigned          uData[1];       // the bit-data for the cube
};


// iterators through the entries in the linked lists of cubes
#define Min_CoverForEachCube( pCover, pCube )                   \
    for ( pCube = pCover;                                       \
          pCube;                                                \
          pCube = pCube->pNext )
#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )       \
    for ( pCube = pCover,                                       \
          pCube2 = pCube? pCube->pNext: NULL;                   \
          pCube;                                                \
          pCube = pCube2,                                       \
          pCube2 = pCube? pCube->pNext: NULL )
#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev )       \
    for ( pCube = pCover,                                       \
          ppPrev = &(pCover);                                   \
          pCube;                                                \
          ppPrev = &pCube->pNext,                               \
          pCube = pCube->pNext )

// macros to get hold of bits and values in the cubes
static inline int  Min_CubeHasBit( Min_Cube_t * p, int i )              { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0;     }
static inline void Min_CubeSetBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] |= (1<<((i) & 31));                 }
static inline void Min_CubeXorBit( Min_Cube_t * p, int i )              { p->uData[(i)>>5] ^= (1<<((i) & 31));                 }
static inline int  Min_CubeGetVar( Min_Cube_t * p, int Var )            { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31));     }

/*=== covMinEsop.c ==========================================================*/
extern void         Min_EsopMinimize( Min_Man_t * p );
extern void         Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== covMinSop.c ==========================================================*/
extern void         Min_SopMinimize( Min_Man_t * p );
extern void         Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== covMinMan.c ==========================================================*/
extern Min_Man_t *  Min_ManAlloc( int nVars );
extern void         Min_ManClean( Min_Man_t * p, int nSupp );
extern void         Min_ManFree( Min_Man_t * p );
/*=== covMinUtil.c ==========================================================*/
extern void         Min_CoverCreate( Vec_Str_t * vCover, Min_Cube_t * pCover, char Type );
extern void         Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
extern void         Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
extern void         Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
extern void         Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
extern void         Min_CoverCheck( Min_Man_t * p );
extern int          Min_CubeCheck( Min_Cube_t * pCube );
extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
extern void         Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
extern int          Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Creates the cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
{
    Min_Cube_t * pCube;
    pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
    pCube->pNext  = NULL;
    pCube->nVars  = p->nVars;
    pCube->nWords = p->nWords;
    pCube->nLits  = 0;
    memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
    return pCube;
}

/**Function*************************************************************

  Synopsis    [Creates the cube representing elementary var.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
{
    Min_Cube_t * pCube;
    pCube = Min_CubeAlloc( p );
    Min_CubeXorBit( pCube, iVar*2+fCompl );
    pCube->nLits = 1;
    return pCube;
}

/**Function*************************************************************

  Synopsis    [Creates the cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
{
    Min_Cube_t * pCube;
    pCube = Min_CubeAlloc( p );
    memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
    pCube->nLits = pCopy->nLits;
    return pCube;
}

/**Function*************************************************************

  Synopsis    [Recycles the cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
{
    Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
}

/**Function*************************************************************

  Synopsis    [Recycles the cube cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
{
    Min_Cube_t * pCube, * pCube2;
    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
        Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
}


/**Function*************************************************************

  Synopsis    [Counts the number of cubes in the cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubeCountLits( Min_Cube_t * pCube )
{
    unsigned uData;
    int Count = 0, i, w;
    for ( w = 0; w < (int)pCube->nWords; w++ )
    {
        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
        for ( i = 0; i < 32; i += 2 )
            if ( uData & (1 << i) )
                Count++;
    }
    return Count;
}

/**Function*************************************************************

  Synopsis    [Counts the number of cubes in the cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
{
    unsigned uData;
    int i, w;
    Vec_IntClear( vLits );
    for ( w = 0; w < (int)pCube->nWords; w++ )
    {
        uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
        for ( i = 0; i < 32; i += 2 )
            if ( uData & (1 << i) )
                Vec_IntPush( vLits, w*16 + i/2 );
    }
}

/**Function*************************************************************

  Synopsis    [Counts the number of cubes in the cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
{
    Min_Cube_t * pCube;
    int Count = 0;
    Min_CoverForEachCube( pCover, pCube )
        Count++;
    return Count;
}


/**Function*************************************************************

  Synopsis    [Checks if two cubes are disjoint.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
{
    unsigned uData;
    int i;
    assert( pCube0->nVars == pCube1->nVars );
    for ( i = 0; i < (int)pCube0->nWords; i++ )
    {
        uData = pCube0->uData[i] & pCube1->uData[i];
        uData = (uData | (uData >> 1)) & 0x55555555;
        if ( uData != 0x55555555 )
            return 1;
    }
    return 0;
}

/**Function*************************************************************

  Synopsis    [Collects the disjoint variables of the two cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
{
    unsigned uData;
    int i, w;
    Vec_IntClear( vVars );
    for ( w = 0; w < (int)pCube->nWords; w++ )
    {
        uData  = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
        uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
        if ( uData == 0 )
            continue;
        for ( i = 0; i < 32; i += 2 )
            if ( uData & (1 << i) )
                Vec_IntPush( vVars, w*16 + i/2 );
    }
}

/**Function*************************************************************

  Synopsis    [Checks if two cubes are disjoint.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
{
    unsigned uData;
    int i, fFound = 0;
    for ( i = 0; i < (int)pCube0->nWords; i++ )
    {
        uData = pCube0->uData[i] ^ pCube1->uData[i];
        if ( uData == 0 )
        {
            if ( pTemp ) pTemp->uData[i] = 0;
            continue;
        }
        if ( fFound )
            return 0;
        uData = (uData | (uData >> 1)) & 0x55555555;
        if ( (uData & (uData-1)) > 0 ) // more than one 1
            return 0;
        if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
        fFound = 1;
    }
    if ( fFound == 0 )
    {
        printf( "\n" );
        Min_CubeWrite( stdout, pCube0 );
        Min_CubeWrite( stdout, pCube1 );
        printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Checks if two cubes are disjoint.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
{
    unsigned uData;//, uData2;
    int i, k, Var0 = -1, Var1 = -1;
    for ( i = 0; i < (int)pCube0->nWords; i++ )
    {
        uData = pCube0->uData[i] ^ pCube1->uData[i];
        if ( uData == 0 )
            continue;
        if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
            return 0;
        uData = (uData | (uData >> 1)) & 0x55555555;
        if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
            return 0;
        for ( k = 0; k < 32; k += 2 )
            if ( uData & (1 << k) )
            {
                if ( Var0 == -1 )
                    Var0 = 16 * i + k/2;
                else if ( Var1 == -1 )
                    Var1 = 16 * i + k/2;
                else
                    return 0;
            }
        /*
        if ( Var0 >= 0 )
        {
            uData &= 0xFFFF;
            uData2 = (uData >> 16);
            if ( uData && uData2 )
                return 0;
            if ( uData )
            {
            }
            uData }= uData2;
            uData &= 0x
        }
        */
    }
    if ( Var0 >= 0 && Var1 >= 0 )
    {
        *pVar0 = Var0;
        *pVar1 = Var1;
        return 1;
    }
    if ( Var0 == -1 || Var1 == -1 )
    {
        printf( "\n" );
        Min_CubeWrite( stdout, pCube0 );
        Min_CubeWrite( stdout, pCube1 );
        printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
    }
    return 0;
}

/**Function*************************************************************

  Synopsis    [Makes the produce of two cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
{
    Min_Cube_t * pCube;
    int i;
    assert( pCube0->nVars == pCube1->nVars );
    pCube = Min_CubeAlloc( p );
    for ( i = 0; i < p->nWords; i++ )
        pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
    pCube->nLits = Min_CubeCountLits( pCube );
    return pCube;
}

/**Function*************************************************************

  Synopsis    [Makes the produce of two cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
{
    Min_Cube_t * pCube;
    int i;
    assert( pCube0->nVars == pCube1->nVars );
    pCube = Min_CubeAlloc( p );
    for ( i = 0; i < p->nWords; i++ )
        pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
    pCube->nLits = Min_CubeCountLits( pCube );
    return pCube;
}

/**Function*************************************************************

  Synopsis    [Makes the produce of two cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
{
    int i;
    for ( i = 0; i < (int)pCube0->nWords; i++ )
        if ( pCube0->uData[i] != pCube1->uData[i] )
            return 0;
    return 1;
}

/**Function*************************************************************

  Synopsis    [Returns 1 if pCube1 is contained in pCube0, bitwise.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
{
    int i;
    for ( i = 0; i < (int)pCube0->nWords; i++ )
        if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
            return 0;
    return 1;
}

/**Function*************************************************************

  Synopsis    [Transforms the cube into the result of merging.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
{
    int w;
    for ( w = 0; w < (int)pCube->nWords; w++ )
    {
        pCube->uData[w]  =  pCube->uData[w] ^ pDist->uData[w];
        pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
    }
}

/**Function*************************************************************

  Synopsis    [Transforms the cube into the result of distance-1 merging.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
{
    int w;
    for ( w = 0; w < (int)pCube->nWords; w++ )
        pCube->uData[w] |= pDist->uData[w];
}


/**Function*************************************************************

  Synopsis    [Sorts the cover in the increasing number of literals.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
{
    Min_Cube_t * pCube, * pCube2, * pThis;
    if ( pCover == NULL )
    {
        Min_ManClean( p, p->nVars );
        return;
    }
    Min_ManClean( p, pCover->nVars );
    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
    {
        // go through the linked list
        Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
            if ( Min_CubesAreEqual( pCube, pThis ) )
            {
                Min_CubeRecycle( p, pCube );
                break;
            }
        if ( pThis != NULL )
            continue;
        pCube->pNext = p->ppStore[pCube->nLits];
        p->ppStore[pCube->nLits] = pCube;
        p->nCubes++;
    }
}

/**Function*************************************************************

  Synopsis    [Returns 1 if the given cube is contained in one of the cubes of the cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
{
    Min_Cube_t * pThis;
    int i;
/*
    // this cube cannot be equal to any cube
    Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
    {
        if ( Min_CubesAreEqual( pCube, pThis ) )
        {
            Min_CubeWrite( stdout, pCube );
            assert( 0 );
        }
    }
*/
    // try to find a containing cube
    for ( i = 0; i <= (int)pCube->nLits; i++ )
    Min_CoverForEachCube( p->ppStore[i], pThis )
    {
        // skip the bubble
        if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
            return 1;
    }
    return 0;
}


ABC_NAMESPACE_HEADER_END

#endif


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////