diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-29 10:39:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-29 10:39:55 -0700 |
| commit | ccaa96549ff1d5dabbd95fdce4777a104ea9c139 (patch) | |
| tree | 8481ee5a3f0c53aa03f2a65aaba1e429b14226ff /src/aig | |
| parent | bfa48cef2aab9e21f0fe9bd24a0bcfd7ce464686 (diff) | |
| download | abc-ccaa96549ff1d5dabbd95fdce4777a104ea9c139.tar.gz abc-ccaa96549ff1d5dabbd95fdce4777a104ea9c139.tar.bz2 abc-ccaa96549ff1d5dabbd95fdce4777a104ea9c139.zip | |
Fixing the problem with 'phase -c'.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaCex.c | 47 |
2 files changed, 48 insertions, 0 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 62b7c89a..052966f7 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -963,6 +963,7 @@ extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ); /*=== giaCex.c ============================================================*/ extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); +extern int Gia_ManSetFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ); extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ); extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ); extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ); diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c index fdc0c709..5a8125f3 100644 --- a/src/aig/gia/giaCex.c +++ b/src/aig/gia/giaCex.c @@ -121,6 +121,53 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) return RetValue; } +/**Function************************************************************* + + Synopsis [Determines the failed PO when its exact frame is not known.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSetFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ) +{ + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int i, k, iBit = 0; + assert( Gia_ManPiNum(pAig) == p->nPis ); + Gia_ManCleanMark0(pAig); + p->iPo = -1; +// Gia_ManForEachRo( pAig, pObj, i ) +// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + iBit = p->nRegs; + for ( i = 0; i <= p->iFrame; i++ ) + { + Gia_ManForEachPi( pAig, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); + Gia_ManForEachAnd( pAig, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( pAig, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + // check the POs + Gia_ManForEachPo( pAig, pObj, k ) + { + if ( !pObj->fMark0 ) + continue; + p->iPo = k; + p->iFrame = i; + p->nBits = iBit; + break; + } + } + Gia_ManCleanMark0(pAig); + return p->iPo; +} + /**Function************************************************************* |