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

  FileName    [kitCloud.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Computation kit.]

  Synopsis    [Procedures using BDD package CLOUD.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - Dec 6, 2006.]

  Revision    [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]

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

#include "kit.h"

ABC_NAMESPACE_IMPL_START


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

// internal representation of the function to be decomposed
typedef struct Kit_Mux_t_ Kit_Mux_t;
struct Kit_Mux_t_
{
    unsigned      v  :  5;          // variable 
    unsigned      t  : 12;          // then edge
    unsigned      e  : 12;          // else edge
    unsigned      c  :  1;          // complemented attr of else edge
    unsigned      i  :  1;          // complemented attr of top node
};

static inline int        Kit_Mux2Int( Kit_Mux_t m )  { union { Kit_Mux_t x; int y; } v; v.x = m; return v.y;  }
static inline Kit_Mux_t  Kit_Int2Mux( int m )        { union { Kit_Mux_t x; int y; } v; v.y = m; return v.x;  }

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

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

  Synopsis    [Derive BDD from the truth table for 5 variable functions.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
{
    static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    CloudNode * pCof0, * pCof1;
    unsigned uCof0, uCof1;
    assert( nVars <= 5 );
    if ( uTruth == 0 )
        return dd->zero;
    if ( uTruth == ~0 )
        return dd->one;
    if ( nVars == 1 )
    {
        if ( uTruth == uVars[0] )
            return dd->vars[nVarsAll-1];
        if ( uTruth == ~uVars[0] )
            return Cloud_Not(dd->vars[nVarsAll-1]);
        assert( 0 );
    }
//    Count++;
    assert( nVars > 1 );
    uCof0 = uTruth & ~uVars[nVars-1];
    uCof1 = uTruth &  uVars[nVars-1];
    uCof0 |= uCof0 << (1<<(nVars-1));
    uCof1 |= uCof1 >> (1<<(nVars-1));
    if ( uCof0 == uCof1 )
        return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
    if ( uCof0 == ~uCof1 )
    {
        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
        pCof1 = Cloud_Not( pCof0 );
    }
    else
    {
        pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
        pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
    }
    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
}

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

  Synopsis    [Compute BDD for the truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
{
    CloudNode * pCof0, * pCof1;
    unsigned * pTruth0, * pTruth1;
    if ( nVars <= 5 )
        return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
    if ( Kit_TruthIsConst0(pTruth, nVars) )
        return dd->zero;
    if ( Kit_TruthIsConst1(pTruth, nVars) )
        return dd->one;
//    Count++;
    pTruth0 = pTruth;
    pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
    if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
        return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
    if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
    {
        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
        pCof1 = Cloud_Not( pCof0 );
    }
    else
    {
        pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
        pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
    }
    return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
}

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

  Synopsis    [Compute BDD for the truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
{
    CloudNode * pRes;
    pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
//    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
    return pRes;
}

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

  Synopsis    [Transforms the array of BDDs into the integer array.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
{
    Kit_Mux_t Mux;
    int nNodes, i;
    // collect BDD nodes
    nNodes = Cloud_DagCollect( dd, pFunc );
    if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
        return 0;
    assert( nNodes == Cloud_DagSize( dd, pFunc ) );
    assert( nNodes < dd->nNodesLimit );
    Vec_IntClear( vNodes );
    Vec_IntPush( vNodes, 0 ); // const1 node
    dd->ppNodes[0]->s = 0;
    for ( i = 1; i < nNodes; i++ )
    {
        dd->ppNodes[i]->s = i;
        Mux.v = dd->ppNodes[i]->v;
        Mux.t = dd->ppNodes[i]->t->s;
        Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
        Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
        Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
        // put the MUX into the array
        Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
    }
    assert( Vec_IntSize(vNodes) == nNodes );
    // reset signatures
    for ( i = 0; i < nNodes; i++ )
        dd->ppNodes[i]->s = dd->nSignCur;
    return 1;
}

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

  Synopsis    [Transforms the array of BDDs into the integer array.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
{
    CloudNode * pFunc;
    Cloud_Restart( dd );
    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
    Vec_IntClear( vNodes );
    return Kit_CreateCloud( dd, pFunc, vNodes );
}

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

  Synopsis    [Computes composition of truth tables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
{
    unsigned * pThis, * pFan0, * pFan1;
    Kit_Mux_t Mux;
    int i, Entry;
    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
    pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
    Kit_TruthFill( pThis, nVars );
    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
        pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
        pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
        pThis = (unsigned *)Vec_PtrEntry( vStore, i );
        Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
    } 
    // complement the result
    if ( Mux.i )
        Kit_TruthNot( pThis, pThis, nVars );
    return pThis;
}

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

  Synopsis    [Computes composition of truth tables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, 
    unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
{
    CloudNode * pFunc;
    unsigned * pThis, * pFan0, * pFan1;
    Kit_Mux_t Mux;
    int i, Entry, RetValue;
    // derive BDD from truth table
    Cloud_Restart( dd );
    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
    // convert it into nodes
    RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
    if ( RetValue == 0 )
        printf( "Kit_TruthCompose(): Internal failure!!!\n" );
    // verify the result
//    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
//    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
//        printf( "Failed!\n" );
    // compute truth table from the BDD
    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
    pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
    Kit_TruthFill( pThis, nVarsAll );
    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
        pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
        pThis = (unsigned *)Vec_PtrEntry( vStore, i );
        Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
    }
    // complement the result
    if ( Mux.i )
        Kit_TruthNot( pThis, pThis, nVarsAll );
    return pThis;
}

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

  Synopsis    [Compute BDD for the truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
{
    Kit_Mux_t Mux;
    unsigned * puSuppAll;
    unsigned * pThis = NULL; // Suppress "might be used uninitialized"
    unsigned * pFan0, * pFan1;
    int i, v, Var, Entry, nSupps;
    nSupps = 2 * nVars;

    // extend storage
    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
    puSuppAll = (unsigned *)Vec_IntArray( vMemory );
    // clear storage for the const node
    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
    // compute supports from nodes
    Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        Var = nVars - 1 - Mux.v;
        pFan0 = puSuppAll + nSupps * Mux.e;
        pFan1 = puSuppAll + nSupps * Mux.t;
        pThis = puSuppAll + nSupps * i;
        for ( v = 0; v < nSupps; v++ )
            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
    }
    // copy the result
    memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
    // compute the inverse

    // extend storage
    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
    puSuppAll = (unsigned *)Vec_IntArray( vMemory );
    // clear storage for the const node
    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
    // compute supports from nodes
    Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
//        Var = nVars - 1 - Mux.v;
        Var = Mux.v;
        pFan0 = puSuppAll + nSupps * Mux.e;
        pFan1 = puSuppAll + nSupps * Mux.t;
        pThis = puSuppAll + nSupps * i;
        for ( v = 0; v < nSupps; v++ )
            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
    }

    // merge supports
    for ( Var = 0; Var < nSupps; Var++ )
        puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
}

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


ABC_NAMESPACE_IMPL_END