diff options
Diffstat (limited to 'src/aig/gia/giaCex.c')
-rw-r--r-- | src/aig/gia/giaCex.c | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c index 58415f73..fdc0c709 100644 --- a/src/aig/gia/giaCex.c +++ b/src/aig/gia/giaCex.c @@ -241,6 +241,101 @@ void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex ) } +/**Function************************************************************* + + Synopsis [Returns CEX containing PI+CS values for each timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex ) +{ + Abc_Cex_t * pNew; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int i, k, iBit = 0; + assert( pCex->nRegs > 0 ); + // start the counter-example + pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 ); + pNew->iFrame = pCex->iFrame; + pNew->iPo = pCex->iPo; + // set const0 + Gia_ManConst0(p)->fMark0 = 0; + // set init state + Gia_ManForEachRi( p, pObjRi, k ) + pObjRi->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + assert( iBit == pCex->nRegs ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + Gia_ManForEachCi( p, pObj, k ) + if ( pObj->fMark0 ) + Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k ); + Gia_ManForEachAnd( p, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( p, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + } + assert( iBit == pCex->nBits ); + assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 ); + Gia_ManCleanMark0(p); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns CEX containing all object valuess for each timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex ) +{ + Abc_Cex_t * pNew; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int i, k, iBit = 0; + assert( pCex->nRegs > 0 ); + // start the counter-example + pNew = Abc_CexAlloc( 0, Gia_ManObjNum(p), pCex->iFrame + 1 ); + pNew->iFrame = pCex->iFrame; + pNew->iPo = pCex->iPo; + // set const0 + Gia_ManConst0(p)->fMark0 = 0; + // set init state + Gia_ManForEachRi( p, pObjRi, k ) + pObjRi->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + assert( iBit == pCex->nRegs ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + Gia_ManForEachObj( p, pObj, k ) + if ( pObj->fMark0 ) + Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k ); + Gia_ManForEachAnd( p, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( p, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + } + assert( iBit == pCex->nBits ); + assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 ); + Gia_ManCleanMark0(p); + return pNew; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |