diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/cec/cecSeq.c | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 8 | ||||
| -rw-r--r-- | src/aig/saig/saig.h | 1 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 59 |
4 files changed, 63 insertions, 9 deletions
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 0e49cd7c..e9f3df37 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -242,8 +242,8 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex Vec_PtrFree( vSimInfo ); if ( pPars->fVerbose ) ABC_PRT( "Time", clock() - clkTotal ); - if ( RetValue && pPars->fCheckMiter ) - Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); +// if ( RetValue && pPars->fCheckMiter ) +// Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); return RetValue; } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 125f3592..d94a0412 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1191,9 +1191,11 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; + assert( Gia_ManPiNum(pAig) == p->nPis ); Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); +// Gia_ManForEachRo( pAig, pObj, i ) +// pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) @@ -1207,7 +1209,7 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) pObjRo->fMark0 = pObjRi->fMark0; } assert( iBit == p->nBits ); - // remember the number of failed output + // figure out the number of failed output RetValue = -1; for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- ) { diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 62ac35ac..c21ac625 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -62,6 +62,7 @@ struct Saig_ParBmc_t_ int nFramesMax; // maximum number of timeframes int nConfLimit; // maximum number of conflicts at a node int nTimeOut; // approximate timeout in seconds + int nPisAbstract; // the number of PIs to abstract int fSolveAll; // does not stop at the first SAT output int fDropSatOuts; // replace sat outputs by constant 0 int fVerbose; // verbose diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index e038d7a0..d82b4c39 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -551,10 +551,6 @@ void Saig_ManBmcMappingTest( Aig_Man_t * p ) - - - - /**Function************************************************************* Synopsis [Create manager.] @@ -613,6 +609,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) ***********************************************************************/ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) { + Aig_ManCleanMarkA( p->pAig ); if ( p->vCexes ) { assert( p->pAig->pSeqModelVec == NULL ); @@ -1002,6 +999,58 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) /**Function************************************************************* + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeCompareRefsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) +{ + int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2); + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Mark PIs to be skipped based on nPisAbstract.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) +{ + Vec_Ptr_t * vPis; + Aig_Obj_t * pObj; + int i; + 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_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i ) + if ( i > Saig_ManPiNum(pAig) - nPisAbstract ) + pObj->fMarkA = 1; +} + +/**Function************************************************************* + Synopsis [This procedure sets default parameters.] Description [] @@ -1018,6 +1067,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->nFramesMax = 2000; // maximum number of timeframes p->nConfLimit = 2000; // maximum number of conflicts at a node p->nTimeOut = 0; // approximate timeout in seconds + p->nPisAbstract = 0; // the number of PIs to abstract p->fSolveAll = 0; // stops on the first SAT instance p->fDropSatOuts = 0; // replace sat outputs by constant 0 p->fVerbose = 0; // verbose @@ -1058,6 +1108,7 @@ 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 ); for ( f = 0; f < pPars->nFramesMax; f++ ) { pPars->iFrame = f; |