Commit 8de10802 by Alan Mishchenko

Updates for the new BMC engine.

parent e9d04664
...@@ -32966,7 +32966,7 @@ usage: ...@@ -32966,7 +32966,7 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Gia_Man_t * pTemp = NULL; // Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0; int c, fVerbose = 0;
int nFrames = 10; int nFrames = 10;
int fSwitch = 0; int fSwitch = 0;
...@@ -89,14 +89,16 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ...@@ -89,14 +89,16 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{ {
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "Frame %4d : Trivally UNSAT. Memory = %5.1f Mb ", f, Gia_ManMemory(pFrames) ); printf( "Frame %4d : AIG =%9d. Trivally UNSAT. Memory = %5.1f Mb ",
f, Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
} }
continue; continue;
} }
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "Frame %4d : AIG =%9d. Memory = %5.1f Mb ", f, Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) ); printf( "Frame %4d : AIG =%9d. And =%9d. Memory = %5.1f Mb ",
f, Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
} }
if ( ++Counter == 10 ) if ( ++Counter == 10 )
......
...@@ -166,7 +166,7 @@ void Bmc_LadStop( Bmc_Lad_t * p ) ...@@ -166,7 +166,7 @@ void Bmc_LadStop( Bmc_Lad_t * p )
***********************************************************************/ ***********************************************************************/
void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{ {
int nConfLimit = 0; // int nConfLimit = 0;
Bmc_Lad_t * p; Bmc_Lad_t * p;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, status, Lit; int i, status, Lit;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment