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/proof/fraig/fraigSat.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/proof/fraig/fraigSat.c')
| -rw-r--r-- | src/proof/fraig/fraigSat.c | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/proof/fraig/fraigSat.c b/src/proof/fraig/fraigSat.c index 6ccd1b86..7a11c072 100644 --- a/src/proof/fraig/fraigSat.c +++ b/src/proof/fraig/fraigSat.c @@ -85,7 +85,8 @@ int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * void Fraig_ManProveMiter( Fraig_Man_t * p ) { Fraig_Node_t * pNode; - int i, clk; + int i; + clock_t clk; if ( !p->fTryProve ) return; @@ -300,7 +301,8 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ***********************************************************************/ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) { - int RetValue, RetValue1, i, fComp, clk; + int RetValue, RetValue1, i, fComp; + clock_t clk; int fVerbose = 0; int fSwitch = 0; @@ -548,7 +550,8 @@ p->time3 += clock() - clk; ***********************************************************************/ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) { - int RetValue, RetValue1, i, fComp, clk; + int RetValue, RetValue1, i, fComp; + clock_t clk; int fVerbose = 0; // make sure the nodes are not complemented @@ -650,7 +653,8 @@ p->time3 += clock() - clk; int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) { Fraig_Node_t * pNode1R, * pNode2R; - int RetValue, RetValue1, i, clk; + int RetValue, RetValue1, i; + clock_t clk; int fVerbose = 0; pNode1R = Fraig_Regular(pNode1); |