From 7e486af8323d447395c9d31b508d5f5926863f34 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 27 Jul 2012 15:59:20 -0700 Subject: Minor updates to the BMC engines. --- src/aig/gia/giaAbsGla2.c | 3 +++ src/aig/gia/giaMan.c | 2 ++ src/aig/saig/saigBmc2.c | 3 ++- src/aig/saig/saigBmc3.c | 46 ++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 51 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 17fb5d87..88ea6f5f 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -26,6 +26,7 @@ ABC_NAMESPACE_IMPL_START +#if 0 //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1142,6 +1143,8 @@ finish: return RetValue; } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index b8a8afb8..a0208376 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -443,6 +443,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch ) Gia_ManPrintObjClasses( p ); if ( fTents ) { +/* int k, Entry, Prev = 1; Vec_Int_t * vLimit = Vec_IntAlloc( 1000 ); Gia_Man_t * pNew = Gia_ManUnrollDup( p, vLimit ); @@ -453,6 +454,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch ) printf( "\n" ); Vec_IntFree( vLimit ); Gia_ManStop( pNew ); +*/ Gia_ManPrintTents( p ); } } diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 94c8d2c0..a1dee6e4 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -469,10 +469,11 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited ); Vec_PtrPush( p->vTargets, pTarget ); Aig_ObjCreateCo( p->pFrm, pTarget ); - Aig_ManCleanup( p->pFrm ); + Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!! // check if the node is gone Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i ) Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame ); + // it is not efficient to remove nodes, which may be used later!!! } } } diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 2fbe88de..bb59f677 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -38,6 +38,7 @@ struct Gia_ManBmc_t_ Vec_Ptr_t * vCexes; // counter-examples // intermediate data Vec_Int_t * vMapping; // mapping + Vec_Int_t * vMapRefs; // mapping references Vec_Vec_t * vSects; // sections Vec_Int_t * vId2Num; // number of each node Vec_Ptr_t * vTerInfo; // ternary information @@ -50,7 +51,9 @@ struct Gia_ManBmc_t_ int nHashOver; int nBufNum; // the number of simple nodes int nDupNum; // the number of simple nodes - int nUniProps; // propagating learned clause values + int nUniProps; // propagating learned clause values + int nLitUsed; // used literals + int nLitUseless; // useless literals // SAT solver sat_solver * pSat; // SAT solver int nSatVars; // SAT variables @@ -655,6 +658,36 @@ void Saig_ManBmcMappingTest( Aig_Man_t * p ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap ) +{ + Vec_Int_t * vRefs; + Aig_Obj_t * pObj; + int i, iFan, * pData; + vRefs = Vec_IntStart( Aig_ManObjNumMax(p) ); + Aig_ManForEachCo( p, pObj, i ) + Vec_IntAddToEntry( vRefs, Aig_ObjFaninId0(pObj), 1 ); + Aig_ManForEachNode( p, pObj, i ) + { + if ( Vec_IntEntry(vMap, i) == 0 ) + continue; + pData = Vec_IntEntryP( vMap, Vec_IntEntry(vMap, i) ); + for ( iFan = 0; iFan < 4; iFan++ ) + if ( pData[iFan+1] >= 0 ) + Vec_IntAddToEntry( vRefs, pData[iFan+1], 1 ); + } + return vRefs; +} /**Function************************************************************* @@ -677,6 +710,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) p->pAig = pAig; // create mapping p->vMapping = Cnf_DeriveMappingArray( pAig ); + p->vMapRefs = Saig_ManBmcComputeMappingRefs( pAig, p->vMapping ); // create sections p->vSects = Saig_ManBmcSections( pAig ); // map object IDs into their numbers and section numbers @@ -730,6 +764,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) } // Vec_PtrFreeFree( p->vCexes ); Vec_IntFree( p->vMapping ); + Vec_IntFree( p->vMapRefs ); Vec_VecFree( p->vSects ); Vec_IntFree( p->vId2Num ); Vec_VecFree( (Vec_Vec_t *)p->vId2Var ); @@ -803,6 +838,12 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) ); vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame ); Vec_IntWriteEntry( vFrame, ObjNum, iLit ); +/* + if ( Vec_IntEntry( p->vMapRefs, Aig_ObjId(pObj) ) > 1 ) + p->nLitUsed++; + else + p->nLitUseless++; +*/ return iLit; } @@ -1478,7 +1519,7 @@ clkOther += clock() - clk2; return RetValue; } } - if ( pPars->fVerbose ) + if ( pPars->fVerbose ) { if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 ) { @@ -1495,6 +1536,7 @@ clkOther += clock() - clk2; // printf( "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) ); printf( "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) ); printf( "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); +// printf( " %6d %6d ", p->nLitUsed, p->nLitUseless ); printf( "%9.2f sec ", 1.0*(clock() - clkTotal)/CLOCKS_PER_SEC ); // printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); -- cgit v1.2.3