diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-08 15:04:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-08 15:04:00 -0700 |
commit | 519b9fdf7ceab41c44828adc633322a3ae3e363b (patch) | |
tree | 297384376b2f65329cb823fd21a8078e49de156d /src | |
parent | 002117c0e9bd45c9cc0f623a72a3a1a368034fd2 (diff) | |
download | abc-519b9fdf7ceab41c44828adc633322a3ae3e363b.tar.gz abc-519b9fdf7ceab41c44828adc633322a3ae3e363b.tar.bz2 abc-519b9fdf7ceab41c44828adc633322a3ae3e363b.zip |
Updating &gla_refine to perform suffix refinement.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAbsOut.c | 22 |
2 files changed, 15 insertions, 9 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 7cd6abb4..7c7afc40 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1781,7 +1781,7 @@ finish: Abc_Print( 1, "\n" ); if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); - Abc_Print( 1, "Counter-example detected in frame %d. ", f ); + Abc_Print( 1, "True counter-example detected in frame %d. ", f ); p->pPars->iFrame = f - 1; Vec_IntFreeP( &pAig->vGateClasses ); RetValue = 0; diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c index bdcf754e..cfaf0283 100644 --- a/src/aig/gia/giaAbsOut.c +++ b/src/aig/gia/giaAbsOut.c @@ -324,9 +324,9 @@ void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame ) RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; Gia_ManCleanMark0(pAig); if ( RetValue == 1 ) - printf( "CEX holds for the transformed model.\n" ); + printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" ); else - printf( "CEX does not hold for the transformed model.\n" ); + printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" ); } /**Function************************************************************* @@ -376,7 +376,8 @@ Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose ) { Gia_Man_t * pAbs, * pNew; - Vec_Int_t * vPis, * vPPis, * vFlops, * vInit; + Vec_Int_t * vFlops, * vInit; + Vec_Int_t * vCopy; clock_t clk = clock(); int RetValue; ABC_FREE( p->pCexSeq ); @@ -385,6 +386,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" ); return -1; } + vCopy = Vec_IntDup( p->vGateClasses ); 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 ); @@ -394,6 +396,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra { Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" ); Gia_ManStop( pAbs ); + Vec_IntFree( vCopy ); return -1; } // get the state in frame iFrameStart @@ -402,30 +405,27 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra { Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" ); Gia_ManStop( pAbs ); + Vec_IntFree( vCopy ); return -1; } if ( fVerbose ) Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" ); // get inputs - Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, NULL ); + Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL ); assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); Gia_ManStop( pAbs ); //Vec_IntPrint( vFlops ); //Vec_IntPrint( vInit ); // transform the manager to have new init state pNew = Gia_ManTransformFlops( p, vFlops, vInit ); - Vec_IntFree( vPis ); - Vec_IntFree( vPPis ); Vec_IntFree( vFlops ); Vec_IntFree( vInit ); // verify abstraction -/* { Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses ); Gia_ManCheckCex( pAbs, pCex, iFrameStart ); Gia_ManStop( pAbs ); } -*/ // transfer abstraction assert( pNew->vGateClasses == NULL ); pNew->vGateClasses = Vec_IntDup( p->vGateClasses ); @@ -436,6 +436,11 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra; pPars->fVerbose = fVerbose; RetValue = Ga2_ManPerform( pNew, pPars ); + if ( RetValue == 0 ) // spurious SAT + { + Vec_IntFreeP( &pNew->vGateClasses ); + pNew->vGateClasses = Vec_IntDup( vCopy ); + } } // move the abstraction map Vec_IntFreeP( &p->vGateClasses ); @@ -443,6 +448,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra pNew->vGateClasses = NULL; // cleanup Gia_ManStop( pNew ); + Vec_IntFree( vCopy ); return -1; } |