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

  FileName    [llb1Hint.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD based reachability.]

  Synopsis    [Cofactors the circuit w.r.t. the high-fanout variables.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "llbInt.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Returns CI index with the largest number of fanouts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_ManMaxFanoutCi( Aig_Man_t * pAig )
{
    Aig_Obj_t * pObj; 
    int i, WeightMax = -ABC_INFINITY, iInput = -1;
    Aig_ManForEachCi( pAig, pObj, i )
        if ( WeightMax < Aig_ObjRefs(pObj) )
        {
            WeightMax = Aig_ObjRefs(pObj);
            iInput = i;
        }
    assert( iInput >= 0 );
    return iInput;
}

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

  Synopsis    [Derives AIG whose PI is substituted by a constant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Llb_ManPerformHints( Aig_Man_t * pAig, int nHintDepth )
{
    Aig_Man_t * pNew, * pTemp;
    int i, iInput;
    pNew = Aig_ManDupDfs( pAig );
    for ( i = 0; i < nHintDepth; i++ )
    {
        iInput = Llb_ManMaxFanoutCi( pNew );
        Abc_Print( 1, "%d %3d\n", i, iInput );
        pNew = Aig_ManDupCof( pTemp = pNew, iInput, 1 );
        Aig_ManStop( pTemp );
    }
    return pNew;
}

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

  Synopsis    [Returns CI index with the largest number of fanouts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int fCisOnly )
{
    Vec_Int_t * vFanouts, * vResult;
    Aig_Obj_t * pObj; 
    int i, fChanges, PivotValue;
//    int Entry;
    // collect fanout counts
    vFanouts = Vec_IntAlloc( 100 );
    Aig_ManForEachObj( pAig, pObj, i )
    {
//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
        if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
            continue;
        Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) );
    }
    Vec_IntSort( vFanouts, 1 );
    // pick the separator
    nCandMax = Abc_MinInt( nCandMax, Vec_IntSize(vFanouts) - 1 );
    PivotValue = Vec_IntEntry( vFanouts, nCandMax );
    Vec_IntFree( vFanouts );
    // collect obj satisfying the constraints
    vResult = Vec_IntAlloc( 100 );
    Aig_ManForEachObj( pAig, pObj, i )
    {
//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
        if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
            continue;
        if ( Aig_ObjRefs(pObj) < PivotValue )
            continue;
        Vec_IntPush( vResult, Aig_ObjId(pObj) );
    }
    assert( Vec_IntSize(vResult) >= nCandMax );
    // order in the decreasing order of fanouts
    do
    {
        fChanges = 0;
        for ( i = 0; i < Vec_IntSize(vResult) - 1; i++ )
            if ( Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i))) < 
                 Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i+1))) )
            {
                int Temp = Vec_IntEntry( vResult, i );
                Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vResult, i+1) );
                Vec_IntWriteEntry( vResult, i+1, Temp );
                fChanges = 1;
            }
    }
    while ( fChanges );
/*
    Vec_IntForEachEntry( vResult, Entry, i )
        printf( "%d ", Aig_ObjRefs(Aig_ManObj(pAig, Entry)) );
printf( "\n" );
*/
    return vResult;
}

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

  Synopsis    [Derives AIG whose PI is substituted by a constant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars )
{
    DdManager * ddGlo = NULL;
    Vec_Int_t * vHints;
    Vec_Int_t * vHFCands;
    int i, Entry, RetValue = -1;
    abctime clk = Abc_Clock();
    assert( pPars->nHintDepth > 0 );
/*
    // perform reachability without hints
    RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL );
    if ( RetValue >= 0 )
        return RetValue;
*/
    // create hints representation
    vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 );
    vHints   = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) );
    // add one hint at a time till the problem is solved
    Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst )
    {
        Vec_IntWriteEntry( vHints, Entry, 1 );   // change to 1 to start from zero cof!!!
        // solve under hints
        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
        if ( RetValue == 0 )
            goto Finish;
        if ( RetValue == 1 )
            break;
    }
    if ( RetValue == -1 )
        goto Finish;
    // undo the hints one at a time
    for ( ; i >= pPars->HintFirst; i-- )
    {
        Entry = Vec_IntEntry( vHFCands, i );
        Vec_IntWriteEntry( vHints, Entry, -1 );        
        // solve under relaxed hints
        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
        if ( RetValue == 0 )
            goto Finish;
        if ( RetValue == 1 )
            continue;
        break;
    }
Finish:
    if ( ddGlo )
    {
        if ( ddGlo->bFunc )
            Cudd_RecursiveDeref( ddGlo, ddGlo->bFunc ); 
        Extra_StopManager( ddGlo );
    }
    Vec_IntFreeP( &vHFCands );
    Vec_IntFreeP( &vHints );
    if ( pPars->fVerbose )
        Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk );
    return RetValue;
}


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


ABC_NAMESPACE_IMPL_END