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

  FileName    [giaFront.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Frontier representation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Find the next place on the frontier.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManFrontFindNext( char * pFront, int nFront, int iFront )
{
    assert( iFront < nFront );
    for ( ; pFront[iFront]; iFront = (iFront + 1) % nFront );
    assert( pFront[iFront] == 0 );
    pFront[iFront] = 1;
    return iFront;
}

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

  Synopsis    [Transforms the frontier manager to its initial state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManFrontTransform( Gia_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i, * pFrontToId; // mapping of nodes into frontier variables
    assert( p->nFront > 0 );
    pFrontToId = ABC_FALLOC( int, p->nFront );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsCo(pObj) )
        {
            assert( pObj->Value == GIA_NONE );
            pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
        }
        else if ( Gia_ObjIsAnd(pObj) )
        {
            assert( (int)pObj->Value < p->nFront );
            pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
            pObj->iDiff1 = i - pFrontToId[Gia_ObjDiff1(pObj)];
            pFrontToId[pObj->Value] = i;
        }
        else
        {
            assert( (int)pObj->Value < p->nFront );
            pFrontToId[pObj->Value] = i;
        }
        pObj->Value = 0;
    }
    ABC_FREE( pFrontToId );
}

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

  Synopsis    [Determine the frontier.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCrossCutSimple( Gia_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i, nCutCur = 0, nCutMax = 0;
    Gia_ManCreateValueRefs( p );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( pObj->Value )
            nCutCur++;
        if ( nCutMax < nCutCur )
            nCutMax = nCutCur;
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
                nCutCur--;
            if ( --Gia_ObjFanin1(pObj)->Value == 0 )
                nCutCur--;
        }
        else if ( Gia_ObjIsCo(pObj) )
        {
            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
                nCutCur--;
        }
    }
//    Gia_ManForEachObj( p, pObj, i )
//        assert( pObj->Value == 0 );
    return nCutMax;
}


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

  Synopsis    [Determine the frontier.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
    char * pFront;    // places used for the frontier
    int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
    int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
    int iFront = 0;//, clk = Abc_Clock(); 
    // set references for all objects
    Gia_ManCreateValueRefs( p );
    // start the new manager
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); 
    // start the frontier
    pFront = ABC_CALLOC( char, pNew->nFront );
    // add constant node
    Gia_ManConst0(pNew)->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
    if ( Gia_ObjValue(Gia_ManConst0(p)) == 0 )
        pFront[iFront] = 0;
    else
        nCrossCut = 1;
    // iterate through the objects
    Gia_ManForEachObj1( p, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) )
        {
            if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
                nCrossCutMax = nCrossCut;
            // create new node
            iLit = Gia_ManAppendCi( pNew );
            pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
            assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
            pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
            // handle CIs without fanout
            if ( Gia_ObjValue(pObj) == 0 )
                pFront[iFront] = 0;
            continue;
        }
        if ( Gia_ObjIsCo(pObj) )
        {
            assert( Gia_ObjValue(pObj) == 0 );
            // create new node
            iLit = Gia_ManAppendCo( pNew, 0 );
            pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
            assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
            // get the fanin
            pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
            assert( pFanin0New->Value != GIA_NONE );
            pObjNew->Value = GIA_NONE;
            pObjNew->iDiff0 = pFanin0New->Value;
            pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
            // deref the fanin
            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
            {
                pFront[pFanin0New->Value] = 0;
                nCrossCut--;
            }
            continue;
        }
        if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
            nCrossCutMax = nCrossCut;
        // create new node
        pObjNew = Gia_ManAppendObj( pNew );
        assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
        // assign the first fanin
        pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
        assert( pFanin0New->Value != GIA_NONE );
        pObjNew->iDiff0 = pFanin0New->Value;
        pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
        // assign the second fanin
        pFanin1New = Gia_ManObj( pNew, Gia_ObjFaninId1(pObj, i) );
        assert( pFanin1New->Value != GIA_NONE );
        pObjNew->iDiff1 = pFanin1New->Value;
        pObjNew->fCompl1 = Gia_ObjFaninC1(pObj);
        // assign the frontier number
        pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
        // deref the fanins
        if ( --Gia_ObjFanin0(pObj)->Value == 0 )
        {
            pFront[pFanin0New->Value] = 0;
            nCrossCut--;
        }
        if ( --Gia_ObjFanin1(pObj)->Value == 0 )
        {
            pFront[pFanin1New->Value] = 0;
            nCrossCut--;
        }
        // handle nodes without fanout (choice nodes)
        if ( Gia_ObjValue(pObj) == 0 )
            pFront[iFront] = 0;
    }
    assert( pNew->nObjs == p->nObjs );
    assert( nCrossCut == 0 || nCrossCutMax == nCrossCutMaxInit );
    for ( i = 0; i < pNew->nFront; i++ )
        assert( pFront[i] == 0 );
    ABC_FREE( pFront );
//printf( "Crosscut = %6d. Frontier = %6d. ", nCrossCutMaxInit, pNew->nFront );
//ABC_PRT( "Time", Abc_Clock() - clk );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    return pNew;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManFrontTest( Gia_Man_t * p )
{
    Gia_Man_t * pNew;
    pNew  = Gia_ManFront( p );
    Gia_ManFrontTransform( pNew );
//    Gia_ManCleanValue( p );
//    Gia_ManCleanValue( pNew );
    if ( memcmp( pNew->pObjs, p->pObjs, sizeof(Gia_Obj_t) * p->nObjs ) )
    {
/*
        Gia_Obj_t * pObj, * pObjNew;
        int i;
        Gia_ManForEachObj( p, pObj, i )
        {
            pObjNew = Gia_ManObj( pNew, i );
            printf( "%5d %5d   %5d %5d\n", 
                pObj->iDiff0, pObjNew->iDiff0, 
                pObj->iDiff1, pObjNew->iDiff1 );
        }
*/
        printf( "Verification failed.\n" );
    }
    else
        printf( "Verification successful.\n" );
    Gia_ManStop( pNew );
}

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


ABC_NAMESPACE_IMPL_END