Commit 825bcd82 by Alan Mishchenko

Added code to collect experimental results.

parent 4c06c8af
...@@ -1537,7 +1537,6 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl ...@@ -1537,7 +1537,6 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
} }
void Gla_ManReportMemory( Gla_Man_t * p ) void Gla_ManReportMemory( Gla_Man_t * p )
{ {
extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
Gla_Obj_t * pGla; Gla_Obj_t * pGla;
double memTot = 0; double memTot = 0;
double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t); double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
...@@ -1559,7 +1558,6 @@ void Gla_ManReportMemory( Gla_Man_t * p ) ...@@ -1559,7 +1558,6 @@ void Gla_ManReportMemory( Gla_Man_t * p )
ABC_PRMP( "Memory: Refine ", memRef, memTot ); ABC_PRMP( "Memory: Refine ", memRef, memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot ); ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
// Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrame, 1 );
} }
...@@ -1642,6 +1640,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose ) ...@@ -1642,6 +1640,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
{ {
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN );
Gla_Man_t * p; Gla_Man_t * p;
Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL; Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
Abc_Cex_t * pCex = NULL; Abc_Cex_t * pCex = NULL;
...@@ -1944,6 +1943,7 @@ finish: ...@@ -1944,6 +1943,7 @@ finish:
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Gla_ManReportMemory( p ); Gla_ManReportMemory( p );
} }
Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 );
Gla_ManStop( p ); Gla_ManStop( p );
fflush( stdout ); fflush( stdout );
return RetValue; return RetValue;
......
...@@ -415,7 +415,7 @@ void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSa ...@@ -415,7 +415,7 @@ void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSa
char pFileName[32]; char pFileName[32];
sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" ); sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" );
pFile = fopen( pFileName, "wb+" ); pFile = fopen( pFileName, "a+" );
fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d", fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d",
pGia->pName, pGia->pName,
...@@ -458,7 +458,6 @@ void Ga2_ManReportMemory( Ga2_Man_t * p ) ...@@ -458,7 +458,6 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
ABC_PRMP( "Memory: Hash ", memHash,memTot ); ABC_PRMP( "Memory: Hash ", memHash,memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot ); ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot ); ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
// Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
} }
void Ga2_ManStop( Ga2_Man_t * p ) void Ga2_ManStop( Ga2_Man_t * p )
{ {
...@@ -1822,6 +1821,7 @@ finish: ...@@ -1822,6 +1821,7 @@ finish:
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Ga2_ManReportMemory( p ); Ga2_ManReportMemory( p );
} }
Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
Ga2_ManStop( p ); Ga2_ManStop( p );
fflush( stdout ); fflush( stdout );
return RetValue; return RetValue;
......
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