summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/pdr.h2
-rw-r--r--src/proof/pdr/pdrCore.c84
-rw-r--r--src/proof/pdr/pdrInt.h28
-rw-r--r--src/proof/pdr/pdrInv.c6
-rw-r--r--src/proof/pdr/pdrMan.c2
-rw-r--r--src/proof/pdr/pdrSat.c14
-rw-r--r--src/proof/pdr/pdrTsim.c4
7 files changed, 70 insertions, 70 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 10d2af3b..f32fe0b3 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -66,7 +66,7 @@ struct Pdr_Par_t_
int RunId; // PDR id in this run
int(*pFuncStop)(int); // callback to terminate
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
- clock_t timeLastSolved; // the time when the last output was solved
+ abctime timeLastSolved; // the time when the last output was solved
Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
};
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 987a1a3e..7cd60d9e 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -135,7 +135,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
Vec_Ptr_t * vArrayK, * vArrayK1;
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
int Counter = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
{
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
@@ -218,7 +218,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
m--;
}
}
- p->tPush += clock() - clk;
+ p->tPush += Abc_Clock() - clk;
return RetValue;
}
@@ -300,7 +300,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
{
Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
int i, j, n, Lit, RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int * pOrder;
// if there is no induction, return
*ppCubeMin = NULL;
@@ -309,7 +309,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
return -1;
if ( RetValue == 0 )
{
- p->tGeneral += clock() - clk;
+ p->tGeneral += Abc_Clock() - clk;
return 0;
}
@@ -403,7 +403,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
assert( ppCubeMin != NULL );
*ppCubeMin = pCubeMin;
- p->tGeneral += clock() - clk;
+ p->tGeneral += Abc_Clock() - clk;
return 1;
}
@@ -424,7 +424,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
Pdr_Set_t * pPred, * pCubeMin;
int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
int kMax = Vec_PtrSize(p->vSolvers)-1;
- clock_t clk;
+ abctime clk;
p->nBlocks++;
// create first proof obligation
assert( p->pQueue == NULL );
@@ -447,14 +447,14 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
assert( pThis->iFrame > 0 );
assert( !Pdr_SetIsInit(pThis->pState, -1) );
- clk = clock();
+ clk = Abc_Clock();
if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
{
- p->tContain += clock() - clk;
+ p->tContain += Abc_Clock() - clk;
Pdr_OblDeref( pThis );
continue;
}
- p->tContain += clock() - clk;
+ p->tContain += Abc_Clock() - clk;
// check if the cube is already contained
RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
@@ -536,11 +536,11 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
// check termination
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
return -1;
- if ( p->timeToStop && clock() > p->timeToStop )
+ if ( p->timeToStop && Abc_Clock() > p->timeToStop )
return -1;
- if ( p->timeToStopOne && clock() > p->timeToStopOne )
+ if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
return -1;
- if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
return -1;
}
return 1;
@@ -564,11 +564,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Aig_Obj_t * pObj;
int k, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
- clock_t clkStart = clock(), clkOne = 0;
- p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
+ abctime clkStart = Abc_Clock(), clkOne = 0;
+ p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
assert( Vec_PtrSize(p->vSolvers) == 0 );
// create the first timeframe
- p->pPars->timeLastSolved = clock();
+ p->pPars->timeLastSolved = Abc_Clock();
Pdr_ManCreateSolver( p, (k = 0) );
while ( 1 )
{
@@ -604,7 +604,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Quitting due to callback on fail.\n" );
p->pPars->iFrame = k;
@@ -612,22 +612,22 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
- p->pPars->timeLastSolved = clock();
+ p->pPars->timeLastSolved = Abc_Clock();
continue;
}
// try to solve this output
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[p->iOutCur] > 0 );
- clkOne = clock();
- p->timeToStopOne = p->pTime4Outs[p->iOutCur] + clock();
+ clkOne = Abc_Clock();
+ p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
}
while ( 1 )
{
- if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
p->pPars->iFrame = k;
@@ -639,7 +639,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->pPars->nConfLimit )
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
else if ( p->pPars->fVerbose )
@@ -653,14 +653,14 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->pPars->nConfLimit )
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
- else if ( p->timeToStop && clock() > p->timeToStop )
+ else if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
- else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
- else if ( p->timeToStopOne && clock() > p->timeToStopOne )
+ else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
{
Pdr_QueueClean( p );
pCube = NULL;
@@ -679,7 +679,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, clock() - clkStart );
+ Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
p->pPars->iFrame = k;
if ( !p->pPars->fSolveAll )
@@ -696,7 +696,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Quitting due to callback on fail.\n" );
p->pPars->iFrame = k;
@@ -712,12 +712,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
break; // keep solving
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 0, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
}
}
if ( p->pTime4Outs )
{
- clock_t timeSince = clock() - clkOne;
+ abctime timeSince = Abc_Clock() - clkOne;
assert( p->pTime4Outs[p->iOutCur] > 0 );
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL )
@@ -730,7 +730,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );
@@ -746,10 +746,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
{
- if ( p->timeToStop && clock() > p->timeToStop )
+ if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
else
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
@@ -760,7 +760,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( RetValue )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent )
@@ -776,7 +776,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return p->vCexes ? 0 : 1; // UNSAT
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 0, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
// check termination
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
@@ -784,7 +784,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = k;
return -1;
}
- if ( p->timeToStop && clock() > p->timeToStop )
+ if ( p->timeToStop && Abc_Clock() > p->timeToStop )
{
if ( fPrintClauses )
{
@@ -792,13 +792,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
return -1;
}
- if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
if ( fPrintClauses )
{
@@ -806,7 +806,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
p->pPars->iFrame = k;
@@ -815,7 +815,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
{
if ( p->pPars->fVerbose )
- Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = k;
@@ -841,7 +841,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{
Pdr_Man_t * p;
int k, RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
@@ -872,7 +872,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
}
if ( p->pPars->fDumpInv )
Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
- p->tTotal += clock() - clk;
+ p->tTotal += Abc_Clock() - clk;
Pdr_ManStop( p );
pPars->iFrame--;
// convert all -2 (unknown) entries into -1 (undec)
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 3f74dd5f..72393077 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -97,7 +97,7 @@ struct Pdr_Man_t_
Vec_Int_t * vRes; // final result
Vec_Int_t * vSuppLits; // support literals
Pdr_Set_t * pCubeJust; // justification
- clock_t * pTime4Outs;// timeout per output
+ abctime * pTime4Outs;// timeout per output
// statistics
int nBlocks; // the number of times blockState was called
int nObligs; // the number of proof obligations derived
@@ -115,18 +115,18 @@ struct Pdr_Man_t_
int nQueMax;
int nQueLim;
// runtime
- time_t timeToStop;
- time_t timeToStopOne;
+ abctime timeToStop;
+ abctime timeToStopOne;
// time stats
- clock_t tSat;
- clock_t tSatSat;
- clock_t tSatUnsat;
- clock_t tGeneral;
- clock_t tPush;
- clock_t tTsim;
- clock_t tContain;
- clock_t tCnf;
- clock_t tTotal;
+ abctime tSat;
+ abctime tSatSat;
+ abctime tSatUnsat;
+ abctime tGeneral;
+ abctime tPush;
+ abctime tTsim;
+ abctime tContain;
+ abctime tCnf;
+ abctime tTotal;
};
////////////////////////////////////////////////////////////////////////
@@ -135,7 +135,7 @@ struct Pdr_Man_t_
static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
-static inline clock_t Pdr_ManTimeLimit( Pdr_Man_t * p )
+static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p )
{
if ( p->timeToStop == 0 )
return p->timeToStopOne;
@@ -160,7 +160,7 @@ extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k
/*=== pdrCore.c ==========================================================*/
extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
/*=== pdrInv.c ==========================================================*/
-extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time );
+extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index bb8d110d..b1bff676 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
+void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
{
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
@@ -328,7 +328,7 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
Vec_Ptr_t * vCubes;
Pdr_Set_t * pCube;
int i, kStart, kThis, RetValue, Counter = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect cubes used in the inductive invariant
kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart );
@@ -361,7 +361,7 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
else
{
Abc_Print( 1, "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// sat_solver_delete( pSat );
Vec_PtrFree( vCubes );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 36a62029..c5380147 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -77,7 +77,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
if ( pPars->nTimeOutOne )
{
int i;
- p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
+ p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
}
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index c9028c24..663a0e2f 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -144,7 +144,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
{
Aig_Obj_t * pObj;
int i, iVar, iVarMax = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Vec_IntClear( p->vLits );
for ( i = 0; i < pCube->nLits; i++ )
{
@@ -159,7 +159,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
}
// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
- p->tCnf += clock() - clk;
+ p->tCnf += Abc_Clock() - clk;
return p->vLits;
}
@@ -256,7 +256,7 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
{
sat_solver * pSat;
Vec_Int_t * vLits;
- clock_t Limit;
+ abctime Limit;
int RetValue;
pSat = Pdr_ManFetchSolver( p, k );
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
@@ -287,12 +287,12 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
sat_solver * pSat;
Vec_Int_t * vLits;
int Lit, RetValue;
- clock_t clk, Limit;
+ abctime clk, Limit;
p->nCalls++;
pSat = Pdr_ManFetchSolver( p, k );
if ( pCube == NULL ) // solve the property
{
- clk = clock();
+ clk = Abc_Clock();
Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
@@ -324,7 +324,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
// solve
- clk = clock();
+ clk = Abc_Clock();
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
@@ -349,7 +349,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
}
*/
}
- clk = clock() - clk;
+ clk = Abc_Clock() - clk;
p->tSat += clk;
assert( RetValue != l_Undef );
if ( RetValue == l_False )
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 1865e14b..32d1c857 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -364,7 +364,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
Vec_Int_t * vRes = p->vRes; // final result (flop literals)
Aig_Obj_t * pObj;
int i, Entry, RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect CO objects
Vec_IntClear( vCoObjs );
@@ -474,7 +474,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
// derive the set of resulting registers
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
assert( Vec_IntSize(vRes) > 0 );
- p->tTsim += clock() - clk;
+ p->tTsim += Abc_Clock() - clk;
pRes = Pdr_SetCreate( vRes, vPiLits );
assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
return pRes;
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:01:30 +0000