diff options
Diffstat (limited to 'src/aig/saig/saigGlaPba.c')
-rw-r--r-- | src/aig/saig/saigGlaPba.c | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 5834db76..cdbc05c7 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -432,11 +432,10 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo Vec_Int_t * vCore; void * pSatCnf; Intp_Man_t * pManProof; - int RetValue; + int RetValue, clk = clock(); if ( piRetValue ) *piRetValue = -1; // solve the problem - Abc_Clock(2,1); RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_Undef ) { @@ -453,19 +452,19 @@ 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_CPS)*CLOCKS_PER_SEC ); + Abc_PrintTime( 1, "Time", clock() - clk ); } assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); // derive the UNSAT core - Abc_Clock(2,1); + clk = clock(); pManProof = Intp_ManAlloc(); vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 ); Intp_ManFree( pManProof ); 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_CPS)*CLOCKS_PER_SEC ); + printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) ); + Abc_PrintTime( 1, "Time", clock() - clk ); } Sto_ManFree( (Sto_Man_t *)pSatCnf ); return vCore; @@ -561,7 +560,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in int clk, clk2 = clock(); assert( Saig_ManPoNum(pAig) == 1 ); - Abc_Clock(0,1); if ( fVerbose ) { if ( TimeLimit ) @@ -572,7 +570,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in // start the solver clk = clock(); - Abc_Clock(1,1); p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose ); if ( !Aig_Gla2CreateSatSolver( p ) ) { @@ -581,7 +578,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in return NULL; } sat_solver_set_random( p->pSat, fSkipRand ); -// p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; p->timePre += clock() - clk; // set runtime limit @@ -590,15 +586,12 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in // compute UNSAT core clk = clock(); - Abc_Clock(1,1); vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); if ( vCore == NULL ) { Aig_Gla2ManStop( p ); return NULL; } -// p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; -// p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC; p->timeSat += clock() - clk; p->timeTotal += clock() - clk2; |