diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 16:10:50 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 16:10:50 -0700 |
| commit | 92c7c6f7e5a3a66f7876498ef4027d7bc7105b0d (patch) | |
| tree | 95b74f34b4b0a85dbd1ee120d0be05b3d380f467 | |
| parent | 61126bfba4e9d0b9e474078c78cb60be3eeda68f (diff) | |
| download | abc-92c7c6f7e5a3a66f7876498ef4027d7bc7105b0d.tar.gz abc-92c7c6f7e5a3a66f7876498ef4027d7bc7105b0d.tar.bz2 abc-92c7c6f7e5a3a66f7876498ef4027d7bc7105b0d.zip | |
Updates for the new BMC engine.
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 89935b17..51239d7d 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -75,7 +75,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Gia_Man_t * pFrames; abctime clk = Abc_Clock(); int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY; - int i, f, iStart, status = -1, Counter = 0; + int i, f, iStart, status = -1;//, Counter = 0; p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose ); for ( f = 0; f < nFramesMax; f++ ) { @@ -89,7 +89,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { if ( pPars->fVerbose ) { - printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%6.1f Mb ", + printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%7.1f Mb ", f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } @@ -97,13 +97,19 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) } if ( pPars->fVerbose ) { - printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%6.1f Mb ", + printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%7.1f Mb ", f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } // if ( ++Counter == 10 ) // break; } + // dump unfolded frames + pFrames = Gia_ManCleanup( pFrames ); + Gia_AigerWrite( pFrames, "frames.aig", 0, 0 ); + printf( "Dumped unfolded frames into file \"frames.aig\".\n" ); + Gia_ManStop( pFrames ); + // cleanup Unr_ManFree( p ); return status; } |