diff options
Diffstat (limited to 'src/proof/llb')
-rw-r--r-- | src/proof/llb/llb.h | 2 | ||||
-rw-r--r-- | src/proof/llb/llb1Core.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb1Hint.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb1Reach.c | 24 | ||||
-rw-r--r-- | src/proof/llb/llb2Bad.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb2Core.c | 32 | ||||
-rw-r--r-- | src/proof/llb/llb2Driver.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb2Flow.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb2Image.c | 18 | ||||
-rw-r--r-- | src/proof/llb/llb3Image.c | 42 | ||||
-rw-r--r-- | src/proof/llb/llb3Nonlin.c | 66 | ||||
-rw-r--r-- | src/proof/llb/llb4Cex.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb4Image.c | 10 | ||||
-rw-r--r-- | src/proof/llb/llb4Nonlin.c | 48 | ||||
-rw-r--r-- | src/proof/llb/llb4Sweep.c | 2 | ||||
-rw-r--r-- | src/proof/llb/llbInt.h | 12 |
16 files changed, 140 insertions, 140 deletions
diff --git a/src/proof/llb/llb.h b/src/proof/llb/llb.h index 464f4526..f465359d 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 - clock_t TimeTarget; // the time to stop + abctime 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 3aa7a6e5..213f2cd9 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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); if ( pPars->fIndConstr ) { @@ -176,7 +176,7 @@ int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * RetValue = Llb_ManReachability( p, vHints, pddGlo ); Llb_ManStop( p ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( pPars->fIndConstr ) Vec_IntFreeP( &vHints ); diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c index 07877a98..353b4c69 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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); assert( pPars->nHintDepth > 0 ); /* // perform reachability without hints @@ -212,7 +212,7 @@ Finish: Vec_IntFreeP( &vHFCands ); Vec_IntFreeP( &vHints ); if ( pPars->fVerbose ) - Abc_PrintTime( 1, "Total runtime", clock() - clk ); + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk ); return RetValue; } diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index b7d79994..2acd3020 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -48,7 +48,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; int i; - clock_t TimeStop; + abctime TimeStop; if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) ) return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) ); TimeStop = dd->TimeStop; dd->TimeStop = 0; @@ -157,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; - clock_t TimeStop; + abctime 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 ) @@ -207,7 +207,7 @@ DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; int i, iGroupLast; - clock_t TimeStop; + abctime 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 ) @@ -251,7 +251,7 @@ DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; int i, iGroupFirst; - clock_t TimeStop; + abctime 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 ) @@ -299,7 +299,7 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd ) Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; int i, iVar; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( p->pAig, pObj, i ) @@ -414,7 +414,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs DdNode * bConstr, * bFunc, * bTemp; Aig_Obj_t * pObj; int i, Entry; - clock_t TimeStop; + abctime TimeStop; if ( vHints == NULL ) return Cudd_ReadOne( p->dd ); TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; @@ -586,12 +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; - clock_t clk2, clk = clock(); + abctime clk2, clk = Abc_Clock(); int nIters, nBddSize = 0; // int nThreshold = 10000; // compute time to stop - p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0; // define variable limits Llb_ManPrepareVarLimits( p ); @@ -660,9 +660,9 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo //Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) { - clk2 = clock(); + clk2 = Abc_Clock(); // check the runtime limit - if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); @@ -702,7 +702,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters ); else Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; @@ -839,7 +839,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo fprintf( stdout, "(%4d %3d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); fprintf( stdout, "Rea =%6d ", Cudd_DagSize(bReached) ); fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) ); - Abc_PrintTime( 1, "Time", clock() - clk2 ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); } /* if ( p->pPars->fVerbose ) diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c index 57745c1d..ac04b563 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, clock_t TimeOut ) +DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, abctime TimeOut ) { Vec_Ptr_t * vNodes; DdNode * bBdd0, * bBdd1, * bTemp, * bResult; @@ -111,7 +111,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) DdNode * bVar, * bCube, * bTemp; Aig_Obj_t * pObj; int i; - clock_t TimeStop; + abctime 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 a6f16aeb..3d62b322 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -69,7 +69,7 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde { DdNode * bRes, * bVar, * bTemp; int i, iVar, Index; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Vec_IntForEachEntry( vVars, Index, i ) @@ -210,17 +210,17 @@ 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; - clock_t clk2, clk = clock(); + abctime clk2, clk = Abc_Clock(); int nIters, nBddSize;//, iOutFail = -1; /* // compute time to stop if ( p->pPars->TimeLimit ) - p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; + p->pPars->TimeTarget = Abc_Clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; else p->pPars->TimeTarget = 0; */ - if ( clock() > p->pPars->TimeTarget ) + if ( Abc_Clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit ); @@ -286,9 +286,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ // compute onion rings for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) { - clk2 = clock(); + clk2 = Abc_Clock(); // check the runtime limit - if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -326,7 +326,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters ); else Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = nIters - 1; return 0; @@ -428,7 +428,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) ); fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) ); - Abc_PrintTime( 1, "Time", clock() - clk2 ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); } // check timeframe limit @@ -471,7 +471,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( !p->pPars->fSilent ) { printf( "Verified only for states reachable in %d frames. ", nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = p->pPars->nIterMax; return -1; // undecided @@ -479,7 +479,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( !p->pPars->fSilent ) { printf( "The miter is proved unreachable after %d iterations. ", nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = nIters - 1; return 1; // unreachable @@ -531,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, clock_t TimeTarget ) +Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, abctime TimeTarget ) { DdManager * dd; Vec_Ptr_t * vDdMans; @@ -691,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, clock_t TimeTarget ) +int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, abctime TimeTarget ) { int RetValue; Llb_Img_t * p; @@ -728,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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); // compute time to stop - pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; + pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0; p = Aig_ManDupFlopsOnly( pAig ); //Aig_ManShow( p, 0, NULL ); @@ -743,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 && clock() > pPars->TimeTarget ) + if ( pPars->TimeLimit && Abc_Clock() > pPars->TimeTarget ) { if ( !pPars->fSilent ) printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit ); @@ -764,7 +764,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) Aig_ManStop( p ); if ( RetValue == -1 ) - Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", clock() - clk ); + Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", Abc_Clock() - clk ); return RetValue; } diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c index 40d7a116..1471f377 100644 --- a/src/proof/llb/llb2Driver.c +++ b/src/proof/llb/llb2Driver.c @@ -130,7 +130,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager DdNode * bCube, * bVar, * bTemp; Aig_Obj_t * pObj; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); Saig_ManForEachLi( pAig, pObj, i ) @@ -160,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, clock_t TimeTarget ) +DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, abctime TimeTarget ) { // int fVerbose = 1; DdManager * dd; diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index a04998fc..9fa40b9e 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -1227,7 +1227,7 @@ 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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); vResult = Vec_PtrAlloc( 100 ); Vec_PtrPush( vResult, Llb_ManComputeCutLo(p) ); Vec_PtrPush( vResult, Llb_ManComputeCutLi(p) ); @@ -1277,7 +1277,7 @@ Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryV if ( fVerbose ) { printf( "Finished computing %d partitions. ", Vec_PtrSize(vResult) - 1 ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Llb_ManResultPrint( p, vResult ); } return vResult; diff --git a/src/proof/llb/llb2Image.c b/src/proof/llb/llb2Image.c index cfaef13c..36ff2df5 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, clock_t TimeTarget ) +DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, abctime TimeTarget ) { Vec_Ptr_t * vNodes, * vRange; Aig_Obj_t * pObj; @@ -260,7 +260,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * DdNode * bProd, * bTemp; Aig_Obj_t * pObj; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd ); Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i ) @@ -289,7 +289,7 @@ void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQ DdManager * dd; DdNode * bProd, * bRes, * bTemp; int i; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i ) { // remember unquantified ones @@ -320,7 +320,7 @@ void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQ if ( fVerbose ) Abc_Print( 1, "Supp = %3d. ", Cudd_SupportSize(dd, bRes) ); if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } } @@ -362,13 +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, - clock_t TimeTarget, int fBackward, int fReorder, int fVerbose ) + abctime TimeTarget, int fBackward, int fReorder, int fVerbose ) { // int fCheckSupport = 0; DdManager * ddPart; DdNode * bImage, * bGroup, * bCube, * bTemp; int i; - clock_t clk, clk0 = clock(); + abctime clk, clk0 = Abc_Clock(); bImage = bInit; Cudd_Ref( bImage ); if ( fBackward ) @@ -397,7 +397,7 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * // perform image computation Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i ) { - clk = clock(); + clk = Abc_Clock(); if ( fVerbose ) printf( " %2d : ", i ); // transfer the BDD from the group manager to the main manager @@ -434,7 +434,7 @@ printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) ); if ( fVerbose ) printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) ); if ( fVerbose ) -Abc_PrintTime( 1, "T", clock() - clk ); +Abc_PrintTime( 1, "T", Abc_Clock() - clk ); } if ( !fBackward ) @@ -464,7 +464,7 @@ Abc_PrintTime( 1, "T", clock() - clk ); // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); // Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) ); if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk0 ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk0 ); // Abc_Print( 1, "\n" ); } diff --git a/src/proof/llb/llb3Image.c b/src/proof/llb/llb3Image.c index dcce8441..72c6120a 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 -clock_t timeBuild, timeAndEx, timeOther; +abctime timeBuild, timeAndEx, timeOther; int nSuppMax; //////////////////////////////////////////////////////////////////////// @@ -141,7 +141,7 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) DdNode * bCube, * bTemp; Llb_Var_t * pVar; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart, pVar, i ) @@ -174,7 +174,7 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p DdNode * bCube, * bTemp; Llb_Var_t * pVar; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart1, pVar, i ) @@ -747,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 ) { - clock_t clk = clock(); + abctime clk = Abc_Clock(); if ( fVerbose ) Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); @@ -760,7 +760,7 @@ void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose ) Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); } if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } /**Function************************************************************* @@ -888,9 +888,9 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo Llb_Mgr_t * p; DdNode * bFunc, * bTemp; int i, nReorders, timeInside; - clock_t clk = clock(), clk2; + abctime clk = Abc_Clock(), clk2; // start the manager - clk2 = clock(); + clk2 = Abc_Clock(); p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd ); if ( !Llb_NonlinStart( p ) ) { @@ -903,8 +903,8 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo Llb_MgrForEachPart( p, pPart, i ) if ( Llb_NonlinHasSingletonVars(p, pPart) ) Llb_NonlinQuantify1( p, pPart, 0 ); - timeBuild += clock() - clk2; - timeInside = clock() - clk2; + timeBuild += Abc_Clock() - clk2; + timeInside = Abc_Clock() - clk2; // compute scores Llb_NonlinRecomputeScores( p ); // save permutation @@ -913,15 +913,15 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo // iteratively quantify variables while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) ) { - clk2 = clock(); + clk2 = Abc_Clock(); nReorders = Cudd_ReadReorderings(dd); if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) ) { Llb_NonlinFree( p ); return NULL; } - timeAndEx += clock() - clk2; - timeInside += clock() - clk2; + timeAndEx += Abc_Clock() - clk2; + timeInside += Abc_Clock() - clk2; if ( nReorders < Cudd_ReadReorderings(dd) ) Llb_NonlinRecomputeScores( p ); // else @@ -939,7 +939,7 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo // reorder variables if ( fReorder ) Llb_NonlinReorder( dd, 0, fVerbose ); - timeOther += clock() - clk - timeInside; + timeOther += Abc_Clock() - clk - timeInside; // return Cudd_Deref( bFunc ); return bFunc; @@ -960,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, clock_t TimeTarget ) +DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, abctime TimeTarget ) { DdManager * dd; - clock_t clk = clock(); + abctime clk = Abc_Clock(); assert( p == NULL ); // start a new manager (disable reordering) dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); @@ -979,7 +979,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr p = NULL; return NULL; } - timeBuild += clock() - clk; + timeBuild += Abc_Clock() - clk; // if ( !fFirst ) // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); return dd; @@ -1001,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; - clock_t clk = clock(), clk2; + abctime clk = Abc_Clock(), clk2; // add partition Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent ); @@ -1020,15 +1020,15 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int // iteratively quantify variables while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) ) { - clk2 = clock(); + clk2 = Abc_Clock(); nReorders = Cudd_ReadReorderings(p->dd); if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) ) { Llb_NonlinFree( p ); return NULL; } - timeAndEx += clock() - clk2; - timeInside += clock() - clk2; + timeAndEx += Abc_Clock() - clk2; + timeInside += Abc_Clock() - clk2; if ( nReorders < Cudd_ReadReorderings(p->dd) ) Llb_NonlinRecomputeScores( p ); // else @@ -1055,7 +1055,7 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int // save permutation // memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) ); - timeOther += clock() - clk - timeInside; + timeOther += Abc_Clock() - clk - timeInside; // return Cudd_Deref( bFunc ); return bFunc; diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 22e23337..94a48bbf 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -54,18 +54,18 @@ struct Llb_Mnn_t_ int ddLocReos; int ddLocGrbs; - clock_t timeImage; - clock_t timeTran1; - clock_t timeTran2; - clock_t timeGloba; - clock_t timeOther; - clock_t timeTotal; - clock_t timeReo; - clock_t timeReoG; + abctime timeImage; + abctime timeTran1; + abctime timeTran2; + abctime timeGloba; + abctime timeOther; + abctime timeTotal; + abctime timeReo; + abctime timeReoG; }; -extern clock_t timeBuild, timeAndEx, timeOther; +extern abctime timeBuild, timeAndEx, timeOther; extern int nSuppMax; //////////////////////////////////////////////////////////////////////// @@ -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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Size = Cudd_DagSize(bFunc); // printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n", // Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) ); @@ -134,7 +134,7 @@ printf( "S =%6d\n", iValue ); } printf( "BestVar = %4d/%4d. Value =%6d. Orig =%6d. Size0 =%6d. ", iVarBest, Aig_ObjId(Saig_ManLo(pAig,iVarBest)), iValueBest, Size, Size0Best ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return iVarBest; } @@ -216,7 +216,7 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; int i, iVar; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( pAig, pObj, i ) @@ -430,11 +430,11 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) { DdNode * bTemp, * bNext; int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax; - clock_t clk2, clk3, clk = clock(); + abctime clk2, clk3, clk = Abc_Clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); // compute time to stop - p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0; // set the stop time parameter p->dd->TimeStop = p->pPars->TimeTarget; @@ -472,8 +472,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) { // check the runtime limit - clk2 = clock(); - if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) + clk2 = Abc_Clock(); + if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -507,7 +507,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters ); else Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = nIters - 1; Llb_NonlinImageQuit(); @@ -515,7 +515,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } // compute the next states - clk3 = clock(); + clk3 = Abc_Clock(); nBddSize0 = Cudd_DagSize( p->dd->bFunc ); bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref // bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, @@ -530,11 +530,11 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( bNext ); nBddSize = Cudd_DagSize( bNext ); - p->timeImage += clock() - clk3; + p->timeImage += Abc_Clock() - clk3; // transfer to the state manager - clk3 = clock(); + clk3 = Abc_Clock(); Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 ); p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); // p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) ); @@ -549,7 +549,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->dd, bNext ); - p->timeTran1 += clock() - clk3; + p->timeTran1 += Abc_Clock() - clk3; // save permutation NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 ); @@ -571,7 +571,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 ); // derive new states - clk3 = clock(); + clk3 = Abc_Clock(); p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) ); if ( p->ddG->bFunc2 == NULL ) { @@ -584,12 +584,12 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->ddG, bTemp ); - p->timeGloba += clock() - clk3; + p->timeGloba += Abc_Clock() - clk3; if ( Cudd_IsConstant(p->ddG->bFunc2) ) break; // add to the reached set - clk3 = clock(); + clk3 = Abc_Clock(); p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); if ( p->ddG->bFunc == NULL ) { @@ -602,7 +602,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddG->bFunc ); Cudd_RecursiveDeref( p->ddG, bTemp ); - p->timeGloba += clock() - clk3; + p->timeGloba += Abc_Clock() - clk3; // reset permutation // RetValue = Cudd_CheckZeroRef( dd ); @@ -610,7 +610,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // Cudd_ShuffleHeap( dd, pOrderG ); // move new states to the working manager - clk3 = clock(); + clk3 = Abc_Clock(); p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); if ( p->dd->bFunc == NULL ) { @@ -621,7 +621,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) return -1; } Cudd_Ref( p->dd->bFunc ); - p->timeTran2 += clock() - clk3; + p->timeTran2 += Abc_Clock() - clk3; // report the results if ( p->pPars->fVerbose ) @@ -635,7 +635,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) printf( "S =%4d ", nSuppMax ); printf( "cL =%5d ", NumCmp ); printf( "cG =%5d ", Llb_NonlinCompPerms( p->ddG, p->pOrderG ) ); - Abc_PrintTime( 1, "T", clock() - clk2 ); + Abc_PrintTime( 1, "T", Abc_Clock() - clk2 ); memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size ); } /* @@ -680,7 +680,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) if ( !p->pPars->fSilent ) printf( "The miter is proved unreachable after %d iterations. ", nIters ); p->pPars->iFrame = nIters - 1; - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return 1; // unreachable } @@ -808,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; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Llb_ManSetDefaultParams( pPars ); pPars->fVerbose = 1; @@ -820,7 +820,7 @@ void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num ) pMnn = Llb_MnnStart( pAig, p, pPars ); Llb_NonlinReachability( pMnn ); - pMnn->timeTotal = clock() - clk; + pMnn->timeTotal = Abc_Clock() - clk; Llb_MnnStop( pMnn ); Aig_ManStop( p ); @@ -852,10 +852,10 @@ int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) if ( !pPars->fSkipReach ) { - clock_t clk = clock(); + abctime clk = Abc_Clock(); pMnn = Llb_MnnStart( pAig, p, pPars ); RetValue = Llb_NonlinReachability( pMnn ); - pMnn->timeTotal = clock() - clk; + pMnn->timeTotal = Abc_Clock() - clk; Llb_MnnStop( pMnn ); } diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c index c676b76e..18aeaf04 100644 --- a/src/proof/llb/llb4Cex.c +++ b/src/proof/llb/llb4Cex.c @@ -52,7 +52,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int sat_solver * pSat; Aig_Obj_t * pObj; unsigned * pNext, * pThis; - int i, k, iBit, status, nRegs;//, clk = clock(); + int i, k, iBit, status, nRegs;//, clk = Abc_Clock(); /* Vec_PtrForEachEntry( unsigned *, vStates, pNext, i ) { @@ -187,7 +187,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int } // report the results // if ( fVerbose ) -// Abc_PrintTime( 1, "SAT-based cex generation time", clock() - clk ); +// Abc_PrintTime( 1, "SAT-based cex generation time", Abc_Clock() - clk ); return pCex; } diff --git a/src/proof/llb/llb4Image.c b/src/proof/llb/llb4Image.c index 4ae087b5..2ba4fcfd 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 -//clock_t timeBuild, timeAndEx, timeOther; +//abctime timeBuild, timeAndEx, timeOther; //int nSuppMax; //////////////////////////////////////////////////////////////////////// @@ -140,7 +140,7 @@ DdNode * Llb_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) DdNode * bCube, * bTemp; Llb_Var_t * pVar; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart, pVar, i ) @@ -173,7 +173,7 @@ DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * DdNode * bCube, * bTemp; Llb_Var_t * pVar; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart1, pVar, i ) @@ -808,7 +808,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV Vec_Ptr_t * vGroups; Llb_Prt_t * pPart, * pPart1, * pPart2; Llb_Mgr_t * p; - int i, nReorders;//, clk = clock(); + int i, nReorders;//, clk = Abc_Clock(); // start the manager p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax ); // remove singles @@ -849,7 +849,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV //Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" ); } Llb_Nonlin4Free( p ); -//Abc_PrintTime( 1, "Reparametrization time", clock() - clk ); +//Abc_PrintTime( 1, "Reparametrization time", Abc_Clock() - clk ); return vGroups; } diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index 51f9d602..6d5826a0 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 - clock_t timeImage; - clock_t timeRemap; - clock_t timeReo; - clock_t timeOther; - clock_t timeTotal; + abctime timeImage; + abctime timeRemap; + abctime timeReo; + abctime timeOther; + abctime timeTotal; }; //extern int timeBuild, timeAndEx, timeOther; @@ -447,7 +447,7 @@ DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_ Aig_Obj_t * pObjLi, * pObjLo; DdNode * bRes, * bVar, * bTemp; int i; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) @@ -477,7 +477,7 @@ 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; - clock_t TimeStop; + abctime TimeStop; TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) @@ -579,7 +579,7 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose ) Vec_Ptr_t * vStates, * vRootsNew; Aig_Obj_t * pObj; DdNode * bState = NULL, * bImage, * bOneCube, * bRing; - int i, v, RetValue;//, clk = clock(); + int i, v, RetValue;//, clk = Abc_Clock(); char * pValues; assert( Vec_PtrSize(p->vRings) > 0 ); // disable the timeout @@ -649,7 +649,7 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose ) if ( fBackward ) Vec_PtrReverseOrder( vStates ); // if ( fVerbose ) -// Abc_PrintTime( 1, "BDD-based cex generation time", clock() - clk ); +// Abc_PrintTime( 1, "BDD-based cex generation time", Abc_Clock() - clk ); return vStates; } @@ -669,7 +669,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) { DdNode * bAux; int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0; - clock_t clkTemp, clkIter, clk = clock(); + abctime clkTemp, clkIter, clk = Abc_Clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); if ( p->pPars->fBackward ) @@ -736,9 +736,9 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) p->bReached = p->bCurrent; Cudd_Ref( p->bReached ); for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) { - clkIter = clock(); + clkIter = Abc_Clock(); // check the runtime limit - if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget ) + if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); @@ -760,14 +760,14 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) if ( !p->pPars->fSilent ) { Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAig->pSeqModel->iPo, p->pAig->pName, nIters ); - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } p->pPars->iFrame = nIters - 1; return 0; } // compute the next states - clkTemp = clock(); + clkTemp = Abc_Clock(); p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q ); if ( p->bNext == NULL ) { @@ -777,10 +777,10 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) return -1; } Cudd_Ref( p->bNext ); - p->timeImage += clock() - clkTemp; + p->timeImage += Abc_Clock() - clkTemp; // remap into current states - clkTemp = clock(); + clkTemp = Abc_Clock(); p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext ); if ( p->bNext == NULL ) { @@ -792,7 +792,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) } Cudd_Ref( p->bNext ); Cudd_RecursiveDeref( p->dd, bAux ); - p->timeRemap += clock() - clkTemp; + p->timeRemap += Abc_Clock() - clkTemp; // collect statistics if ( p->pPars->fVerbose ) @@ -847,7 +847,7 @@ printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurr printf( "ImCs =%7d ", nBddSizeTo2 ); printf( "Rea =%7d ", Cudd_DagSize(p->bReached) ); printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); - Abc_PrintTime( 1, "T", clock() - clkIter ); + Abc_PrintTime( 1, "T", Abc_Clock() - clkIter ); } /* if ( pPars->fVerbose ) @@ -889,7 +889,7 @@ printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurr if ( !p->pPars->fSilent ) printf( "The miter is proved unreachable after %d iterations. ", nIters ); p->pPars->iFrame = nIters - 1; - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return 1; // unreachable } @@ -906,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 ) { - clock_t clk = clock(); + abctime clk = Abc_Clock(); if ( fVerbose ) Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); @@ -919,7 +919,7 @@ void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose ) Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); } if ( fVerbose ) - Abc_PrintTime( 1, "Time", clock() - clk ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } /**Function************************************************************* @@ -942,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 ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0; + p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0; if ( pPars->fCluster ) { @@ -1073,12 +1073,12 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) return RetValue; } { - clock_t clk = clock(); + abctime clk = Abc_Clock(); pMnn = Llb_MnxStart( pAig, pPars ); //Llb_MnxCheckNextStateVars( pMnn ); if ( !pPars->fSkipReach ) RetValue = Llb_Nonlin4Reachability( pMnn ); - pMnn->timeTotal = clock() - clk; + pMnn->timeTotal = Abc_Clock() - clk; Llb_MnxStop( pMnn ); } return RetValue; diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c index 709bd61a..6b318572 100644 --- a/src/proof/llb/llb4Sweep.c +++ b/src/proof/llb/llb4Sweep.c @@ -287,7 +287,7 @@ DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdMa Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; int i; - clock_t TimeStop; + abctime 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 208d291c..0c53c01f 100644 --- a/src/proof/llb/llbInt.h +++ b/src/proof/llb/llbInt.h @@ -152,28 +152,28 @@ 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, clock_t TimeOut ); +extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, abctime 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, clock_t TimeTarget ); +extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, abctime 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, clock_t TimeTarget ); +extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, abctime 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, clock_t TimeTarget ); +extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, abctime 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, - clock_t TimeTarget, int fBackward, int fReorder, int fVerbose ); + abctime 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, clock_t TimeTarget ); +extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, abctime TimeTarget ); extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ); extern void Llb_NonlinImageQuit(); |