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

  FileName    [absRefSelect.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Abstraction package.]

  Synopsis    [Post-processes the set of selected refinement objects.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#include "abs.h"
#include "absRef.h"

ABC_NAMESPACE_IMPL_START 

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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis )
{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
        if ( Gia_ObjIsPi(p->pGia, pObj) ) 
            printf( "-" );
        else if ( Vec_IntFind(vNewPPis, Gia_ObjId(p->pGia, pObj)) >= 0 )// this is PPI
            printf( "1" ), Counter++;
        else
            printf( "0" );
    printf( " %3d\n", Counter );
}

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

  Synopsis    [Perform structural analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
{
    Vec_Int_t * vFanins;
    Gia_Obj_t * pObj, * pFanin;
    int i, k;
    // clean labels
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = pObj->fMark1 = 0;
    // label frontier
    Gia_ManForEachObjVec( vFront, p, pObj, i )
        pObj->fMark0 = 1, pObj->fMark1 = 0;
    // label objects
    Gia_ManForEachObjVec( vInter, p, pObj, i )
        pObj->fMark1 = 0, pObj->fMark1 = 1;
    // label selected
    Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
        pObj->fMark1 = 1, pObj->fMark1 = 1;
    // explore selected
    Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
    {
        printf( "Selected PPI %3d : ", i+1 );
        printf( "%6d ",  Gia_ObjId(p, pObj) );
        printf( "\n" );
        vFanins = Ga2_ObjLeaves( p, pObj );
        Gia_ManForEachObjVec( vFanins, p, pFanin, k )
        {
            printf( "    " );
            printf( "%6d ", Gia_ObjId(p, pFanin) );
            if ( pFanin->fMark0 && pFanin->fMark1 )
                printf( "selected PPI" );
            else if ( pFanin->fMark0 && !pFanin->fMark1 )
                printf( "frontier (original PI or PPI)" );
            else if ( !pFanin->fMark0 &&  pFanin->fMark1 )
                printf( "abstracted node" );
            else if ( !pFanin->fMark0 && !pFanin->fMark1 )
                printf( "free variable" );
            printf( "\n" );
        }
    }
}

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

  Synopsis    [Postprocessing the set of PPIs using structural analysis.]

  Description [The following sets are used:
  The set of all PI+PPI is in p->vMap.
  The set of all abstracted objects is in p->vObjs;
  The set of important PPIs is in vOldPPis.
  The new set of selected PPIs is in vNewPPis.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
{
    int fVerbose = 0;
    Vec_Int_t * vNewPPis, * vFanins;
    Gia_Obj_t * pObj, * pFanin;
    int i, k, RetValue, Counters[3] = {0};

    // (0) make sure fanin counters are 0 at the beginning
//    Gia_ManForEachObj( p->pGia, pObj, i )
//        assert( Rnm_ObjCount(p, pObj) == 0 );

    // (1) increment PPI fanin counters
    Vec_IntClear( p->vFanins );
    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
    {
        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
            if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it
                Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
    }

    // (3) select objects with reconvergence, which create potential constraints
    // - flop objects
    // - objects whose fanin belongs to the justified area
    // - objects whose fanins overlap
    // (these do not guantee reconvergence, but may potentially have it)
    // (other objects cannot have reconvergence, even if they are added)
    vNewPPis = Vec_IntAlloc( 100 );
    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
    {
        if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( fVerbose )
                Counters[0]++;
            Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
            continue;
        }
        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
        {
            if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
            {
                if ( fVerbose )
                    Counters[1] += Rnm_ObjIsJust(p, pFanin);
                if ( fVerbose )
                    Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
                Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
                break;
            }
        }
    }
    RetValue = Vec_IntUniqify( vNewPPis );
    assert( RetValue == 0 );

    // (4) clear fanin counters
    // this is important for counters to be correctly set in the future iterations -- see step (0)
    Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
        Rnm_ObjSetCount( p, pObj, 0 );

    // visualize
    if ( fVerbose )
        printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d.   FF =%4d. Just =%4d. Shared =%4d.\n", 
            p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );

//    Rnm_ManPrintSelected( p, vNewPPis );
//    Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
    return vNewPPis;
}


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

  Synopsis    [Improved postprocessing the set of PPIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
{
    static int Counter = 0;
    int fVerbose = 0;
    Vec_Int_t * vNewPPis, * vFanins, * vFanins2;
    Gia_Obj_t * pObj, * pFanin, * pFanin2;
    int i, k, k2, RetValue, Counters[3] = {0};

    // return full set of PPIs once in a while
    if ( ++Counter % 9 == 0 )
        return Vec_IntDup( vOldPPis );
    return Rnm_ManFilterSelected( p, vOldPPis );

    // (0) make sure fanin counters are 0 at the beginning
//    Gia_ManForEachObj( p->pGia, pObj, i )
//        assert( Rnm_ObjCount(p, pObj) == 0 );

    // (1) increment two levels of PPI fanin counters
    Vec_IntClear( p->vFanins );
    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
    {
        // go through the fanins
        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
        {
            Rnm_ObjAddToCount(p, pFanin);
            if ( Rnm_ObjIsJust(p, pFanin) )   // included in the abstraction
                Rnm_ObjAddToCount(p, pFanin); // count it second time!
            Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );

            // go through the fanins of the fanins
            vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
            Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
            {
                Rnm_ObjAddToCount(p, pFanin2);
                if ( Rnm_ObjIsJust(p, pFanin2) )   // included in the abstraction
                    Rnm_ObjAddToCount(p, pFanin2); // count it second time!
                Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin2) );
            }
        }
    }

    // (3) select objects with reconvergence, which create potential constraints
    // - flop objects - yes
    // - objects whose fanin (or fanins' fanin) belongs to the justified area - yes
    // - objects whose fanins (or fanins' fanin) overlap - yes
    // (these do not guantee reconvergence, but may potentially have it)
    // (other objects cannot have reconvergence, even if they are added)
    vNewPPis = Vec_IntAlloc( 100 );
    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
    {
        if ( Gia_ObjIsRo(p->pGia, pObj) )
        {
            if ( fVerbose )
                Counters[0]++;
            Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
            continue;
        } 
        // go through the first fanins
        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
        {
            if ( Rnm_ObjCount(p, pFanin) > 1 )
                Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
            continue;

            // go through the fanins of the fanins
            vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
            Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
            {
                if ( Rnm_ObjCount(p, pFanin2) > 1 )
                {
//                    Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pFanin) );
                    Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
                }
            }
        }
    }
    RetValue = Vec_IntUniqify( vNewPPis );
//    assert( RetValue == 0 ); // we will have duplicated entries here!

    // (4) clear fanin counters
    // this is important for counters to be correctly set in the future iterations -- see step (0)
    Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
        Rnm_ObjSetCount( p, pObj, 0 );

    // visualize
    if ( fVerbose )
        printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d.   FF =%4d. Just =%4d. Shared =%4d.\n", 
            p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );

//    Rnm_ManPrintSelected( p, vNewPPis );
//    Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
    return vNewPPis;
}

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


ABC_NAMESPACE_IMPL_END