From b2da2c3dc7a1b1ba2b44f51e5ef37d06c846a945 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Jul 2012 14:44:14 -0700 Subject: Other improvements to &vta and &gla. --- src/aig/gia/giaAbsGla.c | 19 +++++++++++-------- src/aig/gia/giaAbsVta.c | 17 ++++++++++------- 2 files changed, 21 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index f6ada0c8..cdfc7712 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1925,14 +1925,17 @@ finish: p->pPars->iFrame = pCex->iFrame - 1; } Abc_PrintTime( 1, "Time", clock() - clk ); - p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; - ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk ); - ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); - ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); - ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); - ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); - ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); - Gla_ManReportMemory( p ); + if ( p->pPars->fVerbose ) + { + p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; + ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + Gla_ManReportMemory( p ); + } Gla_ManStop( p ); fflush( stdout ); return RetValue; diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 1a442a79..e762c112 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1816,13 +1816,16 @@ finish: } Abc_PrintTime( 1, "Time", clock() - clk ); - p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; - ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); - ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); - ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); - ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); - ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); - Gia_VtaPrintMemory( p ); + if ( p->pPars->fVerbose ) + { + p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + Gia_VtaPrintMemory( p ); + } Vga_ManStop( p ); fflush( stdout ); -- cgit v1.2.3