diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 23:17:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-28 23:17:31 -0800 |
| commit | 5e91f13247eddd977fdf6339fde5e7cef997aaf5 (patch) | |
| tree | bad1ba180871d2bfdfb51297240b98d4b026ea59 /src | |
| parent | 095bf1c91bba6323cf6aae960fc386dc50066f5d (diff) | |
| download | abc-5e91f13247eddd977fdf6339fde5e7cef997aaf5.tar.gz abc-5e91f13247eddd977fdf6339fde5e7cef997aaf5.tar.bz2 abc-5e91f13247eddd977fdf6339fde5e7cef997aaf5.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 9 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 6 |
2 files changed, 8 insertions, 7 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index db79550b..472257b2 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1161,10 +1161,10 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nC // printf( "%5d%5d", pCountAll[0], pCountUni[0] ); printf( "%6d", p->nSeenGla ); printf( "%5d", nCexes ); - printf( "%6d", pCountAll[0] ); + printf( "%7d", pCountAll[0] ); for ( k = 0; k < nFrames; k++ ) // printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); - printf( "%4d", pCountAll[k+1] ); + printf( "%5d", pCountAll[k+1] ); printf( "\n" ); fflush( stdout ); } @@ -1356,7 +1356,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p = Vga_ManStart( pAig, pPars ); // perform initial abstraction if ( p->pPars->fVerbose ) - printf( "Frame Confl One Cex All F0 F1 F2 F3 ...\n" ); + printf( "Frame Confl One Cex All F0 F1 F2 F3 ...\n" ); for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) { if ( p->pPars->fVerbose ) @@ -1369,6 +1369,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) i = 0; if ( f < p->pPars->nFramesStart ) { +// printf( " Adding %8d ", Vec_IntSize(Vec_PtrEntry(p->vFrames, f)) ); Vga_ManAddClausesOne( p, 0, f ); Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 ); } @@ -1421,7 +1422,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); p->timeUnsat += clock() - clk2; if ( p->pPars->fVerbose ) - printf( "%5d", nConfls ); + printf( "%6d", nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached break; diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 972958bb..fd8bb062 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -278,7 +278,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) nObjMask = (1 << nObjBits) - 1; assert( Gia_ManObjNum(p) <= nObjMask ); // print info about frames - printf( "Frame All F0 F1 F2 F3 ...\n" ); + printf( "Frame All F0 F1 F2 F3 ...\n" ); for ( i = 0; i < nFrames; i++ ) { iStart = Vec_IntEntry( vAbs, i+1 ); @@ -302,11 +302,11 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) assert( pCountAll[0] == (iStop - iStart) ); // printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); printf( "%3d :", i ); - printf( "%6d", pCountAll[0] ); + printf( "%7d", pCountAll[0] ); for ( k = 0; k < nFrames; k++ ) if ( k <= i ) // printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] ); - printf( "%4d", pCountAll[k+1] ); + printf( "%5d", pCountAll[k+1] ); printf( "\n" ); } assert( iStop == Vec_IntSize(vAbs) ); |