diff options
Diffstat (limited to 'src/proof/cec/cecCec.c')
| -rw-r--r-- | src/proof/cec/cecCec.c | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index 37df4d8d..aa6d753a 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -73,7 +73,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); int RetValue, iOut, nOuts; - clock_t clkTotal = clock(); + abctime clkTotal = Abc_Clock(); if ( piOutFail ) *piOutFail = -1; Gia_ManStop( pTemp ); @@ -83,12 +83,12 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) if ( RetValue == 1 ) { Abc_Print( 1, "Networks are equivalent. " ); -Abc_PrintTime( 1, "Time", clock() - clkTotal ); +Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); } else if ( RetValue == 0 ) { Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); -Abc_PrintTime( 1, "Time", clock() - clkTotal ); +Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); if ( pMiterCec->pData == NULL ) Abc_Print( 1, "Counter-example is not available.\n" ); else @@ -113,7 +113,7 @@ Abc_PrintTime( 1, "Time", clock() - clkTotal ); else { Abc_Print( 1, "Networks are UNDECIDED. " ); -Abc_PrintTime( 1, "Time", clock() - clkTotal ); +Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); } fflush( stdout ); Aig_ManStop( pMiterCec ); @@ -136,7 +136,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) Gia_Obj_t * pObj1, * pObj2; Gia_Obj_t * pDri1, * pDri2; int i; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Gia_ManSetPhase( p ); Gia_ManForEachPo( p, pObj1, i ) { @@ -146,7 +146,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) ) { Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different phase). ", i/2 ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); return 0; @@ -158,7 +158,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 ) { Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different PIs). ", i/2 ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); // if their compl attributes are the same - one should be complemented @@ -171,7 +171,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) ) { Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (PI vs. constant). ", i/2 ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); // the compl attributes are the same - the PI should be complemented @@ -186,7 +186,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) if ( Gia_ManAndNum(p) == 0 ) { Abc_Print( 1, "Networks are equivalent. " ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return 1; } return -1; @@ -209,8 +209,8 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Cec_ParFra_t ParsFra, * pParsFra = &ParsFra; Gia_Man_t * p, * pNew; int RetValue; - clock_t clk = clock(); - clock_t clkTotal = clock(); + abctime clk = Abc_Clock(); + abctime clkTotal = Abc_Clock(); // consider special cases: // 1) (SAT) a pair of POs have different value under all-0 pattern // 2) (SAT) a pair of POs has different PI/Const drivers @@ -245,7 +245,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return 0; } p = Gia_ManDup( pInit ); @@ -257,7 +257,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) if ( pPars->fVerbose ) { Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } if ( fDumpUndecided ) { @@ -266,7 +266,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 ); Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); } - if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) + if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) { Gia_ManStop( pNew ); return -1; |