summaryrefslogtreecommitdiffstats
path: root/src/proof/abs
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/abs')
-rw-r--r--src/proof/abs/absGla.c72
-rw-r--r--src/proof/abs/absGlaOld.c62
-rw-r--r--src/proof/abs/absIter.c8
-rw-r--r--src/proof/abs/absOldCex.c16
-rw-r--r--src/proof/abs/absOldRef.c6
-rw-r--r--src/proof/abs/absOldSat.c24
-rw-r--r--src/proof/abs/absOldSim.c6
-rw-r--r--src/proof/abs/absOut.c8
-rw-r--r--src/proof/abs/absRef.c18
-rw-r--r--src/proof/abs/absRef.h8
-rw-r--r--src/proof/abs/absRpm.c4
-rw-r--r--src/proof/abs/absVta.c58
12 files changed, 145 insertions, 145 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 4063757c..5daa953f 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -73,12 +73,12 @@ struct Ga2_Man_t_
Vec_Int_t * vIsopMem;
char * pSopSizes, ** pSops; // CNF representation
// statistics
- clock_t timeStart;
- clock_t timeInit;
- clock_t timeSat;
- clock_t timeUnsat;
- clock_t timeCex;
- clock_t timeOther;
+ abctime timeStart;
+ abctime timeInit;
+ abctime timeSat;
+ abctime timeUnsat;
+ abctime timeCex;
+ abctime timeOther;
};
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
@@ -243,7 +243,7 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea
int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
{
static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
-// clock_t clk = clock();
+// abctime clk = Abc_Clock();
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj;
int i, k, Leaf, CountMarks;
@@ -330,20 +330,20 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
CountMarks++;
}
-// Abc_PrintTime( 1, "Time", clock() - clk );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_IntFree( vLeaves );
Gia_ManCleanValue( p );
return CountMarks;
}
void Ga2_ManComputeTest( Gia_Man_t * p )
{
- clock_t clk;
+ abctime clk;
// unsigned uTruth;
Gia_Obj_t * pObj;
int i, Counter = 0;
- clk = clock();
+ clk = Abc_Clock();
Ga2_ManMarkup( p, 5, 0 );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !pObj->fPhase )
@@ -355,7 +355,7 @@ void Ga2_ManComputeTest( Gia_Man_t * p )
Counter++;
}
Abc_Print( 1, "Marked AND nodes = %6d. ", Counter );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
@@ -373,7 +373,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
{
Ga2_Man_t * p;
p = ABC_CALLOC( Ga2_Man_t, 1 );
- p->timeStart = clock();
+ p->timeStart = Abc_Clock();
p->fUseNewLine = 1;
// user data
p->pGia = pGia;
@@ -1366,7 +1366,7 @@ int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd )
SeeAlso []
***********************************************************************/
-void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, clock_t Time, int fFinal )
+void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal )
{
int fUseNewLine = ((fFinal && nCexes) || p->pPars->fVeryVerbose);
if ( Abc_FrameIsBatchMode() && !fUseNewLine )
@@ -1502,7 +1502,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
int fUseSecondCore = 1;
Ga2_Man_t * p;
Vec_Int_t * vCore, * vPPis;
- clock_t clk2, clk = clock();
+ abctime clk2, clk = Abc_Clock();
int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
int i, c, f, Lit;
pPars->iFrame = -1;
@@ -1529,7 +1529,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
}
// start the manager
p = Ga2_ManStart( pAig, pPars );
- p->timeInit = clock() - clk;
+ p->timeInit = Abc_Clock() - clk;
// perform initial abstraction
if ( p->pPars->fVerbose )
{
@@ -1600,12 +1600,12 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
break;
}
// perform SAT solving
- clk2 = clock();
+ clk2 = Abc_Clock();
Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( Status == l_True ) // perform refinement
{
p->nCexes++;
- p->timeSat += clock() - clk2;
+ p->timeSat += Abc_Clock() - clk2;
// cancel old one if it was sent
if ( Abc_FrameIsBridgeMode() && fOneIsSent )
@@ -1620,14 +1620,14 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
}
// perform refinement
- clk2 = clock();
+ clk2 = Abc_Clock();
Rnm_ManSetRefId( p->pRnm, c );
vPPis = Ga2_ManRefine( p );
- p->timeCex += clock() - clk2;
+ p->timeCex += Abc_Clock() - clk2;
if ( vPPis == NULL )
{
if ( pPars->fVerbose )
- Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+ Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
goto finish;
}
@@ -1657,13 +1657,13 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Ga2_ManAddToAbs( p, vPPis );
Vec_IntFree( vPPis );
if ( pPars->fVerbose )
- Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, clock() - clk, 0 );
+ Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
continue;
}
- p->timeUnsat += clock() - clk2;
+ p->timeUnsat += Abc_Clock() - clk2;
if ( Status == l_Undef ) // ran out of resources
goto finish;
- if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout
+ if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
goto finish;
if ( c == 0 )
{
@@ -1706,12 +1706,12 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_IntFree( vCore );
}
// run SAT solver
- clk2 = clock();
+ clk2 = Abc_Clock();
Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( Status == l_Undef )
goto finish;
assert( Status == l_False );
- p->timeUnsat += clock() - clk2;
+ p->timeUnsat += Abc_Clock() - clk2;
// derive the core
assert( p->pSat->pPrf2 != NULL );
@@ -1734,7 +1734,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
p->pPars->iFrameProved = f;
// print statistics
if ( pPars->fVerbose )
- Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+ Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
// check if abstraction was proved
if ( Gia_GlaProveCheck( pPars->fVerbose ) )
{
@@ -1817,7 +1817,7 @@ finish:
{
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Ga2_ManAbsTranslate( p );
- if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
+ if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
@@ -1838,16 +1838,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 );
Ga2_ManReportMemory( p );
}
// Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
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 );
diff --git a/src/proof/abs/absIter.c b/src/proof/abs/absIter.c
index e8e5730b..7b660359 100644
--- a/src/proof/abs/absIter.c
+++ b/src/proof/abs/absIter.c
@@ -70,7 +70,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU
int i, iFrame0, iFrame;
int nTotal = 0, nRemoved = 0;
Vec_Int_t * vGScopy;
- clock_t clk, clkTotal = clock();
+ abctime clk, clkTotal = Abc_Clock();
assert( Gia_ManPoNum(p) == 1 );
assert( p->vGateClasses != NULL );
vGScopy = Vec_IntDup( p->vGateClasses );
@@ -99,7 +99,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU
if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj))) )
continue;
}
- clk = clock();
+ clk = Abc_Clock();
printf( "%5d : ", nTotal );
printf( "Obj =%7d ", i );
Gia_ObjRemFromGla( p, pObj );
@@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU
printf( "Removing " );
Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 );
}
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
nTotal++;
// update the classes
Vec_IntFreeP( &p->vGateClasses );
@@ -135,7 +135,7 @@ Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fU
Vec_IntFree( vGScopy );
printf( "Tried = %d. ", nTotal );
printf( "Removed = %d. (%.2f %%) ", nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return NULL;
}
diff --git a/src/proof/abs/absOldCex.c b/src/proof/abs/absOldCex.c
index e5eaee27..c57d8ed9 100644
--- a/src/proof/abs/absOldCex.c
+++ b/src/proof/abs/absOldCex.c
@@ -720,9 +720,9 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
Saig_ManCba_t * p;
Vec_Int_t * vReasons;
Abc_Cex_t * pCare;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
- clk = clock();
+ clk = Abc_Clock();
p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
// p->vReg2Frame = Vec_VecStart( pCex->iFrame );
@@ -743,7 +743,7 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
Vec_IntFree( vRes );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
pCare = Saig_ManCbaReason2Cex( p, vReasons );
@@ -786,7 +786,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex
{
Saig_ManCba_t * p;
Vec_Int_t * vRes, * vReasons;
- clock_t clk;
+ abctime clk;
if ( Saig_ManPiNum(pAig) != pCex->nPis )
{
printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n",
@@ -794,7 +794,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex
return NULL;
}
-clk = clock();
+clk = Abc_Clock();
p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
vReasons = Saig_ManCbaFindReason( p );
@@ -804,7 +804,7 @@ clk = clock();
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
Vec_IntFree( vReasons );
@@ -831,7 +831,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
{
Vec_Int_t * vAbsFfsToAdd;
int RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// assert( pAbs->nRegs > 0 );
// perform BMC
RetValue = Saig_ManBmcScalable( pAbs, pPars );
@@ -859,7 +859,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
{
printf( "Adding %d registers to the abstraction (total = %d). ",
Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return vAbsFfsToAdd;
}
diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c
index 6cc5ff6d..b42053dd 100644
--- a/src/proof/abs/absOldRef.c
+++ b/src/proof/abs/absOldRef.c
@@ -257,7 +257,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC
Aig_Man_t * pAbs;
Vec_Int_t * vFlopsNew;
int i, Entry;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
pAbs = Saig_ManDupAbstraction( p, vFlops );
if ( fSensePath )
vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
@@ -281,7 +281,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// vFlopsNew contains PI numbers that should be kept in pAbs
// select the most useful flops among those to be added
@@ -411,7 +411,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
int nUseStart = 0;
Aig_Man_t * pAbs, * pTemp;
Vec_Int_t * vFlops;
- int Iter;//, clk = clock(), clk2 = clock();//, iFlop;
+ int Iter;//, clk = Abc_Clock(), clk2 = Abc_Clock();//, iFlop;
assert( Aig_ManRegNum(p) > 0 );
if ( pPars->fVerbose )
printf( "Performing counter-example-based refinement.\n" );
diff --git a/src/proof/abs/absOldSat.c b/src/proof/abs/absOldSat.c
index 14f59667..7ee54b29 100644
--- a/src/proof/abs/absOldSat.c
+++ b/src/proof/abs/absOldSat.c
@@ -510,7 +510,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
Vec_Int_t * vAssumps, * vVar2PiId;
int i, k, Entry, RetValue;//, f = 0, Counter = 0;
int nCoreLits, * pCoreLits;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// create CNF
assert( Aig_ManRegNum(p->pFrames) == 0 );
// pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
@@ -530,7 +530,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
Cnf_DataFree( pCnf );
return NULL;
}
-//Abc_PrintTime( 1, "Preparing", clock() - clk );
+//Abc_PrintTime( 1, "Preparing", Abc_Clock() - clk );
// look for a true counter-example
if ( p->nInputs > 0 )
{
@@ -582,10 +582,10 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
}
// solve
-clk = clock();
+clk = Abc_Clock();
RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-//Abc_PrintTime( 1, "Solving", clock() - clk );
+//Abc_PrintTime( 1, "Solving", Abc_Clock() - clk );
if ( RetValue != l_False )
{
if ( RetValue == l_True )
@@ -868,9 +868,9 @@ Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nIn
Saig_RefMan_t * p;
Vec_Int_t * vReasons;
Abc_Cex_t * pCare;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
- clk = clock();
+ clk = Abc_Clock();
p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
vReasons = Saig_RefManFindReason( p );
@@ -883,7 +883,7 @@ Aig_ManPrintStats( p->pFrames );
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
Vec_IntFree( vRes );
@@ -900,7 +900,7 @@ ABC_PRT( "Time", clock() - clk );
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
Vec_IntFree( vRes );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
*/
}
@@ -931,7 +931,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP
{
Saig_RefMan_t * p;
Vec_Int_t * vRes, * vReasons;
- clock_t clk;
+ abctime clk;
if ( Saig_ManPiNum(pAig) != pCex->nPis )
{
printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n",
@@ -939,7 +939,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP
return NULL;
}
-clk = clock();
+clk = Abc_Clock();
p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
vReasons = Saig_RefManFindReason( p );
@@ -950,7 +950,7 @@ clk = clock();
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
/*
@@ -967,7 +967,7 @@ ABC_PRT( "Time", clock() - clk );
printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
*/
diff --git a/src/proof/abs/absOldSim.c b/src/proof/abs/absOldSim.c
index e5c1e938..5d316935 100644
--- a/src/proof/abs/absOldSim.c
+++ b/src/proof/abs/absOldSim.c
@@ -444,7 +444,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi,
{
Vec_Int_t * vRes;
Vec_Ptr_t * vSimInfo;
- clock_t clk;
+ abctime clk;
if ( Saig_ManPiNum(p) != pCex->nPis )
{
printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n",
@@ -455,12 +455,12 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi,
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );
-clk = clock();
+clk = Abc_Clock();
vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
if ( fVerbose )
{
printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
Vec_PtrFree( vSimInfo );
Aig_ManFanoutStop( p );
diff --git a/src/proof/abs/absOut.c b/src/proof/abs/absOut.c
index c230acb4..0cd9e0e2 100644
--- a/src/proof/abs/absOut.c
+++ b/src/proof/abs/absOut.c
@@ -97,7 +97,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
Abc_Cex_t * pCare;
Vec_Int_t * vPis, * vPPis;
int f, i, iObjId;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int nOnes = 0, Counter = 0;
if ( p->vGateClasses == NULL )
{
@@ -175,7 +175,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
if ( fVerbose )
{
Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
}
@@ -209,7 +209,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
if ( fVerbose )
{
Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// consider the case of SAT
if ( iObjId == -1 )
@@ -375,7 +375,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra
Gia_Man_t * pAbs, * pNew;
Vec_Int_t * vFlops, * vInit;
Vec_Int_t * vCopy;
-// clock_t clk = clock();
+// abctime clk = Abc_Clock();
int RetValue;
ABC_FREE( p->pCexSeq );
if ( p->vGateClasses == NULL )
diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c
index f72d86e2..dda0c8cb 100644
--- a/src/proof/abs/absRef.c
+++ b/src/proof/abs/absRef.c
@@ -290,7 +290,7 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
{
double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
double MemOther = sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
- clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
+ abctime timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
printf( "Abstraction refinement runtime statistics:\n" );
ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal );
ABC_PRTP( "Justification", p->timeBwd, p->timeTotal );
@@ -674,7 +674,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
{
int fVerify = 1;
Vec_Int_t * vGoodPPis, * vNewPPis;
- clock_t clk, clk2 = clock();
+ abctime clk, clk2 = Abc_Clock();
int RetValue;
p->nCalls++;
// Gia_ManCleanValue( p->pGia );
@@ -692,27 +692,27 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) );
memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
// propagate priorities
- clk = clock();
+ clk = Abc_Clock();
vGoodPPis = Vec_IntAlloc( 100 );
if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
{
- p->timeFwd += clock() - clk;
+ p->timeFwd += Abc_Clock() - clk;
// select refinement
- clk = clock();
+ clk = Abc_Clock();
p->nVisited = 0;
Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
RetValue = Vec_IntUniqify( vGoodPPis );
// assert( RetValue == 0 );
- p->timeBwd += clock() - clk;
+ p->timeBwd += Abc_Clock() - clk;
}
// verify (empty) refinement
// (only works when post-processing is not applied)
if ( fVerify )
{
- clk = clock();
+ clk = Abc_Clock();
Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
- p->timeVer += clock() - clk;
+ p->timeVer += Abc_Clock() - clk;
}
// at this point array vGoodPPis contains the set of important PPIs
@@ -737,7 +737,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
Rnm_ManCleanValues( p );
// Vec_IntReverseOrder( vGoodPPis );
- p->timeTotal += clock() - clk2;
+ p->timeTotal += Abc_Clock() - clk2;
p->nRefines += Vec_IntSize(vGoodPPis);
return vGoodPPis;
}
diff --git a/src/proof/abs/absRef.h b/src/proof/abs/absRef.h
index 9bae40a3..93c054aa 100644
--- a/src/proof/abs/absRef.h
+++ b/src/proof/abs/absRef.h
@@ -83,10 +83,10 @@ struct Rnm_Man_t_
int nRefines; // total refined objects
int nVisited; // visited during justification
// statistics
- clock_t timeFwd; // forward propagation
- clock_t timeBwd; // backward propagation
- clock_t timeVer; // ternary simulation
- clock_t timeTotal; // other time
+ abctime timeFwd; // forward propagation
+ abctime timeBwd; // backward propagation
+ abctime timeVer; // ternary simulation
+ abctime timeTotal; // other time
};
// accessing the refinement object
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c
index edb60083..ef5747c1 100644
--- a/src/proof/abs/absRpm.c
+++ b/src/proof/abs/absRpm.c
@@ -110,7 +110,7 @@ void Gia_ManTestDoms2( Gia_Man_t * p )
{
Vec_Int_t * vNodes;
Gia_Obj_t * pObj, * pDom;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int i;
assert( p->vDoms == NULL );
Gia_ManComputeDoms( p );
@@ -119,7 +119,7 @@ void Gia_ManTestDoms2( Gia_Man_t * p )
if ( Gia_ObjId(p, pObj) != Gia_ObjDom(p, pObj) )
printf( "PI =%6d Id =%8d. Dom =%8d.\n", i, Gia_ObjId(p, pObj), Gia_ObjDom(p, pObj) );
*/
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator
Gia_ManCleanMark1( p );
Gia_ManForEachPi( p, pObj, i )
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 4b943870..01680a3f 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -71,10 +71,10 @@ struct Vta_Man_t_
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vAddedNew; // the IDs of variables added to the solver
// statistics
- clock_t timeSat;
- clock_t timeUnsat;
- clock_t timeCex;
- clock_t timeOther;
+ abctime timeSat;
+ abctime timeUnsat;
+ abctime timeCex;
+ abctime timeOther;
};
@@ -1082,7 +1082,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
***********************************************************************/
Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
{
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Vec_Int_t * vCore;
int RetValue, nConfPrev = pSat->stats.conflicts;
if ( piRetValue )
@@ -1115,16 +1115,16 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fV
{
// 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 ( 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;
}
@@ -1140,7 +1140,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fV
SeeAlso []
***********************************************************************/
-int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, clock_t Time, int fVerbose )
+int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose )
{
unsigned * pInfo;
int * pCountAll = NULL, * pCountUni = NULL;
@@ -1495,7 +1495,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_Int_t * vCore;
Abc_Cex_t * pCex = NULL;
int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
- clock_t clk = clock(), clk2;
+ abctime clk = Abc_Clock(), clk2;
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@@ -1525,7 +1525,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
p = Vga_ManStart( pAig, pPars );
// 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 )
{
@@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
- clk2 = clock();
+ clk2 = Abc_Clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
@@ -1573,27 +1573,27 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
goto finish;
}
// check timeout
- if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
+ if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
if ( vCore != NULL )
{
- p->timeUnsat += clock() - clk2;
+ p->timeUnsat += Abc_Clock() - clk2;
break;
}
- p->timeSat += clock() - clk2;
+ p->timeSat += Abc_Clock() - clk2;
assert( Status == 0 );
p->nCexes++;
// perform the refinement
- clk2 = clock();
+ clk2 = Abc_Clock();
pCex = Vta_ManRefineAbstraction( p, f );
- p->timeCex += clock() - clk2;
+ p->timeCex += Abc_Clock() - clk2;
if ( pCex != NULL )
goto finish;
// print the result (do not count it towards change)
- Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
+ Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose );
}
assert( Status == 1 );
// valid core is obtained
@@ -1608,9 +1608,9 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_IntFree( vCore );
// run SAT solver
- clk2 = clock();
+ clk2 = Abc_Clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(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) );
if ( Status == -1 ) // resource limit is reached
break;
@@ -1628,7 +1628,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_IntSort( vCore, 1 );
Vec_PtrPush( p->vCores, vCore );
// print the result
- if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ) )
+ if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) )
{
// reset the counter of frames without change
nCountNoChange = 1;
@@ -1682,7 +1682,7 @@ finish:
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
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 );
@@ -1711,16 +1711,16 @@ finish:
Vec_IntFreeP( &pAig->vObjClasses );
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;
- 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;
+ 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 );
Gia_VtaPrintMemory( p );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 17:11:11 +0000