diff options
Diffstat (limited to 'src/aig')
78 files changed, 280 insertions, 253 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 3c390a37..adad1837 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/vec/vec.h" #include "src/misc/util/utilCex.h" @@ -165,8 +164,8 @@ struct Aig_Man_t_ Vec_Int_t * vCiNumsOrig; // original CI names int nComplEdges; // complemented edges // timing statistics - int time1; - int time2; + clock_t time1; + clock_t time2; }; // cut computation diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c index ed824fac..5e3bb93a 100644 --- a/src/aig/aig/aigCuts.c +++ b/src/aig/aig/aigCuts.c @@ -632,7 +632,8 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in { Aig_ManCut_t * p; Aig_Obj_t * pObj; - int i, clk = clock(); + int i; + clock_t clk = clock(); assert( pAig->pManCuts == NULL ); // start the manager p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index ace723a2..b4b7862e 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -767,7 +767,8 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ) int Aig_SupportSizeTest( Aig_Man_t * p ) { Aig_Obj_t * pObj; - int i, Counter = 0, clk = clock(); + int i, Counter = 0; + clock_t clk = clock(); Aig_ManForEachObj( p, pObj, i ) if ( Aig_ObjIsNode(pObj) ) Counter += (Aig_SupportSize(p, pObj) <= 16); diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c index 00350304..fe9403b5 100644 --- a/src/aig/aig/aigDoms.c +++ b/src/aig/aig/aigDoms.c @@ -623,7 +623,8 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit ) Aig_Sto_t * pSto; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; - int i, clk = clock(); + int i; + clock_t clk = clock(); pSto = Aig_ManDomStart( pAig, Limit ); // initialize flop inputs Saig_ManForEachLi( pAig, pObj, i ) @@ -663,7 +664,8 @@ Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit ) Aig_Sto_t * pSto; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; - int i, clk = clock(); + int i; + clock_t clk = clock(); pSto = Aig_ManDomStart( pAig, Limit ); // initialize flop inputs Aig_ManForEachCo( pAig, pObj, i ) @@ -703,7 +705,8 @@ Aig_Sto_t * Aig_ManComputeDomsNodes( Aig_Man_t * pAig, int Limit ) Aig_Sto_t * pSto; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; - int i, clk = clock(); + int i; + clock_t clk = clock(); pSto = Aig_ManDomStart( pAig, Limit ); // initialize flop inputs Aig_ManForEachCo( pAig, pObj, i ) diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c index fcf32236..6f183925 100644 --- a/src/aig/aig/aigInter.c +++ b/src/aig/aig/aigInter.c @@ -29,9 +29,9 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int timeCnf; -extern int timeSat; -extern int timeInt; +extern clock_t timeCnf; +extern clock_t timeSat; +extern clock_t timeInt; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -156,7 +156,7 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation Vec_Int_t * vVarsAB; Aig_Obj_t * pObj, * pObj2; int Lits[3], status, i; - int clk; + clock_t clk; int iLast = -1; // Suppress "might be used uninitialized" assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) ); diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c index 2c524c85..2ee60748 100644 --- a/src/aig/aig/aigJust.c +++ b/src/aig/aig/aigJust.c @@ -253,7 +253,9 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig ) Aig_ManPack_t * pPack; Vec_Int_t * vSuppLits, * vNodes; Aig_Obj_t * pObj; - int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0; + int i; + clock_t clk = clock(); + int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0; int nTotalLits = 0; vSuppLits = Vec_IntAlloc( 100 ); pPack = Aig_ManPackStart( pAig ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 56d2fd3f..fdbba36a 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -688,7 +688,8 @@ Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nSuppSizeLimit, int fVerbo Vec_Ptr_t * vPartSuppsBit; Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr; Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; - int i, iPart, iOut, clk; + int i, iPart, iOut; + clock_t clk; // compute the supports for all outputs clk = clock(); @@ -812,7 +813,8 @@ Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit Vec_Ptr_t * vPartSuppsBit; Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll; Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp; - int i, iPart, iOut, clk; + int i, iPart, iOut; + clock_t clk; // add output number to each clk = clock(); diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c index 839a17ee..d187a19b 100644 --- a/src/aig/aig/aigPartSat.c +++ b/src/aig/aig/aigPartSat.c @@ -497,7 +497,8 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize, Aig_Man_t * pAig, * pTemp; Vec_Int_t * vNode2Part, * vNode2Var; int nConfRemaining = nConfTotal, nNodes = 0; - int i, clk, status, RetValue = -1; + int i, status, RetValue = -1; + clock_t clk; // perform partitioning according to the selected algorithm clk = clock(); diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c index 1b017346..7f9699fd 100644 --- a/src/aig/aig/aigRepar.c +++ b/src/aig/aig/aigRepar.c @@ -129,7 +129,7 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) Cnf_Dat_t * pCnf; Aig_Obj_t * pObj; int Lit, Cid, Var, status, i; - int clk = clock(); + clock_t clk = clock(); assert( Aig_ManRegNum(pMan) == 0 ); assert( Aig_ManCoNum(pMan) == 1 ); @@ -251,7 +251,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) int nOuts = Aig_ManCoNum(pMan); int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume; int Cid, Lit, status, i, k, c; - int clk = clock(); + clock_t clk = clock(); assert( Aig_ManRegNum(pMan) == 0 ); // derive CNFs diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c index 58a04fb0..1cf45ebe 100644 --- a/src/aig/aig/aigRet.c +++ b/src/aig/aig/aigRet.c @@ -839,7 +839,7 @@ Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerb Rtm_Obj_t * pObj, * pNext; Aig_Obj_t * pObjAig; int i, k, nAutos, Degree, DegreeMax = 0; - int clk; + clock_t clk; // create the retiming manager clk = clock(); diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c index f187860f..50f96a81 100644 --- a/src/aig/aig/aigSplit.c +++ b/src/aig/aig/aigSplit.c @@ -258,7 +258,8 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose ) DdNode * bFunc; DdManager * dd; Vec_Ptr_t * vSupp, * vSubs, * vCofs; - int i, clk = clock(); + int i; + clock_t clk = clock(); if ( Saig_ManPoNum(p) != 1 ) { printf( "Currently works only for one primary output.\n" ); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index ec2531c7..abd9960a 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -70,7 +70,8 @@ void Aig_TableResize( Aig_Man_t * p ) { Aig_Obj_t * pEntry, * pNext; Aig_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, i, clk; + int nTableSizeOld, Counter, i; + clock_t clk; assert( p->pTable != NULL ); clk = clock(); // save the old table diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a5c075c3..0d97dd61 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/vec/vec.h" #include "src/misc/util/utilCex.h" diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 1a4e9cd2..c25c6e48 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -800,13 +800,10 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p ) // select objects vSelect = Vec_IntAlloc( 100 ); -// Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 ); Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 ); Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign ); Vec_IntUniqify( vSelect ); -// printf( "\nSelected %d.\n", Vec_IntSize(vSelect) ); - /* for ( f = 0; f < p->pPars->iFrame; f++ ) printf( "%2d", Vec_IntEntry(p->vObjCounts, f) ); @@ -976,7 +973,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping ); if ( pPars->fPropFanout ) Gia_ManStaticFanoutStart( p->pGia ); -//printf( "Old GIA = %d. New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) ); // derive new gate map assert( pGia0->vGateClasses != 0 ); @@ -1797,7 +1793,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) p->timeInit = clock() - clk; // set runtime limit if ( p->pPars->nTimeOut ) - sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1831,9 +1827,9 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) goto finish; } // check timeout - if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit ) + if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) { - Gla_ManRollBack( p ); // 1155046 + Gla_ManRollBack( p ); goto finish; } if ( vCore != NULL ) @@ -1960,7 +1956,7 @@ finish: pAig->vGateClasses = Gla_ManTranslate( p ); if ( Status == -1 ) { - if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 7b66b7dd..11c84853 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) p = Vga_ManStart( pAig, pPars ); // set runtime limit if ( p->pPars->nTimeOut ) - sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 ); + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() ); // perform initial abstraction if ( p->pPars->fVerbose ) { @@ -1609,7 +1609,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) goto finish; } // check timeout - if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit ) + if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) { Vga_ManRollBack( p, nObjOld ); goto finish; @@ -1716,7 +1716,7 @@ finish: pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores ); if ( Status == -1 ) { - if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c index 6fbd1095..ce863051 100644 --- a/src/aig/gia/giaCCof.c +++ b/src/aig/gia/giaCCof.c @@ -219,8 +219,9 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp ) ***********************************************************************/ int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit ) { - int ObjPrev = 0, ConfPrev = 0, clk; + int ObjPrev = 0, ConfPrev = 0; int Count = 0, LitOut, RetValue; + clock_t clk; // try solving for the first time and quit if converged RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 ); if ( RetValue == l_False ) @@ -268,8 +269,8 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n Ccf_Man_t * p; Gia_Obj_t * pObj; int f, i, Lit, RetValue = -1, fFailed = 0; - int nTimeToStop = time(NULL) + nTimeMax; - int clk = clock(); + clock_t nTimeToStop = clock() + nTimeMax * CLOCKS_PER_SEC; + clock_t clk = clock(); assert( Gia_ManPoNum(pGia) == 1 ); // create reachability manager @@ -309,7 +310,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n } // report the result - if ( nTimeToStop && time(NULL) > nTimeToStop ) + if ( nTimeToStop && clock() > nTimeToStop ) printf( "Runtime limit (%d sec) is reached after %d frames. ", nTimeMax, f ); else if ( f == nFrameMax ) printf( "Completed %d frames without converging. ", f ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index d83f79e9..b4bc5b3e 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -81,10 +81,10 @@ struct Cbs_Man_t_ int nConfSat; // conflicts in sat problems int nConfUndec; // conflicts in undec problems // runtime stats - int timeSatUnsat; // unsat - int timeSatSat; // sat - int timeSatUndec; // undecided - int timeTotal; // total runtime + clock_t timeSatUnsat; // unsat + clock_t timeSatSat; // sat + clock_t timeSatUndec; // undecided + clock_t timeTotal; // total runtime }; static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } @@ -1003,7 +1003,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt Vec_Int_t * vCex, * vVisit, * vCexStore; Vec_Str_t * vStatus; Gia_Obj_t * pRoot; - int i, status, clk, clkTotal = clock(); + int i, status; + clock_t clk, clkTotal = clock(); assert( Gia_ManRegNum(pAig) == 0 ); // Gia_ManCollectTest( pAig ); // prepare AIG diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c index 8198c17f..1dd4a425 100644 --- a/src/aig/gia/giaCSatOld.c +++ b/src/aig/gia/giaCSatOld.c @@ -73,10 +73,10 @@ struct Cbs0_Man_t_ int nConfSat; // conflicts in sat problems int nConfUndec; // conflicts in undec problems // runtime stats - int timeSatUnsat; // unsat - int timeSatSat; // sat - int timeSatUndec; // undecided - int timeTotal; // total runtime + clock_t timeSatUnsat; // unsat + clock_t timeSatSat; // sat + clock_t timeSatUndec; // undecided + clock_t timeTotal; // total runtime }; static inline int Cbs0_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } @@ -712,7 +712,8 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat Vec_Int_t * vCex, * vVisit, * vCexStore; Vec_Str_t * vStatus; Gia_Obj_t * pRoot; - int i, status, clk, clkTotal = clock(); + int i, status; + clock_t clk, clkTotal = clock(); assert( Gia_ManRegNum(pAig) == 0 ); // prepare AIG Gia_ManCreateRefs( pAig ); diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c index 8cfa9efc..6dd0e0fa 100644 --- a/src/aig/gia/giaCTas.c +++ b/src/aig/gia/giaCTas.c @@ -108,10 +108,10 @@ struct Tas_Man_t_ int nConfSat; // conflicts in sat problems int nConfUndec; // conflicts in undec problems // runtime stats - int timeSatUnsat; // unsat - int timeSatSat; // sat - int timeSatUndec; // undecided - int timeTotal; // total runtime + clock_t timeSatUnsat; // unsat + clock_t timeSatSat; // sat + clock_t timeSatUndec; // undecided + clock_t timeTotal; // total runtime }; static inline int Tas_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } @@ -1524,7 +1524,8 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt Gia_Obj_t * pRoot;//, * pRootCopy; // Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp; - int i, status, clk, clkTotal = clock(); + int i, status; + clock_t clk, clkTotal = clock(); assert( Gia_ManRegNum(pAig) == 0 ); // Gia_ManCollectTest( pAig ); // prepare AIG @@ -1703,7 +1704,8 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve Vec_Int_t * vCex, * vVisit, * vCexStore; Vec_Str_t * vStatus; Gia_Obj_t * pRoot, * pOldRoot; - int i, status, clk, clkTotal = clock(); + int i, status; + clock_t clk, clkTotal = clock(); int Tried = 0, Stored = 0, Step = Gia_ManCoNum(pAig) / nPatMax; assert( Gia_ManRegNum(pAig) == 0 ); // Gia_ManCollectTest( pAig ); diff --git a/src/aig/gia/giaCTas2.c b/src/aig/gia/giaCTas2.c index 855dcdd3..2b1d7169 100644 --- a/src/aig/gia/giaCTas2.c +++ b/src/aig/gia/giaCTas2.c @@ -115,10 +115,10 @@ struct Tas_Man_t_ int nConfUndec; // conflicts in undec problems int nConfTotal; // total conflicts // runtime stats - int timeSatUnsat; // unsat - int timeSatSat; // sat - int timeSatUndec; // undecided - int timeTotal; // total runtime + clock_t timeSatUnsat; // unsat + clock_t timeSatSat; // sat + clock_t timeSatUndec; // undecided + clock_t timeTotal; // total runtime }; static inline int Tas_VarIsAssigned( Tas_Var_t * pVar ) { return pVar->fAssign; } diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index cf8ecf00..68d269cd 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -672,7 +672,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p ) void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ) { Cof_Man_t * p; - int clk = clock(); + clock_t clk = clock(); p = Cof_ManCreateLogicSimple( pGia ); p->nLevels = 1 + Gia_ManLevelNum( pGia ); p->pLevels = ABC_CALLOC( int, p->nLevels ); diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index 1ec18767..1da2da1f 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -209,7 +209,8 @@ void Gia_ManCollectTest( Gia_Man_t * p ) { Vec_Int_t * vNodes; Gia_Obj_t * pObj; - int i, iNode, clk = clock(); + int i, iNode; + clock_t clk = clock(); vNodes = Vec_IntAlloc( 100 ); Gia_ManIncrementTravId( p ); Gia_ManForEachCo( p, pObj, i ) @@ -275,7 +276,8 @@ int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj ) int Gia_ManSuppSizeTest( Gia_Man_t * p ) { Gia_Obj_t * pObj; - int i, Counter = 0, clk = clock(); + int i, Counter = 0; + clock_t clk = clock(); Gia_ManForEachObj( p, pObj, i ) if ( Gia_ObjIsAnd(pObj) ) Counter += (Gia_ManSuppSizeOne(p, pObj) <= 16); diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index 1daf52a1..f71281cb 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -838,7 +838,8 @@ int Emb_ManComputeDistance_old( Emb_Man_t * p, Emb_Obj_t * pPivot ) void Gia_ManTestDistanceInternal( Emb_Man_t * p ) { int nAttempts = 20; - int i, iNode, Dist, clk; + int i, iNode, Dist; + clock_t clk; Emb_Obj_t * pPivot, * pNext; Gia_ManRandom( 1 ); Emb_ManResetTravId( p ); @@ -903,7 +904,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p ) void Gia_ManTestDistance( Gia_Man_t * pGia ) { Emb_Man_t * p; - int clk = clock(); + clock_t clk = clock(); p = Emb_ManStart( pGia ); // Emb_ManPrintFanio( p ); Emb_ManPrintStats( p ); @@ -1529,7 +1530,7 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose ) float VertX, VertY; int * pPermX, * pPermY; int i, k, Iter, iMinX, iMaxX, iMinY, iMaxY; - int clk = clock(); + clock_t clk = clock(); if ( p->pPlacement == NULL ) return; pEdgeX = ABC_ALLOC( float, p->nObjs ); @@ -1790,7 +1791,8 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars ) { Emb_Man_t * p; - int i, clk, clkSetup; + int i, clkSetup; + clock_t clk; // Gia_ManTestDistance( pGia ); // transform AIG into internal data-structure diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c index 672149bc..03832e4a 100644 --- a/src/aig/gia/giaEra.c +++ b/src/aig/gia/giaEra.c @@ -501,7 +501,8 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f { Gia_ManEra_t * p; Gia_ObjEra_t * pState; - int Hash, clk = clock(); + int Hash; + clock_t clk = clock(); int RetValue = 1; assert( Gia_ManPiNum(pAig) <= 12 ); assert( Gia_ManRegNum(pAig) > 0 ); diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c index 265335e2..f5f9fdb3 100644 --- a/src/aig/gia/giaEra2.c +++ b/src/aig/gia/giaEra2.c @@ -1536,7 +1536,8 @@ int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) Gia_Obj_t * pPivot; Vec_Int_t * vLits, * vTfos; Gia_Obj_t * pObj; - int i, clk; + int i; + clock_t clk; if ( ++p->nRecCalls == MAX_CALL_NUM ) return 0; if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL ) @@ -1611,7 +1612,8 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) { Gia_StaAre_t * pSta; Gia_Obj_t * pObj; - int i, RetValue, clk = clock(); + int i, RetValue; + clock_t clk = clock(); pSta = Gia_ManAreSta( p, Sta ); if ( Gia_StaIsUnused(pSta) ) return 0; @@ -1671,7 +1673,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) SeeAlso [] ***********************************************************************/ -void Gia_ManArePrintReport( Gia_ManAre_t * p, int Time, int fFinal ) +void Gia_ManArePrintReport( Gia_ManAre_t * p, clock_t Time, int fFinal ) { printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f Mb. ", p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur), @@ -1703,7 +1705,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos // extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ); extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ); Gia_ManAre_t * p; - int clk = clock(); + clock_t clk = clock(); int RetValue = 1; if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM ) { diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c index 94ad069b..a905b220 100644 --- a/src/aig/gia/giaForce.c +++ b/src/aig/gia/giaForce.c @@ -892,7 +892,7 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose ) float * pVertX, VertX; int * pPermX, * pHandles; int k, h, Iter, iMinX, iMaxX, Counter, nCutStart, nCutCur, nCutCur2, nCutPrev; - int clk = clock(), clk2, clk2Total = 0; + clock_t clk = clock(), clk2, clk2Total = 0; // create starting one-dimensional placement vCoOrder = Frc_ManCollectCos( p ); if ( fRandomize ) @@ -1068,7 +1068,7 @@ void For_ManFileExperiment() FILE * pFile; int * pBuffer; int i, Size, Exp = 25; - int clk = clock(); + clock_t clk = clock(); int RetValue; Size = (1 << Exp); diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index 48a0568e..f3dbd95c 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -226,7 +226,7 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) Gia_ManUnr_t * p; Gia_Obj_t * pObj; int i, k, iRank, iFanin, Degree, Shift; - int clk = clock(); + clock_t clk = clock(); p = ABC_CALLOC( Gia_ManUnr_t, 1 ); p->pAig = pAig; @@ -605,7 +605,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p ) Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) { Gia_Man_t * pNew; - int clk = clock(); + clock_t clk = clock(); pNew = Gia_ManUnroll( pAig, pPars ); if ( pPars->fVerbose ) Abc_PrintTime( 1, "Time", clock() - clk ); diff --git a/src/aig/gia/giaGiarf.c b/src/aig/gia/giaGiarf.c index 2f18c16d..1e2d1d18 100644 --- a/src/aig/gia/giaGiarf.c +++ b/src/aig/gia/giaGiarf.c @@ -764,7 +764,7 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr; int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember; int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0; - int clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock(); + clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock(); if ( Vec_PtrSize(vOldRoots) == 0 ) return 0; // start SAT solvers @@ -1031,7 +1031,8 @@ void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, i Hcd_Man_t * p; Vec_Ptr_t * vRoots; Gia_Man_t * pGiaLev; - int i, Lev, nLevels, nIters, clk; + int i, Lev, nLevels, nIters; + clock_t clk; Gia_ManRandom( 1 ); Gia_ManSetPhase( pGia ); nLevels = Gia_ManLevelNum( pGia ); diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index fc4d2736..2b958cba 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -740,7 +740,8 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb ) ***********************************************************************/ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose ) { - int i, k, clk = clock(); + int i, k; + clock_t clk = clock(); Gia_ManRandom( 1 ); Gli_ManFinalize( p ); if ( p->nRegs == 0 ) diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c index 3f37e724..656c880a 100644 --- a/src/aig/gia/giaHcd.c +++ b/src/aig/gia/giaHcd.c @@ -44,7 +44,7 @@ struct Hcd_Pars_t_ int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver int fVerbose; // verbose stats - int timeSynth; // synthesis runtime + clock_t timeSynth; // synthesis runtime int nNodesAhead; // the lookahead in terms of nodes int nCallsRecycle; // calls to perform before recycling SAT solver }; @@ -610,7 +610,8 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis, Vec_Ptr_t * vGias; Gia_Man_t * pGia, * pMiter; Aig_Man_t * pAigNew; - int i, clk = clock(); + int i; + clock_t clk = clock(); // perform synthesis if ( fSynthesis ) { diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index dcfee68f..16d0e46c 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -82,12 +82,12 @@ struct Gia_IsoMan_t_ Vec_Int_t * vClasses; Vec_Int_t * vClasses2; // statistics - int timeStart; - int timeSim; - int timeRefine; - int timeSort; - int timeOther; - int timeTotal; + clock_t timeStart; + clock_t timeSim; + clock_t timeRefine; + clock_t timeSort; + clock_t timeOther; + clock_t timeTotal; }; static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); } @@ -178,7 +178,7 @@ void Gia_IsoPrintClasses( Gia_IsoMan_t * p ) printf( "\n" ); } } -void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int Time ) +void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, clock_t Time ) { printf( "Iter %4d : ", Iter ); printf( "Entries =%8d. ", p->nEntries ); @@ -298,8 +298,9 @@ void Gia_IsoAssignUnique( Gia_IsoMan_t * p ) int Gia_IsoSort( Gia_IsoMan_t * p ) { Gia_Obj_t * pObj, * pObj0; - int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew, clk; + int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew; int fRefined = 0; + clock_t clk; // go through the equiv classes p->nSingles = 0; @@ -722,7 +723,8 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose Gia_IsoMan_t * p; Vec_Ptr_t * vEquivs = NULL; int fRefined, fRefinedAll; - int i, c, clk = clock(), clkTotal = clock(); + int i, c; + clock_t clk = clock(), clkTotal = clock(); assert( Gia_ManCiNum(pGia) > 0 ); assert( Gia_ManPoNum(pGia) > 0 ); @@ -1070,7 +1072,8 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, int f Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings; Vec_Int_t * vRemain, * vLevel, * vLevel2; Vec_Str_t * vStr, * vStr2; - int i, k, s, sStart, Entry, Counter, clk = clock(); + int i, k, s, sStart, Entry, Counter; + clock_t clk = clock(); if ( pvPosEquivs ) *pvPosEquivs = NULL; @@ -1203,7 +1206,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, int f void Gia_IsoTest( Gia_Man_t * p, int fVerbose ) { Vec_Ptr_t * vEquivs; - int clk = clock(); + clock_t clk = clock(); vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose ); printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 ); Abc_PrintTime( 1, "Time", clock() - clk ); diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c index 0b9a6bfb..c1ff852e 100644 --- a/src/aig/gia/giaRetime.c +++ b/src/aig/gia/giaRetime.c @@ -266,7 +266,8 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose ) { Gia_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/gia/giaShrink.c b/src/aig/gia/giaShrink.c index ad03f1e4..2db815fc 100644 --- a/src/aig/gia/giaShrink.c +++ b/src/aig/gia/giaShrink.c @@ -52,7 +52,8 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pFanin; unsigned * pTruth; - int i, k, iFan, clk = clock(); + int i, k, iFan; + clock_t clk = clock(); // int ClassCounts[222] = {0}; int * pLutClass, Counter = 0; assert( p->pMapping != NULL ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 37406c8d..3f11679d 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -109,7 +109,7 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia ) int i, k, Lit, Count; int Counter0 = 0, Counter1 = 0; int CounterPi0 = 0, CounterPi1 = 0; - int clk = clock(); + clock_t clk = clock(); // create reset counters for each literal vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) ); @@ -609,9 +609,9 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) { extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); Gia_ManSim_t * p; - int i, clkTotal = clock(); - int iOut, iPat, RetValue = 0; -// int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0; + clock_t clkTotal = clock(); + int i, iOut, iPat, RetValue = 0; + clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; if ( pAig->pReprs && pAig->pNexts ) return Gia_ManSimSimulateEquiv( pAig, pPars ); ABC_FREE( pAig->pCexSeq ); @@ -648,7 +648,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) RetValue = 1; break; } - if ( time(NULL) > pPars->TimeLimit ) + if ( clock() > nTimeToStop ) { i++; break; diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c index 74a34d1b..5ac1392f 100644 --- a/src/aig/gia/giaSim2.c +++ b/src/aig/gia/giaSim2.c @@ -639,9 +639,9 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) { Gia_Sim2_t * p; Gia_Obj_t * pObj; - int i, clkTotal = clock(); - int RetValue = 0, iOut, iPat; - int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0; + clock_t clkTotal = clock(); + int i, RetValue = 0, iOut, iPat; + clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; assert( pAig->pReprs && pAig->pNexts ); ABC_FREE( pAig->pCexSeq ); p = Gia_Sim2Create( pAig, pPars ); @@ -682,7 +682,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars ) } if ( pAig->pReprs && pAig->pNexts ) Gia_Sim2InfoRefineEquivs( p ); - if ( time(NULL) > nTimeToStop ) + if ( clock() > nTimeToStop ) { i++; break; diff --git a/src/aig/gia/giaSort.c b/src/aig/gia/giaSort.c index f73e92bb..5183c441 100644 --- a/src/aig/gia/giaSort.c +++ b/src/aig/gia/giaSort.c @@ -160,7 +160,7 @@ void Gia_SortTest() { int nSize = 100000000; int * pArray; - int clk = clock(); + clock_t clk = clock(); printf( "Sorting %d integers\n", nSize ); pArray = Gia_SortGetTest( nSize ); diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index 628427d0..d1440ae0 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -559,7 +559,8 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) Gia_Obj_t * pObj; Vec_Int_t * vSwitching; float * pSwitching; - int i, clk, clkTotal = clock(); + int i; + clock_t clk, clkTotal = clock(); if ( pPars->fProbOne && pPars->fProbTrans ) printf( "Conflict of options: Can either compute probability of 1, or probability of switching by observing transitions.\n" ); // create manager diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c index c306e867..2f5e0293 100644 --- a/src/aig/gia/giaTsim.c +++ b/src/aig/gia/giaTsim.c @@ -669,7 +669,8 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose ) { Gia_ManTer_t * p; unsigned * pState, * pPrev, * pLoop; - int i, Counter, clk, clkTotal = clock(); + int i, Counter; + clock_t clk, clkTotal = clock(); assert( Gia_ManRegNum(pAig) > 0 ); // create manager clk = clock(); diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index 6411265f..d23f3508 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/vec/vec.h" @@ -106,8 +105,8 @@ struct Hop_Man_t_ Vec_Ptr_t * vPages; // memory pages used by nodes Hop_Obj_t * pListFree; // the list of free nodes // timing statistics - int time1; - int time2; + clock_t time1; + clock_t time2; }; //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/hop/hopTable.c b/src/aig/hop/hopTable.c index 7db93f62..1adab015 100644 --- a/src/aig/hop/hopTable.c +++ b/src/aig/hop/hopTable.c @@ -167,7 +167,8 @@ void Hop_TableResize( Hop_Man_t * p ) { Hop_Obj_t * pEntry, * pNext; Hop_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, nEntries, i, clk; + int nTableSizeOld, Counter, nEntries, i; + clock_t clk; clk = clock(); // save the old table pTableOld = p->pTable; diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h index a427f507..809e8e3f 100644 --- a/src/aig/ioa/ioa.h +++ b/src/aig/ioa/ioa.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/vec/vec.h" //#include "bar.h" diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h index 8d062134..f0292e6c 100644 --- a/src/aig/ivy/ivy.h +++ b/src/aig/ivy/ivy.h @@ -125,8 +125,8 @@ struct Ivy_Man_t_ Vec_Ptr_t * vPages; // memory pages used by nodes Ivy_Obj_t * pListFree; // the list of free nodes // timing statistics - int time1; - int time2; + clock_t time1; + clock_t time2; }; struct Ivy_FraigParams_t_ diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c index d5a31dee..19d37bb2 100644 --- a/src/aig/ivy/ivyCut.c +++ b/src/aig/ivy/ivyCut.c @@ -969,7 +969,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p ) { Ivy_Obj_t * pObj; int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver; - int clk = clock(); + clock_t clk = clock(); nNodeTotal = nNodeOver = 0; nCutsTotal = -Ivy_ManNodeNum(p); Ivy_ManForEachObj( p, pObj, i ) diff --git a/src/aig/ivy/ivyCutTrav.c b/src/aig/ivy/ivyCutTrav.c index a053c713..5834a6fc 100644 --- a/src/aig/ivy/ivyCutTrav.c +++ b/src/aig/ivy/ivyCutTrav.c @@ -439,7 +439,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p ) Vec_Int_t * vStore; Vec_Vec_t * vBitCuts; int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver; - int clk = clock(); + clock_t clk = clock(); vNodes = Vec_PtrAlloc( 100 ); vFront = Vec_PtrAlloc( 100 ); diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c index 1d9efca1..feeb36f2 100644 --- a/src/aig/ivy/ivyFastMap.c +++ b/src/aig/ivy/ivyFastMap.c @@ -67,7 +67,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj return pSupp; } -static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr ); +static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr ); static int Ivy_FastMapDelay( Ivy_Man_t * pAig ); static int Ivy_FastMapArea( Ivy_Man_t * pAig ); static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ); @@ -83,8 +83,8 @@ static int Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); static int Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); -extern int s_MappingTime; -extern int s_MappingMem; +extern clock_t s_MappingTime; +extern clock_t s_MappingMem; //////////////////////////////////////////////////////////////////////// @@ -106,7 +106,8 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo { Ivy_SuppMan_t * pMan; Ivy_Obj_t * pObj; - int i, Delay, Area, clk, clkTotal = clock(); + int i, Delay, Area; + clock_t clk, clkTotal = clock(); // start the memory for supports pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 ); memset( pMan, 0, sizeof(Ivy_SuppMan_t) ); @@ -210,7 +211,7 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr ) +void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr ) { printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area ); ABC_PRT( "Time", Time ); diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index cc6250e4..411402fb 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -93,16 +93,16 @@ struct Ivy_FraigMan_t_ int nSatFails; int nSatFailsReal; // runtime - int timeSim; - int timeTrav; - int timeSat; - int timeSatUnsat; - int timeSatSat; - int timeSatFail; - int timeRef; - int timeTotal; - int time1; - int time2; + clock_t timeSim; + clock_t timeTrav; + clock_t timeSat; + clock_t timeSatUnsat; + clock_t timeSatSat; + clock_t timeSatFail; + clock_t timeRef; + clock_t timeTotal; + clock_t time1; + clock_t time2; }; typedef struct Prove_ParamsStruct_t_ Prove_Params_t; @@ -198,7 +198,7 @@ static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew ); static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan ); static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ); -static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose ); +static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose ); static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p ); static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 ); @@ -257,7 +257,8 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) Prove_Params_t * pParams = (Prove_Params_t *)pPars; Ivy_FraigParams_t Params, * pIvyParams = &Params; Ivy_Man_t * pManAig, * pManTemp; - int RetValue, nIter, clk;//, Counter; + int RetValue, nIter; + clock_t clk;//, Counter; ABC_INT64_T nSatConfs = 0, nSatInspects = 0; // start the network and parameters @@ -414,7 +415,7 @@ Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pPara { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; - int clk; + clock_t clk; if ( Ivy_ManNodeNum(pManAig) == 0 ) return Ivy_ManDup(pManAig); clk = clock(); @@ -451,7 +452,7 @@ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; - int clk; + clock_t clk; if ( Ivy_ManNodeNum(pManAig) == 0 ) return Ivy_ManDup(pManAig); clk = clock(); @@ -481,7 +482,8 @@ Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; Ivy_Obj_t * pObj; - int i, clk; + int i; + clock_t clk; clk = clock(); assert( Ivy_ManLatchNum(pManAig) == 0 ); p = Ivy_FraigStartSimple( pManAig, pParams ); @@ -988,7 +990,8 @@ unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; - int i, clk; + int i; + clock_t clk; clk = clock(); Ivy_ManForEachNode( p->pManAig, pObj, i ) { @@ -1020,7 +1023,7 @@ p->nSimRounds++; void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p ) { Ivy_FraigSim_t * pSims; - int clk; + clock_t clk; clk = clock(); for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext ) Ivy_NodeSimulateSim( p, pSims ); @@ -1384,7 +1387,8 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p ) int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pClass2; - int clk, RetValue, Counter = 0; + int RetValue, Counter = 0; + clock_t clk; // check if some outputs already became non-constant // this is a special case when computation can be stopped!!! if ( p->pParams->fProve ) @@ -1789,7 +1793,7 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose ) +void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose ) { if ( !fVerbose ) return; @@ -1876,7 +1880,8 @@ int Ivy_FraigMiterStatus( Ivy_Man_t * pMan ) void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj, * pObjNew; - int i, RetValue, clk = clock(); + int i, RetValue; + clock_t clk = clock(); int fVerbose = 0; Ivy_ManForEachPo( p->pManAig, pObj, i ) { @@ -2093,7 +2098,8 @@ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p ) ***********************************************************************/ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { - int pLits[4], RetValue, RetValue1, nBTLimit, clk; //, clk2 = clock(); + int pLits[4], RetValue, RetValue1, nBTLimit; + clock_t clk; //, clk2 = clock(); // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); @@ -2259,7 +2265,8 @@ p->timeSatFail += clock() - clk; ***********************************************************************/ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) { - int pLits[2], RetValue1, clk; + int pLits[2], RetValue1; + clock_t clk; int RetValue; // make sure the nodes are not complemented @@ -2628,7 +2635,8 @@ int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int L ***********************************************************************/ int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { - int clk, LevelMin, LevelMax; + int LevelMin, LevelMax; + clock_t clk; assert( pOld || pNew ); clk = clock(); // reset the active variables diff --git a/src/aig/ivy/ivyResyn.c b/src/aig/ivy/ivyResyn.c index 8d571110..dc483bf6 100644 --- a/src/aig/ivy/ivyResyn.c +++ b/src/aig/ivy/ivyResyn.c @@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose ) { - int clk; + clock_t clk; Ivy_Man_t * pTemp; if ( fVerbose ) { printf( "Original:\n" ); } @@ -85,7 +85,7 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan ); ***********************************************************************/ Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose ) { - int clk; + clock_t clk; Ivy_Man_t * pTemp; if ( fVerbose ) { printf( "Original:\n" ); } @@ -154,7 +154,7 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan ); ***********************************************************************/ Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose ) { - int clk; + clock_t clk; Ivy_Man_t * pTemp; if ( fVerbose ) { printf( "Original:\n" ); } diff --git a/src/aig/ivy/ivyRwr.c b/src/aig/ivy/ivyRwr.c index 39131210..292bd3f9 100644 --- a/src/aig/ivy/ivyRwr.c +++ b/src/aig/ivy/ivyRwr.c @@ -57,7 +57,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV Rwt_Man_t * pManRwt; Ivy_Obj_t * pNode; int i, nNodes, nGain; - int clk, clkStart = clock(); + clock_t clk, clkStart = clock(); // start the rewriting manager pManRwt = Rwt_ManStart( 0 ); p->pData = pManRwt; @@ -164,7 +164,7 @@ int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUp int Required, nNodesSaved; int nNodesSaveCur = -1; // Suppress "might be used uninitialized" int i, c, GainCur, GainBest = -1; - int clk, clk2; + clock_t clk, clk2; p->nNodesConsidered++; // get the required times diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c index 283bf9fe..4a999780 100644 --- a/src/aig/ivy/ivySeq.c +++ b/src/aig/ivy/ivySeq.c @@ -65,7 +65,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) Rwt_Man_t * pManRwt; Ivy_Obj_t * pNode; int i, nNodes, nGain; - int clk, clkStart = clock(); + clock_t clk, clkStart = clock(); // set the DC latch values Ivy_ManForEachLatch( p, pNode, i ) @@ -157,7 +157,7 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int int nNodesSaved; int nNodesSaveCur = -1; // Suppress "might be used uninitialized" int i, c, GainCur, GainBest = -1; - int clk, clk2;//, clk3; + clock_t clk, clk2;//, clk3; p->nNodesConsidered++; // get the node's cuts @@ -1110,7 +1110,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs ) Ivy_Store_t * pStore; Ivy_Obj_t * pObj; int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver; - int clk = clock(); + clock_t clk = clock(); if ( nInputs > IVY_CUT_INPUT ) { printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT ); diff --git a/src/aig/ivy/ivyTable.c b/src/aig/ivy/ivyTable.c index d2c1ab9a..d2753aa8 100644 --- a/src/aig/ivy/ivyTable.c +++ b/src/aig/ivy/ivyTable.c @@ -206,7 +206,8 @@ int Ivy_TableCountEntries( Ivy_Man_t * p ) void Ivy_TableResize( Ivy_Man_t * p ) { int * pTableOld, * pPlace; - int nTableSizeOld, Counter, nEntries, e, clk; + int nTableSizeOld, Counter, nEntries, e; + clock_t clk; clk = clock(); // save the old table pTableOld = p->pTable; 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 |