diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 13:48:48 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 13:48:48 -0800 |
| commit | a2df331852bb86830ff6df726a92396497a0deed (patch) | |
| tree | bc89c866667b07eb5b39e276d03b6991e8dcf2df /src/aig/gia | |
| parent | 7a87f20c18f042fe4e8679d08227eb8f5ca34b84 (diff) | |
| download | abc-a2df331852bb86830ff6df726a92396497a0deed.tar.gz abc-a2df331852bb86830ff6df726a92396497a0deed.tar.bz2 abc-a2df331852bb86830ff6df726a92396497a0deed.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index cd499a75..8577a2d6 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1366,7 +1366,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) if ( f == p->nWords * 32 ) p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords ); // check this timeframe - i = 0; + i = 0; if ( f < p->pPars->nFramesStart ) Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 ); else @@ -1380,7 +1380,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i ); // iterate as long as there are counter-examples for ( i = 0; ; i++ ) - { + { clk2 = clock(); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); assert( (vCore != NULL) == (Status == 1) ); @@ -1410,7 +1410,6 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Vga_ManRollBack( p, nObjOld ); Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 ); // load this timeframe - nObjOld = p->nObjs; Vga_ManLoadSlice( p, vCore, 0 ); Vec_IntFree( vCore ); } |