summaryrefslogtreecommitdiffstats
path: root/src/proof/abs/absGlaOld.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/abs/absGlaOld.c')
-rw-r--r--src/proof/abs/absGlaOld.c62
1 files changed, 31 insertions, 31 deletions
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index e2f83e96..70bd2e91 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -93,11 +93,11 @@ struct Gla_Man_t_
Gia_Man_t * pGia2;
Rnm_Man_t * pRnm;
// statistics
- clock_t timeInit;
- clock_t timeSat;
- clock_t timeUnsat;
- clock_t timeCex;
- clock_t timeOther;
+ abctime timeInit;
+ abctime timeSat;
+ abctime timeUnsat;
+ abctime timeCex;
+ abctime timeOther;
};
// declarations
@@ -1447,7 +1447,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon
Vec_Int_t * vCore = NULL;
int nConfPrev = pSat->stats.conflicts;
int RetValue, iLit = Gla_ManGetOutLit( p, f );
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( piRetValue )
*piRetValue = 1;
// consider special case when PO points to the flop
@@ -1478,18 +1478,18 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon
{
// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
-// Abc_PrintTime( 1, "Time", clock() - clk );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
assert( RetValue == l_False );
// derive the UNSAT core
- clk = clock();
+ clk = Abc_Clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( vCore )
Vec_IntSort( vCore, 1 );
if ( fVerbose )
{
// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
-// Abc_PrintTime( 1, "Time", clock() - clk );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return vCore;
}
@@ -1506,7 +1506,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon
SeeAlso []
***********************************************************************/
-void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, clock_t Time )
+void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, abctime Time )
{
if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
return;
@@ -1643,7 +1643,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
Abc_Cex_t * pCex = NULL;
int f, i, iPrev, nConfls, Status, nVarsOld = 0, nCoreSize, fOneIsSent = 0, RetValue = -1;
- clock_t clk2, clk = clock();
+ abctime clk2, clk = Abc_Clock();
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@@ -1696,10 +1696,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
}
// start the manager
p = Gla_ManStart( pAig, pPars );
- p->timeInit = clock() - clk;
+ p->timeInit = Abc_Clock() - clk;
// set runtime limit
if ( p->pPars->nTimeOut )
- sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
+ sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
// perform initial abstraction
if ( p->pPars->fVerbose )
{
@@ -1721,10 +1721,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
- clk2 = clock();
+ clk2 = Abc_Clock();
vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
// assert( (vCore != NULL) == (Status == 1) );
- if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
+ if ( Status == -1 || (p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
{
Prf_ManStopP( &p->pSat->pPrf2 );
// if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstraction
@@ -1734,10 +1734,10 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
if ( Status == 1 )
{
Prf_ManStopP( &p->pSat->pPrf2 );
- p->timeUnsat += clock() - clk2;
+ p->timeUnsat += Abc_Clock() - clk2;
break;
}
- p->timeSat += clock() - clk2;
+ p->timeSat += Abc_Clock() - clk2;
assert( Status == 0 );
p->nCexes++;
@@ -1749,7 +1749,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
}
// perform the refinement
- clk2 = clock();
+ clk2 = Abc_Clock();
if ( pPars->fAddLayer )
{
vPPis = Gla_ManCollectPPis( p, NULL );
@@ -1803,7 +1803,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
// print the result (do not count it towards change)
if ( p->pPars->fVerbose )
- Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+ Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
}
if ( pCex != NULL )
break;
@@ -1836,9 +1836,9 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore );
// run SAT solver
- clk2 = clock();
+ clk2 = Abc_Clock();
vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
- p->timeUnsat += clock() - clk2;
+ p->timeUnsat += Abc_Clock() - clk2;
// assert( (vCore != NULL) == (Status == 1) );
Vec_IntFreeP( &vCore );
if ( Status == -1 ) // resource limit is reached
@@ -1855,7 +1855,7 @@ int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta )
}
// print the result
if ( p->pPars->fVerbose )
- Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+ Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk );
if ( f > 2 && iPrev > 0 && i == 0 ) // change has happened
{
@@ -1901,7 +1901,7 @@ finish:
pAig->vGateClasses = Gla_ManTranslate( p );
if ( Status == -1 )
{
- if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
+ if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
@@ -1929,16 +1929,16 @@ finish:
Vec_IntFreeP( &pAig->vGateClasses );
RetValue = 0;
}
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( p->pPars->fVerbose )
{
- p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
- ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk );
- ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk );
- ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk );
- ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk );
- ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk );
- ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
+ p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
+ ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk );
+ ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
+ ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
+ ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
+ ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
+ ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
Gla_ManReportMemory( p );
}
// Ga2_ManDumpStats( pAig, p->pPars, p->pSat, p->pPars->iFrame, 1 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-26 18:06:00 +0000