From cc6da1f905ef1dd4fc25860c1ed8df02f676bf61 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 8 Sep 2012 00:19:46 -0700 Subject: Updating &gla_refine to perform suffix refinement. --- src/aig/gia/giaAbsOut.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c index 65df1073..bdcf754e 100644 --- a/src/aig/gia/giaAbsOut.c +++ b/src/aig/gia/giaAbsOut.c @@ -259,8 +259,8 @@ Vec_Int_t * Gia_ManGetStateAndCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFr assert( iFrame >= 0 && iFrame <= p->iFrame ); Gia_ManCleanMark0(pAig); Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - for ( i = 0; i <= p->iFrame; i++ ) + pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++); + for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ ) { if ( i == iFrame ) { @@ -305,8 +305,8 @@ void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame ) assert( iFrame >= 0 && iFrame <= p->iFrame ); Gia_ManCleanMark0(pAig); Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); - for ( i = iFrame, iBit += Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ ) + pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++); + for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); @@ -388,8 +388,8 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra ); // derive abstraction pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); -// Gia_ManStop( pAbs ); -// pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); + Gia_ManStop( pAbs ); + pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); if ( Gia_ManPiNum(pAbs) != pCex->nPis ) { Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" ); -- cgit v1.2.3