Commit b2da2c3d by Alan Mishchenko

Other improvements to &vta and &gla.

parent 8b0302cd
...@@ -1925,14 +1925,17 @@ finish: ...@@ -1925,14 +1925,17 @@ finish:
p->pPars->iFrame = pCex->iFrame - 1; p->pPars->iFrame = pCex->iFrame - 1;
} }
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; if ( p->pPars->fVerbose )
ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk ); {
ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk );
ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk );
ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk );
Gla_ManReportMemory( p ); ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Gla_ManReportMemory( p );
}
Gla_ManStop( p ); Gla_ManStop( p );
fflush( stdout ); fflush( stdout );
return RetValue; return RetValue;
......
...@@ -1816,13 +1816,16 @@ finish: ...@@ -1816,13 +1816,16 @@ finish:
} }
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; if ( p->pPars->fVerbose )
ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); {
ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk );
ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk );
Gia_VtaPrintMemory( p ); ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Gia_VtaPrintMemory( p );
}
Vga_ManStop( p ); Vga_ManStop( p );
fflush( stdout ); fflush( stdout );
......
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