diff options
Diffstat (limited to 'src/proof')
82 files changed, 409 insertions, 311 deletions
diff --git a/src/proof/bbr/bbrCex.c b/src/proof/bbr/bbrCex.c index 7ee95e7c..60fef07c 100644 --- a/src/proof/bbr/bbrCex.c +++ b/src/proof/bbr/bbrCex.c @@ -55,7 +55,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, DdNode * bTemp, * bVar, * bRing; int i, v, RetValue, nPiOffset; char * pValues; - int clk = clock(); + clock_t clk = clock(); //printf( "\nDeriving counter-example.\n" ); // allocate room for the counter-example diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 1cce1a90..19d87bc2 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -246,7 +246,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D DdNode * bTemp; Cudd_ReorderingType method; int i, nIters, nBddSize = 0, status; - int nThreshold = 10000, clk = clock(); + int nThreshold = 10000; + clock_t clk = clock(); Vec_Ptr_t * vOnionRings; status = Cudd_ReorderingStatus( dd, &method ); @@ -280,7 +281,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D for ( nIters = 0; nIters < pPars->nIterMax; nIters++ ) { // check the runtime limit - if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) ) + if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC ) { printf( "Reached timeout after image computation (%d seconds).\n", pPars->TimeLimit ); Vec_PtrFree( vOnionRings ); @@ -433,7 +434,8 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) DdManager * dd; DdNode ** pbParts, ** pbOutputs; DdNode * bInitial, * bTemp; - int RetValue, i, clk = clock(); + int RetValue, i; + clock_t clk = clock(); Vec_Ptr_t * vOnionRings; assert( Saig_ManRegNum(p) > 0 ); @@ -450,7 +452,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // check the runtime limit - if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) ) + if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC ) { printf( "Reached timeout after constructing global BDDs (%d seconds).\n", pPars->TimeLimit ); Cudd_Quit( dd ); diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index b9b3e1f1..841b6a0b 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -72,7 +72,8 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); - int RetValue, iOut, nOuts, clkTotal = clock(); + int RetValue, iOut, nOuts; + clock_t clkTotal = clock(); if ( piOutFail ) *piOutFail = -1; Gia_ManStop( pTemp ); @@ -134,7 +135,8 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) { Gia_Obj_t * pObj1, * pObj2; Gia_Obj_t * pDri1, * pDri2; - int i, clk = clock(); + int i; + clock_t clk = clock(); Gia_ManSetPhase( p ); Gia_ManForEachPo( p, pObj1, i ) { @@ -206,8 +208,9 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) int fDumpUndecided = 0; Cec_ParFra_t ParsFra, * pParsFra = &ParsFra; Gia_Man_t * p, * pNew; - int RetValue, clk = clock(); - double clkTotal = clock(); + int RetValue; + clock_t clk = clock(); + clock_t clkTotal = clock(); // consider special cases: // 1) (SAT) a pair of POs have different value under all-0 pattern // 2) (SAT) a pair of POs has different PI/Const drivers @@ -263,7 +266,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 ); Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); } - if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) + if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) { Gia_ManStop( pNew ); return -1; diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 3ddb975e..05b372f8 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -208,8 +208,8 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) Cec_ManSim_t * pSim; Gia_Man_t * pSrm; int r, RetValue; - int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock(); - int clk2, clk = clock(); + clock_t clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock(); + clock_t clk2, clk = clock(); ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); Gia_ManRandom( 1 ); diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 65c4b970..71519323 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -257,7 +257,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars ) { Cec_ManSim_t * pSim; - int RetValue = 0, clkTotal = clock(); + int RetValue = 0; + clock_t clkTotal = clock(); pSim = Cec_ManSimStart( pAig, pPars ); if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) || (RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) ) @@ -342,8 +343,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) Cec_ManFra_t * p; Cec_ManSim_t * pSim; Cec_ManPat_t * pPat; - int i, fTimeOut = 0, nMatches = 0, clk, clk2; - double clkTotal = clock(); + int i, fTimeOut = 0, nMatches = 0; + clock_t clk, clk2, clkTotal = clock(); // duplicate AIG and transfer equivalence classes Gia_ManRandom( 1 ); @@ -457,7 +458,7 @@ p->timeSat += clock() - clk; break; } // check resource limits - if ( p->pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit ) + if ( p->pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit ) { fTimeOut = 1; break; diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index d080dfea..e8b25b48 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -719,7 +719,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ) +void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time ) { int nLits, CounterX = 0, Counter0 = 0, Counter = 0; int i, Entry, nProve = 0, nDispr = 0, nFail = 0; @@ -789,7 +789,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr fChanges = 1; while ( fChanges ) { - int clkBmc = clock(); + clock_t clkBmc = clock(); fChanges = 0; pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); if ( Gia_ManPoNum(pSrm) == 0 ) @@ -844,9 +844,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; Cec_ManSim_t * pSim; Gia_Man_t * pSrm; - int r, RetValue, clkTotal = clock(); - int clkSat = 0, clkSim = 0, clkSrm = 0; - int clk2, clk = clock(); + int r, RetValue; + clock_t clkTotal = clock(); + clock_t clkSat = 0, clkSim = 0, clkSrm = 0; + clock_t clk2, clk = clock(); if ( Gia_ManRegNum(pAig) == 0 ) { Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c index 1db30705..3bea8dbf 100644 --- a/src/proof/cec/cecCorr_updated.c +++ b/src/proof/cec/cecCorr_updated.c @@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ) +void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time ) { int nLits, CounterX = 0, Counter0 = 0, Counter = 0; int i, Entry, nProve = 0, nDispr = 0, nFail = 0; diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index 371dedda..8d9fe472 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -61,13 +61,13 @@ struct Cec_ManPat_t_ int nSeries; // simulation series int fVerbose; // verbose stats // runtime statistics - int timeFind; // detecting the pattern - int timeShrink; // minimizing the pattern - int timeVerify; // verifying the result of minimisation - int timeSort; // sorting literals - int timePack; // packing into sim info structures - int timeTotal; // total runtime - int timeTotalSave; // total runtime for saving + clock_t timeFind; // detecting the pattern + clock_t timeShrink; // minimizing the pattern + clock_t timeVerify; // verifying the result of minimisation + clock_t timeSort; // sorting literals + clock_t timePack; // packing into sim info structures + clock_t timeTotal; // total runtime + clock_t timeTotalSave; // total runtime for saving }; // SAT solving manager @@ -154,10 +154,10 @@ struct Cec_ManFra_t_ int nAllDisproved; // total number of disproved nodes int nAllFailed; // total number of failed nodes // runtime stats - int timeSim; // unsat - int timePat; // unsat - int timeSat; // sat - int timeTotal; // total runtime + clock_t timeSim; // unsat + clock_t timePat; // unsat + clock_t timeSat; // sat + clock_t timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// @@ -169,7 +169,7 @@ struct Cec_ManFra_t_ //////////////////////////////////////////////////////////////////////// /*=== cecCorr.c ============================================================*/ -extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ); +extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time ); /*=== cecClass.c ============================================================*/ extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ); diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c index cb1dae46..f372f3bb 100644 --- a/src/proof/cec/cecPat.c +++ b/src/proof/cec/cecPat.c @@ -359,7 +359,8 @@ void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj ) void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t * pObj ) { Vec_Int_t * vPat; - int nPatLits, clk, clkTotal = clock(); + int nPatLits; + clock_t clk, clkTotal = clock(); assert( Gia_ObjIsCo(pObj) ); pMan->nPats++; pMan->nPatsAll++; @@ -451,7 +452,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW int iStartOld = pMan->iStart; int nWords = nWordsInit; int nBits = 32 * nWords; - int clk = clock(); + clock_t clk = clock(); vInfo = Vec_PtrAllocSimInfo( nInputs, nWords ); Gia_ManRandomInfo( vInfo, 0, 0, nWords ); vPres = Vec_PtrAllocSimInfo( nInputs, nWords ); diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c index 2ccbe524..3afbd1c8 100644 --- a/src/proof/cec/cecSeq.c +++ b/src/proof/cec/cecSeq.c @@ -215,7 +215,8 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ) { Vec_Ptr_t * vSimInfo; - int RetValue, clkTotal = clock(); + int RetValue; + clock_t clkTotal = clock(); if ( pCex == NULL ) { Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" ); diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index e779e68c..5e108ae5 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -471,7 +471,8 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { Gia_Obj_t * pObjR = Gia_Regular(pObj); int nBTLimit = p->pPars->nBTLimit; - int Lit, RetValue, status, clk, clk2, nConflicts; + int Lit, RetValue, status, nConflicts; + clock_t clk, clk2; if ( pObj == Gia_ManConst0(p->pAig) ) return 1; @@ -570,7 +571,8 @@ int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pOb Gia_Obj_t * pObjR1 = Gia_Regular(pObj1); Gia_Obj_t * pObjR2 = Gia_Regular(pObj2); int nBTLimit = p->pPars->nBTLimit; - int Lits[2], RetValue, status, clk, clk2, nConflicts; + int Lits[2], RetValue, status, nConflicts; + clock_t clk, clk2; if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) ) return 1; @@ -676,7 +678,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; Gia_Obj_t * pObj; - int i, status, clk = clock(), clk2; + int i, status; + clock_t clk = clock(), clk2; // reset the manager if ( pPat ) { @@ -717,7 +720,7 @@ clk2 = clock(); // save the pattern if ( pPat ) { - int clk3 = clock(); + clock_t clk3 = clock(); Cec_ManPatSavePattern( pPat, p, pObj ); pPat->timeTotalSave += clock() - clk3; } @@ -799,7 +802,8 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat Cec_ManSat_t * p; Gia_Obj_t * pObj; int iPat = 0, nPatsInit, nPats; - int i, status, clk = clock(); + int i, status; + clock_t clk = clock(); nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); @@ -957,7 +961,8 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St Vec_Str_t * vStatus; Cec_ManSat_t * p; Gia_Obj_t * pObj; - int i, status, clk = clock(); + int i, status; + clock_t clk = clock(); // prepare AIG Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c index 4523810e..505de076 100644 --- a/src/proof/cec/cecSweep.c +++ b/src/proof/cec/cecSweep.c @@ -188,7 +188,8 @@ int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t { Vec_Ptr_t * vInfo; Gia_Obj_t * pObj, * pObjOld, * pReprOld; - int i, k, iRepr, iNode, clk; + int i, k, iRepr, iNode; + clock_t clk; clk = clock(); vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords ); p->timePat += clock() - clk; diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c index 21470dd4..b13b5204 100644 --- a/src/proof/cec/cecSynth.c +++ b/src/proof/cec/cecSynth.c @@ -297,7 +297,8 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) Vec_Int_t * vPart; int * pMapBack, * pReprs; int i, nCountPis, nCountRegs; - int nClasses, clk = clock(); + int nClasses; + clock_t clk = clock(); // save parameters if ( fPrintParts ) diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h index 731eb776..ff29f0da 100644 --- a/src/proof/dch/dch.h +++ b/src/proof/dch/dch.h @@ -54,7 +54,7 @@ struct Dch_Pars_t_ int fUseCSat; // uses circuit-based solver int fLightSynth; // uses lighter version of synthesis 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 }; diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index bc78682b..bfef8d8c 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -89,7 +89,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; - int clk, clkTotal = clock(); + clock_t clk, clkTotal = clock(); // reset random numbers Aig_ManRandom(1); // start the choicing manager @@ -131,7 +131,7 @@ p->timeTotal = clock() - clkTotal; void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; - int clk, clkTotal = clock(); + clock_t clk, clkTotal = clock(); // reset random numbers Aig_ManRandom(1); // start the choicing manager diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h index c9f2f4f6..b22834cf 100644 --- a/src/proof/dch/dchInt.h +++ b/src/proof/dch/dchInt.h @@ -84,15 +84,15 @@ struct Dch_Man_t_ int nEquivs; // the number of final equivalences int nChoices; // the number of final choice nodes // runtime stats - int timeSimInit; // simulation and class computation - int timeSimSat; // simulation of the counter-examples - int timeSat; // solving SAT - int timeSatSat; // sat - int timeSatUnsat; // unsat - int timeSatUndec; // undecided - int timeChoice; // choice computation - int timeOther; // other runtime - int timeTotal; // total runtime + clock_t timeSimInit; // simulation and class computation + clock_t timeSimSat; // simulation of the counter-examples + clock_t timeSat; // solving SAT + clock_t timeSatSat; // sat + clock_t timeSatUnsat; // unsat + clock_t timeSatUndec; // undecided + clock_t timeChoice; // choice computation + clock_t timeOther; // other runtime + clock_t timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c index f5e346ef..fefd5ce2 100644 --- a/src/proof/dch/dchSat.c +++ b/src/proof/dch/dchSat.c @@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int nBTLimit = p->pPars->nBTLimit; - int pLits[2], RetValue, RetValue1, status, clk; + int pLits[2], RetValue, RetValue1, status; + clock_t clk; p->nSatCalls++; // sanity checks diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c index 6f69b47e..26de4643 100644 --- a/src/proof/dch/dchSimSat.c +++ b/src/proof/dch/dchSimSat.c @@ -177,7 +177,8 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { Aig_Obj_t * pRoot, ** ppClass; - int i, k, nSize, RetValue1, RetValue2, clk = clock(); + int i, k, nSize, RetValue1, RetValue2; + clock_t clk = clock(); // get the equivalence classes Dch_ManCollectTfoCands( p, pObj, pRepr ); // resimulate the cone of influence of the solved nodes @@ -224,7 +225,8 @@ p->timeSimSat += clock() - clk; void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { Aig_Obj_t * pRoot; - int i, RetValue, clk = clock(); + int i, RetValue; + clock_t clk = clock(); // get the equivalence class if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) ) Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots ); diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h index 3e50ff57..c1dd6b44 100644 --- a/src/proof/fra/fra.h +++ b/src/proof/fra/fra.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/aig/aig/aig.h" @@ -238,17 +237,17 @@ struct Fra_Man_t_ int nSatCallsRecent; int nSatCallsSkipped; // runtime - int timeSim; - int timeTrav; - int timeRwr; - int timeSat; - int timeSatUnsat; - int timeSatSat; - int timeSatFail; - int timeRef; - int timeTotal; - int time1; - int time2; + clock_t timeSim; + clock_t timeTrav; + clock_t timeRwr; + clock_t timeSat; + clock_t timeSatUnsat; + clock_t timeSatSat; + clock_t timeSatFail; + clock_t timeRef; + clock_t timeTotal; + clock_t time1; + clock_t time2; }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c index 2ddecf48..4b68a79a 100644 --- a/src/proof/fra/fraBmc.c +++ b/src/proof/fra/fraBmc.c @@ -311,7 +311,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ) { Aig_Obj_t * pObj; - int i, nImpsOld = 0, clk = clock(); + int i, nImpsOld = 0; + clock_t clk = clock(); assert( p->pBmc == NULL ); // derive and fraig the frames p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth ); @@ -385,7 +386,8 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew Fra_Man_t * pTemp; Fra_Bmc_t * pBmc; Aig_Man_t * pAigTemp; - int clk, iOutput; + clock_t clk; + int iOutput; // derive and fraig the frames clk = clock(); pBmc = Fra_BmcStart( pAig, 0, nFrames ); diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index 0acca245..20805ec2 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -53,7 +53,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi sat_solver2 * pSat; Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); + int status, RetValue; + clock_t clk = clock(); Vec_Int_t * vCiIds; assert( Aig_ManRegNum(pMan) == 0 ); @@ -159,7 +160,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi { sat_solver * pSat; Cnf_Dat_t * pCnf; - int status, RetValue, clk = clock(); + int status, RetValue; + clock_t clk = clock(); Vec_Int_t * vCiIds; assert( Aig_ManRegNum(pMan) == 0 ); @@ -282,7 +284,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) Fra_Par_t Params, * pParams = &Params; Aig_Man_t * pAig = *ppAig, * pTemp; - int i, RetValue, clk; + int i, RetValue; + clock_t clk; // report the original miter if ( fVerbose ) @@ -457,7 +460,8 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n { Aig_Man_t * pTemp; //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); - int RetValue, clkTotal = clock(); + int RetValue; + clock_t clkTotal = clock(); if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) ) { diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c index f651b0ad..97ac3e40 100644 --- a/src/proof/fra/fraClaus.c +++ b/src/proof/fra/fraClaus.c @@ -605,7 +605,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs ) Fra_Sml_t * pComb, * pSeq; Aig_Obj_t * pObj; Dar_Cut_t * pCut; - int Scores[16], uScores, i, k, j, clk, nCuts = 0; + int Scores[16], uScores, i, k, j, nCuts = 0; + clock_t clk; // simulate the AIG clk = clock(); @@ -727,7 +728,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs ) Fra_Sml_t * pComb, * pSeq; Aig_Obj_t * pObj; Aig_Cut_t * pCut; - int i, k, j, clk, nCuts = 0; + int i, k, j, nCuts = 0; + clock_t clk; int ScoresSeq[1<<12], ScoresComb[1<<12]; assert( p->nLutSize < 13 ); @@ -1622,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) unsigned * pResultTot, * pResultOne; int nCovered, Beg, End, i, w; int * pStart, * pVar2Id; - int clk = clock(); + clock_t clk = clock(); // simulate the circuit with nCombSimWords * 32 = 64K patterns // srand( 0xAABBAABB ); Aig_ManRandom(1); @@ -1680,7 +1682,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose ) { Clu_Man_t * p; - int clk, clkTotal = clock(), clkInd; + clock_t clk, clkTotal = clock(), clkInd; int b, Iter, Counter, nPrefOld; int nClausesBeg = 0; diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c index 37aaa0da..35888f43 100644 --- a/src/proof/fra/fraCore.c +++ b/src/proof/fra/fraCore.c @@ -376,7 +376,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ) { Fra_Man_t * p; Aig_Man_t * pManAigNew; - int clk; + clock_t clk; if ( Aig_ManNodeNum(pManAig) == 0 ) return Aig_ManDupOrdered(pManAig); clk = clock(); @@ -402,7 +402,7 @@ Fra_ClassesPrint( p->pCla, 1 ); Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) { -int clk2 = clock(); +clock_t clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); pManAigNew = Aig_ManDupRepr( p->pManAig, 1 ); Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) ); diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c index 338b5717..a91c939f 100644 --- a/src/proof/fra/fraHot.c +++ b/src/proof/fra/fraHot.c @@ -332,7 +332,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) Vec_Ptr_t * vSimInfo; unsigned * pSim1, * pSim2, * pSimTot; int i, w, Out1, Out2, nCovered, Counter = 0; - int clk = clock(); + clock_t clk = clock(); // generate random sim-info at register outputs vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords ); diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c index f65aca5c..4d33717a 100644 --- a/src/proof/fra/fraImp.c +++ b/src/proof/fra/fraImp.c @@ -327,7 +327,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in int * pImpCosts, * pNodesI, * pNodesK; int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; int CostMin = ABC_INFINITY, CostMax = 0; - int i, k, Imp, CostRange, clk = clock(); + int i, k, Imp, CostRange; + clock_t clk = clock(); assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c index 29a76eea..633f8979 100644 --- a/src/proof/fra/fraInd.c +++ b/src/proof/fra/fraInd.c @@ -49,7 +49,8 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p ) { Aig_Man_t * pTemp; Aig_Obj_t * pObj, * pObjPo; - int nTruePis, k, i, clk = clock(); + int nTruePis, k, i; + clock_t clk = clock(); // perform AIG rewriting on the speculated frames // pTemp = Dar_ManRwsat( pTemp, 1, 0 ); pTemp = Dar_ManRewriteDefault( p->pManFraig ); @@ -259,7 +260,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) int * pMapBack; int i, nCountPis, nCountRegs; int nClasses, nPartSize, fVerbose; - int clk = clock(); + clock_t clk = clock(); // save parameters nPartSize = pPars->nPartSize; pPars->nPartSize = 0; @@ -357,8 +358,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) Aig_Man_t * pManAigNew = NULL; int nNodesBeg, nRegsBeg; int nIter = -1; // Suppress "might be used uninitialized" - int i, clk = clock(), clk2; - int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC); + int i; + clock_t clk = clock(), clk2; + clock_t TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + clock() : 0; if ( Aig_ManNodeNum(pManAig) == 0 ) { @@ -473,7 +475,7 @@ ABC_PRT( "Time", clock() - clk ); int nLitsOld = Fra_ClassesCountLits(p->pCla); int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; - int clk3 = clock(); + clock_t clk3 = clock(); if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) { diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c index 7c5e9e70..099256ac 100644 --- a/src/proof/fra/fraIndVer.c +++ b/src/proof/fra/fraIndVer.c @@ -50,7 +50,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve int * pStart; int RetValue, Beg, End, i, k; int CounterBase = 0, CounterInd = 0; - int clk = clock(); + clock_t clk = clock(); if ( nFrames != 1 ) { diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c index 8ea6d297..2941f24f 100644 --- a/src/proof/fra/fraLcr.c +++ b/src/proof/fra/fraLcr.c @@ -54,12 +54,12 @@ struct Fra_Lcr_t_ int nRegsBeg; int nRegsEnd; // runtime - int timeSim; - int timePart; - int timeTrav; - int timeFraig; - int timeUpdate; - int timeTotal; + clock_t timeSim; + clock_t timePart; + clock_t timeTrav; + clock_t timeFraig; + clock_t timeUpdate; + clock_t timeTotal; }; //////////////////////////////////////////////////////////////////////// @@ -538,8 +538,9 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC Fra_Man_t * pTemp; Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL; Vec_Int_t * vPart; - int i, nIter, timeSim, clk2, clk3, clk = clock(); - int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC); + int i, nIter; + clock_t timeSim, clk2, clk3, clk = clock(); + clock_t TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock() : 0; if ( Aig_ManNodeNum(pAig) == 0 ) { if ( pnIter ) *pnIter = 0; diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c index e3bb2850..e1c8ddf4 100644 --- a/src/proof/fra/fraPart.c +++ b/src/proof/fra/fraPart.c @@ -53,7 +53,7 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ) int i, k, nCommon, CountOver, CountQuant; int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar; double Ratio, R; - int clk; + clock_t clk; nTotalSupp = 0; nTotalSupp2 = 0; @@ -190,7 +190,8 @@ void Fra_ManPartitionTest2( Aig_Man_t * p ) Vec_Int_t * vSup, * vSup2, * vSup3; Aig_Obj_t * pObj; int Entry, Entry2, Entry3, Counter; - int i, k, m, n, clk; + int i, k, m, n; + clock_t clk; char * pSupp; // compute supports diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c index 2702113c..fc95fd62 100644 --- a/src/proof/fra/fraSat.c +++ b/src/proof/fra/fraSat.c @@ -47,7 +47,8 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * ***********************************************************************/ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { - int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock(); + int pLits[4], RetValue, RetValue1, nBTLimit; + clock_t clk;//, clk2 = clock(); int status; // make sure the nodes are not complemented @@ -207,7 +208,8 @@ p->timeSatFail += clock() - clk; ***********************************************************************/ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ) { - int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock(); + int pLits[4], RetValue, RetValue1, nBTLimit; + clock_t clk;//, clk2 = clock(); int status; // make sure the nodes are not complemented @@ -314,7 +316,8 @@ p->timeSatFail += clock() - clk; ***********************************************************************/ int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ) { - int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock(); + int pLits[4], RetValue, RetValue1, nBTLimit; + clock_t clk;//, clk2 = clock(); int status; // make sure the nodes are not complemented @@ -421,7 +424,8 @@ p->timeSatFail += clock() - clk; ***********************************************************************/ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ) { - int pLits[2], RetValue1, RetValue, clk; + int pLits[2], RetValue1, RetValue; + clock_t clk; // make sure the nodes are not complemented assert( !Aig_IsComplement(pNew) ); @@ -535,7 +539,8 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i ***********************************************************************/ int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_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/proof/fra/fraSec.c b/src/proof/fra/fraSec.c index cde56809..ac6cd67e 100644 --- a/src/proof/fra/fraSec.c +++ b/src/proof/fra/fraSec.c @@ -98,7 +98,8 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult ) Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; - int nFrames, RetValue, nIter, clk, clkTotal = clock(); + int nFrames, RetValue, nIter; + clock_t clk, clkTotal = clock(); int TimeOut = 0; int fLatchCorr = 0; float TimeLeft = 0.0; diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c index 66579be3..555789e2 100644 --- a/src/proof/fra/fraSim.c +++ b/src/proof/fra/fraSim.c @@ -662,7 +662,8 @@ int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p ) void Fra_SmlSimulateOne( Fra_Sml_t * p ) { Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int f, i, clk; + int f, i; + clock_t clk; clk = clock(); for ( f = 0; f < p->nFrames; f++ ) { @@ -700,7 +701,8 @@ p->nSimRounds++; ***********************************************************************/ void Fra_SmlResimulate( Fra_Man_t * p ) { - int nChanges, clk; + int nChanges; + clock_t clk; Fra_SmlAssignDist1( p->pSml, p->pPatWords ); Fra_SmlSimulateOne( p->pSml ); // if ( p->pPars->fPatScores ) @@ -735,7 +737,8 @@ p->timeRef += clock() - clk; void Fra_SmlSimulate( Fra_Man_t * p, int fInit ) { int fVerbose = 0; - int nChanges, nClasses, clk; + int nChanges, nClasses; + clock_t clk; assert( !fInit || Aig_ManRegNum(p->pManAig) ); // start the classes Fra_SmlInitialize( p->pSml, fInit ); diff --git a/src/proof/fraig/fraig.h b/src/proof/fraig/fraig.h index 6d672716..0c021feb 100644 --- a/src/proof/fraig/fraig.h +++ b/src/proof/fraig/fraig.h @@ -154,9 +154,6 @@ extern void Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse extern void Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ); extern void Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve ); extern void Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose ); -extern void Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time ); -extern void Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time ); -extern void Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time ); extern void Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ); extern void Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames ); extern void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode ); diff --git a/src/proof/fraig/fraigApi.c b/src/proof/fraig/fraigApi.c index 6e0ab959..b0b47075 100644 --- a/src/proof/fraig/fraigApi.c +++ b/src/proof/fraig/fraigApi.c @@ -91,9 +91,6 @@ void Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse ) { p- void Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ) { p->fChoicing = fChoicing; } void Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve ) { p->fTryProve = fTryProve; } void Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose ) { p->fVerbose = fVerbose; } -void Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time ) { p->timeToAig = Time; } -void Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time ) { p->timeToNet = Time; } -void Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time ) { p->timeTotal = Time; } void Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppOutputNames = ppNames; } void Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppInputNames = ppNames; } diff --git a/src/proof/fraig/fraigChoice.c b/src/proof/fraig/fraigChoice.c index 21d4fe10..e1d6e8a7 100644 --- a/src/proof/fraig/fraigChoice.c +++ b/src/proof/fraig/fraigChoice.c @@ -45,7 +45,7 @@ void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit ) { // ProgressBar * pProgress; char Buffer[100]; - int clkTotal = clock(); + clock_t clkTotal = clock(); int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes; int /*nMaxLevel,*/ nDistributive; Fraig_Node_t *pNode, *pRepr; diff --git a/src/proof/fraig/fraigFeed.c b/src/proof/fraig/fraigFeed.c index 47f946e1..4cb1276b 100644 --- a/src/proof/fraig/fraigFeed.c +++ b/src/proof/fraig/fraigFeed.c @@ -80,7 +80,8 @@ void Fraig_FeedBackInit( Fraig_Man_t * p ) void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) { int nVarsPi, nWords; - int i, clk = clock(); + int i; + clock_t clk = clock(); // get the number of PI vars in the feedback (also sets the PI values) nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars ); diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h index f6a5d74f..1ff8727e 100644 --- a/src/proof/fraig/fraigInt.h +++ b/src/proof/fraig/fraigInt.h @@ -28,7 +28,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/util/abc_global.h" #include "fraig.h" @@ -189,18 +188,18 @@ struct Fraig_ManStruct_t_ int nImplies1; // runtime statistics - int timeToAig; // time to transfer to the mapping structure - int timeSims; // time to compute k-feasible cuts - int timeTrav; // time to traverse the network - int timeFeed; // time for solver feedback (recording and resimulating) - int timeImply; // time to analyze implications - int timeSat; // time to compute the truth table for each cut - int timeToNet; // time to transfer back to the network - int timeTotal; // the total mapping time - int time1; // time to perform one task - int time2; // time to perform another task - int time3; // time to perform another task - int time4; // time to perform another task + clock_t timeToAig; // time to transfer to the mapping structure + clock_t timeSims; // time to compute k-feasible cuts + clock_t timeTrav; // time to traverse the network + clock_t timeFeed; // time for solver feedback (recording and resimulating) + clock_t timeImply; // time to analyze implications + clock_t timeSat; // time to compute the truth table for each cut + clock_t timeToNet; // time to transfer back to the network + clock_t timeTotal; // the total mapping time + clock_t time1; // time to perform one task + clock_t time2; // time to perform another task + clock_t time3; // time to perform another task + clock_t time4; // time to perform another task }; // the mapping node diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c index 125a4da1..bc7c423d 100644 --- a/src/proof/fraig/fraigMan.c +++ b/src/proof/fraig/fraigMan.c @@ -25,8 +25,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -int timeSelect; -int timeAssign; +clock_t timeSelect; +clock_t timeAssign; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -323,8 +323,8 @@ void Fraig_ManFree( Fraig_Man_t * p ) ***********************************************************************/ void Fraig_ManCreateSolver( Fraig_Man_t * p ) { - extern int timeSelect; - extern int timeAssign; + extern clock_t timeSelect; + extern clock_t timeAssign; assert( p->pSat == NULL ); // allocate data for SAT solving p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 ); diff --git a/src/proof/fraig/fraigNode.c b/src/proof/fraig/fraigNode.c index 609d5f65..5310534b 100644 --- a/src/proof/fraig/fraigNode.c +++ b/src/proof/fraig/fraigNode.c @@ -87,7 +87,8 @@ Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p ) Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p ) { Fraig_Node_t * pNode, * pNodeRes; - int i, clk; + int i; + clock_t clk; // create the node pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes ); @@ -159,7 +160,7 @@ p->timeSims += clock() - clk; Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 ) { Fraig_Node_t * pNode; - int clk; + clock_t clk; // create the node pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes ); diff --git a/src/proof/fraig/fraigSat.c b/src/proof/fraig/fraigSat.c index 6ccd1b86..7a11c072 100644 --- a/src/proof/fraig/fraigSat.c +++ b/src/proof/fraig/fraigSat.c @@ -85,7 +85,8 @@ int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * void Fraig_ManProveMiter( Fraig_Man_t * p ) { Fraig_Node_t * pNode; - int i, clk; + int i; + clock_t clk; if ( !p->fTryProve ) return; @@ -300,7 +301,8 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ***********************************************************************/ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) { - int RetValue, RetValue1, i, fComp, clk; + int RetValue, RetValue1, i, fComp; + clock_t clk; int fVerbose = 0; int fSwitch = 0; @@ -548,7 +550,8 @@ p->time3 += clock() - clk; ***********************************************************************/ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) { - int RetValue, RetValue1, i, fComp, clk; + int RetValue, RetValue1, i, fComp; + clock_t clk; int fVerbose = 0; // make sure the nodes are not complemented @@ -650,7 +653,8 @@ p->time3 += clock() - clk; int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) { Fraig_Node_t * pNode1R, * pNode2R; - int RetValue, RetValue1, i, clk; + int RetValue, RetValue1, i; + clock_t clk; int fVerbose = 0; pNode1R = Fraig_Regular(pNode1); diff --git a/src/proof/fraig/fraigTable.c b/src/proof/fraig/fraigTable.c index 6611e4fa..d184ab7f 100644 --- a/src/proof/fraig/fraigTable.c +++ b/src/proof/fraig/fraigTable.c @@ -260,7 +260,8 @@ void Fraig_TableResizeS( Fraig_HashTable_t * p ) { Fraig_Node_t ** pBinsNew; Fraig_Node_t * pEnt, * pEnt2; - int nBinsNew, Counter, i, clk; + int nBinsNew, Counter, i; + clock_t clk; unsigned Key; clk = clock(); @@ -303,7 +304,8 @@ void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR ) { Fraig_Node_t ** pBinsNew; Fraig_Node_t * pEnt, * pEnt2; - int nBinsNew, Counter, i, clk; + int nBinsNew, Counter, i; + clock_t clk; unsigned Key; clk = clock(); diff --git a/src/proof/fraig/fraigUtil.c b/src/proof/fraig/fraigUtil.c index ae78a61f..316b492e 100644 --- a/src/proof/fraig/fraigUtil.c +++ b/src/proof/fraig/fraigUtil.c @@ -844,7 +844,7 @@ int Fraig_ManPrintRefs( Fraig_Man_t * pMan ) Fraig_NodeVec_t * vPivots; Fraig_Node_t * pNode, * pNode2; int i, k, Counter, nProved; - int clk; + clock_t clk; vPivots = Fraig_NodeVecAlloc( 1000 ); for ( i = 0; i < pMan->vNodes->nSize; i++ ) diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c index 2b14d8ae..28ef54a7 100644 --- a/src/proof/int/intCheck.c +++ b/src/proof/int/intCheck.c @@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB ) SeeAlso [] ***********************************************************************/ -int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut ) +int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, clock_t nTimeNewOut ) { Aig_Obj_t * pObj, * pObj2; int i, f, VarA, VarB, RetValue, Entry, status; diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index d4ef1f94..c226c7e1 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -80,8 +80,9 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, Inter_Man_t * p; Inter_Check_t * pCheck = NULL; Aig_Man_t * pAigTemp; - int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp = 0; - int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0; + int s, i, RetValue, Status; + clock_t clk, clk2, clkTotal = clock(), timeTemp = 0; + clock_t nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + clock() : 0; // enable ORing of the interpolants, if containment check is performed inductively with K > 1 if ( pPars->nFramesK > 1 ) @@ -256,7 +257,7 @@ p->timeEqu += clock() - clk; } else if ( RetValue == -1 ) { - if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out + if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out { if ( pPars->fVerbose ) printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); @@ -341,7 +342,7 @@ p->timeEqu += clock() - clk - timeTemp; Inter_CheckStop( pCheck ); return 1; } - if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) + if ( pPars->nSecLimit && clock() > nTimeNewOut ) { printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); p->timeTotal = clock() - clkTotal; diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c index 04aaa271..840ae75d 100644 --- a/src/proof/int/intCtrex.c +++ b/src/proof/int/intCtrex.c @@ -99,7 +99,8 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) Aig_Man_t * pFrames; sat_solver * pSat; Cnf_Dat_t * pCnf; - int status, clk = clock(); + int status; + clock_t clk = clock(); Vec_Int_t * vCiIds; // create timeframes assert( Saig_ManPoNum(pAig) == 1 ); diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h index 6a033d85..ec2a0356 100644 --- a/src/proof/int/intInt.h +++ b/src/proof/int/intInt.h @@ -70,13 +70,13 @@ struct Inter_Man_t_ int nConfLimit; // the limit on the number of conflicts int fVerbose; // the verbosiness flag // runtime - int timeRwr; - int timeCnf; - int timeSat; - int timeInt; - int timeEqu; - int timeOther; - int timeTotal; + clock_t timeRwr; + clock_t timeCnf; + clock_t timeSat; + clock_t timeInt; + clock_t timeEqu; + clock_t timeOther; + clock_t timeTotal; }; // containment checking manager @@ -93,7 +93,7 @@ typedef struct Inter_Check_t_ Inter_Check_t; /*=== intCheck.c ============================================================*/ extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ); extern void Inter_CheckStop( Inter_Check_t * p ); -extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut ); +extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, clock_t nTimeNewOut ); /*=== intContain.c ============================================================*/ extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); @@ -117,7 +117,7 @@ extern void Inter_ManClean( Inter_Man_t * p ); extern void Inter_ManStop( Inter_Man_t * p, int fProved ); /*=== intM114.c ============================================================*/ -extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ); +extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut ); /*=== intM114p.c ============================================================*/ #ifdef ABC_USE_LIBRARIES diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c index ed3ef80e..bf44696d 100644 --- a/src/proof/int/intM114.c +++ b/src/proof/int/intM114.c @@ -200,15 +200,16 @@ sat_solver * Inter_ManDeriveSatSolver( SeeAlso [] ***********************************************************************/ -int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ) +int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut ) { sat_solver * pSat; void * pSatCnf = NULL; Inta_Man_t * pManInterA; // Intb_Man_t * pManInterB; int * pGlobalVars; - int clk, status, RetValue; + int status, RetValue; int i, Var; + clock_t clk; // assert( p->pInterNew == NULL ); // derive the SAT solver diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c index 8027bdef..b93a7453 100644 --- a/src/proof/int/intUtil.c +++ b/src/proof/int/intUtil.c @@ -49,7 +49,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p ) Aig_Obj_t * pObj; sat_solver * pSat; int i, status; - int clk = clock(); + clock_t clk = clock(); pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 ); if ( pSat == NULL ) @@ -87,7 +87,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p ) Cnf_Dat_t * pCnf; sat_solver * pSat; int status; - int clk = clock(); + clock_t clk = clock(); pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); Cnf_DataFree( pCnf ); diff --git a/src/proof/llb/llb.h b/src/proof/llb/llb.h index a9bfd891..464f4526 100644 --- a/src/proof/llb/llb.h +++ b/src/proof/llb/llb.h @@ -65,7 +65,7 @@ struct Gia_ParLlb_t_ int TimeLimit; // time limit for one reachability run int TimeLimitGlo; // time limit for all reachability runs // internal parameters - int TimeTarget; // the time to stop + clock_t TimeTarget; // the time to stop int iFrame; // explored up to this frame }; diff --git a/src/proof/llb/llb1Core.c b/src/proof/llb/llb1Core.c index 56e0cc6b..b16fdee7 100644 --- a/src/proof/llb/llb1Core.c +++ b/src/proof/llb/llb1Core.c @@ -114,7 +114,7 @@ int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * Llb_Man_t * p = NULL; Aig_Man_t * pAig; int RetValue = -1; - int clk = clock(); + clock_t clk = clock(); if ( pPars->fIndConstr ) { diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c index 51d3a9fc..07877a98 100644 --- a/src/proof/llb/llb1Hint.c +++ b/src/proof/llb/llb1Hint.c @@ -165,7 +165,7 @@ int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars ) Vec_Int_t * vHints; Vec_Int_t * vHFCands; int i, Entry, RetValue = -1; - int clk = clock(); + clock_t clk = clock(); assert( pPars->nHintDepth > 0 ); /* // perform reachability without hints diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index 60124378..fed0389a 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -47,7 +47,8 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager DdNode * bBdd0, * bBdd1, * bFunc; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; - int i, TimeStop; + int i; + clock_t TimeStop; if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) ) return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) ); TimeStop = dd->TimeStop; dd->TimeStop = 0; @@ -156,7 +157,7 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; int i, iGroupFirst, iGroupLast; - int TimeStop; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) @@ -205,7 +206,8 @@ DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG { Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; - int i, iGroupLast, TimeStop; + int i, iGroupLast; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) @@ -248,7 +250,8 @@ DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG { Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; - int i, iGroupFirst, TimeStop; + int i, iGroupFirst; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) @@ -295,7 +298,8 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd ) { Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; - int i, iVar, TimeStop; + int i, iVar; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( p->pAig, pObj, i ) @@ -409,7 +413,8 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs { DdNode * bConstr, * bFunc, * bTemp; Aig_Obj_t * pObj; - int i, Entry, TimeStop; + int i, Entry; + clock_t TimeStop; if ( vHints == NULL ) return Cudd_ReadOne( p->dd ); TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; @@ -581,11 +586,12 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs ); DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube; DdNode * bConstrCs, * bConstrNs; - int clk2, clk = clock(), nIters, nBddSize = 0; + clock_t clk2, clk = clock(); + int nIters, nBddSize = 0; // int nThreshold = 10000; // compute time to stop - p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; // define variable limits Llb_ManPrepareVarLimits( p ); @@ -656,7 +662,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo { clk2 = clock(); // check the runtime limit - if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c index f4359493..57745c1d 100644 --- a/src/proof/llb/llb2Bad.c +++ b/src/proof/llb/llb2Bad.c @@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) +DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, clock_t TimeOut ) { Vec_Ptr_t * vNodes; DdNode * bBdd0, * bBdd1, * bTemp, * bResult; @@ -110,7 +110,8 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) { DdNode * bVar, * bCube, * bTemp; Aig_Obj_t * pObj; - int i, TimeStop; + int i; + clock_t TimeStop; assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) ); TimeStop = dd->TimeStop; dd->TimeStop = 0; // create PI cube diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c index 3b98c32a..f19f757e 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -68,7 +68,8 @@ struct Llb_Img_t_ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues ) { DdNode * bRes, * bVar, * bTemp; - int i, iVar, Index, TimeStop; + int i, iVar, Index; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Vec_IntForEachEntry( vVars, Index, i ) @@ -209,7 +210,8 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo ); int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs ); DdNode * bCurrent, * bReached, * bNext, * bTemp; - int clk2, clk = clock(), nIters, nBddSize;//, iOutFail = -1; + clock_t clk2, clk = clock(); + int nIters, nBddSize;//, iOutFail = -1; /* // compute time to stop if ( p->pPars->TimeLimit ) @@ -218,7 +220,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ p->pPars->TimeTarget = 0; */ - if ( time(NULL) > p->pPars->TimeTarget ) + if ( clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit ); @@ -286,7 +288,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ { clk2 = clock(); // check the runtime limit - if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -529,7 +531,7 @@ int Llb_CoreReachability( Llb_Img_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, int TimeTarget ) +Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, clock_t TimeTarget ) { DdManager * dd; Vec_Ptr_t * vDdMans; @@ -689,7 +691,7 @@ void Llb_CoreStop( Llb_Img_t * p ) SeeAlso [] ***********************************************************************/ -int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ) +int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, clock_t TimeTarget ) { int RetValue; Llb_Img_t * p; @@ -726,10 +728,10 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) Vec_Ptr_t * vResult; Aig_Man_t * p; int RetValue = -1; - int clk = clock(); + clock_t clk = clock(); // compute time to stop - pPars->TimeTarget = pPars->TimeLimit ? time(NULL) + pPars->TimeLimit : 0; + pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; p = Aig_ManDupFlopsOnly( pAig ); //Aig_ManShow( p, 0, NULL ); @@ -741,7 +743,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose ); - if ( pPars->TimeLimit && time(NULL) > pPars->TimeTarget ) + if ( pPars->TimeLimit && clock() > pPars->TimeTarget ) { if ( !pPars->fSilent ) printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit ); diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c index 4998b1ad..40d7a116 100644 --- a/src/proof/llb/llb2Driver.c +++ b/src/proof/llb/llb2Driver.c @@ -129,7 +129,8 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager { DdNode * bCube, * bVar, * bTemp; Aig_Obj_t * pObj; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); Saig_ManForEachLi( pAig, pObj, i ) @@ -159,7 +160,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager SeeAlso [] ***********************************************************************/ -DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ) +DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, clock_t TimeTarget ) { // int fVerbose = 1; DdManager * dd; diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index 40ca19e5..f82fcf58 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -1226,7 +1226,8 @@ Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryV { int nVolMax = Aig_ManNodeNum(p) / Num; Vec_Ptr_t * vResult, * vMinCut = NULL, * vLower, * vUpper; - int i, k, nVol, clk = clock(); + int i, k, nVol; + clock_t clk = clock(); vResult = Vec_PtrAlloc( 100 ); Vec_PtrPush( vResult, Llb_ManComputeCutLo(p) ); Vec_PtrPush( vResult, Llb_ManComputeCutLi(p) ); diff --git a/src/proof/llb/llb2Image.c b/src/proof/llb/llb2Image.c index 99ffbdc4..cfaef13c 100644 --- a/src/proof/llb/llb2Image.c +++ b/src/proof/llb/llb2Image.c @@ -179,7 +179,7 @@ void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pv SeeAlso [] ***********************************************************************/ -DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ) +DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, clock_t TimeTarget ) { Vec_Ptr_t * vNodes, * vRange; Aig_Obj_t * pObj; @@ -259,7 +259,8 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * { DdNode * bProd, * bTemp; Aig_Obj_t * pObj; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd ); Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i ) @@ -287,7 +288,8 @@ void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQ { DdManager * dd; DdNode * bProd, * bRes, * bTemp; - int i, clk = clock(); + int i; + clock_t clk = clock(); Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) { // remember unquantified ones @@ -360,12 +362,13 @@ void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans ) ***********************************************************************/ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, - int TimeTarget, int fBackward, int fReorder, int fVerbose ) + clock_t TimeTarget, int fBackward, int fReorder, int fVerbose ) { // int fCheckSupport = 0; DdManager * ddPart; DdNode * bImage, * bGroup, * bCube, * bTemp; - int i, clk, clk0 = clock(); + int i; + clock_t clk, clk0 = clock(); bImage = bInit; Cudd_Ref( bImage ); if ( fBackward ) diff --git a/src/proof/llb/llb3Image.c b/src/proof/llb/llb3Image.c index 708af6d5..dcce8441 100644 --- a/src/proof/llb/llb3Image.c +++ b/src/proof/llb/llb3Image.c @@ -79,7 +79,7 @@ static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pPart for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ ) // statistics -int timeBuild, timeAndEx, timeOther; +clock_t timeBuild, timeAndEx, timeOther; int nSuppMax; //////////////////////////////////////////////////////////////////////// @@ -140,7 +140,8 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart, pVar, i ) @@ -172,7 +173,8 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart1, pVar, i ) @@ -337,7 +339,7 @@ int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset ) SeeAlso [] ***********************************************************************/ -int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit, int TimeOut ) +int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 ) { int fVerbose = 0; Llb_Var_t * pVar; @@ -373,7 +375,7 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" ); RetValue = Llb_NonlinQuantify1( p, pPart2, 1 ); if ( RetValue ) Limit = Limit + 1000; - Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ); + Llb_NonlinQuantify2( p, pPart1, pPart2 ); return 0; } Cudd_Ref( bFunc ); @@ -537,7 +539,7 @@ Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * v SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd, int TimeOut ) +Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd ) { Vec_Ptr_t * vNodes, * vResult; Aig_Obj_t * pObj; @@ -655,13 +657,13 @@ void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc ) SeeAlso [] ***********************************************************************/ -int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut ) +int Llb_NonlinStart( Llb_Mgr_t * p ) { Vec_Ptr_t * vRootBdds; DdNode * bFunc; int i; // create and collect BDDs - vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced + vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced if ( vRootBdds == NULL ) return 0; // add pairs (refs are consumed inside) @@ -745,7 +747,7 @@ int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ***********************************************************************/ void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose ) { - int clk = clock(); + clock_t clk = clock(); if ( fVerbose ) Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); @@ -880,17 +882,17 @@ void Llb_NonlinFree( Llb_Mgr_t * p ) ***********************************************************************/ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, - DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeOut ) + DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder ) { Llb_Prt_t * pPart, * pPart1, * pPart2; Llb_Mgr_t * p; DdNode * bFunc, * bTemp; int i, nReorders, timeInside; - int clk = clock(), clk2; + clock_t clk = clock(), clk2; // start the manager clk2 = clock(); p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd ); - if ( !Llb_NonlinStart( p, TimeOut ) ) + if ( !Llb_NonlinStart( p ) ) { Llb_NonlinFree( p ); return NULL; @@ -913,7 +915,7 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo { clk2 = clock(); nReorders = Cudd_ReadReorderings(dd); - if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ) ) + if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) ) { Llb_NonlinFree( p ); return NULL; @@ -958,10 +960,10 @@ static Llb_Mgr_t * p = NULL; SeeAlso [] ***********************************************************************/ -DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget ) +DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, clock_t TimeTarget ) { DdManager * dd; - int clk = clock(); + clock_t clk = clock(); assert( p == NULL ); // start a new manager (disable reordering) dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); @@ -971,7 +973,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); // start the manager p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd ); - if ( !Llb_NonlinStart( p, 0 ) ) + if ( !Llb_NonlinStart( p ) ) { Llb_NonlinFree( p ); p = NULL; @@ -999,7 +1001,7 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int Llb_Prt_t * pPart, * pPart1, * pPart2; DdNode * bFunc, * bTemp; int i, nReorders, timeInside = 0; - int clk = clock(), clk2; + clock_t clk = clock(), clk2; // add partition Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent ); @@ -1020,7 +1022,7 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int { clk2 = clock(); nReorders = Cudd_ReadReorderings(p->dd); - if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, 0, 0 ) ) + if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) ) { Llb_NonlinFree( p ); return NULL; diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 38d9b8ae..48724136 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -54,14 +54,14 @@ struct Llb_Mnn_t_ int ddLocReos; int ddLocGrbs; - int timeImage; - int timeTran1; - int timeTran2; - int timeGloba; - int timeOther; - int timeTotal; - int timeReo; - int timeReoG; + clock_t timeImage; + clock_t timeTran1; + clock_t timeTran2; + clock_t timeGloba; + clock_t timeOther; + clock_t timeTotal; + clock_t timeReo; + clock_t timeReoG; }; @@ -90,7 +90,7 @@ int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig ) DdNode * bCof, * bVar; int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1; int Size, Size0, Size1; - int clk = clock(); + clock_t clk = clock(); Size = Cudd_DagSize(bFunc); // printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n", // Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) ); @@ -215,7 +215,8 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) { Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; - int i, iVar, TimeStop; + int i, iVar; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( pAig, pObj, i ) @@ -302,7 +303,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) //Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" ); // compute the next states bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState, - p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, ABC_INFINITY ); // consumed reference + p->pPars->fReorder, p->pPars->fVeryVerbose, NULL ); // consumed reference assert( bImage != NULL ); Cudd_Ref( bImage ); //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" ); @@ -429,11 +430,11 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) { DdNode * bTemp, * bNext; int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax; - int clk2, clk3, clk = clock(); + clock_t clk2, clk3, clk = clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); // compute time to stop - p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; // set the stop time parameter p->dd->TimeStop = p->pPars->TimeTarget; @@ -472,7 +473,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) { // check the runtime limit clk2 = clock(); - if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -807,7 +808,7 @@ void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num ) Llb_Mnn_t * pMnn; Gia_ParLlb_t Pars, * pPars = &Pars; Aig_Man_t * p; - int clk = clock(); + clock_t clk = clock(); Llb_ManSetDefaultParams( pPars ); pPars->fVerbose = 1; @@ -851,7 +852,7 @@ int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) if ( !pPars->fSkipReach ) { - int clk = clock(); + clock_t clk = clock(); pMnn = Llb_MnnStart( pAig, p, pPars ); RetValue = Llb_NonlinReachability( pMnn ); pMnn->timeTotal = clock() - clk; diff --git a/src/proof/llb/llb4Image.c b/src/proof/llb/llb4Image.c index 039be164..4ae087b5 100644 --- a/src/proof/llb/llb4Image.c +++ b/src/proof/llb/llb4Image.c @@ -77,7 +77,7 @@ static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pPart for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ ) // statistics -//int timeBuild, timeAndEx, timeOther; +//clock_t timeBuild, timeAndEx, timeOther; //int nSuppMax; //////////////////////////////////////////////////////////////////////// @@ -139,7 +139,8 @@ DdNode * Llb_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart, pVar, i ) @@ -171,7 +172,8 @@ DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart1, pVar, i ) diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index af8dad75..f2973922 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -47,11 +47,11 @@ struct Llb_Mnx_t_ Vec_Int_t * vOrder; // for each object ID, its BDD variable number or -1 Vec_Int_t * vVars2Q; // 1 if variable is quantifiable; 0 othervise - int timeImage; - int timeRemap; - int timeReo; - int timeOther; - int timeTotal; + clock_t timeImage; + clock_t timeRemap; + clock_t timeReo; + clock_t timeOther; + clock_t timeTotal; }; //extern int timeBuild, timeAndEx, timeOther; @@ -446,7 +446,8 @@ DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_ { Aig_Obj_t * pObjLi, * pObjLo; DdNode * bRes, * bVar, * bTemp; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) @@ -475,7 +476,8 @@ DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * v { Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp; DdNode * bRes, * bVar, * bTemp; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) @@ -667,7 +669,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) { DdNode * bAux; int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0; - int clkTemp, clkIter, clk = clock(); + clock_t clkTemp, clkIter, clk = clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); if ( p->pPars->fBackward ) @@ -736,7 +738,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) { clkIter = clock(); // check the runtime limit - if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -904,7 +906,7 @@ printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurr ***********************************************************************/ void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose ) { - int clk = clock(); + clock_t clk = clock(); if ( fVerbose ) Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); @@ -940,7 +942,7 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) p->pPars = pPars; // compute time to stop - p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; if ( pPars->fCluster ) { @@ -1071,7 +1073,7 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) return RetValue; } { - int clk = clock(); + clock_t clk = clock(); pMnn = Llb_MnxStart( pAig, pPars ); //Llb_MnxCheckNextStateVars( pMnn ); if ( !pPars->fSkipReach ) diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c index 6b223ab9..709bd61a 100644 --- a/src/proof/llb/llb4Sweep.c +++ b/src/proof/llb/llb4Sweep.c @@ -286,7 +286,8 @@ DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdMa { Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; - int i, TimeStop; + int i; + clock_t TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachPo( pAig, pObj, i ) diff --git a/src/proof/llb/llbInt.h b/src/proof/llb/llbInt.h index d81aadcf..58e2b543 100644 --- a/src/proof/llb/llbInt.h +++ b/src/proof/llb/llbInt.h @@ -152,34 +152,34 @@ extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, D extern void Llb_MtrSchedule( Llb_Mtr_t * p ); /*=== llb2Bad.c ======================================================*/ -extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ); +extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, clock_t TimeOut ); extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ); /*=== llb2Core.c ======================================================*/ extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues ); -extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ); +extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, clock_t TimeTarget ); /*=== llb2Driver.c ======================================================*/ extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p ); extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs ); extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig ); extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd ); -extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ); +extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, clock_t TimeTarget ); /*=== llb2Image.c ======================================================*/ extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose ); extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose ); -extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ); +extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, clock_t TimeTarget ); extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose ); extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans ); extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, - int TimeTarget, int fBackward, int fReorder, int fVerbose ); + clock_t TimeTarget, int fBackward, int fReorder, int fVerbose ); -extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget ); +extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, clock_t TimeTarget ); extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ); extern void Llb_NonlinImageQuit(); /*=== llb3Image.c =======================================================*/ extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, - DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget ); + DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder ); /*=== llb3Nonlin.c ======================================================*/ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ); diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 9cecbd78..765894e3 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -418,7 +418,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) Pdr_Obl_t * pThis; Pdr_Set_t * pPred, * pCubeMin; int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0; - int kMax = Vec_PtrSize(p->vSolvers)-1, clk; + int kMax = Vec_PtrSize(p->vSolvers)-1; + clock_t clk; p->nBlocks++; // create first proof obligation assert( p->pQueue == NULL ); @@ -528,7 +529,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) } // check the timeout - if ( p->timeToStop && time(NULL) > p->timeToStop ) + if ( p->timeToStop && clock() > p->timeToStop ) return -1; } return 1; @@ -551,7 +552,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_Set_t * pCube; int k, RetValue = -1; clock_t clkStart = clock(); - p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0; + p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // create the first timeframe Pdr_ManCreateSolver( p, (k = 0) ); @@ -633,7 +634,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } // check the timeout - if ( p->timeToStop && time(NULL) > p->timeToStop ) + if ( p->timeToStop && clock() > p->timeToStop ) { if ( fPrintClauses ) { diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c index ff428fa1..4fa9c07a 100644 --- a/src/proof/ssw/sswBmc.c +++ b/src/proof/ssw/sswBmc.c @@ -128,7 +128,8 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo Ssw_Frm_t * pFrm; Ssw_Sat_t * pSat; Aig_Obj_t * pObj, * pObjFrame; - int status, clkPart, Lit, i, f, RetValue; + int status, Lit, i, f, RetValue; + clock_t clkPart; // start managers assert( Saig_ManRegNum(pAig) > 0 ); diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c index 581b8aed..28c4947a 100644 --- a/src/proof/ssw/sswClass.c +++ b/src/proof/ssw/sswClass.c @@ -610,7 +610,8 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, Ssw_Sml_t * pSml; Vec_Ptr_t * vCands; Aig_Obj_t * pObj; - int i, k, RetValue, clk; + int i, k, RetValue; + clock_t clk; // start the classes p = Ssw_ClassesStart( pAig ); diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index 82977edb..5459aa72 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -408,7 +408,8 @@ int Ssw_ManSweepBmcConstr_old( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; - int i, f, iLits, clk; + int i, f, iLits; + clock_t clk; clk = clock(); // start initialized timeframes @@ -497,7 +498,8 @@ p->timeBmc += clock() - clk; int Ssw_ManSweepBmcConstr( Ssw_Man_t * p ) { Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; - int i, f, iLits, clk; + int i, f, iLits; + clock_t clk; clk = clock(); // start initialized timeframes @@ -618,7 +620,8 @@ int Ssw_ManSweepConstr( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; - int nConstrPairs, clk, i, f, iLits; + int nConstrPairs, i, f, iLits; + clock_t clk; //Ssw_ManPrintPolarity( p->pAig ); // perform speculative reduction diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index c51d421c..b27e7eaf 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques; Aig_Man_t * pAigNew; int RetValue, nIter = -1; - int clk, clkTotal = clock(); + clock_t clk, clkTotal = clock(); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesBeg = Aig_ManNodeNum(p->pAig); diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index 617bb40f..760f457a 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -262,7 +262,8 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) ***********************************************************************/ int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f ) { - int RetValue1, RetValue2, clk = clock(); + int RetValue1, RetValue2; + clock_t clk = clock(); // transfer PI simulation information from storage // Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); Ssw_ManSweepTransferDyn( p ); @@ -294,7 +295,8 @@ p->timeSimSat += clock() - clk; int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f ) { Aig_Obj_t * pObj, * pRepr, ** ppClass; - int i, k, nSize, RetValue1, RetValue2, clk = clock(); + int i, k, nSize, RetValue1, RetValue2; + clock_t clk = clock(); p->nSimRounds++; // transfer PI simulation information from storage // Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); @@ -372,7 +374,8 @@ int Ssw_ManSweepDyn( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObjNew; - int clk, i, f; + int i, f; + clock_t clk; // perform speculative reduction clk = clock(); diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c index 5f467123..3fff79bb 100644 --- a/src/proof/ssw/sswFilter.c +++ b/src/proof/ssw/sswFilter.c @@ -278,7 +278,8 @@ Aig_Obj_t * Ssw_ManSweepBmcFilter_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) { Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; - int f, f1, i, clkTotal = clock(); + int f, f1, i; + clock_t clkTotal = clock(); // start initialized timeframes p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); Saig_ManForEachLo( p->pAig, pObj, i ) @@ -383,7 +384,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun Ssw_Pars_t Pars, * pPars = &Pars; Ssw_Man_t * p; int r, TimeLimitPart;//, clkTotal = clock(); - int nTimeToStop = TimeLimit ? TimeLimit + time(NULL) : 0; + clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); // consider the case of empty AIG @@ -429,7 +430,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun Ssw_ClassesPrint( p->ppClasses, 0 ); } p->pMSat = Ssw_SatStart( 0 ); - TimeLimitPart = TimeLimit ? nTimeToStop - time(NULL) : 0; + TimeLimitPart = TimeLimit ? (nTimeToStop - clock()) / CLOCKS_PER_SEC : 0; if ( TimeLimit2 ) { if ( TimeLimitPart ) @@ -444,7 +445,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun // simulate pattern forward Ssw_ManRollForward( p, p->pPars->nFramesK ); // check timeout - if ( TimeLimit && time(NULL) > nTimeToStop ) + if ( TimeLimit && clock() > nTimeToStop ) { printf( "Reached timeout (%d seconds).\n", TimeLimit ); break; diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h index acd273fd..8749cec1 100644 --- a/src/proof/ssw/sswInt.h +++ b/src/proof/ssw/sswInt.h @@ -127,16 +127,16 @@ struct Ssw_Man_t_ int nRegsBegC; int nRegsEndC; // runtime stats - int timeBmc; // bounded model checking - int timeReduce; // speculative reduction - int timeMarkCones; // marking the cones not to be refined - int timeSimSat; // simulation of the counter-examples - int timeSat; // solving SAT - int timeSatSat; // sat - int timeSatUnsat; // unsat - int timeSatUndec; // undecided - int timeOther; // other runtime - int timeTotal; // total runtime + clock_t timeBmc; // bounded model checking + clock_t timeReduce; // speculative reduction + clock_t timeMarkCones; // marking the cones not to be refined + clock_t timeSimSat; // simulation of the counter-examples + clock_t timeSat; // solving SAT + clock_t timeSatSat; // sat + clock_t timeSatUnsat; // unsat + clock_t timeSatUndec; // undecided + clock_t timeOther; // other runtime + clock_t timeTotal; // total runtime }; // internal SAT manager diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c index 8f54432d..97e9cf54 100644 --- a/src/proof/ssw/sswIslands.c +++ b/src/proof/ssw/sswIslands.c @@ -479,7 +479,8 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai { Ssw_Pars_t Pars; Aig_Man_t * pAigRes; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); // derive parameters if not given if ( pPars == NULL ) Ssw_ManSetDefaultParams( pPars = &Pars ); diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c index 71f148e3..e58e9b50 100644 --- a/src/proof/ssw/sswLcorr.c +++ b/src/proof/ssw/sswLcorr.c @@ -77,7 +77,8 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) ***********************************************************************/ int Ssw_ManSweepResimulate( Ssw_Man_t * p ) { - int RetValue1, RetValue2, clk = clock(); + int RetValue1, RetValue2; + clock_t clk = clock(); // transfer PI simulation information from storage Ssw_ManSweepTransfer( p ); // simulate internal nodes @@ -159,7 +160,8 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj ) { Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi; - int RetValue, clk; + int RetValue; + clock_t clk; assert( Aig_ObjIsCi(pObj) ); assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) ); // check if it makes sense to skip some calls diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c index e356aa60..e4228685 100644 --- a/src/proof/ssw/sswPairs.c +++ b/src/proof/ssw/sswPairs.c @@ -320,7 +320,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) Ssw_Pars_t Pars, * pPars = &Pars; Vec_Int_t * vIds1, * vIds2; Aig_Obj_t * pObj, * pRepr; - int RetValue, i, clk = clock(); + int RetValue, i; + clock_t clk = clock(); Ssw_ManSetDefaultParams( pPars ); pPars->fVerbose = 1; pAigNew = Ssw_SignalCorrespondence( pAig, pPars ); @@ -379,7 +380,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) { Aig_Man_t * pAigRes; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); assert( vIds1 != NULL && vIds2 != NULL ); // try the new AIGs printf( "Performing specialized verification with node pairs.\n" ); @@ -413,7 +415,8 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) { Aig_Man_t * pAigRes, * pMiter; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); // try the new AIGs printf( "Performing general verification without node pairs.\n" ); pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); @@ -449,7 +452,8 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) { Aig_Man_t * pAigRes; - int RetValue, clk = clock(); + int RetValue; + clock_t clk = clock(); // try the new AIGs // printf( "Performing general verification without node pairs.\n" ); pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c index 5a3aea10..22340779 100644 --- a/src/proof/ssw/sswPart.c +++ b/src/proof/ssw/sswPart.c @@ -53,7 +53,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) int * pMapBack; int i, nCountPis, nCountRegs; int nClasses, nPartSize, fVerbose; - int clk = clock(); + clock_t clk = clock(); if ( pPars->fConstrs ) { printf( "Cannot use partitioned computation with constraints.\n" ); diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 032bc5ba..7048927f 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -286,7 +286,8 @@ void transpose64Simple( word A[64], word B[64] ) void TransposeTest() { word M[64], N[64]; - int i, clk; + int i; + clock_t clk; Aig_ManRandom64( 1 ); // for ( i = 0; i < 64; i++ ) // M[i] = Aig_ManRandom64( 0 ); @@ -896,8 +897,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in int fTryBmc = 0; int fMiter = 1; Ssw_RarMan_t * p; - int r, f = -1, clk, clkTotal = clock(); - int nTimeToStop = time(NULL) + TimeOut; + int r, f = -1; + clock_t clk, clkTotal = clock(); + clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; int RetValue = -1; int iFrameFail = -1; assert( Aig_ManRegNum(pAig) > 0 ); @@ -945,7 +947,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in goto finish; } // check timeout - if ( TimeOut && time(NULL) > nTimeToStop ) + if ( TimeOut && clock() > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); @@ -1013,8 +1015,9 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, in int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) { Ssw_RarMan_t * p; - int r, f = -1, i, k, clkTotal = clock(); - int nTimeToStop = time(NULL) + TimeOut; + int r, f = -1, i, k; + clock_t clkTotal = clock(); + clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -1084,7 +1087,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize goto finish; } // check timeout - if ( TimeOut && time(NULL) > nTimeToStop ) + if ( TimeOut && clock() > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c index 0851cf3d..1d93de60 100644 --- a/src/proof/ssw/sswRarity2.c +++ b/src/proof/ssw/sswRarity2.c @@ -308,8 +308,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i { int fMiter = 1; Ssw_RarMan_t * p; - int r, clk, clkTotal = clock(); - int nTimeToStop = time(NULL) + TimeOut; + int r; + clock_t clk, clkTotal = clock(); + clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -352,7 +353,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i printf( "." ); } // check timeout - if ( TimeOut && time(NULL) > nTimeToStop ) + if ( TimeOut && clock() > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); @@ -386,8 +387,9 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz { int fMiter = 0; Ssw_RarMan_t * p; - int r, i, k, clkTotal = clock(); - int nTimeToStop = time(NULL) + TimeOut; + int r, i, k; + clock_t clkTotal = clock(); + clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; int RetValue = -1; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); @@ -460,7 +462,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz Ssw_RarTransferPatterns( p, p->vInits ); Ssw_SmlInitializeSpecial( p->pSml, p->vInits ); // check timeout - if ( TimeOut && time(NULL) > nTimeToStop ) + if ( TimeOut && clock() > nTimeToStop ) { if ( fVerbose ) printf( "\n" ); printf( "Reached timeout (%d seconds).\n", TimeOut ); diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c index 7d371cac..e5971a64 100644 --- a/src/proof/ssw/sswSat.c +++ b/src/proof/ssw/sswSat.c @@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int nBTLimit = p->pPars->nBTLimit; - int pLits[3], nLits, RetValue, RetValue1, clk;//, status; + int pLits[3], nLits, RetValue, RetValue1; + clock_t clk;//, status; p->nSatCalls++; p->pMSat->nSolverCalls++; diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c index a04f6f54..e58ba848 100644 --- a/src/proof/ssw/sswSemi.c +++ b/src/proof/ssw/sswSemi.c @@ -179,7 +179,8 @@ int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets ) Ssw_Man_t * p = pBmc->pMan; Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; unsigned * pInfo; - int i, f, clk, RetValue, fFirst = 0; + int i, f, RetValue, fFirst = 0; + clock_t clk; clk = clock(); // start initialized timeframes @@ -260,7 +261,8 @@ p->timeBmc += clock() - clk; int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ) { Ssw_Sem_t * p; - int RetValue, Frames, Iter, clk = clock(); + int RetValue, Frames, Iter; + clock_t clk = clock(); p = Ssw_SemManStart( pMan, nConfMax, fVerbose ); if ( fCheckTargets && Ssw_SemCheckTargets( p ) ) { diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c index b53e8baf..bb4a55d2 100644 --- a/src/proof/ssw/sswSim.c +++ b/src/proof/ssw/sswSim.c @@ -38,7 +38,7 @@ struct Ssw_Sml_t_ int nWordsPref; // the number of word in the prefix int fNonConstOut; // have seen a non-const-0 output during simulation int nSimRounds; // statistics - int timeSim; // statistics + clock_t timeSim; // statistics unsigned pData[0]; // simulation data for the nodes }; @@ -1005,7 +1005,8 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ) void Ssw_SmlSimulateOne( Ssw_Sml_t * p ) { Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int f, i, clk; + int f, i; + clock_t clk; clk = clock(); for ( f = 0; f < p->nFrames; f++ ) { @@ -1116,7 +1117,8 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p ) { Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, clk; + int i; + clock_t clk; clk = clock(); // simulate the nodes Aig_ManForEachNode( p->pAig, pObj, i ) diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c index 098b1e0f..4d1b3ba2 100644 --- a/src/proof/ssw/sswSimSat.c +++ b/src/proof/ssw/sswSimSat.c @@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr ) { Aig_Obj_t * pObj; - int i, RetValue1, RetValue2, clk = clock(); + int i, RetValue1, RetValue2; + clock_t clk = clock(); // set the PI simulation information Aig_ManConst1(p->pAig)->fMarkB = 1; Aig_ManForEachCi( p->pAig, pObj, i ) @@ -90,7 +91,8 @@ p->timeSimSat += clock() - clk; ***********************************************************************/ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) { - int RetValue1, RetValue2, clk = clock(); + int RetValue1, RetValue2; + clock_t clk = clock(); // set the PI simulation information Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); // simulate internal nodes diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 5dd7a1f2..ab6952a2 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -187,7 +187,8 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs ) { Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; - int RetValue, clk; + int RetValue; + clock_t clk; // get representative of this class pObjRepr = Aig_ObjRepr( p->pAig, pObj ); if ( pObjRepr == NULL ) @@ -267,7 +268,8 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; - int i, f, clk; + int i, f; + clock_t clk; clk = clock(); // start initialized timeframes @@ -365,7 +367,8 @@ int Ssw_ManSweep( Ssw_Man_t * p ) static int Counter; Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; - int nConstrPairs, clk, i, f; + int nConstrPairs, i, f; + clock_t clk; Vec_Int_t * vDisproved; // perform speculative reduction |