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

  FileName    [lpkMulti.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: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "lpkInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Records variable order.]

  Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
{
    Kit_DsdObj_t * pObj;
    unsigned uSuppFanins, k;
    int Above[16], Below[16];
    int nAbove, nBelow, iFaninLit, i, x, y;
    // iterate through the nodes
    Kit_DsdNtkForEachObj( pNtk, pObj, i )
    {
        // collect fanin support of this node
        nAbove = 0;
        uSuppFanins = 0;
        Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
        {
            if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
                Above[nAbove++] = Abc_Lit2Var(iFaninLit);
            else
                uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
        }
        // find the below variables
        nBelow = 0;
        for ( y = 0; y < 16; y++ )
            if ( uSuppFanins & (1 << y) )
                Below[nBelow++] = y;
        // create all pairs
        for ( x = 0; x < nAbove; x++ )
            for ( y = 0; y < nBelow; y++ )
                pTable[Above[x]][Below[y]]++;
    }
}

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

  Synopsis    [Creates commmon variable order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
{
    int Score[16] = {0}, pPres[16];
    int i, y, x, iVarBest, ScoreMax, PrioCount;

    // mark the present variables
    for ( i = 0; i < nVars; i++ )
        pPres[i] = 1;
    // remove cofactored variables
    for ( i = 0; i < nCBars; i++ )
        pPres[piCofVar[i]] = 0;

    // compute scores for each leaf
    for ( i = 0; i < nVars; i++ )
    {
        if ( pPres[i] == 0 )
            continue;
        for ( y = 0; y < nVars; y++ )
            Score[i] += pTable[i][y];
        for ( x = 0; x < nVars; x++ )
            Score[i] -= pTable[x][i];
    }

    // print the scores
    if ( fVerbose )
    {
        printf( "Scores: " );
        for ( i = 0; i < nVars; i++ )
            printf( "%c=%d ", 'a'+i, Score[i] );
        printf( "   " );
        printf( "Prios: " );
    }

    // derive variable priority
    // variables with equal score receive the same priority
    for ( i = 0; i < nVars; i++ )
        pPrios[i] = 16;

    // iterate until variables remain
    for ( PrioCount = 1; ; PrioCount++ )
    {
        // find the present variable with the highest score
        iVarBest = -1;
        ScoreMax = -100000;
        for ( i = 0; i < nVars; i++ )
        {
            if ( pPres[i] == 0 )
                continue;
            if ( ScoreMax < Score[i] )
            {
                ScoreMax = Score[i];
                iVarBest = i;
            }
        }
        if ( iVarBest == -1 )
            break;
        // give the next priority to all vars having this score
        if ( fVerbose )
            printf( "%d=", PrioCount );
        for ( i = 0; i < nVars; i++ )
        {
            if ( pPres[i] == 0 )
                continue;
            if ( Score[i] == ScoreMax )
            {
                pPrios[i] = PrioCount;
                pPres[i] = 0;
                if ( fVerbose )
                    printf( "%c", 'a'+i );
            }
        }
        if ( fVerbose )
            printf( " " );
    }
    if ( fVerbose )
        printf( "\n" );
}

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

  Synopsis    [Finds components with the highest priority.]

  Description [Returns the number of components selected.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
{
    Kit_DsdObj_t * pObj;
    unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
    int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;

    // find individual support and total support 
    uSuppTotal = 0;
    for ( i = 0; i < nSize; i++ )
    {
        pTriv[i] = 1;
        if ( piLits[i] < 0 ) 
            uSupps[i] = 0;
        else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
        else
        {
            pObj = Kit_DsdNtkObj( ppNtks[i], Abc_Lit2Var(piLits[i]) );
            if ( pObj->Type == KIT_DSD_PRIME )
            {
                pTriv[i] = 0;
                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
            }
            else
            {
                assert( pObj->nFans == 2 );
                if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
                    pTriv[i] = 0;
                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
            }
            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
        }
        assert( uSupps[i] <= 0xFFFF );
        uSuppTotal |= uSupps[i];
    }
    if ( uSuppTotal == 0 )
        return 0;

    // find one support variable with the highest priority
    PrioMin = ABC_INFINITY;
    iVarMax = -1;
    for ( i = 0; i < 16; i++ )
        if ( uSuppTotal & (1 << i) )
            if ( PrioMin > pPrio[i] )
            {
                PrioMin = pPrio[i];
                iVarMax = i;
            }
    assert( iVarMax != -1 );

    // select components, which have this variable
    nComps = 0;
    fOneNonTriv = 0;
    uSuppLarge = 0;
    for ( i = 0; i < nSize; i++ )
        if ( uSupps[i] & (1<<iVarMax) )
        {
            if ( pTriv[i] || !fOneNonTriv )
            {
                if ( !pTriv[i] )
                {
                    uSuppLarge = uSupps[i];
                    fOneNonTriv = 1;
                }
                pDecision[i] = 1;
                nComps++;
            }
            else
                pDecision[i] = 0;
        }
        else
            pDecision[i] = 0;

    // add other non-trivial not-taken components whose support is contained in the current large component support
    if ( fOneNonTriv )
        for ( i = 0; i < nSize; i++ )
            if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
            {
                pDecision[i] = 1;
                nComps++;
            }

    return nComps;
}

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

  Synopsis    [Prepares the mapping manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio )
{
    Kit_DsdObj_t * pObj;
    If_Obj_t * pObjsNew[4][8], * pResPrev;
    int piLitsNew[8], pDecision[8];
    int i, k, nComps, nSize;

    // find which of the variables is highest in the order
    nSize = (1 << nCBars);
    nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
    if ( nComps == 0 )
        return If_Not( If_ManConst1(p->pIfMan) );

    // iterate over the nodes
    if ( p->pPars->fVeryVerbose )
        printf( "Decision: " );
    for ( i = 0; i < nSize; i++ )
    {
        if ( pDecision[i] )
        {
            if ( p->pPars->fVeryVerbose )
                printf( "%d ", i );
            assert( piLits[i] >= 0 );
            pObj = Kit_DsdNtkObj( ppNtks[i], Abc_Lit2Var(piLits[i]) );
            if ( pObj == NULL )
                piLitsNew[i] = -2;
            else if ( pObj->Type == KIT_DSD_PRIME )
                piLitsNew[i] = pObj->pFans[0];
            else
                piLitsNew[i] = pObj->pFans[1];
        }
        else
            piLitsNew[i] = piLits[i];
    }
    if ( p->pPars->fVeryVerbose )
        printf( "\n" );

    // call again
    pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );

    // create new set of nodes
    for ( i = 0; i < nSize; i++ )
    {
        if ( pDecision[i] )
            pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
        else if ( piLits[i] == -1 )
            pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
        else if ( piLits[i] == -2 )
            pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
        else
            pObjsNew[nCBars][i] = pResPrev;
    }

    // create MUX using these outputs
    for ( k = nCBars; k > 0; k-- )
    {
        nSize /= 2;
        for ( i = 0; i < nSize; i++ )
            pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
    }
    assert( nSize == 1 );
    return pObjsNew[0][0];  
}

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

  Synopsis    [Prepares the mapping manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
    static int Counter = 0;
    If_Obj_t * pResult;
    Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
    Kit_DsdObj_t * pRoot;
    int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
    int i, k, nCBars, nSize, nMemSize;
    unsigned * ppCofs[4][8], uSupport;
    char pTable[16][16] = {
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
    };
    int fVerbose = p->pPars->fVeryVerbose;

    Counter++;
//    printf( "Run %d.\n", Counter );

    // allocate storage for cofactors
    nMemSize = Kit_TruthWordNum(nVars);
    ppCofs[0][0] = ABC_ALLOC( unsigned, 32 * nMemSize );
    nSize = 0;
    for ( i = 0; i < 4; i++ )
    for ( k = 0; k < 8; k++ )
        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
    assert( nSize == 32 );

    // find the best cofactoring variables
    nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
//    nCBars = 2;
//    piCofVar[0] = 0;
//    piCofVar[1] = 1;


    // copy the function
    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );

    // decompose w.r.t. these variables
    for ( k = 0; k < nCBars; k++ )
    {
        nSize = (1 << k);
        for ( i = 0; i < nSize; i++ )
        {
            Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
            Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
        }
    }
    nSize = (1 << nCBars);
    // compute DSD networks
    for ( i = 0; i < nSize; i++ )
    {
        ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
        ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
        Kit_DsdNtkFree( pTemp );
        if ( fVerbose )
        {
            printf( "Cof%d%d: ", nCBars, i );
            Kit_DsdPrint( stdout, ppNtks[i] );
        }
    }

    // compute variable frequences
    for ( i = 0; i < nSize; i++ )
    {
        uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
        for ( k = 0; k < nVars; k++ )
            if ( uSupport & (1<<k) )
                pFreqs[k]++;
    }

    // find common variable order
    for ( i = 0; i < nSize; i++ )
    {
        Kit_DsdGetSupports( ppNtks[i] );
        Lpk_CreateVarOrder( ppNtks[i], pTable );
    }
    Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
    // update priorities with frequences
    for ( i = 0; i < nVars; i++ )
        pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;

    if ( fVerbose )
        printf( "After restructuring with priority:\n" );

    // transform all networks according to the variable order
    for ( i = 0; i < nSize; i++ )
    {
        ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
        Kit_DsdNtkFree( pTemp );
        Kit_DsdGetSupports( ppNtks[i] );
        assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
        // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
        Kit_DsdRotate( ppNtks[i], pFreqs );
        // print the resulting networks
        if ( fVerbose )
        {
            printf( "Cof%d%d: ", nCBars, i );
            Kit_DsdPrint( stdout, ppNtks[i] );
        }
    }
 
    for ( i = 0; i < nSize; i++ )
    {
        // collect the roots
        pRoot = Kit_DsdNtkRoot(ppNtks[i]);
        if ( pRoot->Type == KIT_DSD_CONST1 )
            piLits[i] = Abc_LitIsCompl(ppNtks[i]->Root)? -2: -1;
        else if ( pRoot->Type == KIT_DSD_VAR )
            piLits[i] = Abc_LitNotCond( pRoot->pFans[0], Abc_LitIsCompl(ppNtks[i]->Root) );
        else
            piLits[i] = ppNtks[i]->Root;
    }


    // recursively construct AIG for mapping
    p->fCofactoring = 1;
    pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
    p->fCofactoring = 0;

    if ( fVerbose )
        printf( "\n" );

    // verify the transformations
    nSize = (1 << nCBars);
    for ( i = 0; i < nSize; i++ )
        Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
    // mux the truth tables
    for ( k = nCBars-1; k >= 0; k-- )
    {
        nSize = (1 << k);
        for ( i = 0; i < nSize; i++ )
            Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
    }
    if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
        printf( "Verification failed.\n" );


    // free the networks
    for ( i = 0; i < 8; i++ )
        if ( ppNtks[i] )
            Kit_DsdNtkFree( ppNtks[i] );
    ABC_FREE( ppCofs[0][0] );

    return pResult;
}

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


ABC_NAMESPACE_IMPL_END