diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 14:18:38 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-12 14:18:38 -0800 |
| commit | b38df9feec7d5858e978a0243d98f362337ac8f1 (patch) | |
| tree | 5829e2feba7f5681fd2c538d482e431c8980910f /src | |
| parent | 814ee4841b4f7ab2edd7cc370632e9677e620e35 (diff) | |
| download | abc-b38df9feec7d5858e978a0243d98f362337ac8f1.tar.gz abc-b38df9feec7d5858e978a0243d98f362337ac8f1.tar.bz2 abc-b38df9feec7d5858e978a0243d98f362337ac8f1.zip | |
Experiment with time reporting in GLA PBA.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/saig/saigGlaPba.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 7b1efbf9..00e04346 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -72,7 +72,7 @@ struct Aig_Gla2Man_t_ ***********************************************************************/ int Abc_Clock( int Timer, int fReset ) { - static Time[16], Clock[16]; + static int Time[16], Clock[16]; int Clock2, Diff; assert( Timer >= 0 && Timer < 16 ); if ( fReset ) @@ -453,7 +453,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo if ( fVerbose ) { printf( "SAT solver returned UNSAT after %7d conflicts. ", pSat->stats.conflicts ); - ABC_PRT( "Time", Abc_Clock(2,0) ); + ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC ); } assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); @@ -465,7 +465,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo if ( fVerbose ) { printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots ); - ABC_PRT( "Time", Abc_Clock(2,0) ); + ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC ); } Sto_ManFree( (Sto_Man_t *)pSatCnf ); return vCore; |