diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 23:03:25 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 23:03:25 -0800 |
| commit | 095bf1c91bba6323cf6aae960fc386dc50066f5d (patch) | |
| tree | 1ffa6f111a128ae3a07a7a5de255c9d754f25f61 | |
| parent | 5e1c28338bdab9d941f7c06880e59213256ed812 (diff) | |
| download | abc-095bf1c91bba6323cf6aae960fc386dc50066f5d.tar.gz abc-095bf1c91bba6323cf6aae960fc386dc50066f5d.tar.bz2 abc-095bf1c91bba6323cf6aae960fc386dc50066f5d.zip | |
Variable timeframe abstraction.
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 8577a2d6..db79550b 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1368,7 +1368,10 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // check this timeframe i = 0; if ( f < p->pPars->nFramesStart ) + { + Vga_ManAddClausesOne( p, 0, f ); Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 ); + } else { // create bookmark to be used for rollback @@ -1421,12 +1424,14 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) printf( "%5d", nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached - goto finish; + break; if ( Status == 0 ) { + Vta_ManSatVerify( p ); // make sure, there was no initial abstraction (otherwise, it was invalid) assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); pCex = Vga_ManDeriveCex( p ); + break; } // add the core Vta_ManUnsatCoreRemap( p, vCore ); @@ -1455,7 +1460,7 @@ finish: ABC_FREE( p->pGia->pCexSeq ); p->pGia->pCexSeq = pCex; if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) ) - printf( "Gia_VtaPerform(): CEX verification has failed!\n" ); + printf( " Gia_VtaPerform(): CEX verification has failed!\n" ); printf( "Counter-example detected in frame %d. ", f ); } Abc_PrintTime( 1, "Time", clock() - clk ); |