diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-01 16:46:40 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-01 16:46:40 -0700 |
| commit | 3fed776860e2b4439ea503dc8d59fb12b5ff5440 (patch) | |
| tree | 42fa939a43a06d9b2d3dd8adc40c544b89d446ff /src/aig/saig | |
| parent | 2140c5d980cafc6d3daece9e6f2e04dc3cc1fb44 (diff) | |
| download | abc-3fed776860e2b4439ea503dc8d59fb12b5ff5440.tar.gz abc-3fed776860e2b4439ea503dc8d59fb12b5ff5440.tar.bz2 abc-3fed776860e2b4439ea503dc8d59fb12b5ff5440.zip | |
Added switch to bmc3, which allows to replace some PIs with constants.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index d82b4c39..453ea918 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1008,12 +1008,12 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) SeeAlso [] ***********************************************************************/ -int Aig_NodeCompareRefsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) +int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) { int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2); - if ( Diff > 0 ) + if ( Diff < 0 ) return -1; - if ( Diff < 0 ) + if ( Diff > 0 ) return 1; return 0; } @@ -1037,16 +1037,23 @@ void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) if ( nPisAbstract < 1 ) return; // sort PIs by the number of their fanouts -// Saig_ManForEachPi( pAig, pObj, i ) -// printf( "%d=%d ", i, Aig_ObjRefs(pObj) ); -// printf( "\n" ); vPis = Vec_PtrAlloc( 100 ); Saig_ManForEachPi( pAig, pObj, i ) Vec_PtrPush( vPis, pObj ); - Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsDecrease ); + Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsIncrease ); Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i ) - if ( i > Saig_ManPiNum(pAig) - nPisAbstract ) + { + if ( i < nPisAbstract ) + { pObj->fMarkA = 1; +// printf( "%d=%d ", Aig_ObjPioNum(pObj), Aig_ObjRefs(pObj) ); + } + } +// printf( "\n" ); + // print primary inputs +// Saig_ManForEachPi( pAig, pObj, i ) +// printf( "%d=%d ", i, Aig_ObjRefs(pObj) ); +// printf( "\n" ); } /**Function************************************************************* @@ -1108,7 +1115,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) if ( p->pPars->nTimeOut ) sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC ); // perform frames -// Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); + Aig_ManRandom( 1 ); + Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); for ( f = 0; f < pPars->nFramesMax; f++ ) { pPars->iFrame = f; @@ -1129,6 +1137,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) if ( f == 0 ) Saig_ManForEachLo( p->pAig, pObj, i ) Saig_ManBmcSetLiteral( p, pObj, 0, 0 ); + // set PIs to zero if they are marked + Saig_ManForEachPi( p->pAig, pObj, i ) + if ( pObj->fMarkA ) + Saig_ManBmcSetLiteral( p, pObj, f, Aig_ManRandom(0) & 1 ); // add the constraints for this frame Saig_ManForEachPo( pAig, pObj, i ) { |