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

  FileName    [llbFlow.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD based reachability.]

  Synopsis    [Flow computation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "llbInt.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Llb_Flw_t_ Llb_Flw_t;
struct Llb_Flw_t_
{
    unsigned    Source  :    1;  // source of the graph
    unsigned    Sink    :    1;  // sink of the graph
    unsigned    Flow    :    1;  // node has flow
    unsigned    Mark    :    1;  // visited node
    unsigned    Id      :   14;  // ID of the corresponding node
    unsigned    nFanins :   14;  // number of fanins
    Llb_Flw_t * Fanins[0];       // fanins
};

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Flw_t * Llb_FlwAlloc( Vec_Int_t * vMem, Vec_Ptr_t * vStore, int Id, int nFanins )
{
    Llb_Flw_t * p;
    int nWords = (sizeof(Llb_Flw_t) + nFanins * sizeof(void *)) / sizeof(int);
    p = (Llb_Flw_t *)Vec_IntFetch( vMem, nWords );
    memset( p, 1, nWords * sizeof(int) );
    p->Id      = Id;
    p->nFanins = 0;//nFanins;
    Vec_PtrWriteEntry( vStore, Id, p );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_FlwAddFanin( Llb_Flw_t * pFrom, Llb_Flw_t * pTo )
{
    pFrom->Fanins[pFrom->nFanins++] = pTo;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_AigCreateFlw( Aig_Man_t * p, Vec_Int_t ** pvMem, Vec_Ptr_t ** pvTops, Vec_Ptr_t ** pvBots )
{
    Llb_Flw_t * pFlwTop, * pFlwBot;
    Vec_Ptr_t * vTops, * vBots;
    Vec_Int_t * vMem;
    Aig_Obj_t * pObj;
    int i;
    vMem  = Vec_IntAlloc( Aig_ManObjNumMax(p) * (sizeof(Llb_Flw_t) + sizeof(void *) * 8) );
    vBots = Vec_PtrStart( Aig_ManObjNumMax(p) );
    vTops = Vec_PtrStart( Aig_ManObjNumMax(p) );
    Aig_ManForEachObj( p, pObj, i )
    {
        pFlwBot = Llb_FlwAlloc( vMem, vBots, i, Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
        pFlwTop = Llb_FlwAlloc( vMem, vTops, i, Aig_ObjRefs(pObj) + 1 );
        Llb_FlwAddFanin( pFlwBot, pFlwTop );
        Llb_FlwAddFanin( pFlwTop, pFlwBot );
        Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)) );
        Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)) );
        Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)), pFlwBot );
        Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)), pFlwBot );
    }
    Aig_ManForEachObj( p, pObj, i )
    {
        pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
        pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
        assert( pFlwBot->nFanins == (unsigned)Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
        assert( pFlwTop->nFanins == (unsigned)Aig_ObjRefs(pObj) + 1 );
    }
    *pvMem  = vMem;
    *pvTops = vTops;
    *pvBots = vBots;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_AigCleanMarks( Vec_Ptr_t * vFlw )
{
    Llb_Flw_t * pFlw;
    int i;
    Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
        pFlw->Mark = 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_AigCleanFlow( Vec_Ptr_t * vFlw )
{
    Llb_Flw_t * pFlw;
    int i;
    Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
        pFlw->Flow = 0;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_AigCollectCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vBots, Vec_Ptr_t * vTops )
{
    Vec_Int_t * vCut;
    Llb_Flw_t * pFlwBot, * pFlwTop;
    Aig_Obj_t * pObj;
    int i;
    vCut = Vec_IntAlloc( 100 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
        pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
        if ( pFlwBot->Mark && !pFlwTop->Mark )
            Vec_IntPush( vCut, i );
    }
    return vCut;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_AigPushFlow_rec( Llb_Flw_t * pFlw, Llb_Flw_t * pFlwPrev, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
{
    int i;
    if ( pFlw->Mark )
        return 0;
    pFlw->Mark = 1;
    Vec_PtrPush( vMarked, pFlw );
    if ( pFlw->Source )
        return 0;
    if ( pFlw->Sink )
    {
        pFlw->Flow = 1;
        Vec_PtrPush( vFlowed, pFlw );
        return 1;
    }
//    assert( Aig_ObjIsNode(pObj) );
    for ( i = 0; i < (int)pFlw->nFanins; i++ )
    {
        if ( pFlw->Fanins[i] == pFlwPrev )
            continue;
        if ( Llb_AigPushFlow_rec( pFlw->Fanins[i], pFlw, vMarked, vFlowed ) )
            break;
    }
    if ( i == (int)pFlw->nFanins )
        return 0;
    if ( i == 0 )
    {
        pFlw->Flow = 1;
        Vec_PtrPush( vFlowed, pFlw );
    }
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_AigPushFlow( Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
{
    Llb_Flw_t * pFlw;
    int i, Counter = 0;
    Vec_PtrForEachEntry( Llb_Flw_t *, vFlwBots, pFlw, i )
    {
        pFlw->Mark = 1;
        if ( Llb_AigPushFlow_rec( pFlw->Fanins[0], pFlw, vMarked, vFlowed ) )
        {
            Counter++;
            pFlw->Flow = 1;
            Vec_PtrPush( vFlowed, pFlw );
        }
    }
    return Counter;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_AigFindMinCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vFlwTop, Vec_Ptr_t * vFlwBots2, Vec_Ptr_t * vFlwTop2 )
{
    Vec_Int_t * vCut;
    Vec_Ptr_t * vMarked, * vFlowed;
    int Value;
    vMarked = Vec_PtrAlloc( 100 );
    vFlowed = Vec_PtrAlloc( 100 );
    Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
    Llb_AigCleanMarks( vMarked );
    Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
    assert( Value == 0 );
    vCut = Llb_AigCollectCut( vNodes, vFlwBots, vFlwTop );
    Llb_AigCleanMarks( vMarked );
    Llb_AigCleanFlow( vFlowed );
    return vCut;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_AigCollectFlowTerminals( Aig_Man_t * p, Vec_Ptr_t * vFlws, Vec_Int_t * vCut )
{
    Vec_Ptr_t * pFlwRes;
    Aig_Obj_t * pObj;
    int i;
    pFlwRes = Vec_PtrAlloc( Vec_IntSize(vCut) );
    Aig_ManForEachNodeVec( p, vCut, pObj, i )
        Vec_PtrPush( pFlwRes, Vec_PtrEntry( vFlws, Aig_ObjId(pObj) ) );
    return pFlwRes;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_AigMarkFlowTerminals( Vec_Ptr_t * vFlws, int fSource, int fSink )
{
    Llb_Flw_t * pFlw;
    int i;
    Vec_PtrForEachEntry( Llb_Flw_t *, vFlws, pFlw, i )
    {
        pFlw->Source = fSource;
        pFlw->Sink   = fSink;
    }
}

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

  Synopsis    [Collects internal nodes in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManCollectNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    assert( Aig_ObjIsNode(pObj) );
    Llb_ManCollectNodes_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Llb_ManCollectNodes_rec( p, Aig_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_ManCollectNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    Aig_ManForEachNodeVec( p, vCut1, pObj, i )
        Aig_ObjSetTravIdCurrent( p, pObj );
    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
    Aig_ManForEachNodeVec( p, vCut2, pObj, i )
        Llb_ManCollectNodes_rec( p, pObj, vNodes );
    return vNodes;
}

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

  Synopsis    [Collects internal nodes in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_ManCountNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return 0;
    Aig_ObjSetTravIdCurrent(p, pObj);
    assert( Aig_ObjIsNode(pObj) );
    return 1 + Llb_ManCountNodes_rec( p, Aig_ObjFanin0(pObj) ) +
               Llb_ManCountNodes_rec( p, Aig_ObjFanin1(pObj) );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_ManCountNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManIncrementTravId( p );
    Aig_ManForEachNodeVec( p, vCut1, pObj, i )
        Aig_ObjSetTravIdCurrent( p, pObj );
    Aig_ManForEachNodeVec( p, vCut2, pObj, i )
        Counter += Llb_ManCountNodes_rec( p, pObj );
    return Counter;
}

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

  Synopsis    [Computes starting cuts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_ManComputeCioCut( Aig_Man_t * pAig, int fCollectCos )
{
    Vec_Int_t * vCut;
    Aig_Obj_t * pObj;
    int i;
    vCut = Vec_IntAlloc( 500 );
    if ( fCollectCos )
        Aig_ManForEachPo( pAig, pObj, i )
            Vec_IntPush( vCut, Aig_ObjId(pObj) );
    else
        Aig_ManForEachPi( pAig, pObj, i )
            Vec_IntPush( vCut, Aig_ObjId(pObj) );
    return vCut;
}

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

  Synopsis    [Inserts the new cut into the array.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManCutInsert( Aig_Man_t * p, Vec_Ptr_t * vCuts, Vec_Int_t * vVols, int iEntry, Vec_Int_t * vCutNew )
{
    Vec_Int_t * vCut1, * vCut2; 
    int Vol1, Vol2;
    Vec_PtrInsert( vCuts, iEntry, vCutNew );
    Vec_IntInsert( vVols, iEntry, -1 );
    vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
    vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
    Vol1  = Llb_ManCountNodes( p, vCut1, vCutNew );
    Vol2  = Llb_ManCountNodes( p, vCutNew, vCut2 );
    Vec_IntWriteEntry( vVols, iEntry-1, Vol1 );
    Vec_IntWriteEntry( vVols, iEntry,   Vol2 );
}

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

  Synopsis    [Returns the set of cuts resulting from the flow computation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_ManComputePartitioning( Aig_Man_t * p, int nVolumeMin, int nVolumeMax )
{ 
    Vec_Ptr_t * vCuts, * vFlwTops, * vFlwBots;
    Vec_Int_t * vVols, * vCut1, * vCut2, * vCut, * vMem; 
    int nMaxValue, iEntry;
    vCuts = Vec_PtrAlloc( 1000 );
    vVols = Vec_IntAlloc( 1000 );
    // prepare flow computation
    Llb_AigCreateFlw( p, &vMem, &vFlwTops, &vFlwBots );
    // start with regular cuts
    Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 0) );
    Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 1) );
    Vec_IntPush( vVols, Aig_ManNodeNum(p) );
    // split cuts with the largest volume
    while ( (nMaxValue = Vec_IntFindMax(vVols)) > nVolumeMax )
    {
        Vec_Ptr_t * vNodes, * vFlwBots2, * vFlwTops2; 
        iEntry = Vec_IntFind( vVols, nMaxValue );  assert( iEntry >= 0 );
        vCut1  = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
        vCut2  = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
        // collect nodes
        vNodes = Llb_ManCollectNodes( p, vCut1, vCut1 );
        assert( Vec_PtrSize(vNodes) == nMaxValue );
        assert( Llb_ManCountNodes(p, vCut1, vCut2) == nMaxValue );
        // collect sources and sinks
        vFlwBots2 = Llb_AigCollectFlowTerminals( p, vFlwBots, vCut1 );
        vFlwTops2 = Llb_AigCollectFlowTerminals( p, vFlwTops, vCut2 );
        // mark sources and sinks
        Llb_AigMarkFlowTerminals( vFlwBots2, 1, 0 );
        Llb_AigMarkFlowTerminals( vFlwTops2, 0, 1 );
        vCut = Llb_AigFindMinCut( vNodes, vFlwBots, vFlwTops, vFlwBots2, vFlwTops2 );
        Llb_AigMarkFlowTerminals( vFlwBots2, 0, 0 );
        Llb_AigMarkFlowTerminals( vFlwTops2, 0, 0 );
        // insert new cut
        Llb_ManCutInsert( p, vCuts, vVols, iEntry+1, vCut );
        // deallocate
        Vec_PtrFree( vNodes );
        Vec_PtrFree( vFlwBots2 );
        Vec_PtrFree( vFlwTops2 );
    }
    Vec_IntFree( vMem );
    Vec_PtrFree( vFlwTops );
    Vec_PtrFree( vFlwBots );
    return vCuts;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_ManMarkPivotNodesFlow( Aig_Man_t * p, Vec_Ptr_t * vCuts )
{
    Vec_Int_t * vVar2Obj, * vCut;
    Aig_Obj_t * pObj;
    int i, k;
    // mark inputs/outputs
    Aig_ManForEachPi( p, pObj, i )
        pObj->fMarkA = 1;
    Saig_ManForEachLi( p, pObj, i )
        pObj->fMarkA = 1;

    // mark internal pivot nodes
    Vec_PtrForEachEntry( Vec_Int_t *, vCuts, vCut, i )
        Aig_ManForEachNodeVec( p, vCut, pObj, k )
            pObj->fMarkA = 1;

    // assign variable numbers
    Aig_ManConst1(p)->fMarkA = 0;
    vVar2Obj = Vec_IntAlloc( 100 );
    Aig_ManForEachPi( p, pObj, i )
        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    Aig_ManForEachNode( p, pObj, i )
        if ( pObj->fMarkA )
            Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    Saig_ManForEachLi( p, pObj, i )
        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
    return vVar2Obj;
}

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

  Synopsis    [Returns the set of cuts resulting from the flow computation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManPartitionUsingFlow( Llb_Man_t * p, Vec_Ptr_t * vCuts )
{ 
    Vec_Int_t * vCut1, * vCut2;
    int i;
    vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, 0 );
    Vec_PtrForEachEntryStart( Vec_Int_t *, vCuts, vCut1, i, 1 )
    {
        vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, i );
        Llb_ManGroupCreateFromCuts( p, vCut1, vCut2 );
        vCut1 = vCut2;
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
    Vec_Ptr_t * vCuts;
    Llb_Man_t * p;
    vCuts = Llb_ManComputePartitioning( pAig, pPars->nVolumeMin, pPars->nVolumeMax );
    Aig_ManCleanMarkA( pAig );
    p = ABC_CALLOC( Llb_Man_t, 1 );
    p->pAigGlo  = pAigGlo;
    p->pPars    = pPars;
    p->pAig     = pAig;
    p->vVar2Obj = Llb_ManMarkPivotNodesFlow( p->pAig, vCuts );
    p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
    Llb_ManPrepareVarMap( p );
    Aig_ManCleanMarkA( pAig );
    Llb_ManPartitionUsingFlow( p, vCuts );
    Vec_VecFreeP( (Vec_Vec_t **)&vCuts );
    return p;
}

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


ABC_NAMESPACE_IMPL_END