diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satChecker.c | 2 | ||||
-rw-r--r-- | src/sat/bsat/satInter.c | 14 | ||||
-rw-r--r-- | src/sat/bsat/satInterA.c | 14 | ||||
-rw-r--r-- | src/sat/bsat/satInterB.c | 14 | ||||
-rw-r--r-- | src/sat/bsat/satInterP.c | 16 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 15 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 4 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 6 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 7 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 6 | ||||
-rw-r--r-- | src/sat/bsat/satStore.c | 1 | ||||
-rw-r--r-- | src/sat/cnf/cnf.h | 7 | ||||
-rw-r--r-- | src/sat/cnf/cnfCore.c | 6 | ||||
-rw-r--r-- | src/sat/cnf/cnfFast.c | 2 | ||||
-rw-r--r-- | src/sat/msat/msatInt.h | 1 | ||||
-rw-r--r-- | src/sat/msat/msatOrderH.c | 8 | ||||
-rw-r--r-- | src/sat/msat/msatOrderJ.c | 4 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 2 | ||||
-rw-r--r-- | src/sat/proof/pr.c | 16 |
19 files changed, 72 insertions, 73 deletions
diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c index f478928c..70bb9c85 100644 --- a/src/sat/bsat/satChecker.c +++ b/src/sat/bsat/satChecker.c @@ -22,7 +22,7 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> + #include "misc/vec/vec.h" ABC_NAMESPACE_IMPL_START diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c index 8617def9..6f564225 100644 --- a/src/sat/bsat/satInter.c +++ b/src/sat/bsat/satInter.c @@ -22,7 +22,7 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> + #include "satStore.h" ABC_NAMESPACE_IMPL_START @@ -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 - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation + clock_t timeBcp; // the runtime for BCP + clock_t timeTrace; // the runtime of trace construction + clock_t timeTotal; // the total runtime of interpolation }; // procedure to get hold of the clauses' truth table @@ -535,7 +535,7 @@ Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start ) { Sto_Cls_t * pClause; int i; - int clk = clock(); + clock_t clk = clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Int_ManPropagateOne( p, p->pTrail[i] ); @@ -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; - int clk = clock(); + clock_t clk = clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -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; - int clkTotal = clock(); + clock_t clkTotal = clock(); // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 4057ce7e..8b2ef8b7 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -22,7 +22,7 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> + #include "satStore.h" #include "src/aig/aig/aig.h" @@ -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 - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation + clock_t timeBcp; // the runtime for BCP + clock_t timeTrace; // the runtime of trace construction + clock_t timeTotal; // the total runtime of interpolation }; // procedure to get hold of the clauses' truth table @@ -491,7 +491,7 @@ Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start ) { Sto_Cls_t * pClause; int i; - int clk = clock(); + clock_t clk = clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Inta_ManPropagateOne( p, p->pTrail[i] ); @@ -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; - int clk = clock(); + clock_t clk = clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -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; - int clkTotal = clock(); + clock_t clkTotal = clock(); // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c index a9b18fd5..5a154aa0 100644 --- a/src/sat/bsat/satInterB.c +++ b/src/sat/bsat/satInterB.c @@ -22,7 +22,7 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> + #include "satStore.h" #include "src/aig/aig/aig.h" @@ -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 - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation + clock_t timeBcp; // the runtime for BCP + clock_t timeTrace; // the runtime of trace construction + clock_t timeTotal; // the total runtime of interpolation }; // procedure to get hold of the clauses' truth table @@ -493,7 +493,7 @@ Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start ) { Sto_Cls_t * pClause; int i; - int clk = clock(); + clock_t clk = clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Intb_ManPropagateOne( p, p->pTrail[i] ); @@ -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; - int clk = clock(); + clock_t clk = clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -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; - int clkTotal = clock(); + clock_t clkTotal = clock(); // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c index b8ab473a..2e3caeeb 100644 --- a/src/sat/bsat/satInterP.c +++ b/src/sat/bsat/satInterP.c @@ -22,7 +22,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "satStore.h" #include "src/misc/vec/vec.h" @@ -70,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 - int timeBcp; // the runtime for BCP - int timeTrace; // the runtime of trace construction - int timeTotal; // the total runtime of interpolation + clock_t timeBcp; // the runtime for BCP + clock_t timeTrace; // the runtime of trace construction + clock_t timeTotal; // the total runtime of interpolation }; // reading/writing the proof for a clause @@ -420,7 +419,7 @@ Sto_Cls_t * Intp_ManPropagate( Intp_Man_t * p, int Start ) { Sto_Cls_t * pClause; int i; - int clk = clock(); + clock_t clk = clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Intp_ManPropagateOne( p, p->pTrail[i] ); @@ -476,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; - int clk = clock(); + clock_t clk = clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -864,7 +863,8 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore ) sat_solver * pSat; Sto_Cls_t * pClause; Vec_Ptr_t * vClauses; - int i, iClause, RetValue, clk = clock(); + int i, iClause, RetValue; + clock_t clk = clock(); // collect the clauses vClauses = Vec_PtrAlloc( 1000 ); Sto_ManForEachClauseRoot( pCnf, pClause ) @@ -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; - int clkTotal = clock(); + clock_t clkTotal = clock(); // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index f56c20cc..f7e08592 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -145,7 +145,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f { int fVerify = 0; Vec_Int_t * vUsed, * vStack; - int clk = clock(); + clock_t clk = clock(); int i, Entry, iPrev = 0; vUsed = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 ); @@ -309,8 +309,9 @@ void Sat_ProofReduce2( sat_solver2 * s ) int fVerbose = 0; Vec_Int_t * vUsed; satset * pNode, * pFanin, * pPivot; - int i, k, hTemp, clk = clock(); - static int TimeTotal = 0; + int i, k, hTemp; + clock_t clk = clock(); + static clock_t TimeTotal = 0; // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 ); @@ -371,8 +372,9 @@ void Sat_ProofReduce( sat_solver2 * s ) int fVerbose = 0; Vec_Ptr_t * vUsed; satset * pNode, * pFanin, * pPivot; - int i, j, k, hTemp, nSize, clk = clock(); - static int TimeTotal = 0; + int i, j, k, hTemp, nSize; + clock_t clk = clock(); + static clock_t TimeTotal = 0; // collect visited nodes nSize = Proof_MarkUsedRec( vProof, vRoots ); @@ -525,7 +527,8 @@ void Sat_ProofCheck( sat_solver2 * s ) Vec_Set_t * vResolves; Vec_Int_t * vUsed, * vTemp; satset * pSet, * pSet0 = NULL, * pSet1; - int i, k, hRoot, Handle, Counter = 0, clk = clock(); + int i, k, hRoot, Handle, Counter = 0; + clock_t clk = clock(); hRoot = s->hProofLast; if ( hRoot == -1 ) return; diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 2d41e2fe..f143916a 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1605,7 +1605,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 && time(NULL) > s->nRuntimeLimit ) + if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; if (s->verbosity >= 1) { @@ -1629,7 +1629,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 && time(NULL) > s->nRuntimeLimit ) + if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; } if (s->verbosity >= 1) diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 40f637ee..62ad5e0c 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -142,7 +142,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 - int nRuntimeLimit; // external limit on runtime + clock_t nRuntimeLimit; // external limit on runtime veci act_vars; // variables whose activity has changed double* factors; // the activity factors @@ -198,9 +198,9 @@ static int sat_solver_final(sat_solver* s, int ** ppArray) return s->conf_final.size; } -static int sat_solver_set_runtime_limit(sat_solver* s, int Limit) +static clock_t sat_solver_set_runtime_limit(sat_solver* s, clock_t Limit) { - int nRuntimeLimit = s->nRuntimeLimit; + clock_t nRuntimeLimit = s->nRuntimeLimit; s->nRuntimeLimit = Limit; return nRuntimeLimit; } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 2e0a5f4a..cbe6bc52 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1398,12 +1398,13 @@ void luby2_test() // updates clauses, watches, units, and proof void sat_solver2_reducedb(sat_solver2* s) { - static int TimeTotal = 0; + static clock_t TimeTotal = 0; satset * c, * pivot; cla h,* pArray,* pArray2; int * pPerm, * pClaAct, nClaAct, ActCutOff; int i, j, k, hTemp, hHandle, LastSize = 0; - int Counter, CounterStart, clk = clock(); + int Counter, CounterStart; + clock_t clk = clock(); // check if it is time to reduce if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax ) @@ -1845,7 +1846,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 && time(NULL) > s->nRuntimeLimit ) + if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) break; // reduce the set of learnt clauses: sat_solver2_reducedb(s); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 79eb64ed..ffab91be 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -160,7 +160,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 - int nRuntimeLimit; // external limit on runtime + clock_t nRuntimeLimit; // external limit on runtime }; typedef struct satset_t satset; @@ -240,9 +240,9 @@ static inline int sat_solver2_final(sat_solver2* s, int ** ppArray) return s->conf_final.size; } -static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit) +static inline clock_t sat_solver2_set_runtime_limit(sat_solver2* s, clock_t Limit) { - int temp = s->nRuntimeLimit; + clock_t temp = s->nRuntimeLimit; s->nRuntimeLimit = Limit; return temp; } diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c index ac74c4a6..fab13666 100644 --- a/src/sat/bsat/satStore.c +++ b/src/sat/bsat/satStore.c @@ -22,7 +22,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "satStore.h" diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index 478755d6..16aaa21f 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include "src/misc/vec/vec.h" #include "src/aig/aig/aig.h" @@ -88,9 +87,9 @@ struct Cnf_Man_t_ int nMergeLimit; // the limit on the size of merged cut unsigned * pTruths[4]; // temporary truth tables Vec_Int_t * vMemory; // memory for intermediate ISOP representation - int timeCuts; - int timeMap; - int timeSave; + clock_t timeCuts; + clock_t timeMap; + clock_t timeSave; }; diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c index 65d7ef60..f08ea6d1 100644 --- a/src/sat/cnf/cnfCore.c +++ b/src/sat/cnf/cnfCore.c @@ -50,7 +50,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ) Cnf_Man_t * p; Vec_Ptr_t * vMapped; Aig_MmFixed_t * pMemCuts; - int clk; + clock_t clk; // allocate the CNF manager if ( s_pManCnf == NULL ) s_pManCnf = Cnf_ManStart(); @@ -103,7 +103,7 @@ Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ) Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; Aig_MmFixed_t * pMemCuts; - int clk; + clock_t clk; // allocate the CNF manager if ( s_pManCnf == NULL ) s_pManCnf = Cnf_ManStart(); @@ -156,7 +156,7 @@ Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin ) Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; Aig_MmFixed_t * pMemCuts; - int clk; + clock_t clk; // allocate the CNF manager if ( s_pManCnf == NULL ) s_pManCnf = Cnf_ManStart(); diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index 492ddb61..93b3072b 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -666,7 +666,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs ) { Cnf_Dat_t * pCnf = NULL; - int clk;//, clkTotal = clock(); + clock_t clk;//, clkTotal = clock(); // printf( "\n" ); Aig_ManCleanMarkAB( p ); // create initial marking diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 58baa7b4..a1d9e14d 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -30,7 +30,6 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> #include <math.h> #include "src/misc/util/abc_global.h" diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c index 4bdefc6d..d0c9c997 100644 --- a/src/sat/msat/msatOrderH.c +++ b/src/sat/msat/msatOrderH.c @@ -58,7 +58,7 @@ static void Msat_HeapIncrease( Msat_Order_t * p, int n ); static void Msat_HeapPercolateUp( Msat_Order_t * p, int i ); static void Msat_HeapPercolateDown( Msat_Order_t * p, int i ); -extern int timeSelect; +extern clock_t timeSelect; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -191,7 +191,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p ) // return var_Undef; int Var; - int clk = clock(); + clock_t clk = clock(); while ( !HEMPTY(p) ) { @@ -237,7 +237,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) // if (!heap.inHeap(x)) // heap.insert(x); - int clk = clock(); + clock_t clk = clock(); if ( !HINHEAP(p,Var) ) Msat_HeapInsert( p, Var ); timeSelect += clock() - clk; @@ -259,7 +259,7 @@ void Msat_OrderUpdate( Msat_Order_t * p, int Var ) // if (heap.inHeap(x)) // heap.increase(x); - int clk = clock(); + clock_t clk = clock(); if ( HINHEAP(p,Var) ) Msat_HeapIncrease( p, Var ); timeSelect += clock() - clk; diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c index 2be6b47b..a9c27bd0 100644 --- a/src/sat/msat/msatOrderJ.c +++ b/src/sat/msat/msatOrderJ.c @@ -81,8 +81,8 @@ struct Msat_Order_t_ static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); -extern int timeSelect; -extern int timeAssign; +extern clock_t timeSelect; +extern clock_t timeAssign; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 4ef40ad0..eff1d6d7 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -140,7 +140,7 @@ int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra Msat_SearchParams_t Params = { 0.95, 0.999 }; double nConflictsLimit, nLearnedLimit; Msat_Type_t Status; - int timeStart = clock(); + clock_t timeStart = clock(); // p->pFreq = ABC_ALLOC( int, p->nVarsAlloc ); // memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c index 45bc2e33..f559d851 100644 --- a/src/sat/proof/pr.c +++ b/src/sat/proof/pr.c @@ -22,9 +22,7 @@ #include <stdlib.h> #include <string.h> #include <assert.h> -#include <time.h> -//#include "vec.h" #include "src/misc/util/abc_global.h" #include "pr.h" @@ -90,10 +88,10 @@ struct Pr_Man_t_ int nResLits; // the number of literals of the resolvent int nResLitsAlloc;// the number of literals of the resolvent // runtime stats - int timeBcp; - int timeTrace; - int timeRead; - int timeTotal; + clock_t timeBcp; + clock_t timeTrace; + clock_t timeRead; + clock_t timeTotal; }; // variable assignments @@ -580,7 +578,7 @@ Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start ) { Pr_Cls_t * pClause; int i; - int clk = clock(); + clock_t clk = clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Pr_ManPropagateOne( p, p->pTrail[i] ); @@ -676,7 +674,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) Pr_Cls_t * pReason; int i, v, Var, PrevId; int fPrint = 0; - int clk = clock(); + clock_t clk = clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -1228,7 +1226,7 @@ int Pr_ManProofCount_rec( Pr_Cls_t * pClause ) int Pr_ManProofTest( char * pFileName ) { Pr_Man_t * p; - int clk, clkTotal = clock(); + clock_t clk, clkTotal = clock(); clk = clock(); p = Pr_ManProofRead( pFileName ); |