diff options
Diffstat (limited to 'src/aig/saig')
28 files changed, 94 insertions, 104 deletions
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 55a429e1..0b59274a 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -721,7 +721,7 @@ 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; - int clk = clock(); + clock_t clk = clock(); clk = clock(); p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose ); @@ -831,7 +831,8 @@ ABC_PRT( "Time", clock() - clk ); Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars ) { Vec_Int_t * vAbsFfsToAdd; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); // assert( pAbs->nRegs > 0 ); // perform BMC RetValue = Saig_ManBmcScalable( pAbs, pPars ); diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index 42744459..9a10edb6 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -254,9 +254,9 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nF sat_solver * pSat; Cnf_Dat_t * pCnf; Aig_Obj_t * pObj; - int nTimeToStop = time(NULL) + TimeLimit; int nCoreLits, * pCoreLits; - int i, iVar, RetValue, clk; + int i, iVar, RetValue; + clock_t clk; if ( fVerbose ) { if ( TimeLimit ) @@ -296,7 +296,7 @@ Abc_PrintTime( 1, "Preparing", clock() - clk ); // set runtime limit if ( TimeLimit ) - sat_solver_set_runtime_limit( pSat, nTimeToStop ); + sat_solver_set_runtime_limit( pSat, TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0 ); // run SAT solver clk = clock(); diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 0054d8b0..77517c18 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -172,7 +172,8 @@ 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, clk = clock(); + int i, Entry; + clock_t clk = clock(); pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( fSensePath ) vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c index 24414c5a..e991ac35 100644 --- a/src/aig/saig/saigAbsVfa.c +++ b/src/aig/saig/saigAbsVfa.c @@ -209,7 +209,8 @@ int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f ) void Abs_VfaManCreateFrame( Abs_VfaMan_t * p, int f ) { Aig_Obj_t * pObj; - int i, clk = clock(); + int i; + clock_t clk = clock(); Saig_ManForEachPo( p->pAig, pObj, i ) Abs_VfaManCreateFrame_rec( p, pObj, f ); diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 60f406ad..021ad5d0 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -190,7 +190,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim Cnf_Dat_t * pCnf; Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; - int status, clk, Lit, i, RetValue = -1; + int status, Lit, i, RetValue = -1; + clock_t clk; // derive the timeframes clk = clock(); @@ -264,7 +265,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else { - int clkPart = clock(); + clock_t clkPart = clock(); Aig_ManForEachCo( pFrames, pObj, i ) { //if ( s_fInterrupt ) diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 4a95bdbc..8ff9a7a7 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -202,7 +202,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose Vec_Ptr_t * vSimInfo; Aig_Obj_t * pObj; int i, f, nFramesLimit, nFrameWords; - int clk = clock(); + clock_t clk = clock(); assert( Aig_ManRegNum(p) > 0 ); // the maximum number of frames will be determined to use at most 200Mb of RAM nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p); @@ -742,9 +742,10 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax Saig_Bmc_t * p; Aig_Man_t * pNew; Cnf_Dat_t * pCnf; - int nTimeToStop = time(NULL) + nTimeOut; int nOutsSolved = 0; - int Iter, RetValue = -1, clk = clock(), clk2, clkTotal = clock(); + int Iter, RetValue = -1; + clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0; + clock_t clk = clock(), clk2, clkTotal = clock(); int Status = -1; /* Vec_Ptr_t * vSimInfo; @@ -763,7 +764,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); // set runtime limit if ( nTimeOut ) - sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); + sat_solver_set_runtime_limit( p->pSat, nTimeOut ); for ( Iter = 0; ; Iter++ ) { clk2 = clock(); @@ -796,7 +797,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( RetValue != l_False ) break; // check the timeout - if ( nTimeOut && time(NULL) > nTimeToStop ) + if ( nTimeOut && clock() > nTimeToStop ) { printf( "Reached timeout (%d seconds).\n", nTimeOut ); if ( piFrames ) @@ -839,7 +840,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); - else if ( nTimeOut && time(NULL) > nTimeToStop ) + else if ( nTimeOut && clock() > nTimeToStop ) printf( "Reached timeout (%d seconds).\n", nTimeOut ); else printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 9107a796..12e982cc 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1251,8 +1251,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) unsigned * pInfo; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) ); - int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); - int nTimeToStop = time(NULL) + pPars->nTimeOut; + int i, f, Lit, status; + clock_t clk, clk2, clkOther = 0, clkTotal = clock(); + clock_t nTimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0; p = Saig_Bmc3ManStart( pAig ); p->pPars = pPars; if ( pPars->fVerbose ) @@ -1411,7 +1412,7 @@ clkOther += clock() - clk2; else { assert( status == l_Undef ); - if ( pPars->nTimeOut && time(NULL) > nTimeToStop ) + if ( pPars->nTimeOut && clock() > nTimeToStop ) { printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); Saig_Bmc3ManStop( p ); @@ -1427,7 +1428,7 @@ clkOther += clock() - clk2; Saig_Bmc3ManStop( p ); return RetValue; } - if ( pPars->nTimeOut && time(NULL) > nTimeToStop ) + if ( pPars->nTimeOut && clock() > nTimeToStop ) { printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); Saig_Bmc3ManStop( p ); @@ -1450,7 +1451,7 @@ clkOther += clock() - clk2; // printf( "%4.0f Mb", 4.0*Vec_IntSize(p->vVisited) /(1<<20) ); printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) ); printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); - printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); + printf( "%9.2f sec ", 1.0*(clock() - clkTotal)/CLOCKS_PER_SEC ); // printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index f54f2dbe..85e79e3f 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -59,7 +59,8 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb Vec_Int_t * vProbs, * vProbs2; Aig_Obj_t * pObj, * pObjLi; unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2; - int i, w, f, RetValue = 1, clk = clock(); + int i, w, f, RetValue = 1; + clock_t clk = clock(); if ( fVerbose ) printf( "Simulating %d nodes and %d flops for %d frames with %d words... ", Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords ); diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c index 459d8ede..d39ff944 100644 --- a/src/aig/saig/saigGlaCba.c +++ b/src/aig/saig/saigGlaCba.c @@ -59,9 +59,9 @@ struct Aig_Gla1Man_t_ // SAT solver sat_solver * pSat; // statistics - int timeSat; - int timeRef; - int timeTotal; + clock_t timeSat; + clock_t timeRef; + clock_t timeTotal; }; //////////////////////////////////////////////////////////////////////// @@ -687,8 +687,9 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i Abc_Cex_t * pCex; Vec_Int_t * vPPiRefine; int f, g, r, i, iSatVar, Lit, Entry, RetValue; - int nConfBef, nConfAft, clk, clkTotal = clock(); - int nTimeToStop = time(NULL) + TimeLimit; + int nConfBef, nConfAft; + clock_t clk, clkTotal = clock(); + clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0; assert( Saig_ManPoNum(pAig) == 1 ); if ( nFramesMax == 0 ) @@ -753,7 +754,7 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i printf( "== %3d ==", f ); else printf( " " ); - if ( TimeLimit && time(NULL) > nTimeToStop ) + if ( TimeLimit && clock() > nTimeToStop ) printf( " SAT solver timed out after %d seconds.\n", TimeLimit ); else if ( RetValue != l_False ) printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef ); diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 6f461995..e039ed75 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -48,46 +48,15 @@ struct Aig_Gla2Man_t_ // SAT solver sat_solver * pSat; // statistics - int timePre; - int timeSat; - int timeTotal; + clock_t timePre; + clock_t timeSat; + clock_t timeTotal; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_CPS 1000 - -/**Function************************************************************* - - Synopsis [Procedure returns miliseconds elapsed since the last reset.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_Clock( int Timer, int fReset ) -{ - static int Time[16], Clock[16]; - int Clock2, Diff; - assert( Timer >= 0 && Timer < 16 ); - if ( fReset ) - { - Time[Timer] = time(NULL); - Clock[Timer] = clock(); - return 0; - } - Clock2 = clock(); - if ( Clock2 > Clock[Timer] ) - Diff = (Clock2 - Clock[Timer]) % CLOCKS_PER_SEC; - else - Diff = CLOCKS_PER_SEC - (Clock[Timer] - Clock2) % CLOCKS_PER_SEC; - return (time(NULL) - Time[Timer]) * ABC_CPS + (Diff * ABC_CPS) / CLOCKS_PER_SEC; -} /**Function************************************************************* @@ -432,7 +401,8 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo Vec_Int_t * vCore; void * pSatCnf; Intp_Man_t * pManProof; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); if ( piRetValue ) *piRetValue = -1; // solve the problem @@ -556,8 +526,8 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in { Aig_Gla2Man_t * p; Vec_Int_t * vCore, * vResult; - int nTimeToStop = time(NULL) + TimeLimit; - int clk, clk2 = clock(); + clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0; + clock_t clk, clk2 = clock(); assert( Saig_ManPoNum(pAig) == 1 ); if ( fVerbose ) diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index a7122d01..42850e01 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -47,9 +47,9 @@ struct Aig_Gla3Man_t_ // SAT solver sat_solver2 * pSat; // statistics - int timePre; - int timeSat; - int timeTotal; + clock_t timePre; + clock_t timeSat; + clock_t timeTotal; }; //////////////////////////////////////////////////////////////////////// @@ -393,7 +393,8 @@ void Aig_Gla3ManStop( Aig_Gla3Man_t * p ) Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) { Vec_Int_t * vCore; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); if ( piRetValue ) *piRetValue = -1; // solve the problem @@ -495,8 +496,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in { Aig_Gla3Man_t * p; Vec_Int_t * vCore, * vResult; - int nTimeToStop = time(NULL) + TimeLimit; - int clk, clk2 = clock(); + clock_t clk, clk2 = clock(); assert( Saig_ManPoNum(pAig) == 1 ); if ( fVerbose ) @@ -521,7 +521,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in // set runtime limit if ( TimeLimit ) - sat_solver2_set_runtime_limit( p->pSat, nTimeToStop ); + sat_solver2_set_runtime_limit( p->pSat, TimeLimit * CLOCKS_PER_SEC + clock() ); // compute UNSAT core clk = clock(); diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index aedc98e2..b92b7a9b 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -206,7 +206,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n sat_solver * pSat; Aig_Obj_t * pObj1, * pObj2; int i, RetValue1, RetValue2, Counter, Lits[2], nOvers; - int clk = clock(), clkVerif; + clock_t clk = clock(), clkVerif; nOvers = Aig_ManMapHaigNodes( pHaig ); @@ -412,7 +412,7 @@ int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int sat_solver * pSat; Aig_Obj_t * pObj1, * pObj2; int i, RetValue1, RetValue2, Counter, Lits[2]; - int clk = clock(); + clock_t clk = clock(); int Delta; int Id1, Id2; @@ -624,7 +624,8 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Aig_Man_t * pNew, * pTemp; Aig_Obj_t * pObj; - int i, k, nStepsReal, clk = clock(), clkSynth; + int i, k, nStepsReal; + clock_t clk = clock(), clkSynth; Dar_ManDefaultRwrParams( pParsRwr ); clk = clock(); diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index aa417fb0..39ec734a 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -150,8 +150,9 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL; Vec_Ptr_t * vTop, * vBot; Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo; - int i, k, f, clk, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev; + int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev; int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0; + clock_t clk; assert( fUnique == 0 || fUniqueAll == 0 ); assert( Saig_ManPoNum(p) == 1 ); Aig_ManSetCioIds( p ); diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index 2250126b..ccff1bde 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -426,7 +426,8 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV Vec_Ptr_t * vBuffers, * vClasses; Vec_Int_t * vLevel, * vRemain; Vec_Str_t * vStr, * vPrev; - int i, nPos, clk = clock(); + int i, nPos; + clock_t clk = clock(); int clkDup = 0, clkAig = 0, clkIso = 0, clk2; *pvPosEquivs = NULL; @@ -539,7 +540,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) { Vec_Int_t * vPerm; - int clk = clock(); + clock_t clk = clock(); vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); Vec_IntFree( vPerm ); Abc_PrintTime( 1, "Time", clock() - clk ); @@ -560,7 +561,7 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) { Aig_Man_t * pPart; - int clk = clock(); + clock_t clk = clock(); pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose ); printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); Abc_PrintTime( 1, "Time", clock() - clk ); diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c index a7cc942c..8b60368f 100644 --- a/src/aig/saig/saigIsoFast.c +++ b/src/aig/saig/saigIsoFast.c @@ -160,7 +160,7 @@ void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_In Vec_IntPush( vVisited, Aig_ObjId(pObj) ); } -//static int time_Trav = 0; +//static clock_t time_Trav = 0; /**Function************************************************************* @@ -286,7 +286,8 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ) Aig_Obj_t * pObj; Vec_Ptr_t * vClasses, * vInfos; Vec_Int_t * vInfo, * vPrev, * vLevel; - int i, Number, nUnique = 0, clk = clock(); + int i, Number, nUnique = 0; + clock_t clk = clock(); // collect infos and remember their number pMan = Iso_StoStart( pAig ); diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c index 3dcd7777..25cd68f0 100644 --- a/src/aig/saig/saigIsoSlow.c +++ b/src/aig/saig/saigIsoSlow.c @@ -290,11 +290,11 @@ struct Iso_Man_t_ Vec_Ptr_t * vClasses; // other classes Vec_Ptr_t * vTemp1; // other classes Vec_Ptr_t * vTemp2; // other classes - int timeHash; - int timeFout; - int timeSort; - int timeOther; - int timeTotal; + clock_t timeHash; + clock_t timeFout; + clock_t timeSort; + clock_t timeOther; + clock_t timeTotal; }; static inline Iso_Obj_t * Iso_ManObj( Iso_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } @@ -556,7 +556,8 @@ static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso ) void Iso_ManCollectClasses( Iso_Man_t * p ) { Iso_Obj_t * pIso; - int i, clk = clock(); + int i; + clock_t clk = clock(); Vec_PtrClear( p->vSingles ); Vec_PtrClear( p->vClasses ); for ( i = 0; i < p->nBins; i++ ) @@ -1171,8 +1172,7 @@ Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ) int fVeryVerbose = 0; Vec_Int_t * vRes; Iso_Man_t * p; - int clk, clk2 = clock(); - clk = clock(); + clock_t clk = clock(), clk2 = clock(); p = Iso_ManCreate( pAig ); p->timeFout += clock() - clk; Iso_ManPrintClasses( p, fVerbose, fVeryVerbose ); diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index f7832f10..f3f6f279 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -1076,7 +1076,8 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe // extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); int iOut, nOuts; Aig_Man_t * pMiterCec; - int RetValue, clkTotal = clock(); + int RetValue; + clock_t clkTotal = clock(); if ( fVerbose ) { Aig_ManPrintStats( pPart0 ); diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index 6a351e10..d99320ce 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.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; - int clk = clock(); + clock_t clk = clock(); // create CNF assert( Aig_ManRegNum(p->pFrames) == 0 ); // pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow @@ -868,7 +868,7 @@ 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; - int clk = clock(); + clock_t clk = clock(); clk = clock(); p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose ); @@ -931,7 +931,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP { Saig_RefMan_t * p; Vec_Int_t * vRes, * vReasons; - int clk; + clock_t clk; if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c index bbd7f397..006167d5 100644 --- a/src/aig/saig/saigRetFwd.c +++ b/src/aig/saig/saigRetFwd.c @@ -213,7 +213,8 @@ Aig_Man_t * Saig_ManRetimeForwardOne( Aig_Man_t * p, int * pnRegFixed, int * pnR Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ) { Aig_Man_t * pNew, * pTemp; - int i, clk, nRegFixed, nRegMoves = 1; + int i, nRegFixed, nRegMoves = 1; + clock_t clk; pNew = p; for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ ) { diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index c83a7a64..36f3d903 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -521,7 +521,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; - int clk; + clock_t clk; if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c index f5aecc71..335c4034 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/aig/saig/saigSimExt2.c @@ -337,7 +337,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; - int clk; + clock_t clk; if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", @@ -446,7 +446,7 @@ Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int i { Abc_Cex_t * pCare; Vec_Ptr_t * vSimInfo; - int clk; + clock_t clk; if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c index 27855bfd..e54e58ac 100644 --- a/src/aig/saig/saigSimFast.c +++ b/src/aig/saig/saigSimFast.c @@ -348,7 +348,8 @@ Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref, Vec_Int_t * vSwitching; int * pProbs; float * pSwitching; - int nFramesReal, clk;//, clkTotal = clock(); + int nFramesReal; + clock_t clk;//, clkTotal = clock(); if ( fProbOne ) fTrans = 0; vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) ); diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 11bd088c..71259930 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -881,7 +881,8 @@ Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSa Vec_Ptr_t * vMap; Saig_MvMan_t * p; Saig_MvObj_t * pEntry; - int f, i, iState, clk = clock(); + int f, i, iState; + clock_t clk = clock(); assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur ); // start manager diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index 86c45f37..ee4085b1 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -456,7 +456,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i Raig_Man_t * p; Sec_MtrStatus_t Status; int i, iPat, RetValue = 0; - int clk, clkTotal = clock(); + clock_t clk, clkTotal = clock(); assert( Aig_ManRegNum(pAig) > 0 ); Status = Sec_MiterStatus( pAig ); if ( Status.nSat > 0 ) diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c index 5d33595f..2feaba1b 100644 --- a/src/aig/saig/saigStrSim.c +++ b/src/aig/saig/saigStrSim.c @@ -877,7 +877,8 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis Vec_Int_t * vPairs; Aig_Man_t * pPart0, * pPart1; Aig_Obj_t * pObj0, * pObj1; - int i, nMatches, clk, clkTotal = clock(); + int i, nMatches; + clock_t clk, clkTotal = clock(); Aig_ManRandom( 1 ); // consider the case when a miter is given if ( p1 == NULL ) diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c index 4c54e3ad..8f4f962f 100644 --- a/src/aig/saig/saigSwitch.c +++ b/src/aig/saig/saigSwitch.c @@ -268,7 +268,8 @@ Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref, Saig_SimObj_t * pAig, * pEntry; Vec_Int_t * vSwitching; float * pSwitching; - int nFramesReal, clk;//, clkTotal = clock(); + int nFramesReal; + clock_t clk;//, clkTotal = clock(); vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) ); pSwitching = (float *)vSwitching->pArray; clk = clock(); diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index c592d0a5..28c8150f 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -504,7 +504,8 @@ Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose Aig_Man_t * pAigZero; Vec_Str_t * vSequence; Vec_Ptr_t * vSimInfo; - int RetValue, clk; + int RetValue; + clock_t clk; clk = clock(); // derive synchronization sequence @@ -557,7 +558,8 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, Aig_Man_t * pAig1z, * pAig2z, * pMiter; Vec_Str_t * vSeq1, * vSeq2; Vec_Ptr_t * vSimInfo; - int RetValue, clk; + int RetValue; + clock_t clk; /* { unsigned u = Saig_SynchRandomTernary(); diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index 9be84e31..55c9772a 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -379,7 +379,7 @@ Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFrame { // extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ); Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2; - int clk; + clock_t clk; // create uninitialized timeframes with map1 pFrames = Saig_ManFramesNonInitial( pAig, nFrames ); // perform fraiging for the unrolled timeframes |