diff options
Diffstat (limited to 'src/proof/abs')
-rw-r--r-- | src/proof/abs/absGla.c | 72 | ||||
-rw-r--r-- | src/proof/abs/absGlaOld.c | 62 | ||||
-rw-r--r-- | src/proof/abs/absIter.c | 8 | ||||
-rw-r--r-- | src/proof/abs/absOldCex.c | 16 | ||||
-rw-r--r-- | src/proof/abs/absOldRef.c | 6 | ||||
-rw-r--r-- | src/proof/abs/absOldSat.c | 24 | ||||
-rw-r--r-- | src/proof/abs/absOldSim.c | 6 | ||||
-rw-r--r-- | src/proof/abs/absOut.c | 8 | ||||
-rw-r--r-- | src/proof/abs/absRef.c | 18 | ||||
-rw-r--r-- | src/proof/abs/absRef.h | 8 | ||||
-rw-r--r-- | src/proof/abs/absRpm.c | 4 | ||||
-rw-r--r-- | src/proof/abs/absVta.c | 58 |
12 files changed, 145 insertions, 145 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 4063757c..5daa953f 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -73,12 +73,12 @@ struct Ga2_Man_t_ Vec_Int_t * vIsopMem; char * pSopSizes, ** pSops; // CNF representation // statistics - clock_t timeStart; - clock_t timeInit; - clock_t timeSat; - clock_t timeUnsat; - clock_t timeCex; - clock_t timeOther; + abctime timeStart; + abctime timeInit; + abctime timeSat; + abctime timeUnsat; + abctime timeCex; + abctime timeOther; }; static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); } @@ -243,7 +243,7 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple ) { static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; -// clock_t clk = clock(); +// abctime clk = Abc_Clock(); Vec_Int_t * vLeaves; Gia_Obj_t * pObj; int i, k, Leaf, CountMarks; @@ -330,20 +330,20 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple ) Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter CountMarks++; } -// Abc_PrintTime( 1, "Time", clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Vec_IntFree( vLeaves ); Gia_ManCleanValue( p ); return CountMarks; } void Ga2_ManComputeTest( Gia_Man_t * p ) { - clock_t clk; + abctime clk; // unsigned uTruth; Gia_Obj_t * pObj; int i, Counter = 0; - clk = clock(); + clk = Abc_Clock(); Ga2_ManMarkup( p, 5, 0 ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_ManForEachAnd( p, pObj, i ) { if ( !pObj->fPhase ) @@ -355,7 +355,7 @@ void Ga2_ManComputeTest( Gia_Man_t * p ) Counter++; } Abc_Print( 1, "Marked AND nodes = %6d. ", Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } /**Function************************************************************* @@ -373,7 +373,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars ) { Ga2_Man_t * p; p = ABC_CALLOC( Ga2_Man_t, 1 ); - p->timeStart = clock(); + p->timeStart = Abc_Clock(); p->fUseNewLine = 1; // user data p->pGia = pGia; @@ -1366,7 +1366,7 @@ int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd ) SeeAlso [] ***********************************************************************/ -void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, clock_t Time, int fFinal ) +void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal ) { int fUseNewLine = ((fFinal && nCexes) || p->pPars->fVeryVerbose); if ( Abc_FrameIsBatchMode() && !fUseNewLine ) @@ -1502,7 +1502,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) int fUseSecondCore = 1; Ga2_Man_t * p; Vec_Int_t * vCore, * vPPis; - clock_t clk2, clk = clock(); + abctime clk2, clk = Abc_Clock(); int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0; int i, c, f, Lit; pPars->iFrame = -1; @@ -1529,7 +1529,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) } // start the manager p = Ga2_ManStart( pAig, pPars ); - p->timeInit = clock() - clk; + p->timeInit = Abc_Clock() - clk; // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1600,12 +1600,12 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) break; } // perform SAT solving - clk2 = clock(); + clk2 = Abc_Clock(); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( Status == l_True ) // perform refinement { p->nCexes++; - p->timeSat += clock() - clk2; + p->timeSat += Abc_Clock() - clk2; // cancel old one if it was sent if ( Abc_FrameIsBridgeMode() && fOneIsSent ) @@ -1620,14 +1620,14 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) } // perform refinement - clk2 = clock(); + clk2 = Abc_Clock(); Rnm_ManSetRefId( p->pRnm, c ); vPPis = Ga2_ManRefine( p ); - p->timeCex += clock() - clk2; + p->timeCex += Abc_Clock() - clk2; if ( vPPis == NULL ) { if ( pPars->fVerbose ) - Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 ); goto finish; } @@ -1657,13 +1657,13 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Ga2_ManAddToAbs( p, vPPis ); Vec_IntFree( vPPis ); if ( pPars->fVerbose ) - Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 ); + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 ); continue; } - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; if ( Status == l_Undef ) // ran out of resources goto finish; - if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout + if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout goto finish; if ( c == 0 ) { @@ -1706,12 +1706,12 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Vec_IntFree( vCore ); } // run SAT solver - clk2 = clock(); + clk2 = Abc_Clock(); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( Status == l_Undef ) goto finish; assert( Status == l_False ); - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; // derive the core assert( p->pSat->pPrf2 != NULL ); @@ -1734,7 +1734,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) p->pPars->iFrameProved = f; // print statistics if ( pPars->fVerbose ) - Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); + Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 ); // check if abstraction was proved if ( Gia_GlaProveCheck( pPars->fVerbose ) ) { @@ -1817,7 +1817,7 @@ finish: { Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); - if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange ); @@ -1838,16 +1838,16 @@ finish: Vec_IntFreeP( &pAig->vGateClasses ); RetValue = 0; } - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); 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 ); + p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; + ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk ); Ga2_ManReportMemory( p ); } // Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 ); diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c index e2f83e96..70bd2e91 100644 --- a/src/proof/abs/absGlaOld.c +++ b/src/proof/abs/absGlaOld.c @@ -93,11 +93,11 @@ struct Gla_Man_t_ Gia_Man_t * pGia2; Rnm_Man_t * pRnm; // statistics - clock_t timeInit; - clock_t timeSat; - clock_t timeUnsat; - clock_t timeCex; - clock_t timeOther; + abctime timeInit; + abctime timeSat; + abctime timeUnsat; + abctime timeCex; + abctime timeOther; }; // declarations @@ -1447,7 +1447,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon Vec_Int_t * vCore = NULL; int nConfPrev = pSat->stats.conflicts; int RetValue, iLit = Gla_ManGetOutLit( p, f ); - clock_t clk = clock(); + abctime clk = Abc_Clock(); if ( piRetValue ) *piRetValue = 1; // consider special case when PO points to the flop @@ -1478,18 +1478,18 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon { // Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev ); // Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); -// Abc_PrintTime( 1, "Time", clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } assert( RetValue == l_False ); // derive the UNSAT core - clk = clock(); + clk = Abc_Clock(); vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); if ( vCore ) Vec_IntSort( vCore, 1 ); if ( fVerbose ) { // Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); -// Abc_PrintTime( 1, "Time", clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } return vCore; } @@ -1506,7 +1506,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon SeeAlso [] ***********************************************************************/ -void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, clock_t Time ) +void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, abctime Time ) { if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 ) return; @@ -1643,7 +1643,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL; Abc_Cex_t * pCex = NULL; int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1; - clock_t clk2, clk = clock(); + abctime clk2, clk = Abc_Clock(); // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); @@ -1696,10 +1696,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) } // start the manager p = Gla_ManStart( pAig, pPars ); - p->timeInit = clock() - clk; + p->timeInit = Abc_Clock() - clk; // set runtime limit if ( p->pPars->nTimeOut ) - sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() ); // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1721,10 +1721,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) // iterate as long as there are counter-examples for ( i = 0; ; i++ ) { - clk2 = clock(); + clk2 = Abc_Clock(); vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); // assert( (vCore != NULL) == (Status == 1) ); - if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached + if ( Status == -1 || (p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached { Prf_ManStopP( &p->pSat->pPrf2 ); // if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction @@ -1734,10 +1734,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) if ( Status == 1 ) { Prf_ManStopP( &p->pSat->pPrf2 ); - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; break; } - p->timeSat += clock() - clk2; + p->timeSat += Abc_Clock() - clk2; assert( Status == 0 ); p->nCexes++; @@ -1749,7 +1749,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) } // perform the refinement - clk2 = clock(); + clk2 = Abc_Clock(); if ( pPars->fAddLayer ) { vPPis = Gla_ManCollectPPis( p, NULL ); @@ -1803,7 +1803,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) // print the result (do not count it towards change) if ( p->pPars->fVerbose ) - Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk ); } if ( pCex != NULL ) break; @@ -1836,9 +1836,9 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) Gia_GlaAddOneSlice( p, f, vCore ); Vec_IntFree( vCore ); // run SAT solver - clk2 = clock(); + clk2 = Abc_Clock(); vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; // assert( (vCore != NULL) == (Status == 1) ); Vec_IntFreeP( &vCore ); if ( Status == -1 ) // resource limit is reached @@ -1855,7 +1855,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) } // print the result if ( p->pPars->fVerbose ) - Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); + Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk ); if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened { @@ -1901,7 +1901,7 @@ finish: pAig->vGateClasses = Gla_ManTranslate( p ); if ( Status == -1 ) { - if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); @@ -1929,16 +1929,16 @@ finish: Vec_IntFreeP( &pAig->vGateClasses ); RetValue = 0; } - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); 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 ); + p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; + ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk ); Gla_ManReportMemory( p ); } // Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 ); diff --git a/src/proof/abs/absIter.c b/src/proof/abs/absIter.c index e8e5730b..7b660359 100644 --- a/src/proof/abs/absIter.c +++ b/src/proof/abs/absIter.c @@ -70,7 +70,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU int i, iFrame0, iFrame; int nTotal = 0, nRemoved = 0; Vec_Int_t * vGScopy; - clock_t clk, clkTotal = clock(); + abctime clk, clkTotal = Abc_Clock(); assert( Gia_ManPoNum(p) == 1 ); assert( p->vGateClasses != NULL ); vGScopy = Vec_IntDup( p->vGateClasses ); @@ -99,7 +99,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj))) ) continue; } - clk = clock(); + clk = Abc_Clock(); printf( "%5d : ", nTotal ); printf( "Obj =%7d ", i ); Gia_ObjRemFromGla( p, pObj ); @@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU printf( "Removing " ); Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 ); } - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); nTotal++; // update the classes Vec_IntFreeP( &p->vGateClasses ); @@ -135,7 +135,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU Vec_IntFree( vGScopy ); printf( "Tried = %d. ", nTotal ); printf( "Removed = %d. (%.2f %%) ", nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) ); - Abc_PrintTime( 1, "Time", clock() - clkTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); return NULL; } diff --git a/src/proof/abs/absOldCex.c b/src/proof/abs/absOldCex.c index e5eaee27..c57d8ed9 100644 --- a/src/proof/abs/absOldCex.c +++ b/src/proof/abs/absOldCex.c @@ -720,9 +720,9 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int Saig_ManCba_t * p; Vec_Int_t * vReasons; Abc_Cex_t * pCare; - clock_t clk = clock(); + abctime clk = Abc_Clock(); - clk = clock(); + clk = Abc_Clock(); p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose ); // p->vReg2Frame = Vec_VecStart( pCex->iFrame ); @@ -743,7 +743,7 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); Vec_IntFree( vRes ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); } pCare = Saig_ManCbaReason2Cex( p, vReasons ); @@ -786,7 +786,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex { Saig_ManCba_t * p; Vec_Int_t * vRes, * vReasons; - clock_t clk; + abctime clk; if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n", @@ -794,7 +794,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex return NULL; } -clk = clock(); +clk = Abc_Clock(); p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose ); p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame ); vReasons = Saig_ManCbaFindReason( p ); @@ -804,7 +804,7 @@ clk = clock(); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); } Vec_IntFree( vReasons ); @@ -831,7 +831,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p { Vec_Int_t * vAbsFfsToAdd; int RetValue; - clock_t clk = clock(); + abctime clk = Abc_Clock(); // assert( pAbs->nRegs > 0 ); // perform BMC RetValue = Saig_ManBmcScalable( pAbs, pPars ); @@ -859,7 +859,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p { printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } return vAbsFfsToAdd; } diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c index 6cc5ff6d..b42053dd 100644 --- a/src/proof/abs/absOldRef.c +++ b/src/proof/abs/absOldRef.c @@ -257,7 +257,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC Aig_Man_t * pAbs; Vec_Int_t * vFlopsNew; int i, Entry; - clock_t clk = clock(); + abctime clk = Abc_Clock(); pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( fSensePath ) vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); @@ -281,7 +281,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC if ( fVerbose ) { printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } // vFlopsNew contains PI numbers that should be kept in pAbs // select the most useful flops among those to be added @@ -411,7 +411,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) int nUseStart = 0; Aig_Man_t * pAbs, * pTemp; Vec_Int_t * vFlops; - int Iter;//, clk = clock(), clk2 = clock();//, iFlop; + int Iter;//, clk = Abc_Clock(), clk2 = Abc_Clock();//, iFlop; assert( Aig_ManRegNum(p) > 0 ); if ( pPars->fVerbose ) printf( "Performing counter-example-based refinement.\n" ); diff --git a/src/proof/abs/absOldSat.c b/src/proof/abs/absOldSat.c index 14f59667..7ee54b29 100644 --- a/src/proof/abs/absOldSat.c +++ b/src/proof/abs/absOldSat.c @@ -510,7 +510,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) Vec_Int_t * vAssumps, * vVar2PiId; int i, k, Entry, RetValue;//, f = 0, Counter = 0; int nCoreLits, * pCoreLits; - clock_t clk = clock(); + abctime clk = Abc_Clock(); // create CNF assert( Aig_ManRegNum(p->pFrames) == 0 ); // pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow @@ -530,7 +530,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) Cnf_DataFree( pCnf ); return NULL; } -//Abc_PrintTime( 1, "Preparing", clock() - clk ); +//Abc_PrintTime( 1, "Preparing", Abc_Clock() - clk ); // look for a true counter-example if ( p->nInputs > 0 ) { @@ -582,10 +582,10 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) } // solve -clk = clock(); +clk = Abc_Clock(); RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); -//Abc_PrintTime( 1, "Solving", clock() - clk ); +//Abc_PrintTime( 1, "Solving", Abc_Clock() - clk ); if ( RetValue != l_False ) { if ( RetValue == l_True ) @@ -868,9 +868,9 @@ Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nIn Saig_RefMan_t * p; Vec_Int_t * vReasons; Abc_Cex_t * pCare; - clock_t clk = clock(); + abctime clk = Abc_Clock(); - clk = clock(); + clk = Abc_Clock(); p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose ); vReasons = Saig_RefManFindReason( p ); @@ -883,7 +883,7 @@ Aig_ManPrintStats( p->pFrames ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); Vec_IntFree( vRes ); @@ -900,7 +900,7 @@ ABC_PRT( "Time", clock() - clk ); Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); Vec_IntFree( vRes ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); */ } @@ -931,7 +931,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP { Saig_RefMan_t * p; Vec_Int_t * vRes, * vReasons; - clock_t clk; + abctime clk; if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", @@ -939,7 +939,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP return NULL; } -clk = clock(); +clk = Abc_Clock(); p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose ); vReasons = Saig_RefManFindReason( p ); @@ -950,7 +950,7 @@ clk = clock(); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); } /* @@ -967,7 +967,7 @@ ABC_PRT( "Time", clock() - clk ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); } */ diff --git a/src/proof/abs/absOldSim.c b/src/proof/abs/absOldSim.c index e5c1e938..5d316935 100644 --- a/src/proof/abs/absOldSim.c +++ b/src/proof/abs/absOldSim.c @@ -444,7 +444,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; - clock_t clk; + abctime clk; if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", @@ -455,12 +455,12 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); -clk = clock(); +clk = Abc_Clock(); vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); +ABC_PRT( "Time", Abc_Clock() - clk ); } Vec_PtrFree( vSimInfo ); Aig_ManFanoutStop( p ); diff --git a/src/proof/abs/absOut.c b/src/proof/abs/absOut.c index c230acb4..0cd9e0e2 100644 --- a/src/proof/abs/absOut.c +++ b/src/proof/abs/absOut.c @@ -97,7 +97,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose Abc_Cex_t * pCare; Vec_Int_t * vPis, * vPPis; int f, i, iObjId; - clock_t clk = clock(); + abctime clk = Abc_Clock(); int nOnes = 0, Counter = 0; if ( p->vGateClasses == NULL ) { @@ -175,7 +175,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose if ( fVerbose ) { Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } } } @@ -209,7 +209,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose if ( fVerbose ) { Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } // consider the case of SAT if ( iObjId == -1 ) @@ -375,7 +375,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra Gia_Man_t * pAbs, * pNew; Vec_Int_t * vFlops, * vInit; Vec_Int_t * vCopy; -// clock_t clk = clock(); +// abctime clk = Abc_Clock(); int RetValue; ABC_FREE( p->pCexSeq ); if ( p->vGateClasses == NULL ) diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c index f72d86e2..dda0c8cb 100644 --- a/src/proof/abs/absRef.c +++ b/src/proof/abs/absRef.c @@ -290,7 +290,7 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) { double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc; double MemOther = sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs); - clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer; + abctime timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer; printf( "Abstraction refinement runtime statistics:\n" ); ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal ); ABC_PRTP( "Justification", p->timeBwd, p->timeTotal ); @@ -674,7 +674,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in { int fVerify = 1; Vec_Int_t * vGoodPPis, * vNewPPis; - clock_t clk, clk2 = clock(); + abctime clk, clk2 = Abc_Clock(); int RetValue; p->nCalls++; // Gia_ManCleanValue( p->pGia ); @@ -692,27 +692,27 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) ); memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs ); // propagate priorities - clk = clock(); + clk = Abc_Clock(); vGoodPPis = Vec_IntAlloc( 100 ); if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX { - p->timeFwd += clock() - clk; + p->timeFwd += Abc_Clock() - clk; // select refinement - clk = clock(); + clk = Abc_Clock(); p->nVisited = 0; Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis ); RetValue = Vec_IntUniqify( vGoodPPis ); // assert( RetValue == 0 ); - p->timeBwd += clock() - clk; + p->timeBwd += Abc_Clock() - clk; } // verify (empty) refinement // (only works when post-processing is not applied) if ( fVerify ) { - clk = clock(); + clk = Abc_Clock(); Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis ); - p->timeVer += clock() - clk; + p->timeVer += Abc_Clock() - clk; } // at this point array vGoodPPis contains the set of important PPIs @@ -737,7 +737,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in Rnm_ManCleanValues( p ); // Vec_IntReverseOrder( vGoodPPis ); - p->timeTotal += clock() - clk2; + p->timeTotal += Abc_Clock() - clk2; p->nRefines += Vec_IntSize(vGoodPPis); return vGoodPPis; } diff --git a/src/proof/abs/absRef.h b/src/proof/abs/absRef.h index 9bae40a3..93c054aa 100644 --- a/src/proof/abs/absRef.h +++ b/src/proof/abs/absRef.h @@ -83,10 +83,10 @@ struct Rnm_Man_t_ int nRefines; // total refined objects int nVisited; // visited during justification // statistics - clock_t timeFwd; // forward propagation - clock_t timeBwd; // backward propagation - clock_t timeVer; // ternary simulation - clock_t timeTotal; // other time + abctime timeFwd; // forward propagation + abctime timeBwd; // backward propagation + abctime timeVer; // ternary simulation + abctime timeTotal; // other time }; // accessing the refinement object diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index edb60083..ef5747c1 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -110,7 +110,7 @@ void Gia_ManTestDoms2( Gia_Man_t * p ) { Vec_Int_t * vNodes; Gia_Obj_t * pObj, * pDom; - clock_t clk = clock(); + abctime clk = Abc_Clock(); int i; assert( p->vDoms == NULL ); Gia_ManComputeDoms( p ); @@ -119,7 +119,7 @@ void Gia_ManTestDoms2( Gia_Man_t * p ) if ( Gia_ObjId(p, pObj) != Gia_ObjDom(p, pObj) ) printf( "PI =%6d Id =%8d. Dom =%8d.\n", i, Gia_ObjId(p, pObj), Gia_ObjDom(p, pObj) ); */ - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator Gia_ManCleanMark1( p ); Gia_ManForEachPi( p, pObj, i ) diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c index 4b943870..01680a3f 100644 --- a/src/proof/abs/absVta.c +++ b/src/proof/abs/absVta.c @@ -71,10 +71,10 @@ struct Vta_Man_t_ sat_solver2 * pSat; // incremental SAT solver Vec_Int_t * vAddedNew; // the IDs of variables added to the solver // statistics - clock_t timeSat; - clock_t timeUnsat; - clock_t timeCex; - clock_t timeOther; + abctime timeSat; + abctime timeUnsat; + abctime timeCex; + abctime timeOther; }; @@ -1082,7 +1082,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f ) ***********************************************************************/ Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) { - clock_t clk = clock(); + abctime clk = Abc_Clock(); Vec_Int_t * vCore; int RetValue, nConfPrev = pSat->stats.conflicts; if ( piRetValue ) @@ -1115,16 +1115,16 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fV { // Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev ); // Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts ); -// Abc_PrintTime( 1, "Time", clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } assert( RetValue == l_False ); // derive the UNSAT core - clk = clock(); + clk = Abc_Clock(); vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); if ( fVerbose ) { // Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) ); -// Abc_PrintTime( 1, "Time", clock() - clk ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } return vCore; } @@ -1140,7 +1140,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fV SeeAlso [] ***********************************************************************/ -int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, clock_t Time, int fVerbose ) +int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose ) { unsigned * pInfo; int * pCountAll = NULL, * pCountUni = NULL; @@ -1495,7 +1495,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) Vec_Int_t * vCore; Abc_Cex_t * pCex = NULL; int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0; - clock_t clk = clock(), clk2; + abctime clk = Abc_Clock(), clk2; // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); @@ -1525,7 +1525,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) p = Vga_ManStart( pAig, pPars ); // set runtime limit if ( p->pPars->nTimeOut ) - sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() ); // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) // iterate as long as there are counter-examples for ( i = 0; ; i++ ) { - clk2 = clock(); + clk2 = Abc_Clock(); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls ); assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached @@ -1573,27 +1573,27 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) goto finish; } // check timeout - if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) + if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) { Vga_ManRollBack( p, nObjOld ); goto finish; } if ( vCore != NULL ) { - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; break; } - p->timeSat += clock() - clk2; + p->timeSat += Abc_Clock() - clk2; assert( Status == 0 ); p->nCexes++; // perform the refinement - clk2 = clock(); + clk2 = Abc_Clock(); pCex = Vta_ManRefineAbstraction( p, f ); - p->timeCex += clock() - clk2; + p->timeCex += Abc_Clock() - clk2; if ( pCex != NULL ) goto finish; // print the result (do not count it towards change) - Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ); + Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ); } assert( Status == 1 ); // valid core is obtained @@ -1608,9 +1608,9 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) Vec_IntFree( vCore ); // run SAT solver - clk2 = clock(); + clk2 = Abc_Clock(); vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls ); - p->timeUnsat += clock() - clk2; + p->timeUnsat += Abc_Clock() - clk2; assert( (vCore != NULL) == (Status == 1) ); if ( Status == -1 ) // resource limit is reached break; @@ -1628,7 +1628,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) Vec_IntSort( vCore, 1 ); Vec_PtrPush( p->vCores, vCore ); // print the result - if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ) ) + if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) ) { // reset the counter of frames without change nCountNoChange = 1; @@ -1682,7 +1682,7 @@ finish: pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); if ( Status == -1 ) { - if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); @@ -1711,16 +1711,16 @@ finish: Vec_IntFreeP( &pAig->vObjClasses ); RetValue = 0; } - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); 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 ); + p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex; + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk ); Gia_VtaPrintMemory( p ); } |