Adding memory report to print-outs produced by &vta and &gla.

This commit is contained in:
Alan Mishchenko 2012-07-07 14:33:54 -07:00
parent e22f5d1246
commit 44f04004fd
2 changed files with 3 additions and 0 deletions

View File

@ -1634,6 +1634,7 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
fflush( stdout );
}

View File

@ -1246,6 +1246,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
for ( k = 0; k < 7; k++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
Abc_Print( 1, "\r" );
}
else
@ -1267,6 +1268,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
Abc_Print( 1, " " );
}
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
Abc_Print( 1, "\n" );
}
fflush( stdout );