llb1Hint.c

Go to the documentation of this file.

 
#include "llbInt.h"
 
ABC_NAMESPACE_IMPL_START
 



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;
}

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;
}

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;
}

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;
}
 

 
 
ABC_NAMESPACE_IMPL_END