summaryrefslogtreecommitdiffstats
path: root/src/proof/llb
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/llb')
-rw-r--r--src/proof/llb/llb.h2
-rw-r--r--src/proof/llb/llb1Core.c4
-rw-r--r--src/proof/llb/llb1Hint.c4
-rw-r--r--src/proof/llb/llb1Reach.c24
-rw-r--r--src/proof/llb/llb2Bad.c4
-rw-r--r--src/proof/llb/llb2Core.c32
-rw-r--r--src/proof/llb/llb2Driver.c4
-rw-r--r--src/proof/llb/llb2Flow.c4
-rw-r--r--src/proof/llb/llb2Image.c18
-rw-r--r--src/proof/llb/llb3Image.c42
-rw-r--r--src/proof/llb/llb3Nonlin.c66
-rw-r--r--src/proof/llb/llb4Cex.c4
-rw-r--r--src/proof/llb/llb4Image.c10
-rw-r--r--src/proof/llb/llb4Nonlin.c48
-rw-r--r--src/proof/llb/llb4Sweep.c2
-rw-r--r--src/proof/llb/llbInt.h12
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();
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:12:58 +0000