diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 06:49:49 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 06:49:49 +0700 |
| commit | 853222ee7bf8e1f79120666707ce754cd9169564 (patch) | |
| tree | 5bebbb9245ee6b46895697614072aef47da8aec4 /src/proof | |
| parent | edd4b2a29c3a75709b6394fd205384dd0fe90e5d (diff) | |
| download | abc-853222ee7bf8e1f79120666707ce754cd9169564.tar.gz abc-853222ee7bf8e1f79120666707ce754cd9169564.tar.bz2 abc-853222ee7bf8e1f79120666707ce754cd9169564.zip | |
Fixed a corner-case when 'sim3 -a' does not work for costant POs.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 32 |
1 files changed, 27 insertions, 5 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index d2c6451e..67501d97 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -432,6 +432,28 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) SeeAlso [] ***********************************************************************/ +int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj ) +{ + Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; + word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); + int w; + for ( w = 0; w < p->nWords; w++ ) + if ( pSim[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj ) { Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; @@ -558,7 +580,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFr break; if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; - if ( Ssw_RarManObjIsConst(p, pObj) ) + if ( Ssw_RarManPoIsConst0(p, pObj) ) continue; RetValue = 1; p->iFailPo = i; @@ -936,11 +958,11 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in assert( Aig_ManConstrNum(pAig) == 0 ); ABC_FREE( pAig->pSeqModel ); // consider the case of empty AIG - if ( Aig_ManNodeNum(pAig) == 0 ) - return -1; +// if ( Aig_ManNodeNum(pAig) == 0 ) +// return -1; // check trivially SAT miters - if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) - return 0; +// if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) +// return 0; if ( fVerbose ) Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", nWords, nFrames, nRounds, nRandSeed, TimeOut ); |