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

  FileName    [lpkSets.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Fast Boolean matching for LUT structures.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "lpkInt.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Lpk_Set_t_ Lpk_Set_t;
struct Lpk_Set_t_
{
    char         iVar;        // the cofactoring variable
    char         Over;        // the overlap in supports
    char         SRed;        // the support reduction
    char         Size;        // the size of the boundset
    unsigned     uSubset0;    // the first subset (with removed)
    unsigned     uSubset1;    // the second subset (with removed)
};

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

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

  Synopsis    [Recursively computes decomposable subsets.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
{
    unsigned i, iLitFanin, uSupport, uSuppCur;
    Kit_DsdObj_t * pObj;
    // consider the case of simple gate
    pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
    if ( pObj == NULL )
        return (1 << Abc_Lit2Var(iLit));
    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
    {
        unsigned uSupps[16], Limit, s;
        uSupport = 0;
        Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
        {
            uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
            uSupport |= uSupps[i];
        }
        // create all subsets, except empty and full
        Limit = (1 << pObj->nFans) - 1;
        for ( s = 1; s < Limit; s++ )
        {
            uSuppCur = 0;
            for ( i = 0; i < pObj->nFans; i++ )
                if ( s & (1 << i) )
                    uSuppCur |= uSupps[i];
            Vec_IntPush( vSets, uSuppCur );
        }
        return uSupport;
    }
    assert( pObj->Type == KIT_DSD_PRIME );
    // get the cumulative support of all fanins
    uSupport = 0;
    Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
    {
        uSuppCur  = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
        uSupport |= uSuppCur;
        Vec_IntPush( vSets, uSuppCur );
    }
    return uSupport;
}

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

  Synopsis    [Computes the set of subsets of decomposable variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
{
    unsigned uSupport, Entry;
    int Number, i;
    assert( p->nVars <= 16 );
    Vec_IntClear( vSets );
    Vec_IntPush( vSets, 0 );
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
        return 0;
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
    {
        uSupport = ( 1 << Abc_Lit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
        Vec_IntPush( vSets, uSupport );
        return uSupport;
    }
    uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
    assert( (uSupport & 0xFFFF0000) == 0 );
    Vec_IntPush( vSets, uSupport );
    // set the remaining variables
    Vec_IntForEachEntry( vSets, Number, i )
    {
        Entry = Number;
        Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
    }
    return uSupport;
}

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

  Synopsis    [Prints the sets of subsets.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Lpk_PrintSetOne( int uSupport )
{
    unsigned k;
    for ( k = 0; k < 16; k++ )
        if ( uSupport & (1<<k) )
            printf( "%c", 'a'+k );
    printf( " " );
}
/**Function*************************************************************

  Synopsis    [Prints the sets of subsets.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static void Lpk_PrintSets( Vec_Int_t * vSets )
{
    unsigned uSupport;
    int Number, i;
    printf( "Subsets(%d): ", Vec_IntSize(vSets) );
    Vec_IntForEachEntry( vSets, Number, i )
    {
        uSupport = Number;
        Lpk_PrintSetOne( uSupport );
    }
    printf( "\n" );
}

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

  Synopsis    [Computes maximal support reducing bound-sets.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
    Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
{
    static int nTravId = 0;            // the number of the times this is visited
    static int TravId[1<<16] = {0};    // last visited
    static char SRed[1<<16];           // best support reduction
    static char Over[1<<16];           // best overlaps
    static unsigned Parents[1<<16];    // best set of parents
    static unsigned short Used[1<<16]; // storage for used subsets
    int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
    unsigned Entry, Entry0, Entry1;
    unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
    Lpk_Set_t * pEntry;

    if ( nTravId == (1 << 30) )
        memset( TravId, 0, sizeof(int) * (1 << 16) );

    // collect support reducing subsets
    nUsed = 0;
    nTravId++;
    uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
    Vec_IntForEachEntry( vSets0, Entry0, i )
    Vec_IntForEachEntry( vSets1, Entry1, k )
    {
        uSupp0 = (Entry0 & 0xFFFF);
        uSupp1 = (Entry1 & 0xFFFF);
        // skip trivial
        if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
            continue;
        if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
            continue;
        // get the entry
        Entry = Entry0 | Entry1;
        uSupp = Entry & 0xFFFF;
        // set the bound set size
        nSuppSize = Kit_WordCountOnes( uSupp );
        // get the number of overlapping vars
        nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
        // get the support reduction
        nSuppRed  = nSuppSize - 1 - nSuppOver;
        // only consider support-reducing subsets
        if ( nSuppRed <= 0 )
            continue;
        // check if this support is already used
        if ( TravId[uSupp] < nTravId )
        {
            Used[nUsed++] = uSupp;

            TravId[uSupp] = nTravId;
            SRed[uSupp] = nSuppRed;
            Over[uSupp] = nSuppOver;
            Parents[uSupp] = (k << 16) | i;
        }
        else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
        {
            TravId[uSupp] = nTravId;
            SRed[uSupp] = nSuppRed;
            Over[uSupp] = nSuppOver;
            Parents[uSupp] = (k << 16) | i;
        }
    }

    // find the minimum overlap
    nMinOver = 1000;
    for ( s = 0; s < nUsed; s++ )
        if ( nMinOver > Over[Used[s]] )
            nMinOver = Over[Used[s]];


    // collect the accumulated ones
    for ( s = 0; s < nUsed; s++ )
        if ( Over[Used[s]] == nMinOver )
        {
            // save the entry
            if ( *pSize == nSizeLimit )
                return;
            pEntry = pStore + (*pSize)++;

            i = Parents[Used[s]] & 0xFFFF;
            k = Parents[Used[s]] >> 16;

            pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
            pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
            Entry  = pEntry->uSubset0 | pEntry->uSubset1;

            // record the cofactoring variable
            pEntry->iVar = iCofVar;
            // set the bound set size
            pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
            // get the number of overlapping vars
            pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
            // get the support reduction
            pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
            assert( pEntry->SRed > 0 );
        }
}

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

  Synopsis    [Prints one set.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
{
    unsigned Entry;
    Entry = pSet->uSubset0 | pSet->uSubset1;
    printf( "%2d : ", i );
    printf( "Var = %c  ",  'a' + pSet->iVar );
    printf( "Size = %2d  ", pSet->Size );
    printf( "Over = %2d  ", pSet->Over );
    printf( "SRed = %2d  ", pSet->SRed );
    Lpk_PrintSetOne( Entry );
    printf( "              " );
    Lpk_PrintSetOne( Entry >> 16 );
    printf( "\n" );
}

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

  Synopsis    [Evaluates the cofactors.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
{
    static int nStoreSize = 256;
    static Lpk_Set_t pStore[256], * pSet, * pSetBest;
    Kit_DsdNtk_t * ppNtks[2], * pTemp;
    Vec_Int_t * vSets0 = p->vSets[0];
    Vec_Int_t * vSets1 = p->vSets[1];
    unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
    unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
    int nSets, i, SizeMax;//, SRedMax;
    unsigned Entry;
    int fVerbose = p->pPars->fVeryVerbose;
//    int fVerbose = 0;

    // collect decomposable subsets for each pair of cofactors
    if ( fVerbose )
    {
        printf( "\nExploring support-reducing bound-sets of function:\n" );
        Kit_DsdPrintFromTruth( pTruth, nVars );
    }
    nSets = 0;
    for ( i = 0; i < nVars; i++ )
    {
        if ( fVerbose )
        printf( "Evaluating variable %c:\n", 'a'+i );
        // evaluate the cofactor pair
        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
        // decompose and expand
        ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
        ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
        ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
        ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
        if ( fVerbose )
        Kit_DsdPrint( stdout, ppNtks[0] );
        if ( fVerbose )
        Kit_DsdPrint( stdout, ppNtks[1] );
        // compute subsets
        Lpk_ComputeSets( ppNtks[0], vSets0 );
        Lpk_ComputeSets( ppNtks[1], vSets1 );
        // print subsets
        if ( fVerbose )
        Lpk_PrintSets( vSets0 );
        if ( fVerbose )
        Lpk_PrintSets( vSets1 );
        // free the networks
        Kit_DsdNtkFree( ppNtks[0] );
        Kit_DsdNtkFree( ppNtks[1] );
        // evaluate the pair
        Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
    }

    // print the results
    if ( fVerbose )
    printf( "\n" );
    if ( fVerbose )
    for ( i = 0; i < nSets; i++ )
        Lpk_MapSuppPrintSet( pStore + i, i );

    // choose the best subset
    SizeMax = 0;
    pSetBest = NULL;
    for ( i = 0; i < nSets; i++ )
    {
        pSet = pStore + i;
        if ( pSet->Size > p->pPars->nLutSize - 1 )
            continue;
        if ( SizeMax < pSet->Size )
        {
            pSetBest = pSet;
            SizeMax = pSet->Size;
        }
    }
/*
    // if the best is not choosen, select the one with largest reduction
    SRedMax = 0;
    if ( pSetBest == NULL )
    {
        for ( i = 0; i < nSets; i++ )
        {
            pSet = pStore + i;
            if ( SRedMax < pSet->SRed )
            {
                pSetBest = pSet;
                SRedMax = pSet->SRed;
            }
        }
    }
*/
    if ( pSetBest == NULL )
    {
        if ( fVerbose )
        printf( "Could not select a subset.\n" );
        return 0;
    }
    else
    {
        if ( fVerbose )
        printf( "Selected the following subset:\n" );
        if ( fVerbose )
        Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
    }

    // prepare the return result
    // get the remaining variables
    Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
    // get the variables to be removed
    Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
    // make sure there are some - otherwise it is not supp-red
    assert( Entry );
    // remember the first such variable
    *piVarReused = Kit_WordFindFirstBit( Entry );
    *piVar = pSetBest->iVar;
    return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
}

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


ABC_NAMESPACE_IMPL_END