diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 17:46:54 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 17:46:54 -0700 |
commit | 3aab7245738a69f1dd4d898493d5dabf6596ea61 (patch) | |
tree | 16a23107ca27a250e82c492dcdd1a2bea640cff6 /src/sat/bsat | |
parent | 16d96fcf533fb77ff4a45992991e38ac7ea74bb3 (diff) | |
download | abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.gz abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.bz2 abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.zip |
Fixing time primtouts throughout the code.
Diffstat (limited to 'src/sat/bsat')
-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 |
11 files changed, 51 insertions, 48 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" |