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

  FileName    [llb1Group.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD based reachability.]

  Synopsis    [Initial partition computation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "llbInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan )
{
    Llb_Grp_t * p;
    p = ABC_CALLOC( Llb_Grp_t, 1 );
    p->pMan   = pMan;
    p->vIns   = Vec_PtrAlloc( 8 );
    p->vOuts  = Vec_PtrAlloc( 8 );
    p->Id     = Vec_PtrSize( pMan->vGroups );
    Vec_PtrPush( pMan->vGroups, p );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManGroupStop( Llb_Grp_t * p )
{
    if ( p == NULL )
        return;
    Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
    Vec_PtrFreeP( &p->vIns );
    Vec_PtrFreeP( &p->vOuts );
    Vec_PtrFreeP( &p->vNodes );
    ABC_FREE( p );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Aig_ObjIsCo(pObj) )
    {
        Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
        return;
    }
    assert( Aig_ObjIsAnd(pObj) );
    Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
    Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}
 
/**Function*************************************************************

  Synopsis    [Collects the support of MFFC.]

  Description [Returns the number of internal nodes in the MFFC.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Llb_ManGroupCollect( Llb_Grp_t * pGroup )
{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    vNodes = Vec_PtrAlloc( 100 );
    Aig_ManIncrementTravId( pGroup->pMan->pAig );
    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
        Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
        Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
        Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes );
    return vNodes;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
{ 
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( pObj->fMarkA )
    {
        Vec_PtrPush( vSupp, pObj );
        return;
    }
    assert( Aig_ObjIsAnd(pObj) );
    Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp );
    Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
{
    Llb_Grp_t * p;
    assert( pObj->fMarkA == 1 );
    // derive group
    p = Llb_ManGroupAlloc( pMan );
    Vec_PtrPush( p->vOuts, pObj );
    Aig_ManIncrementTravId( pMan->pAig );
    if ( Aig_ObjIsCo(pObj) )
        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
    else
    {
        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns );
    }
    // derive internal objects
    assert( p->vNodes == NULL );
    p->vNodes = Llb_ManGroupCollect( p );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateFirst( Llb_Man_t * pMan )
{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( pMan );
    Saig_ManForEachLo( pMan->pAig, pObj, i )
        Vec_PtrPush( p->vOuts, pObj );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateLast( Llb_Man_t * pMan )
{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( pMan );
    Saig_ManForEachLi( pMan->pAig, pObj, i )
        Vec_PtrPush( p->vIns, pObj );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 )
{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( p1->pMan );
    // create inputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
        Vec_PtrPush( p->vIns, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
        Vec_PtrPushUnique( p->vIns, pObj );
    // create outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
        Vec_PtrPush( p->vOuts, pObj );
    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
        Vec_PtrPushUnique( p->vOuts, pObj );

    // derive internal objects
    assert( p->vNodes == NULL );
    p->vNodes = Llb_ManGroupCollect( p );
    return p;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManGroupMarkNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    if ( Aig_ObjIsTravIdPrevious(p, pObj) )
    {
        Aig_ObjSetTravIdCurrent(p, pObj);
        return;
    }
    Aig_ObjSetTravIdCurrent(p, pObj);
    assert( Aig_ObjIsNode(pObj) );
    Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin0(pObj) );
    Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin1(pObj) );
}

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

  Synopsis    [Creates group from two cuts derived by the flow computation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
{
    Llb_Grp_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = Llb_ManGroupAlloc( pMan );

    // mark Cut1
    Aig_ManIncrementTravId( pMan->pAig );
    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
        Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
    // collect unmarked Cut2
    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
        if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
            Vec_PtrPush( p->vOuts, pObj );

    // mark nodes reachable from Cut2
    Aig_ManIncrementTravId( pMan->pAig );
    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
        Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
    // collect marked Cut1
    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
        if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
            Vec_PtrPush( p->vIns, pObj );

    // derive internal objects
    assert( p->vNodes == NULL );
    p->vNodes = Llb_ManGroupCollect( p );
    return p;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManPrepareGroups( Llb_Man_t * pMan )
{
    Aig_Obj_t * pObj;
    int i;
    assert( pMan->vGroups == NULL );
    pMan->vGroups = Vec_PtrAlloc( 1000 );
    Llb_ManGroupCreateFirst( pMan );
    Aig_ManForEachNode( pMan->pAig, pObj, i )
    {
        if ( pObj->fMarkA )
            Llb_ManGroupCreate( pMan, pObj );
    }
    Saig_ManForEachLi( pMan->pAig, pObj, i )
    {
        if ( pObj->fMarkA )
            Llb_ManGroupCreate( pMan, pObj );
    }
    Llb_ManGroupCreateLast( pMan );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManPrintSpan( Llb_Man_t * p )
{
    Llb_Grp_t * pGroup;
    Aig_Obj_t * pVar;
    int i, k, Span = 0, SpanMax = 0;
    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
                Span++;
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
                Span++;

        SpanMax = Abc_MaxInt( SpanMax, Span );
printf( "%d ", Span );

        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
                Span--;
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
                Span--;
    }
printf( "\n" );
printf( "Max = %d\n", SpanMax );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar )
{
    Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup );
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
        if ( pObj->Id == iVar )
            return 1;
    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
        if ( pObj->Id == iVar )
            return 1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Llb_ManPrintHisto( Llb_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, k;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( Vec_IntEntry(p->vObj2Var, i) < 0 )
            continue;
        printf( "%3d :", i );
        for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ )
            printf( " " );
        for (      ; k <= Vec_IntEntry(p->vVarEnds, i); k++ )
            printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' );
        printf( "\n" );
    }
}

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


ABC_NAMESPACE_IMPL_END