diff options
Diffstat (limited to 'src/proof/llb/llb1Hint.c')
| -rw-r--r-- | src/proof/llb/llb1Hint.c | 226 |
1 files changed, 0 insertions, 226 deletions
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c deleted file mode 100644 index 353b4c69..00000000 --- a/src/proof/llb/llb1Hint.c +++ /dev/null @@ -1,226 +0,0 @@ -/**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 - |