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/satInter.c | |
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/satInter.c')
-rw-r--r-- | src/sat/bsat/satInter.c | 14 |
1 files changed, 7 insertions, 7 deletions
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 ); |