Fixing time primtouts throughout the code.

10 files changed, 35 insertions, 34 deletions

diff --git a/src/proof/fraig/fraig.h b/src/proof/fraig/fraig.h
index 6d672716..0c021feb 100644
--- a/src/proof/fraig/fraig.h
+++ b/src/proof/fraig/fraig.h
@@ -154,9 +154,6 @@ extern void                Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse
 extern void                Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ); 
 extern void                Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve );
 extern void                Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose );        
-extern void                Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time );        
-extern void                Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time );          
-extern void                Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time );          
 extern void                Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ); 
 extern void                Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames );  
 extern void                Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode );
diff --git a/src/proof/fraig/fraigApi.c b/src/proof/fraig/fraigApi.c
index 6e0ab959..b0b47075 100644
--- a/src/proof/fraig/fraigApi.c
+++ b/src/proof/fraig/fraigApi.c
@@ -91,9 +91,6 @@ void            Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse )      { p-
 void            Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing )      { p->fChoicing = fChoicing; }
 void            Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve )      { p->fTryProve = fTryProve; }
 void            Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose )        { p->fVerbose  = fVerbose;  }
-void            Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time )        { p->timeToAig = Time;      }
-void            Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time )          { p->timeToNet = Time;      }
-void            Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time )          { p->timeTotal = Time;      }
 void            Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppOutputNames = ppNames; }
 void            Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames )  { p->ppInputNames  = ppNames; }
 
diff --git a/src/proof/fraig/fraigChoice.c b/src/proof/fraig/fraigChoice.c
index 21d4fe10..e1d6e8a7 100644
--- a/src/proof/fraig/fraigChoice.c
+++ b/src/proof/fraig/fraigChoice.c
@@ -45,7 +45,7 @@ void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit )
 {
 //    ProgressBar * pProgress;
     char Buffer[100];
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
     int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes;
     int /*nMaxLevel,*/ nDistributive;
     Fraig_Node_t *pNode, *pRepr;
diff --git a/src/proof/fraig/fraigFeed.c b/src/proof/fraig/fraigFeed.c
index 47f946e1..4cb1276b 100644
--- a/src/proof/fraig/fraigFeed.c
+++ b/src/proof/fraig/fraigFeed.c
@@ -80,7 +80,8 @@ void Fraig_FeedBackInit( Fraig_Man_t * p )
 void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
 {
     int nVarsPi, nWords;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     // get the number of PI vars in the feedback (also sets the PI values)
     nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars );
diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h
index f6a5d74f..1ff8727e 100644
--- a/src/proof/fraig/fraigInt.h
+++ b/src/proof/fraig/fraigInt.h
@@ -28,7 +28,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/util/abc_global.h"
 #include "fraig.h"
@@ -189,18 +188,18 @@ struct Fraig_ManStruct_t_
     int                   nImplies1;
 
     // runtime statistics
-    int                   timeToAig;     // time to transfer to the mapping structure
-    int                   timeSims;      // time to compute k-feasible cuts
-    int                   timeTrav;      // time to traverse the network
-    int                   timeFeed;      // time for solver feedback (recording and resimulating)
-    int                   timeImply;     // time to analyze implications
-    int                   timeSat;       // time to compute the truth table for each cut
-    int                   timeToNet;     // time to transfer back to the network
-    int                   timeTotal;     // the total mapping time
-    int                   time1;         // time to perform one task
-    int                   time2;         // time to perform another task
-    int                   time3;         // time to perform another task
-    int                   time4;         // time to perform another task
+    clock_t               timeToAig;     // time to transfer to the mapping structure
+    clock_t               timeSims;      // time to compute k-feasible cuts
+    clock_t               timeTrav;      // time to traverse the network
+    clock_t               timeFeed;      // time for solver feedback (recording and resimulating)
+    clock_t               timeImply;     // time to analyze implications
+    clock_t               timeSat;       // time to compute the truth table for each cut
+    clock_t               timeToNet;     // time to transfer back to the network
+    clock_t               timeTotal;     // the total mapping time
+    clock_t               time1;         // time to perform one task
+    clock_t               time2;         // time to perform another task
+    clock_t               time3;         // time to perform another task
+    clock_t               time4;         // time to perform another task
 };
 
 // the mapping node
diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c
index 125a4da1..bc7c423d 100644
--- a/src/proof/fraig/fraigMan.c
+++ b/src/proof/fraig/fraigMan.c
@@ -25,8 +25,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-int timeSelect;
-int timeAssign;
+clock_t timeSelect;
+clock_t timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -323,8 +323,8 @@ void Fraig_ManFree( Fraig_Man_t * p )
 ***********************************************************************/
 void Fraig_ManCreateSolver( Fraig_Man_t * p )
 {
-    extern int timeSelect;
-    extern int timeAssign;
+    extern clock_t timeSelect;
+    extern clock_t timeAssign;
     assert( p->pSat == NULL );
     // allocate data for SAT solving
     p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
diff --git a/src/proof/fraig/fraigNode.c b/src/proof/fraig/fraigNode.c
index 609d5f65..5310534b 100644
--- a/src/proof/fraig/fraigNode.c
+++ b/src/proof/fraig/fraigNode.c
@@ -87,7 +87,8 @@ Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p )
 Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode, * pNodeRes;
-    int i, clk;
+    int i;
+    clock_t clk;
 
     // create the node
     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
@@ -159,7 +160,7 @@ p->timeSims += clock() - clk;
 Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 )
 {
     Fraig_Node_t * pNode;
-    int clk;
+    clock_t clk;
 
     // create the node
     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
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);
diff --git a/src/proof/fraig/fraigTable.c b/src/proof/fraig/fraigTable.c
index 6611e4fa..d184ab7f 100644
--- a/src/proof/fraig/fraigTable.c
+++ b/src/proof/fraig/fraigTable.c
@@ -260,7 +260,8 @@ void Fraig_TableResizeS( Fraig_HashTable_t * p )
 {
     Fraig_Node_t ** pBinsNew;
     Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
+    int nBinsNew, Counter, i;
+    clock_t clk;
     unsigned Key;
 
 clk = clock();
@@ -303,7 +304,8 @@ void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR )
 {
     Fraig_Node_t ** pBinsNew;
     Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
+    int nBinsNew, Counter, i;
+    clock_t clk;
     unsigned Key;
 
 clk = clock();
diff --git a/src/proof/fraig/fraigUtil.c b/src/proof/fraig/fraigUtil.c
index ae78a61f..316b492e 100644
--- a/src/proof/fraig/fraigUtil.c
+++ b/src/proof/fraig/fraigUtil.c
@@ -844,7 +844,7 @@ int Fraig_ManPrintRefs( Fraig_Man_t * pMan )
     Fraig_NodeVec_t * vPivots;
     Fraig_Node_t * pNode, * pNode2;
     int i, k, Counter, nProved;
-    int clk;
+    clock_t clk;
 
     vPivots = Fraig_NodeVecAlloc( 1000 );
     for ( i = 0; i < pMan->vNodes->nSize; i++ )