summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satInter.c20
-rw-r--r--src/sat/bsat/satInterA.c22
-rw-r--r--src/sat/bsat/satInterB.c22
-rw-r--r--src/sat/bsat/satInterP.c26
-rw-r--r--src/sat/bsat/satProof.c24
-rw-r--r--src/sat/bsat/satSolver.c24
-rw-r--r--src/sat/bsat/satSolver.h6
-rw-r--r--src/sat/bsat/satSolver2.c22
-rw-r--r--src/sat/bsat/satSolver2.h6
9 files changed, 86 insertions, 86 deletions
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 6bd07fb7..45908225 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -71,9 +71,9 @@ struct Int_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -535,17 +535,17 @@ Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Int_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -591,7 +591,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -743,7 +743,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -1006,7 +1006,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
{
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1061,7 +1061,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
*ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index a4a06439..dabb10a3 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -70,9 +70,9 @@ struct Inta_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -491,17 +491,17 @@ Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Inta_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -547,7 +547,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -697,7 +697,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -954,7 +954,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
Aig_Obj_t * pObj;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1008,12 +1008,12 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( fVerbose )
{
-// ABC_PRT( "Interpo", clock() - clkTotal );
+// ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index 07edf7a8..8226fb6d 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -70,9 +70,9 @@ struct Intb_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -493,17 +493,17 @@ Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Intb_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -570,7 +570,7 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -733,7 +733,7 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -990,7 +990,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
Aig_Obj_t * pObj;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1044,12 +1044,12 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( fVerbose )
{
-// ABC_PRT( "Interpo", clock() - clkTotal );
+// ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 404d5503..414879b6 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -69,9 +69,9 @@ struct Intp_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// reading/writing the proof for a clause
@@ -419,17 +419,17 @@ Sto_Cls_t * Intp_ManPropagate( Intp_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Intp_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -475,7 +475,7 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -639,7 +639,7 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
// if ( p->pCnf->nClausesA )
@@ -864,7 +864,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
Sto_Cls_t * pClause;
Vec_Ptr_t * vClauses;
int i, iClause, RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect the clauses
vClauses = Vec_PtrAlloc( 1000 );
Sto_ManForEachClauseRoot( pCnf, pClause )
@@ -896,7 +896,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
printf( "UNSAT core verification FAILED. " );
else
printf( "UNSAT core verification succeeded. " );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
else
{
@@ -962,7 +962,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
Vec_Int_t * vVisited;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1021,12 +1021,12 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
if ( fVerbose )
{
- ABC_PRT( "Core", clock() - clkTotal );
+ ABC_PRT( "Core", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
// derive the UNSAT core
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index e70a60ef..a4067160 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -146,7 +146,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
{
int fVerify = 0;
Vec_Int_t * vUsed, * vStack;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int i, Entry, iPrev = 0;
vUsed = Vec_IntAlloc( 1000 );
vStack = Vec_IntAlloc( 1000 );
@@ -154,10 +154,10 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
if ( Entry >= 0 )
Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
Vec_IntFree( vStack );
-// Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
- clk = clock();
+// Abc_PrintTime( 1, "Iterative clause collection time", Abc_Clock() - clk );
+ clk = Abc_Clock();
Abc_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
-// Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
+// Abc_PrintTime( 1, "Postprocessing with sorting time", Abc_Clock() - clk );
// verify topological order
if ( fVerify )
{
@@ -314,8 +314,8 @@ void Sat_ProofReduce2( sat_solver2 * s )
Vec_Int_t * vUsed;
satset * pNode, * pFanin, * pPivot;
int i, k, hTemp;
- clock_t clk = clock();
- static clock_t TimeTotal = 0;
+ abctime clk = Abc_Clock();
+ static abctime TimeTotal = 0;
// collect visited nodes
vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
@@ -359,7 +359,7 @@ void Sat_ProofReduce2( sat_solver2 * s )
printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
@@ -390,8 +390,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
Vec_Ptr_t * vUsed;
satset * pNode, * pFanin, * pPivot;
int i, j, k, hTemp, nSize;
- clock_t clk = clock();
- static clock_t TimeTotal = 0;
+ abctime clk = Abc_Clock();
+ static abctime TimeTotal = 0;
int RetValue;
//Sat_ProofCheck0( vProof );
@@ -448,7 +448,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
@@ -554,7 +554,7 @@ void Sat_ProofCheck( sat_solver2 * s )
Vec_Int_t * vUsed, * vTemp;
satset * pSet, * pSet0 = NULL, * pSet1;
int i, k, hRoot, Handle, Counter = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
hRoot = s->hProofLast;
if ( hRoot == -1 )
return;
@@ -586,7 +586,7 @@ void Sat_ProofCheck( sat_solver2 * s )
printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts );
else
printf( "Proof verification successful. " );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// cleanup
Vec_SetFree( vResolves );
Vec_IntFree( vUsed );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index d1310c81..8d1bd455 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -224,16 +224,16 @@ static inline void act_var_rescale(sat_solver* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause_rescale(sat_solver* s) {
-// static clock_t Total = 0;
+// static abctime Total = 0;
clause** cs = (clause**)veci_begin(&s->learnts);
- int i;//, clk = clock();
+ int i;//, clk = Abc_Clock();
for (i = 0; i < veci_size(&s->learnts); i++){
float a = clause_activity(cs[i]);
clause_setactivity(cs[i], a * (float)1e-20);
}
s->cla_inc *= (float)1e-20;
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
// printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -282,15 +282,15 @@ static inline void act_var_rescale(sat_solver* s) {
}
static inline void act_clause_rescale(sat_solver* s) {
- static clock_t Total = 0;
- clock_t clk = clock();
+ static abctime Total = 0;
+ abctime clk = Abc_Clock();
unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
int i;
for (i = 0; i < veci_size(&s->act_clas); i++)
activity[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -1226,8 +1226,8 @@ int sat_solver_simplify(sat_solver* s)
void sat_solver_reducedb(sat_solver* s)
{
- static clock_t TimeTotal = 0;
- clock_t clk = clock();
+ static abctime TimeTotal = 0;
+ abctime clk = Abc_Clock();
Sat_Mem_t * pMem = &s->Mem;
int nLearnedOld = veci_size(&s->act_clas);
int * act_clas = veci_begin(&s->act_clas);
@@ -1330,7 +1330,7 @@ void sat_solver_reducedb(sat_solver* s)
assert( Counter == (int)s->stats.learnts );
// report the results
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
@@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
int next;
// Reached bound on number of conflicts:
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){
s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
@@ -1786,7 +1786,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
while (status == l_Undef){
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
if (s->verbosity >= 1)
{
@@ -1810,7 +1810,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
break;
if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
break;
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
}
if (s->verbosity >= 1)
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index e5ea1ba5..50a4727c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -160,7 +160,7 @@ struct sat_solver_t
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
- clock_t nRuntimeLimit; // external limit on runtime
+ abctime nRuntimeLimit; // external limit on runtime
veci act_vars; // variables whose activity has changed
double* factors; // the activity factors
@@ -223,9 +223,9 @@ static int sat_solver_final(sat_solver* s, int ** ppArray)
return s->conf_final.size;
}
-static clock_t sat_solver_set_runtime_limit(sat_solver* s, clock_t Limit)
+static abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
{
- clock_t nRuntimeLimit = s->nRuntimeLimit;
+ abctime nRuntimeLimit = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 12d74c0d..cde1d3b1 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -304,15 +304,15 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause2_rescale(sat_solver2* s) {
- static clock_t Total = 0;
+ static abctime Total = 0;
float * act_clas = (float *)veci_begin(&s->act_clas);
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for (i = 0; i < veci_size(&s->act_clas); i++)
act_clas[i] *= (float)1e-20;
s->cla_inc *= (float)1e-20;
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
Abc_Print(1, "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
Abc_PrintTime( 1, "Time", Total );
}
@@ -344,15 +344,15 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause2_rescale(sat_solver2* s) {
-// static clock_t Total = 0;
-// clock_t clk = clock();
+// static abctime Total = 0;
+// abctime clk = Abc_Clock();
int i;
unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
for (i = 0; i < veci_size(&s->act_clas); i++)
act_clas[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-// Total += clock() - clk;
+// Total += Abc_Clock() - clk;
// Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
// NO CONFLICT
int next;
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){
// Reached bound on number of conflicts:
s->progress_estimate = solver2_progress(s);
solver2_canceluntil(s,s->root_level);
@@ -1390,7 +1390,7 @@ void luby2_test()
// updates clauses, watches, units, and proof
void sat_solver2_reducedb(sat_solver2* s)
{
- static clock_t TimeTotal = 0;
+ static abctime TimeTotal = 0;
Sat_Mem_t * pMem = &s->Mem;
clause * c = NULL;
int nLearnedOld = veci_size(&s->act_clas);
@@ -1398,7 +1398,7 @@ void sat_solver2_reducedb(sat_solver2* s)
int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
int i, j, k, Id, nSelected;//, LastSize = 0;
int Counter, CounterStart;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
static int Count = 0;
Count++;
assert( s->nLearntMax );
@@ -1558,7 +1558,7 @@ void sat_solver2_reducedb(sat_solver2* s)
}
// report the results
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
@@ -1943,7 +1943,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
s->progress_estimate*100);
fflush(stdout);
}
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
// reduce the set of learnt clauses
if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL )
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 8c32cbde..d7d16d73 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -161,7 +161,7 @@ struct sat_solver2_t
stats_t stats;
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
- clock_t nRuntimeLimit; // external limit on runtime
+ abctime nRuntimeLimit; // external limit on runtime
};
static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); }
@@ -220,9 +220,9 @@ static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
return s->conf_final.size;
}
-static inline clock_t sat_solver2_set_runtime_limit(sat_solver2* s, clock_t Limit)
+static inline abctime sat_solver2_set_runtime_limit(sat_solver2* s, abctime Limit)
{
- clock_t temp = s->nRuntimeLimit;
+ abctime temp = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return temp;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:27:02 +0000